From 2455fed25341b39d505bcdad9ae2b07c6cd42a73 Mon Sep 17 00:00:00 2001
From: Warrick Lo <wlo@warricklo.net>
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 <wlo@warricklo.net>
---
 rtl/config_pkg.sv   |  2 +-
 rtl/montreal_pkg.sv |  8 --------
 rtl/regfile.sv      | 21 +++++++++++++++++----
 rtl/types.svh       |  9 +++++++++
 4 files changed, 27 insertions(+), 13 deletions(-)
 delete mode 100644 rtl/montreal_pkg.sv
 create mode 100644 rtl/types.svh

diff --git a/rtl/config_pkg.sv b/rtl/config_pkg.sv
index 0120b14..01d6c20 100644
--- a/rtl/config_pkg.sv
+++ b/rtl/config_pkg.sv
@@ -7,7 +7,7 @@ package config_pkg;
 
   /* We use a byte-sliced datapath, inspired by the
    * classic bit-sliced architecture of old CPUs. */
-  localparam int unsigned SLICE_WIDTH      = 8;
+  localparam int unsigned SLICE_WIDTH = 8;
 
   /* The RV32E ISA defines 16 general-purpose registers.
    * We have two read ports to allow for pipelined reads. */
diff --git a/rtl/montreal_pkg.sv b/rtl/montreal_pkg.sv
deleted file mode 100644
index b3a13a0..0000000
--- a/rtl/montreal_pkg.sv
+++ /dev/null
@@ -1,8 +0,0 @@
-/* SPDX-License-Identifier: CERN-OHL-P-2.0 */
-
-package montreal_pkg;
-
-  typedef logic unsigned [config_pkg::XLEN-1:0]        word_t;
-  typedef logic unsigned [config_pkg::SLICE_WIDTH-1:0] slice_t;
-
-endpackage : montreal_pkg
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
diff --git a/rtl/types.svh b/rtl/types.svh
new file mode 100644
index 0000000..ca8a675
--- /dev/null
+++ b/rtl/types.svh
@@ -0,0 +1,9 @@
+`ifndef TYPES_SVH
+`define TYPES_SVH
+
+typedef logic                                        [config_pkg::XLEN-1:0] word_t;
+typedef logic [2 ** config_pkg::REG_ADDR_WIDTH - 1:0][config_pkg::XLEN-1:0] word_bank_t;
+
+typedef logic [config_pkg::SLICE_WIDTH-1:0] slice_t;
+
+`endif /* TYPES_SVH */
-- 
cgit v1.2.3