From 2455fed25341b39d505bcdad9ae2b07c6cd42a73 Mon Sep 17 00:00:00 2001 From: Warrick Lo Date: Thu, 18 Jun 2026 09:39:41 -0700 Subject: Move typedefs to types.svh from montreal_pkg Yosys has poor support of packaged types. We will move typedefs to header files to prepare for formal verification with sby and the Tiny Tapeout flow later on, which uses yosys. Additionally, a debug port has been exposed to help verify the internal state of the regfile registers. Signed-off-by: Warrick Lo --- rtl/regfile.sv | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) (limited to 'rtl/regfile.sv') diff --git a/rtl/regfile.sv b/rtl/regfile.sv index e18301a..66af045 100644 --- a/rtl/regfile.sv +++ b/rtl/regfile.sv @@ -15,9 +15,9 @@ * read ports (default 2). Register 0 is fixed to 0 for all reads. */ -module regfile - import montreal_pkg::*; -#( +`include "types.svh" + +module regfile #( parameter int unsigned XLEN = config_pkg::XLEN, parameter int unsigned SLICE_WIDTH = config_pkg::SLICE_WIDTH, parameter int unsigned ADDR_WIDTH = config_pkg::REG_ADDR_WIDTH, @@ -26,6 +26,14 @@ module regfile localparam int unsigned NUM_WORDS = 2 ** ADDR_WIDTH, localparam int unsigned SLICE_ADDR_WIDTH = $clog2(XLEN / SLICE_WIDTH) ) ( +/* Expose the internal register state for formal verification. + * Yosys/SBY cannot reliably reference hierarchical signals after + * elaboration and optimisation. */ +`ifdef FORMAL + /* verilog_lint: waive port-name-suffix */ + output word_bank_t register_dbg, +`endif + input logic clk_i, input logic rst_ni, input logic [SLICE_ADDR_WIDTH-1:0] slice_sel_i, @@ -38,7 +46,12 @@ module regfile input logic [SLICE_WIDTH-1:0] wdata_i ); - logic [NUM_WORDS-1:0][XLEN-1:0] register; + word_bank_t register; + +/* Debug signal for formal verification. See above. */ +`ifdef FORMAL + assign register_dbg = register; +`endif always_comb begin for (int i = 0; i < NUM_READ_PORTS; i++) begin : gen_read_block -- cgit v1.2.3