Enable SVA in Verilator (#200)

* Use generic ASSERTS_OFF macro to disable assertions * Override default disable and enable SVA in Verilator for rr_arb_tree * Override default disable and enable SVA in Verilator for stream_xbar * Override default disable and enable SVA in Verilator for stream_omega_net * Fix default disable in stream_xbar * Fix default disable in stream_omega_net * Change ASSERTS_OFF macro to COMMON_CELLS_ASSERTS_OFF * Add newlines to avoid line length lint errors
pulp-platform · Oct 20, 2023 · 52f83ee · 52f83ee
1 parent 2bd027c
commit 52f83ee
Show file tree

Hide file tree

Showing 31 changed files with 78 additions and 57 deletions.
diff --git a/src/addr_decode_dync.sv b/src/addr_decode_dync.sv
@@ -122,7 +122,7 @@ module addr_decode_dync #(
   end
 
   // Assumptions and assertions
-  `ifndef VERILATOR
+  `ifndef COMMON_CELLS_ASSERTS_OFF
   `ifndef XSIM
   // pragma translate_off
   initial begin : proc_check_parameters

diff --git a/src/cb_filter.sv b/src/cb_filter.sv
@@ -235,7 +235,7 @@ module hash_block #(
     end
   end
 
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
   // assertions
   // pragma translate_off
   initial begin

diff --git a/src/cdc_2phase_clearable.sv b/src/cdc_2phase_clearable.sv
@@ -185,7 +185,7 @@ module cdc_2phase_clearable #(
   assign dst_clear_pending_o = s_dst_isolate_req;
 
 
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
 
   no_valid_i_during_clear_i : assert property (
     @(posedge src_clk_i) disable iff (!src_rst_ni) src_clear_i |-> !src_valid_i
@@ -257,7 +257,7 @@ module cdc_2phase_src_clearable #(
   assign async_data_o = data_src_q;
 
 // Assertions
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
   // pragma translate_off
   no_clear_and_request: assume property (
      @(posedge clk_i) disable iff(~rst_ni) (clear_i |-> ~valid_i))

diff --git a/src/cdc_fifo_gray.sv b/src/cdc_fifo_gray.sv
@@ -158,7 +158,7 @@ module cdc_fifo_gray #(
 
   // Check the invariants.
   // pragma translate_off
-  `ifndef VERILATOR
+  `ifndef COMMON_CELLS_ASSERTS_OFF
   initial assert(LOG_DEPTH > 0);
   initial assert(SYNC_STAGES >= 2);
   `endif

diff --git a/src/cdc_fifo_gray_clearable.sv b/src/cdc_fifo_gray_clearable.sv
@@ -255,7 +255,7 @@ module cdc_fifo_gray_clearable #(
 
   // Check the invariants.
   // pragma translate_off
-  `ifndef VERILATOR
+  `ifndef COMMON_CELLS_ASSERTS_OFF
   initial assert(LOG_DEPTH > 0);
   initial assert(SYNC_STAGES >= 2);
   `endif

diff --git a/src/cf_math_pkg.sv b/src/cf_math_pkg.sv
@@ -24,7 +24,7 @@ package cf_math_pkg;
         automatic longint remainder;
 
         // pragma translate_off
-        `ifndef VERILATOR
+        `ifndef COMMON_CELLS_ASSERTS_OFF
         if (dividend < 0) begin
             $fatal(1, "Dividend %0d is not a natural number!", dividend);
         end

diff --git a/src/deprecated/fifo_v2.sv b/src/deprecated/fifo_v2.sv
@@ -68,7 +68,7 @@ module fifo_v2 #(
     );
 
     // pragma translate_off
-    `ifndef VERILATOR
+    `ifndef COMMON_CELLS_ASSERTS_OFF
         initial begin
             assert (ALM_FULL_TH <= DEPTH)  else $error("ALM_FULL_TH can't be larger than the DEPTH.");
             assert (ALM_EMPTY_TH <= DEPTH) else $error("ALM_EMPTY_TH can't be larger than the DEPTH.");

diff --git a/src/exp_backoff.sv b/src/exp_backoff.sv
@@ -82,7 +82,7 @@ module exp_backoff #(
 ///////////////////////////////////////////////////////
 
 //pragma translate_off
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
   initial begin
     // assert wrong parameterizations
     assert (MaxExp>0)

diff --git a/src/fifo_v3.sv b/src/fifo_v3.sv
@@ -138,7 +138,7 @@ module fifo_v3 #(
     end
 
 // pragma translate_off
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
     initial begin
         assert (DEPTH > 0)             else $error("DEPTH must be greater than 0.");
     end

diff --git a/src/id_queue.sv b/src/id_queue.sv
@@ -405,7 +405,7 @@ module id_queue #(
 
     // Validate parameters.
 // pragma translate_off
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
     initial begin: validate_params
         assert (ID_WIDTH >= 1)
             else $fatal(1, "The ID must at least be one bit wide!");

diff --git a/src/isochronous_4phase_handshake.sv b/src/isochronous_4phase_handshake.sv
@@ -70,7 +70,7 @@ module isochronous_4phase_handshake (
 
  // pragma translate_off
  // stability guarantees
-  `ifndef VERILATOR
+  `ifndef COMMON_CELLS_ASSERTS_OFF
   assert property (@(posedge src_clk_i) disable iff (~src_rst_ni)
     (src_valid_i && !src_ready_o |=> $stable(src_valid_i))) else $error("src_valid_i is unstable");
   assert property (@(posedge dst_clk_i) disable iff (~dst_rst_ni)

diff --git a/src/isochronous_spill_register.sv b/src/isochronous_spill_register.sv
@@ -97,7 +97,7 @@ module isochronous_spill_register #(
 
   // pragma translate_off
   // stability guarantees
-  `ifndef VERILATOR
+  `ifndef COMMON_CELLS_ASSERTS_OFF
   assert property (@(posedge src_clk_i) disable iff (~src_rst_ni)
     (src_valid_i && !src_ready_o |=> $stable(src_valid_i))) else $error("src_valid_i is unstable");
   assert property (@(posedge src_clk_i) disable iff (~src_rst_ni)

diff --git a/src/lfsr.sv b/src/lfsr.sv
@@ -289,7 +289,7 @@ end
 ////////////////////////////////////////////////////////////////////////
 // assertions
 ////////////////////////////////////////////////////////////////////////
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
 // pragma translate_off
 initial begin
   // these are the LUT limits

diff --git a/src/lfsr_16bit.sv b/src/lfsr_16bit.sv
@@ -58,7 +58,7 @@ module lfsr_16bit #(
         end
     end
 
-  `ifndef VERILATOR
+  `ifndef COMMON_CELLS_ASSERTS_OFF
     //pragma translate_off
     initial begin
         assert (WIDTH <= 16)

diff --git a/src/lfsr_8bit.sv b/src/lfsr_8bit.sv
@@ -52,7 +52,7 @@ module lfsr_8bit #(
     end
   end
 
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
   //pragma translate_off
   initial begin
     assert (WIDTH <= 8) else $fatal(1, "WIDTH needs to be less than 8 because of the 8-bit LFSR");

diff --git a/src/lzc.sv b/src/lzc.sv
@@ -39,7 +39,7 @@ module lzc #(
 
     localparam int unsigned NumLevels = $clog2(WIDTH);
 
-  `ifndef VERILATOR
+  `ifndef COMMON_CELLS_ASSERTS_OFF
     // pragma translate_off
     initial begin
       assert(WIDTH > 0) else $fatal(1, "input must be at least one bit wide");
@@ -102,7 +102,7 @@ module lzc #(
   end : gen_lzc
 
 // pragma translate_off
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
   initial begin: validate_params
     assert (WIDTH >= 1)
       else $fatal(1, "The WIDTH must at least be one bit wide!");

diff --git a/src/mem_to_banks_detailed.sv b/src/mem_to_banks_detailed.sv
@@ -209,7 +209,7 @@ module mem_to_banks_detailed #(
 
   // Assertions
   // pragma translate_off
-  `ifndef VERILATOR
+  `ifndef COMMON_CELLS_ASSERTS_OFF
   `ifndef SYNTHESIS
     initial begin
       assume (DataWidth != 0 && (DataWidth & (DataWidth - 1)) == 0)

diff --git a/src/multiaddr_decode.sv b/src/multiaddr_decode.sv
@@ -120,7 +120,7 @@ module multiaddr_decode #(
   end
 
   // Assumptions and assertions
-  `ifndef VERILATOR
+  `ifndef COMMON_CELLS_ASSERTS_OFF
   `ifndef XSIM
   // pragma translate_off
   initial begin : proc_check_parameters

diff --git a/src/onehot_to_bin.sv b/src/onehot_to_bin.sv
@@ -30,7 +30,7 @@ module onehot_to_bin #(
     end
 
 // pragma translate_off
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
     assert final ($onehot0(onehot)) else
         $fatal(1, "[onehot_to_bin] More than two bit set in the one-hot signal");
 `endif

diff --git a/src/plru_tree.sv b/src/plru_tree.sv
@@ -110,7 +110,7 @@ module plru_tree #(
     end
 
 // pragma translate_off
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
     initial begin
         assert (ENTRIES == 2**LogEntries) else $error("Entries must be a power of two");
     end

diff --git a/src/rr_arb_tree.sv b/src/rr_arb_tree.sv
@@ -110,12 +110,14 @@ module rr_arb_tree #(
 );
 
   // pragma translate_off
