Merge pull request openhwgroup#2304 from silabs-krdosvik/40s

fix assert
silabs-robin · Nov 30, 2023 · b6bbc40 · b6bbc40
2 parents 6b600f9 + d52afed
commit b6bbc40
Show file tree

Hide file tree

Showing 3 changed files with 77 additions and 15 deletions.
diff --git a/cv32e40s/tb/assertions/uvmt_cv32e40s_pmprvfi_assert.sv b/cv32e40s/tb/assertions/uvmt_cv32e40s_pmprvfi_assert.sv
@@ -23,6 +23,7 @@
 module uvmt_cv32e40s_pmprvfi_assert
   import cv32e40s_pkg::*;
   import support_pkg::*;
+  import isa_decoder_pkg::*;
   import uvm_pkg::*;
   import uvma_rvfi_pkg::*;
   import uvma_rvfi_pkg::EXC_CAUSE_INSTR_BUS_FAULT;
@@ -38,6 +39,7 @@ module uvmt_cv32e40s_pmprvfi_assert
 
   //RVFI INSTR IF
   uvma_rvfi_instr_if_t    rvfi_if,
+  uvmt_cv32e40s_support_logic_module_o_if_t.slave_mp  support_if,
   // RVFI
   input wire              rvfi_valid,
   input wire [31:0]       rvfi_insn,
@@ -146,7 +148,7 @@ module uvmt_cv32e40s_pmprvfi_assert
 
   wire  is_rvfi_csr_write_instr =
     is_rvfi_csr_instr  &&
