diff options
| -rw-r--r-- | rtl/config_pkg.sv | 2 | ||||
| -rw-r--r-- | rtl/montreal_pkg.sv | 8 | ||||
| -rw-r--r-- | rtl/regfile.sv | 21 | ||||
| -rw-r--r-- | rtl/types.svh | 9 |
4 files changed, 27 insertions, 13 deletions
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 */ |