Merge branch 'feature/core'

* feature/core:
  Minor refactor to regfile formal test module
  Add formal verification for regfile
  Move typedefs to types.svh from montreal_pkg
  Move design parameters to config_pkg
  regfile: refactor: 'chunks' are now 'slices'

See-also: #13
See-also: #14
Reviewed-by: Warrick Lo <wlo@warricklo.net>

3 files changed, 58 insertions, 17 deletions

diff --git a/rtl/config_pkg.sv b/rtl/config_pkg.sv
new file mode 100644
index 0000000..01d6c20
--- /dev/null
+++ b/rtl/config_pkg.sv
@@ -0,0 +1,17 @@
+/* SPDX-License-Identifier: CERN-OHL-P-2.0 */
+
+package config_pkg;
+
+  /* Word width as defined in the RISC-V spec. */
+  localparam int unsigned XLEN = 32;
+
+  /* We use a byte-sliced datapath, inspired by the
+   * classic bit-sliced architecture of old CPUs. */
+  localparam int unsigned SLICE_WIDTH = 8;
+
+  /* The RV32E ISA defines 16 general-purpose registers.
+   * We have two read ports to allow for pipelined reads. */
+  localparam int unsigned REG_ADDR_WIDTH     = 4;
+  localparam int unsigned REG_NUM_READ_PORTS = 2;
+
+endpackage : config_pkg
diff --git a/rtl/regfile.sv b/rtl/regfile.sv
index 1758c1a..66af045 100644
--- a/rtl/regfile.sv
+++ b/rtl/regfile.sv
@@ -8,40 +8,55 @@
  * Register file
  *
  * This module contains the register file for the RISC-V core. Each word is
- * partitioned into chunks (default 8 bits). A global chunk selector determines
- * which chunk of each word is accessed for both read and write operations.
+ * partitioned into slices (default 8 bits). A global slice selector determines
+ * which slice of each word is accessed for both read and write operations.
  *
  * The register file has one synchronous write port and a configurable number of
  * read ports (default 2). Register 0 is fixed to 0 for all reads.
  */
 
+`include "types.svh"
+
 module regfile #(
-  parameter int unsigned WORD_WIDTH = 32,
-  parameter int unsigned ADDR_WIDTH = 4,
-  parameter int unsigned CHUNK_WIDTH = 8,
-  parameter int unsigned NUM_READ_PORTS = 2,
+  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,
+  parameter int unsigned NUM_READ_PORTS = config_pkg::REG_NUM_READ_PORTS,
 
-  localparam int unsigned NUM_WORDS  = 2 ** ADDR_WIDTH,
-  localparam int unsigned NUM_CHUNKS = WORD_WIDTH / CHUNK_WIDTH
+  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 [$clog2(NUM_CHUNKS)-1:0] chunk_sel_i,
+  input logic [SLICE_ADDR_WIDTH-1:0] slice_sel_i,
 
-  input  logic [NUM_READ_PORTS-1:0][ ADDR_WIDTH-1:0] raddr_i,
-  output logic [NUM_READ_PORTS-1:0][CHUNK_WIDTH-1:0] rdata_o,
+  input  logic [NUM_READ_PORTS-1:0][ADDR_WIDTH-1:0]  raddr_i,
+  output logic [NUM_READ_PORTS-1:0][SLICE_WIDTH-1:0] rdata_o,
 
   input logic wen_i,
-  input logic [ADDR_WIDTH-1:0] waddr_i,
-  input logic [CHUNK_WIDTH-1:0] wdata_i
+  input logic [ADDR_WIDTH-1:0]  waddr_i,
+  input logic [SLICE_WIDTH-1:0] wdata_i
 );
 
-  logic [NUM_WORDS-1:0][WORD_WIDTH-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
-      rdata_o[i] = (raddr_i[i] == 0)
-          ? '0 : register[raddr_i[i]][chunk_sel_i*CHUNK_WIDTH +: CHUNK_WIDTH];
+      rdata_o[i] = (raddr_i[i] == '0)
+          ? '0 : register[raddr_i[i]][slice_sel_i*SLICE_WIDTH +: SLICE_WIDTH];
     end : gen_read_block
   end
 
@@ -50,7 +65,7 @@ module regfile #(
       register <= '0;
     end else if (wen_i && (waddr_i != '0)) begin
       /* verilog_lint: waive dff-name-style */
-      register[waddr_i][chunk_sel_i*CHUNK_WIDTH +: CHUNK_WIDTH] <= wdata_i;
+      register[waddr_i][slice_sel_i*SLICE_WIDTH +: SLICE_WIDTH] <= wdata_i;
     end
   end
 
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 */