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