detect pma load/store fault, use in assert

Signed-off-by: Robin Pedersen <Robin.Pedersen@silabs.com>
openhwgroup · Dec 14, 2023 · 6a1f2f7 · 6a1f2f7
1 parent afbbe5e
commit 6a1f2f7
Show file tree

Hide file tree

Showing 2 changed files with 48 additions and 5 deletions.
diff --git a/cv32e40s/tb/uvmt/uvmt_cv32e40s_pma_assert.sv b/cv32e40s/tb/uvmt/uvmt_cv32e40s_pma_assert.sv
@@ -146,12 +146,20 @@ module  uvmt_cv32e40s_pma_assert
 
   // After PMA-deny, subsequent accesses are also suppressed  (vplan:"Multi-memory operation instructions")
 
-  a_failure_denies_subsequents: assert property (
-    rvfi_instr_if.is_pma_instr_fault
+  a_failure_denies_subsequents_loads: assert property (
+    rvfi_instr_if.is_pma_data_fault
     |->
-    (rvfi_instr_if.rvfi_mem_wmask == '0)
-    //TODO:ERROR:silabs-robin Zcmp should be able to break this. RVFI bug.
-    //TODO:ERROR:silabs-robin Also reads
+    (rvfi_instr_if.rvfi_mem_rmask != rvfi_instr_if.rvfi_mem_rmask_intended)
+    ||
+    (rvfi_instr_if.rvfi_mem_rmask == 'd 0)
+  ) else `uvm_error(info_tag, "accesses aftmr pma fault should be suppressed");
+
+  a_failure_denies_subsequents_stores: assert property (
+    rvfi_instr_if.is_pma_data_fault
+    |->
+    (rvfi_instr_if.rvfi_mem_wmask != rvfi_instr_if.rvfi_mem_wmask_intended)
+    ||
+    (rvfi_instr_if.rvfi_mem_wmask == 'd 0)
   ) else `uvm_error(info_tag, "accesses aftmr pma fault should be suppressed");
 
   property p_partial_pma_allow (exc_cause);
@@ -174,6 +182,16 @@ module  uvmt_cv32e40s_pma_assert
   );
 
 
+  // PMA-deny on instr, no mem op  (vplan: Not a vplan item. Inspo from a_failure_denies_subsequents.)
+
+  a_failure_denies_memops: assert property (
+    rvfi_instr_if.is_pma_instr_fault
+    |->
+    (rvfi_instr_if.rvfi_mem_wmask == '0)  &&
+    (rvfi_instr_if.rvfi_mem_rmask == '0)
+  ) else `uvm_error(info_tag, "pma-blocked instrs shouldn't access the bus");
+
+
   // MPU-accepted transactions must reach OBI  (vplan: not a vplan item)
 
   property p_eventually_mpu2obi;

diff --git a/lib/uvm_agents/uvma_rvfi/uvma_rvfi_instr_if.sv b/lib/uvm_agents/uvma_rvfi/uvma_rvfi_instr_if.sv
@@ -242,6 +242,9 @@ interface uvma_rvfi_instr_if_t
   logic                             is_umode;
   logic                             is_not_umode;
   logic                             is_pma_instr_fault;
+  logic                             is_pma_data_fault;
+  logic                             is_pma_load_fault;
+  logic                             is_pma_store_fault;
   logic                             is_instr_acc_fault_pmp;
   logic                             is_instr_bus_valid;
   logic                             is_pushpop;
@@ -411,6 +414,28 @@ interface uvma_rvfi_instr_if_t
     is_pma_instr_fault               = is_pma_instr_fault_f();
   end
 
+  always_comb begin
+    is_pma_data_fault = is_pma_load_fault || is_pma_store_fault;
+  end
+
+  always_comb begin
+    is_pma_load_fault =
+      rvfi_valid  &&
+      rvfi_trap.trap  &&
+      rvfi_trap.exception  &&
+      (rvfi_trap.exception_cause == EXC_CAUSE_LOAD_ACC_FAULT)  &&
+      (rvfi_trap.cause_type == 'h 0);
+  end
+
+  always_comb begin
+    is_pma_store_fault =
+      rvfi_valid  &&
+      rvfi_trap.trap  &&
+      rvfi_trap.exception  &&
+      (rvfi_trap.exception_cause == EXC_CAUSE_STORE_ACC_FAULT)  &&
+      (rvfi_trap.cause_type == 'h 0);
+  end
+
   always_comb begin
     is_instr_bus_valid               = is_instr_bus_valid_f();
   end