diff --git a/formal/riscv-formal/Makefile b/formal/riscv-formal/Makefile index 9d1ab262..cefe0766 100644 --- a/formal/riscv-formal/Makefile +++ b/formal/riscv-formal/Makefile @@ -15,6 +15,9 @@ OUTDIR := build # Source directory relative to this Makefile SRC_DIR := ../../rtl +# Synthesis source directory relative to this Makefile +SYN_DIR := ../../syn + # Vendored IP directory relative to this Makefile LOWRISC_IP := ../../vendor/lowrisc_ip @@ -43,10 +46,14 @@ SRCS_SV ?= \ $(SRC_DIR)/ibex_pmp.sv \ $(SRC_DIR)/ibex_register_file_ff.sv \ $(SRC_DIR)/ibex_wb_stage.sv \ - $(SRC_DIR)/ibex_core.sv + $(SRC_DIR)/ibex_core.sv \ + $(SRC_DIR)/ibex_top.sv -PKG ?= $(SRC_DIR)/ibex_pkg.sv -PRIM ?= $(LOWRISC_IP)/ip/prim_generic/rtl/prim_generic_clock_gating.sv +PKGS ?= \ + $(SRC_DIR)/ibex_pkg.sv \ + $(LOWRISC_IP)/ip/prim/rtl/prim_ram_1p_pkg.sv + +PRIM_CLOCK ?= $(SYN_DIR)/rtl/prim_clock_gating.v GEN_V := $(patsubst %.sv,%.v,$(patsubst $(SRC_DIR)%,$(OUTDIR)%,$(SRCS_SV))) @@ -58,17 +65,17 @@ $(OUTDIR): mkdir -p $(OUTDIR) # Convert each SystemVerilog source into a Verilog file -$(GEN_V): $(OUTDIR)%.v: $(SRC_DIR)%.sv $(PKG) | $(OUTDIR) - sv2v --define=RISCV_FORMAL $(addprefix -I,$(INC_DIRS)) $(PKG) \ +$(GEN_V): $(OUTDIR)%.v: $(SRC_DIR)%.sv $(PKGS) | $(OUTDIR) + sv2v --define=RISCV_FORMAL $(addprefix -I,$(INC_DIRS)) $(PKGS) \ $< > $@ # Combine multiple Verilog sources into one Ibex Verilog file # Disable "M" extension -$(IBEX_OUT): $(GEN_V) $(PRIM) - yosys -p "read_verilog -sv $(PRIM) $(GEN_V)" \ - -p "chparam -set RV32M 0 ibex_core" \ - -p "chparam -set WritebackStage $(IBEX_ENABLE_WB) ibex_core" \ - -p "synth -top ibex_core" \ +$(IBEX_OUT): $(GEN_V) $(PRIM_CLOCK) + yosys -p "read_verilog -sv $(PRIM_CLOCK) $(GEN_V)" \ + -p "chparam -set RV32M 0 ibex_top" \ + -p "chparam -set WritebackStage $(IBEX_ENABLE_WB) ibex_top" \ + -p "synth -top ibex_top" \ -p "write_verilog $(IBEX_OUT)" .PHONY: clean