From a22f935d827879706a9b4ae481e05f22810f8b61 Mon Sep 17 00:00:00 2001 From: Warrick Lo Date: Tue, 16 Jun 2026 22:13:10 +0000 Subject: regfile: refactor: 'chunks' are now 'slices' The term 'slice' is more consistent with old CPU architectures and academic literature. Signed-off-by: Warrick Lo --- rtl/regfile.sv | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/rtl/regfile.sv b/rtl/regfile.sv index 1758c1a..8ca992c 100644 --- a/rtl/regfile.sv +++ b/rtl/regfile.sv @@ -8,40 +8,40 @@ * 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. */ module regfile #( - parameter int unsigned WORD_WIDTH = 32, - parameter int unsigned ADDR_WIDTH = 4, - parameter int unsigned CHUNK_WIDTH = 8, + parameter int unsigned WORD_WIDTH = 32, + parameter int unsigned ADDR_WIDTH = 4, + parameter int unsigned SLICE_WIDTH = 8, parameter int unsigned NUM_READ_PORTS = 2, localparam int unsigned NUM_WORDS = 2 ** ADDR_WIDTH, - localparam int unsigned NUM_CHUNKS = WORD_WIDTH / CHUNK_WIDTH + localparam int unsigned NUM_SLICES = WORD_WIDTH / SLICE_WIDTH ) ( input logic clk_i, input logic rst_ni, - input logic [$clog2(NUM_CHUNKS)-1:0] chunk_sel_i, + input logic [$clog2(NUM_SLICES)-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; 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 +50,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 -- cgit v1.2.3 From ef9254b3303a03ea4ab3c32aaf1d79df651e3b92 Mon Sep 17 00:00:00 2001 From: Warrick Lo Date: Wed, 17 Jun 2026 00:44:02 +0000 Subject: Move design parameters to config_pkg Signed-off-by: Warrick Lo --- rtl/config_pkg.sv | 17 +++++++++++++++++ rtl/montreal_pkg.sv | 8 ++++++++ rtl/regfile.sv | 22 ++++++++++++---------- 3 files changed, 37 insertions(+), 10 deletions(-) create mode 100644 rtl/config_pkg.sv create mode 100644 rtl/montreal_pkg.sv diff --git a/rtl/config_pkg.sv b/rtl/config_pkg.sv new file mode 100644 index 0000000..0120b14 --- /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/montreal_pkg.sv b/rtl/montreal_pkg.sv new file mode 100644 index 0000000..b3a13a0 --- /dev/null +++ b/rtl/montreal_pkg.sv @@ -0,0 +1,8 @@ +/* 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 8ca992c..e18301a 100644 --- a/rtl/regfile.sv +++ b/rtl/regfile.sv @@ -15,18 +15,20 @@ * read ports (default 2). Register 0 is fixed to 0 for all reads. */ -module regfile #( - parameter int unsigned WORD_WIDTH = 32, - parameter int unsigned ADDR_WIDTH = 4, - parameter int unsigned SLICE_WIDTH = 8, - parameter int unsigned NUM_READ_PORTS = 2, - - localparam int unsigned NUM_WORDS = 2 ** ADDR_WIDTH, - localparam int unsigned NUM_SLICES = WORD_WIDTH / SLICE_WIDTH +module regfile + import montreal_pkg::*; +#( + 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 SLICE_ADDR_WIDTH = $clog2(XLEN / SLICE_WIDTH) ) ( input logic clk_i, input logic rst_ni, - input logic [$clog2(NUM_SLICES)-1:0] slice_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][SLICE_WIDTH-1:0] rdata_o, @@ -36,7 +38,7 @@ module regfile #( input logic [SLICE_WIDTH-1:0] wdata_i ); - logic [NUM_WORDS-1:0][WORD_WIDTH-1:0] register; + logic [NUM_WORDS-1:0][XLEN-1:0] register; always_comb begin for (int i = 0; i < NUM_READ_PORTS; i++) begin : gen_read_block -- cgit v1.2.3 From 2455fed25341b39d505bcdad9ae2b07c6cd42a73 Mon Sep 17 00:00:00 2001 From: Warrick Lo 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 --- 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 From c8261a040bf328d4d2296f0c91a85a4193195844 Mon Sep 17 00:00:00 2001 From: Warrick Lo Date: Thu, 18 Jun 2026 23:20:11 -0700 Subject: Add formal verification for regfile Successfully verifies the following requirements: * REQ-REGFILE-010 * 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-053 * REQ-REGFILE-060 Verified through construction of regfile: * REQ-REGFILE-040 See-also: #14 Signed-off-by: Warrick Lo --- verif/formal/regfile/regfile.sby | 23 ++++ verif/formal/regfile/regfile_ind.sv | 221 ++++++++++++++++++++++++++++++++++++ 2 files changed, 244 insertions(+) create mode 100644 verif/formal/regfile/regfile.sby create mode 100644 verif/formal/regfile/regfile_ind.sv diff --git a/verif/formal/regfile/regfile.sby b/verif/formal/regfile/regfile.sby new file mode 100644 index 0000000..89f8884 --- /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_ind.sv +prep -top regfile_ind + +[files] +rtl/types.svh +rtl/config_pkg.sv +rtl/regfile.sv +verif/formal/regfile/regfile_ind.sv diff --git a/verif/formal/regfile/regfile_ind.sv b/verif/formal/regfile/regfile_ind.sv new file mode 100644 index 0000000..af200e8 --- /dev/null +++ b/verif/formal/regfile/regfile_ind.sv @@ -0,0 +1,221 @@ +/* SPDX-License-Identifier: CERN-OHL-P-2.0 */ + +/** + * @brief Formal verification of regfile requirements + * @author Warrick Lo + */ + +`include "types.svh" + +module regfile_ind ( + 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 + /* verilog_lint: waive dff-name-style */ + past_valid <= '1; + end + + /* + * REQ-REGFILE-010: + * The module must store NUM_WORDS words, each XLEN bits wide. + * + * Notes: This verification module assumes NUM_WORDS = 16 and XLEN = 32. + * 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]. + * + * Notes: This verification module assumes XLEN = 32 and SLICE_WIDTH = 8. + * These three requirements are easiest to verify together. + */ + + always_comb begin + 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-REGFILE-030: + * Register contents must be 0 at most one clock after the synchronous reset is asserted. + */ + + always_ff @(posedge clk_i) begin + if (past_valid && $past(!rst_ni, 1)) begin + assert (register == '0); + end + end + + /* + * REQ-REGFILE-040: + * Writes to the register file must only occur on the rising edge of clk_i. + */ + + /* Structural requirement satisfied by construction. */ + + /* + * REQ-REGFILE-041: + * Writes to the register file must only occur when wen_i is asserted. + */ + + always_ff @(posedge clk_i) begin + 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-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 + for (int i = 0; i < 16; i++) begin + for (int j = 0; j < 4; j++) begin + /* Ignore reset events. */ + if (!past_valid) begin + end else if ($past(!rst_ni)) begin + end else if ((i == $past(waddr_i)) && (j == $past(slice_sel_i))) begin + assert ($stable(register[i][j*8+:8]) || (register[i][j*8+:8] == $past(wdata_i))); + end else begin + assert ($stable(register[i][j*8+:8])); + end + end + end + end + + /* + * REQ-REGFILE-043: + * Writes to register 0 shall be silently ignored, regardless of the state of wen_i. + */ + + always_ff @(posedge clk_i) begin + if (past_valid && $past(rst_ni && waddr_i == '0)) begin + assert ($stable(register[0])); + end + end + + /* + * 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 + if (raddr_i[0] == '0) assert (rdata[0] == '0); + if (raddr_i[1] == '0) assert (rdata[1] == '0); + end + + /* + * REQ-REGFILE-053: + * Requirement DR-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 + if (!rst_ni) begin + rst_asserted <= '1; + end + + cover (!rst_asserted); + end + + /* + * 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. + */ + + logic [7:0] x0, x8; + assign x0 = register[0]; + assign x8 = register[8]; + + always_comb begin + 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 + +endmodule : regfile_ind -- cgit v1.2.3 From c348e393521750d8dd6d7ba57bd91e4b935dbbd7 Mon Sep 17 00:00:00 2001 From: Warrick Lo Date: Sat, 20 Jun 2026 04:50:19 -0700 Subject: Minor refactor to regfile formal test module Signed-off-by: Warrick Lo --- verif/formal/regfile/regfile.sby | 6 +- verif/formal/regfile/regfile_fv.sv | 248 ++++++++++++++++++++++++++++++++++++ verif/formal/regfile/regfile_ind.sv | 221 -------------------------------- 3 files changed, 251 insertions(+), 224 deletions(-) create mode 100644 verif/formal/regfile/regfile_fv.sv delete mode 100644 verif/formal/regfile/regfile_ind.sv diff --git a/verif/formal/regfile/regfile.sby b/verif/formal/regfile/regfile.sby index 89f8884..69cb7b9 100644 --- a/verif/formal/regfile/regfile.sby +++ b/verif/formal/regfile/regfile.sby @@ -13,11 +13,11 @@ smtbmc [script] read -formal -sv config_pkg.sv read -formal -sv regfile.sv -read -formal -sv regfile_ind.sv -prep -top regfile_ind +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_ind.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 + * + * 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 diff --git a/verif/formal/regfile/regfile_ind.sv b/verif/formal/regfile/regfile_ind.sv deleted file mode 100644 index af200e8..0000000 --- a/verif/formal/regfile/regfile_ind.sv +++ /dev/null @@ -1,221 +0,0 @@ -/* SPDX-License-Identifier: CERN-OHL-P-2.0 */ - -/** - * @brief Formal verification of regfile requirements - * @author Warrick Lo - */ - -`include "types.svh" - -module regfile_ind ( - 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 - /* verilog_lint: waive dff-name-style */ - past_valid <= '1; - end - - /* - * REQ-REGFILE-010: - * The module must store NUM_WORDS words, each XLEN bits wide. - * - * Notes: This verification module assumes NUM_WORDS = 16 and XLEN = 32. - * 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]. - * - * Notes: This verification module assumes XLEN = 32 and SLICE_WIDTH = 8. - * These three requirements are easiest to verify together. - */ - - always_comb begin - 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-REGFILE-030: - * Register contents must be 0 at most one clock after the synchronous reset is asserted. - */ - - always_ff @(posedge clk_i) begin - if (past_valid && $past(!rst_ni, 1)) begin - assert (register == '0); - end - end - - /* - * REQ-REGFILE-040: - * Writes to the register file must only occur on the rising edge of clk_i. - */ - - /* Structural requirement satisfied by construction. */ - - /* - * REQ-REGFILE-041: - * Writes to the register file must only occur when wen_i is asserted. - */ - - always_ff @(posedge clk_i) begin - 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-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 - for (int i = 0; i < 16; i++) begin - for (int j = 0; j < 4; j++) begin - /* Ignore reset events. */ - if (!past_valid) begin - end else if ($past(!rst_ni)) begin - end else if ((i == $past(waddr_i)) && (j == $past(slice_sel_i))) begin - assert ($stable(register[i][j*8+:8]) || (register[i][j*8+:8] == $past(wdata_i))); - end else begin - assert ($stable(register[i][j*8+:8])); - end - end - end - end - - /* - * REQ-REGFILE-043: - * Writes to register 0 shall be silently ignored, regardless of the state of wen_i. - */ - - always_ff @(posedge clk_i) begin - if (past_valid && $past(rst_ni && waddr_i == '0)) begin - assert ($stable(register[0])); - end - end - - /* - * 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 - if (raddr_i[0] == '0) assert (rdata[0] == '0); - if (raddr_i[1] == '0) assert (rdata[1] == '0); - end - - /* - * REQ-REGFILE-053: - * Requirement DR-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 - if (!rst_ni) begin - rst_asserted <= '1; - end - - cover (!rst_asserted); - end - - /* - * 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. - */ - - logic [7:0] x0, x8; - assign x0 = register[0]; - assign x8 = register[8]; - - always_comb begin - 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 - -endmodule : regfile_ind -- cgit v1.2.3