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 <wlo@warricklo.net>

1 files changed, 17 insertions, 4 deletions

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