Merge pull request #953 from silabs-oivind/sva_updates_8

Rewrite assertion to avoid unreachable cover
openhwgroup · Sep 19, 2023 · bf098e3 · bf098e3
2 parents b54d605 + 0188d07
commit bf098e3
Showing 1 changed file with 6 additions and 4 deletions.
diff --git a/sva/cv32e40x_parameter_sva.sv b/sva/cv32e40x_parameter_sva.sv
@@ -46,10 +46,12 @@ module cv32e40x_parameter_sva import cv32e40x_pkg::*;
   generate for (genvar i = 0; i < PMA_NUM_REGIONS; i++)
     begin : a_pma_no_illegal_configs
 
-      a_param_pma_io_noncacheable :
-        assert property (@(posedge clk_i) disable iff (!rst_ni)
-                         !PMA_CFG[i].main |-> !PMA_CFG[i].cacheable)
-        else $fatal(0, "Invalid PMA region configuration: cacheable I/O region");
+      if (!PMA_CFG[i].main) begin
+        a_param_pma_io_noncacheable :
+          assert property (@(posedge clk_i) disable iff (!rst_ni)
+                           !PMA_CFG[i].cacheable)
+            else $fatal(0, "Invalid PMA region configuration: cacheable I/O region");
+      end
 
       a_param_pma_addr_range :
         assert property (@(posedge clk_i) disable iff (!rst_ni)