diff options
Diffstat (limited to 'verif/formal/regfile/regfile_ind.sv')
| -rw-r--r-- | verif/formal/regfile/regfile_ind.sv | 221 |
1 files changed, 0 insertions, 221 deletions
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 |