sv2v.diff

diff --git a/azadi_rtl_v0.6/registers.svh b/azadi_rtl_v0.6/registers.svh
index c1975ed..779f07e 100644
--- a/azadi_rtl_v0.6/registers.svh
+++ b/azadi_rtl_v0.6/registers.svh
@@ -200,9 +200,9 @@
 // __clk: clock input
 // __arst_n: asynchronous reset
 `define FFLARNC(__q, __d, __load, __clear, __reset_value, __clk, __arst_n) \
-    `ifndef VERILATOR                       \
-  /``* synopsys sync_set_reset `"__clear`" *``/                       \
-    `endif                        \
+    //`ifndef VERILATOR                       \
+  ///``* synopsys sync_set_reset `"__clear`" *``/                       \
+    //`endif                        \
   always_ff @(posedge (__clk) or negedge (__arst_n)) begin                 \
     if (!__arst_n) begin                                                   \
       __q <= (__reset_value);                                              \
diff --git a/azadi_rtl_v0.6/rr_arb_tree.sv b/azadi_rtl_v0.6/rr_arb_tree.sv
index 9013a64..6ff5459 100644
--- a/azadi_rtl_v0.6/rr_arb_tree.sv
+++ b/azadi_rtl_v0.6/rr_arb_tree.sv
@@ -109,13 +109,6 @@ module rr_arb_tree #(
   output idx_t                idx_o
 );
 
-  // pragma translate_off
-  `ifndef VERILATOR
-  // Default SVA rst_ni
-  default disable iff (!rst_ni || flush_i);
-  `endif
-  // pragma translate_on
-
   // just pass through in this corner case
   if (NumIn == unsigned'(1)) begin : gen_pass_through
     assign req_o    = req_i[0];
@@ -166,22 +159,6 @@ module rr_arb_tree #(
           end
         end
 
-        // pragma translate_off
-        `ifndef VERILATOR
-          lock: assert property(
-            @(posedge clk_i) LockIn |-> req_o && !gnt_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
-                $fatal (1, "It is disallowed to deassert unserved request signals when LockIn is \
-                            enabled.");
-        `endif
-        // pragma translate_on
-
         always_ff @(posedge clk_i or negedge rst_ni) begin : p_req_regs
           if (!rst_ni) begin
             req_q  <= '0;
@@ -303,41 +280,6 @@ module rr_arb_tree #(
         //////////////////////////////////////////////////////////////
       end
     end
-
-    // pragma translate_off
-    `ifndef VERILATOR
-    initial begin : p_assert
-      assert(NumIn)
-        else $fatal(1, "Input must be at least one element wide.");
-      assert(!(LockIn && ExtPrio))
-        else $fatal(1,"Cannot use LockIn feature together with external ExtPrio.");
-    end
-
-    hot_one : assert property(
-      @(posedge clk_i) $onehot0(gnt_o))
-        else $fatal (1, "Grant signal must be hot1 or zero.");
-
-    gnt0 : assert property(
-      @(posedge clk_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)
-        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])
-        else $fatal (1, "Idx_o / gnt_o do not match.");
-
-    req0 : assert property(
-      @(posedge clk_i) |req_i |-> req_o)
-        else $fatal (1, "Req in implies req out.");
-
-    req1 : assert property(
-      @(posedge clk_i) req_o |-> |req_i)
-        else $fatal (1, "Req out implies req in.");
-    `endif
-    // pragma translate_on
   end
 
 endmodule : rr_arb_tree

sv2v.py

import os
import subprocess

#FIXME:
#Expected to run from the azadi_rtl_v0.6 dir
#Hard coded path to the sv2v binary

src_files = []
packages  = []
for f in os.listdir('.'):
    if not os.path.isfile(f):
        continue
    if '_pkg.sv' in f:
        packages.append(f)
    elif f.endswith('vh'):
        packages.append(f)
    elif f in ['defs_div_sqrt_mvp.sv', 'spi_defines.v']:
        packages.append(f)
    elif f.endswith('v'):
        src_files.append(f)

if not os.path.exists('out'):
    os.makedirs('out')
for f in src_files:
    with open(os.path.join('out', f+'.v'), 'w') as of:
        print(f)
        subprocess.call(['../../sv2v/bin/sv2v']+packages+[f], stdout=of)