Skip to content

Commit

Permalink
Get riscv-formal flow working again
Browse files Browse the repository at this point in the history
No guarantees that this actually does anything useful, but at least
the Makefile works again.
  • Loading branch information
rswarbrick committed Jul 14, 2021
1 parent 7506d4d commit 594c236
Showing 1 changed file with 38 additions and 29 deletions.
67 changes: 38 additions & 29 deletions formal/riscv-formal/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -11,33 +11,42 @@ IBEX_ENABLE_WB ?= 0
IBEX_OUT := ibex.v
# Build folder name
OUTDIR := build

# Source directory relative to this Makefile
SRC_DIR := ../rtl
# Include directory relative to this Makefile
INC_DIR := ../vendor/lowrisc_ip/prim/rtl
SRC_DIR := ../../rtl

# Vendored IP directory relative to this Makefile
LOWRISC_IP := ../../vendor/lowrisc_ip

# Include directories relative to this Makefile
INC_DIRS := \
$(LOWRISC_IP)/ip/prim/rtl \
$(LOWRISC_IP)/dv/sv/dv_utils

# SystemVerilog sources of Ibex
SRCS_SV ?= $(SRC_DIR)/ibex_alu.sv \
$(SRC_DIR)/ibex_compressed_decoder.sv \
$(SRC_DIR)/ibex_controller.sv \
$(SRC_DIR)/ibex_counter.sv \
$(SRC_DIR)/ibex_cs_registers.sv \
$(SRC_DIR)/ibex_decoder.sv \
$(SRC_DIR)/ibex_ex_block.sv \
$(SRC_DIR)/ibex_fetch_fifo.sv \
$(SRC_DIR)/ibex_id_stage.sv \
$(SRC_DIR)/ibex_if_stage.sv \
$(SRC_DIR)/ibex_load_store_unit.sv \
$(SRC_DIR)/ibex_multdiv_fast.sv \
$(SRC_DIR)/ibex_multdiv_slow.sv \
$(SRC_DIR)/ibex_prefetch_buffer.sv \
$(SRC_DIR)/ibex_pmp.sv \
$(SRC_DIR)/ibex_register_file_ff.sv \
$(SRC_DIR)/ibex_wb_stage.sv \
$(SRC_DIR)/ibex_core.sv
SRCS_SV ?= \
$(SRC_DIR)/ibex_alu.sv \
$(SRC_DIR)/ibex_compressed_decoder.sv \
$(SRC_DIR)/ibex_controller.sv \
$(SRC_DIR)/ibex_counter.sv \
$(SRC_DIR)/ibex_csr.sv \
$(SRC_DIR)/ibex_cs_registers.sv \
$(SRC_DIR)/ibex_decoder.sv \
$(SRC_DIR)/ibex_ex_block.sv \
$(SRC_DIR)/ibex_fetch_fifo.sv \
$(SRC_DIR)/ibex_id_stage.sv \
$(SRC_DIR)/ibex_if_stage.sv \
$(SRC_DIR)/ibex_load_store_unit.sv \
$(SRC_DIR)/ibex_multdiv_fast.sv \
$(SRC_DIR)/ibex_multdiv_slow.sv \
$(SRC_DIR)/ibex_prefetch_buffer.sv \
$(SRC_DIR)/ibex_pmp.sv \
$(SRC_DIR)/ibex_register_file_ff.sv \
$(SRC_DIR)/ibex_wb_stage.sv \
$(SRC_DIR)/ibex_core.sv

PKG ?= $(SRC_DIR)/ibex_pkg.sv
PRIM ?= ../syn/rtl/prim_clock_gating.v
PRIM ?= $(LOWRISC_IP)/ip/prim_generic/rtl/prim_generic_clock_gating.sv

GEN_V := $(patsubst %.sv,%.v,$(patsubst $(SRC_DIR)%,$(OUTDIR)%,$(SRCS_SV)))

Expand All @@ -49,18 +58,18 @@ $(OUTDIR):
mkdir -p $(OUTDIR)

# Convert each SystemVerilog source into a Verilog file
$(GEN_V): $(OUTDIR)%.v: $(SRC_DIR)%.sv $(PKG) $(INC_DIR) | $(OUTDIR)
sv2v --define=RISCV_FORMAL -I$(INC_DIR) $(PKG) \
$(GEN_V): $(OUTDIR)%.v: $(SRC_DIR)%.sv $(PKG) | $(OUTDIR)
sv2v --define=RISCV_FORMAL $(addprefix -I,$(INC_DIRS)) $(PKG) \
$< > $@

# 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" \
-p "write_verilog $(IBEX_OUT)"
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" \
-p "write_verilog $(IBEX_OUT)"

.PHONY: clean
clean:
Expand Down

0 comments on commit 594c236

Please sign in to comment.