-    !((rvfi_insn[13:12] inside {2'b 10, 2'b 11}) && !rvfi_rs1_addr);  // CSRRS/C[I] w/ rs1=x0/0
+    !((rvfi_insn[13:12] inside {2'b 01, 2'b 10, 2'b 11}) && !rvfi_rs1_addr);  // CSRRW/S/C[I] w/ rs1=x0/0
 
   wire [1:0]  rvfi_effective_mode =
     rvfi_csr_mstatus_rdata[17]      ?  // "mstatus.MPRV", modify privilege?
@@ -507,26 +509,84 @@ module uvmt_cv32e40s_pmprvfi_assert
 
 
   // Stickiness isn't effectuated before triggered  (vplan:LockingBypass:UntilReset)
+  logic first_MSECCFG_access;
+
+  always @(posedge clk_i, negedge rst_ni) begin
+    if (rst_ni == 0) begin
+      first_MSECCFG_access <= 1'b 1;
+    end else if (
+      rvfi_valid &&
+      !rvfi_trap &&
+      (support_if.asm_rvfi.instr == CSRRW ||
+      support_if.asm_rvfi.instr == CSRRS  ||
+      support_if.asm_rvfi.instr == CSRRC  ||
+      support_if.asm_rvfi.instr == CSRRWI  ||
+      support_if.asm_rvfi.instr == CSRRSI ||
+      support_if.asm_rvfi.instr == CSRRCI)
+    ) begin
+      first_MSECCFG_access <= 1'b 0;
+    end
+  end
 
-  property  p_until_reset_notbefore(logic rlb);
-    $rose(rst_ni)                                               ##0
-    (rvfi_valid [->1])                                          ##0  // First retire
-    (is_rvfi_csr_write_instr && (rvfi_insn[14:12] == 3'b 001))  ##0  // ..."csrrw"
-    (rvfi_insn[31:20] == CSRADDR_MSECCFG)                       ##0  // ...to mseccfg
-    !rvfi_trap                                                  ##0
-    (rvfi_rs1_rdata[2] == rlb)                                       // (Write-attempt's data)
-    |->
-    pmp_csr_rvfi_wmask.mseccfg.rlb          &&  // Must attempt
-    (pmp_csr_rvfi_wdata.mseccfg.rlb == rlb)     // Must succeed
-    ;
-  endproperty : p_until_reset_notbefore
 
   a_until_reset_notbefore_0: assert property (
-    p_until_reset_notbefore(1'b 0)
+
+    // First write access to MSECCFG:
+    (rvfi_valid &&
+    first_MSECCFG_access &&
+
+    support_if.asm_rvfi.csr.address == MSECCFG &&
+    support_if.asm_rvfi.csr.valid &&
+
+    (support_if.asm_rvfi.instr == CSRRW ||
+    support_if.asm_rvfi.instr == CSRRC ||
+    support_if.asm_rvfi.instr == CSRRWI ||
+    support_if.asm_rvfi.instr == CSRRCI) &&
+
+    !rvfi_trap)
+
+    ##0
+
+    // Set RLB bit to 0:
+    ((support_if.asm_rvfi.instr == CSRRW && rvfi_rs1_rdata[2] == 1'b0) ||
+    (support_if.asm_rvfi.instr == CSRRC && rvfi_rs1_rdata[2] == 1'b1) ||
+    (support_if.asm_rvfi.instr == CSRRWI && support_if.asm_rvfi.imm.imm_value[2] == 1'b0) ||
+    (support_if.asm_rvfi.instr == CSRRCI && support_if.asm_rvfi.imm.imm_value[2] == 1'b1))
+
+    |->
+    pmp_csr_rvfi_wmask.mseccfg.rlb          &&  // Must attempt
+    (pmp_csr_rvfi_wdata.mseccfg.rlb == 1'b0)     // Must succeed
   ) else `uvm_error(info_tag, "RLB must be changeable after reset");
 
+
   a_until_reset_notbefore_1: assert property (
-    p_until_reset_notbefore(1'b 1)
+
+    // First write access to MSECCFG:
+    (rvfi_valid &&
+    first_MSECCFG_access &&
+
+    support_if.asm_rvfi.csr.address == MSECCFG &&
+    support_if.asm_rvfi.csr.valid &&
+
+    (support_if.asm_rvfi.instr == CSRRW ||
+    support_if.asm_rvfi.instr == CSRRS ||
+    support_if.asm_rvfi.instr == CSRRWI ||
+    support_if.asm_rvfi.instr == CSRRSI) &&
+
+    !rvfi_trap)
+
+    ##0
+
+    // Set RLB bit to 1:
+    ((support_if.asm_rvfi.instr == CSRRW || support_if.asm_rvfi.instr == CSRRS) &&
+    rvfi_rs1_rdata[2] == 1'b1) ||
+
+    ((support_if.asm_rvfi.instr == CSRRWI || support_if.asm_rvfi.instr == CSRRSI) &&
+    support_if.asm_rvfi.imm.imm_value[2])
+
+    |->
+    pmp_csr_rvfi_wmask.mseccfg.rlb          &&  // Must attempt
+    (pmp_csr_rvfi_wdata.mseccfg.rlb == 1'b1)     // Must succeed
   ) else `uvm_error(info_tag, "RLB must be changeable after reset");
 
 

diff --git a/cv32e40s/tb/uvmt/uvmt_cv32e40s_tb.sv b/cv32e40s/tb/uvmt/uvmt_cv32e40s_tb.sv
@@ -1526,6 +1526,7 @@ module uvmt_cv32e40s_tb;
         .PMP_NUM_REGIONS (uvmt_cv32e40s_base_test_pkg::CORE_PARAM_PMP_NUM_REGIONS)
       ) pmprvfi_assert_i (
         .rvfi_if        (dut_wrap.cv32e40s_wrapper_i.rvfi_instr_if),
+        .support_if     (support_logic_module_o_if.slave_mp),
         .rvfi_mem_addr  (rvfi_mem_addr [31:0]),
         .rvfi_mem_wmask (rvfi_mem_wmask[ 3:0]),
         .rvfi_mem_rmask (rvfi_mem_rmask[ 3:0]),

diff --git a/lib/isa_decoder/isa_typedefs_csr.sv b/lib/isa_decoder/isa_typedefs_csr.sv
@@ -47,6 +47,7 @@
     MSCRATCHCSW   = 12'h348,
     MSCRATCHCSWL  = 12'h349,
     MCLICBASE     = 12'h34A,
+    MSECCFG       = 12'h747,
     TSELECT       = 12'h7A0,
     TDATA1        = 12'h7A1,
     TDATA2        = 12'h7A2,