+  `ifndef COMMON_CELLS_ASSERTS_OFF
   `ifndef VERILATOR
   `ifndef XSIM
   // Default SVA reset
   default disable iff (!rst_ni || flush_i);
   `endif
   `endif
+  `endif
   // pragma translate_on
 
   // just pass through in this corner case
@@ -169,17 +171,18 @@ module rr_arb_tree #(
         end
 
         // pragma translate_off
-        `ifndef VERILATOR
+        `ifndef COMMON_CELLS_ASSERTS_OFF
           lock: assert property(
-            @(posedge clk_i) LockIn |-> req_o &&
-                             (!gnt_i && !flush_i) |=> idx_o == $past(idx_o)) else
+            @(posedge clk_i) disable iff (!rst_ni || flush_i)
+                LockIn |-> req_o && (!gnt_i && !flush_i) |=> idx_o == $past(idx_o)) else
                 $fatal (1, "Lock implies same arbiter decision in next cycle if output is not \
                             ready.");
 
           logic [NumIn-1:0] req_tmp;
           assign req_tmp = req_q & req_i;
           lock_req: assume property(
-            @(posedge clk_i) LockIn |-> lock_d |=> req_tmp == req_q) else
+            @(posedge clk_i) disable iff (!rst_ni || flush_i)
+                LockIn |-> lock_d |=> req_tmp == req_q) else
                 $fatal (1, "It is disallowed to deassert unserved request signals when LockIn is \
                             enabled.");
         `endif
@@ -308,7 +311,7 @@ module rr_arb_tree #(
     end
 
     // pragma translate_off
-    `ifndef VERILATOR
+    `ifndef COMMON_CELLS_ASSERTS_OFF
     `ifndef XSIM
     initial begin : p_assert
       assert(NumIn)
