aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--rtl/config_pkg.sv17
-rw-r--r--rtl/regfile.sv49
-rw-r--r--rtl/types.svh9
-rw-r--r--verif/formal/regfile/regfile.sby23
-rw-r--r--verif/formal/regfile/regfile_fv.sv248
5 files changed, 329 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 */
diff --git a/verif/formal/regfile/regfile.sby b/verif/formal/regfile/regfile.sby
new file mode 100644
index 0000000..69cb7b9
--- /dev/null
+++ b/verif/formal/regfile/regfile.sby
@@ -0,0 +1,23 @@
+[tasks]
+cover
+prove
+
+[options]
+cover: mode cover
+prove: mode prove
+prove: depth 20
+
+[engines]
+smtbmc
+
+[script]
+read -formal -sv config_pkg.sv
+read -formal -sv regfile.sv
+read -formal -sv regfile_fv.sv
+prep -top regfile_fv
+
+[files]
+rtl/types.svh
+rtl/config_pkg.sv
+rtl/regfile.sv
+verif/formal/regfile/regfile_fv.sv
diff --git a/verif/formal/regfile/regfile_fv.sv b/verif/formal/regfile/regfile_fv.sv
new file mode 100644
index 0000000..795024e
--- /dev/null
+++ b/verif/formal/regfile/regfile_fv.sv
@@ -0,0 +1,248 @@
+/* SPDX-License-Identifier: CERN-OHL-P-2.0 */
+
+/*
+ * Copyright 2026 UBC ASIC contributors (Montreal project).
+ *
+ * Author: Warrick Lo <wlo@warricklo.net>
+ *
+ * Formal verification of regfile requirements
+ *
+ * This module verifies the regfile module against the requirements
+ * specified in the design specification.
+ *
+ * The following parameters are used for all tests:
+ * - Word width: 32 bits wide
+ * - Slice width: 8 bits wide
+ * - Number of words: 16 words
+ * - Number of read ports: 2
+ *
+ * The following are design requirements that are assumed to be verifed by construction:
+ * - REQ-REGFILE-010
+ * - REQ-REGFILE-040
+ * REQ-REGFILE-010 is further verified below.
+ *
+ * The following requirements are verified through this module:
+ * - Cover:
+ * - REQ-REGFILE-053
+ * - Bounded model checking:
+ * - REQ-REGFILE-010
+ * - REQ-REGFILE-053
+ * - K-induction:
+ * - REQ-REGFILE-020
+ * - REQ-REGFILE-030
+ * - REQ-REGFILE-041
+ * - REQ-REGFILE-042
+ * - REQ-REGFILE-043
+ * - REQ-REGFILE-050
+ * - REQ-REGFILE-051
+ * - REQ-REGFILE-052
+ * - REQ-REGFILE-060
+ *
+ * See also: MAS, Regfile Specification, version 0.2
+ * rtl/regfile.sv
+ */
+
+`include "types.svh"
+
+module regfile_fv (
+ input logic clk_i,
+ input logic rst_ni,
+ input logic [1:0] slice_sel_i,
+
+ input logic [1:0][3:0] raddr_i,
+
+ input logic wen_i,
+ input logic [3:0] waddr_i,
+ input logic [7:0] wdata_i
+);
+
+ /*
+ * DUT interface and internal signals.
+ */
+
+ word_bank_t register;
+ logic [1:0][7:0] rdata;
+
+ /*
+ * DUT instance.
+ */
+
+ regfile #(
+ .XLEN(32),
+ .SLICE_WIDTH(8),
+ .ADDR_WIDTH(4),
+ .NUM_READ_PORTS(2)
+ ) dut (
+ .register_dbg(register),
+ .clk_i,
+ .rst_ni,
+ .slice_sel_i,
+
+ .raddr_i,
+ .rdata_o(rdata),
+
+ .wen_i,
+ .waddr_i,
+ .wdata_i
+ );
+
+ /*
+ * Some assertions use $past(), which requires at least one clock edge.
+ * Those tests will use past_valid to check if a valid history exists.
+ */
+
+ logic past_valid;
+
+ initial assume (past_valid == '0);
+
+ always_ff @(posedge clk_i) begin : past_valid_dff
+ /* verilog_lint: waive dff-name-style */
+ past_valid <= '1;
+ end : past_valid_dff
+
+ /*
+ * REQ-REGFILE-010:
+ * The module must store NUM_WORDS words, each XLEN bits wide.
+ */
+
+ /* The definition of 'register' must use the type defined in types.svh. */
+ initial assert ($bits(register) == 16 * 32);
+
+ /*
+ * REQ-REGFILE-020:
+ * Slice k of word n shall correspond to bits [(k+1)*SLICE_WIDTH−1:k*SLICE_WIDTH]
+ * of register n, partitioning each word into XLEN/SLICE_WIDTH
+ * non-overlapping slices, each SLICE_WIDTH bits wide.
+ *
+ * REQ-REGFILE-050:
+ * The read output rdata_o[i] shall be combinationally derived from
+ * the current register state, raddr_i[i], and slice_sel_i. There shall not
+ * be any latency on reads.
+ *
+ * REQ-REGFILE-051:
+ * The read output rdata_o[i] must reflect the slice selected by slice_sel_i
+ * within the register selected by raddr_i[i].
+ *
+ * Note: These three requirements are easiest to verify together.
+ */
+
+ /* We explicitly ignore the use of part-selects to verify the description of REQ-REGFILE-020. */
+ always_comb begin : req_020_050_051
+ if (raddr_i[0] != '0) begin
+ assert (rdata[0] == register[raddr_i[0]][(slice_sel_i + 1) * 8 - 1 : slice_sel_i * 8]);
+ end
+ if (raddr_i[1] != '0) begin
+ assert (rdata[1] == register[raddr_i[1]][(slice_sel_i + 1) * 8 - 1 : slice_sel_i * 8]);
+ end
+ end : req_020_050_051
+
+ /*
+ * REQ-REGFILE-030:
+ * Register contents must be 0 at most one clock after the synchronous reset is asserted.
+ */
+
+ always_ff @(posedge clk_i) begin : req_030
+ if (past_valid && $past(!rst_ni, 1)) begin
+ assert (register == '0);
+ end
+ end : req_030
+
+ /*
+ * REQ-REGFILE-041:
+ * Writes to the register file must only occur when wen_i is asserted.
+ */
+
+ always_ff @(posedge clk_i) begin : req_041
+ if (past_valid && $past(rst_ni && !wen_i, 1)) begin
+ /* Satisfies the requirement, but possibly not the intended RTL behaviour.
+ * See ticket #14. */
+ assert ($stable(register));
+ end
+ end : req_041
+
+ /*
+ * REQ-REGFILE-042:
+ * Contents of wdata_i must be written only to the slice selected by slice_sel_i
+ * within the register selected by waddr_i. All other slices of the target register
+ * shall remain unchanged.
+ */
+
+ /* We'll use a part-select to obtain the slice data since we can assume that
+ * slice_sel_i will select the correct slice within the target register,
+ * according to requirement REQ-REGFILE-020. */
+ always_ff @(posedge clk_i) begin : req_042
+ /* For register 0, this test will specifically permit writes targeting
+ * the register to succeed. The stability of register 0 is separately
+ * verified below in REQ-REGFILE-043. */
+ for (int i = 0; i < 16; i++) begin : word_loop
+ for (int j = 0; j < 4; j++) begin : slice_loop
+ /* Ignore reset events. */
+ if (past_valid && $past(rst_ni, 1)) begin
+ if ($past((waddr_i == i) && (slice_sel_i == j), 1)) begin
+ assert ($stable(register[i][j*8+:8]) || (register[i][j*8+:8] == $past(wdata_i, 1)));
+ end else begin
+ assert ($stable(register[i][j*8+:8]));
+ end
+ end
+ end : slice_loop
+ end : word_loop
+ end : req_042
+
+ /*
+ * REQ-REGFILE-043:
+ * Writes to register 0 shall be silently ignored, regardless of the state of wen_i.
+ */
+
+ always_ff @(posedge clk_i) begin : req_043
+ if (past_valid && $past(rst_ni && (waddr_i == '0), 1)) begin
+ assert ($stable(register[0]));
+ end
+ end : req_043
+
+ /*
+ * REQ-REGFILE-052:
+ * The read output rdata[i] must be zero when raddr[i] is zero,
+ * regardless of any prior writes to register 0.
+ */
+
+ always_comb begin : req_052
+ if (raddr_i[0] == '0) assert (rdata[0] == '0);
+ if (raddr_i[1] == '0) assert (rdata[1] == '0);
+ end : req_052
+
+ /*
+ * REQ-REGFILE-053:
+ * Requirement REQ-REGFILE-052 shall be unconditional: it must hold at power-on
+ * without reset having been asserted, and at all times during normal operation.
+ */
+
+ logic rst_asserted;
+
+ initial assume (rst_asserted == '0);
+
+ always_ff @(posedge clk_i) begin : req_053
+ if (!rst_ni) begin
+ rst_asserted <= '1;
+ end
+
+ cover (!rst_asserted && wen_i && (waddr_i == '0));
+ end : req_053
+
+ /*
+ * REQ-REGFILE-060:
+ * The module shall not implement any bypass logic. A read and write to
+ * the same address in the same cycle shall return the value held in
+ * the register prior to the rising clock edge of the current cycle.
+ */
+
+ /* Similar to above, we will use a part-select here. */
+ always_comb begin : req_060
+ if (wen_i && raddr_i[0] != '0 && raddr_i[0] == waddr_i) begin
+ assert (rdata[0] == register[raddr_i[0]][slice_sel_i*8+:8]);
+ end
+ if (wen_i && raddr_i[1] != '0 && raddr_i[1] == waddr_i) begin
+ assert (rdata[1] == register[raddr_i[1]][slice_sel_i*8+:8]);
+ end
+ end : req_060
+
+endmodule : regfile_fv
generated by cgit v1.2.3 (git 2.39.1) at 2026-07-17 11:43:29 +0000