@@ -318,27 +321,27 @@ module rr_arb_tree #(
     end
 
     hot_one : assert property(
-      @(posedge clk_i) $onehot0(gnt_o))
+      @(posedge clk_i) disable iff (!rst_ni || flush_i) $onehot0(gnt_o))
         else $fatal (1, "Grant signal must be hot1 or zero.");
 
     gnt0 : assert property(
-      @(posedge clk_i) |gnt_o |-> gnt_i)
+      @(posedge clk_i) disable iff (!rst_ni || flush_i) |gnt_o |-> gnt_i)
         else $fatal (1, "Grant out implies grant in.");
 
     gnt1 : assert property(
-      @(posedge clk_i) req_o |-> gnt_i |-> |gnt_o)
+      @(posedge clk_i) disable iff (!rst_ni || flush_i) req_o |-> gnt_i |-> |gnt_o)
         else $fatal (1, "Req out and grant in implies grant out.");
 
     gnt_idx : assert property(
-      @(posedge clk_i) req_o |->  gnt_i |-> gnt_o[idx_o])
+      @(posedge clk_i) disable iff (!rst_ni || flush_i) req_o |->  gnt_i |-> gnt_o[idx_o])
         else $fatal (1, "Idx_o / gnt_o do not match.");
 
     req0 : assert property(
-      @(posedge clk_i) |req_i |-> req_o)
+      @(posedge clk_i) disable iff (!rst_ni || flush_i) |req_i |-> req_o)
         else $fatal (1, "Req in implies req out.");
 
     req1 : assert property(
-      @(posedge clk_i) req_o |-> |req_i)
+      @(posedge clk_i) disable iff (!rst_ni || flush_i) req_o |-> |req_i)
         else $fatal (1, "Req out implies req in.");
     `endif
     `endif

diff --git a/src/rstgen_bypass.sv b/src/rstgen_bypass.sv
@@ -58,7 +58,7 @@ module rstgen_bypass #(
         end
     end
     // pragma translate_off
-    `ifndef VERILATOR
+    `ifndef COMMON_CELLS_ASSERTS_OFF
     initial begin : p_assertions
         if (NumRegs < 1) $fatal(1, "At least one register is required.");
     end

diff --git a/src/spill_register_flushable.sv b/src/spill_register_flushable.sv
@@ -95,7 +95,7 @@ module spill_register_flushable #(
     assign data_o = b_full_q ? b_data_q : a_data_q;
 
     // pragma translate_off
-    `ifndef VERILATOR
+    `ifndef COMMON_CELLS_ASSERTS_OFF
     flush_valid : assert property (
       @(posedge clk_i) disable iff (~rst_ni) (flush_i |-> ~valid_i)) else
       $warning("Trying to flush and feed the spill register simultaneously. You will lose data!");

diff --git a/src/stream_fork.sv b/src/stream_fork.sv
@@ -123,7 +123,7 @@ module stream_fork #(
                             // of the '1 literal when assigned to a port of parametrized width.
 
 // pragma translate_off
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
     initial begin: p_assertions
         assert (N_OUP >= 1) else $fatal(1, "Number of outputs must be at least 1!");
     end

diff --git a/src/stream_fork_dynamic.sv b/src/stream_fork_dynamic.sv
@@ -86,7 +86,7 @@ module stream_fork_dynamic #(
   );
 
 // pragma translate_off
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
   initial begin: p_assertions
     assert (N_OUP >= 1) else $fatal(1, "N_OUP must be at least 1!");
   end

diff --git a/src/stream_intf.sv b/src/stream_intf.sv
@@ -41,7 +41,7 @@ interface STREAM_DV #(
 
   // Make sure that the handshake and payload is stable
   // pragma translate_off
-  `ifndef VERILATOR
+  `ifndef COMMON_CELLS_ASSERTS_OFF
   assert property (@(posedge clk_i) (valid && !ready |=> $stable(data)));
   assert property (@(posedge clk_i) (valid && !ready |=> valid));
   `endif

diff --git a/src/stream_join_dynamic.sv b/src/stream_join_dynamic.sv
@@ -38,7 +38,7 @@ module stream_join_dynamic #(
   end
 
 // pragma translate_off
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
   initial begin: p_assertions
     assert (N_INP >= 1) else $fatal(1, "N_INP must be at least 1!");
   end

diff --git a/src/stream_mux.sv b/src/stream_mux.sv
@@ -36,7 +36,7 @@ module stream_mux #(
   assign oup_valid_o  = inp_valid_i[inp_sel_i];
 
 // pragma translate_off
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
   initial begin: p_assertions
     assert (N_INP >= 1) else $fatal (1, "The number of inputs must be at least 1!");
   end

diff --git a/src/stream_omega_net.sv b/src/stream_omega_net.sv
@@ -261,28 +261,37 @@ module stream_omega_net #(
     // Assertions
     // Make sure that the handshake and payload is stable
     // pragma translate_off
+    `ifndef COMMON_CELLS_ASSERTS_OFF
     `ifndef VERILATOR
-    default disable iff rst_ni;
+    default disable iff (~rst_ni);
+    `endif
     for (genvar i = 0; unsigned'(i) < NumInp; i++) begin : gen_sel_assertions
-      assert property (@(posedge clk_i) (valid_i[i] |-> sel_i[i] < sel_oup_t'(NumOut))) else
+      assert property (@(posedge clk_i) disable iff (~rst_ni)
+          (valid_i[i] |-> sel_i[i] < sel_oup_t'(NumOut))) else
           $fatal(1, "Non-existing output is selected!");
     end
 
     if (AxiVldRdy) begin : gen_handshake_assertions
       for (genvar i = 0; unsigned'(i) < NumInp; i++) begin : gen_inp_assertions
-        assert property (@(posedge clk_i) (valid_i[i] && !ready_o[i] |=> $stable(data_i[i]))) else
+        assert property (@(posedge clk_i) disable iff (~rst_ni)
+            (valid_i[i] && !ready_o[i] |=> $stable(data_i[i]))) else
             $error("data_i is unstable at input: %0d", i);
-        assert property (@(posedge clk_i) (valid_i[i] && !ready_o[i] |=> $stable(sel_i[i]))) else
+        assert property (@(posedge clk_i) disable iff (~rst_ni)
+            (valid_i[i] && !ready_o[i] |=> $stable(sel_i[i]))) else
             $error("sel_i is unstable at input: %0d", i);
-        assert property (@(posedge clk_i) (valid_i[i] && !ready_o[i] |=> valid_i[i])) else
+        assert property (@(posedge clk_i) disable iff (~rst_ni)
+            (valid_i[i] && !ready_o[i] |=> valid_i[i])) else
             $error("valid_i at input %0d has been taken away without a ready.", i);
       end
       for (genvar i = 0; unsigned'(i) < NumOut; i++) begin : gen_out_assertions
-        assert property (@(posedge clk_i) (valid_o[i] && !ready_i[i] |=> $stable(data_o[i]))) else
+        assert property (@(posedge clk_i) disable iff (~rst_ni)
+            (valid_o[i] && !ready_i[i] |=> $stable(data_o[i]))) else
             $error("data_o is unstable at output: %0d Check that parameter LockIn is set.", i);
-        assert property (@(posedge clk_i) (valid_o[i] && !ready_i[i] |=> $stable(idx_o[i]))) else
+        assert property (@(posedge clk_i) disable iff (~rst_ni)
+            (valid_o[i] && !ready_i[i] |=> $stable(idx_o[i]))) else
             $error("idx_o is unstable at output: %0d Check that parameter LockIn is set.", i);
-        assert property (@(posedge clk_i) (valid_o[i] && !ready_i[i] |=> valid_o[i])) else
+        assert property (@(posedge clk_i) disable iff (~rst_ni)
+            (valid_o[i] && !ready_i[i] |=> valid_o[i])) else
             $error("valid_o at output %0d has been taken away without a ready.", i);
       end
     end

diff --git a/src/stream_to_mem.sv b/src/stream_to_mem.sv
@@ -117,7 +117,7 @@ module stream_to_mem #(
 
 // Assertions
 // pragma translate_off
-`ifndef VERILATOR
+`ifndef COMMON_CELLS_ASSERTS_OFF
   if (BufDepth > 0) begin : gen_buf_asserts
     assert property (@(posedge clk_i) mem_resp_valid_i |-> buf_ready)
       else $error("Memory response lost!");