add RISCV_FORMAL_UNBOUNDED variable

checks/genchecks.py

@@ -33,7 +33,7 @@
 dumpsmt2 = False
 sbycmd = "sby"
 config = dict()
-mode = "bmc" # bmc/prove/live/cover/equiv/synth
+mode = "bmc"
 
 if len(sys.argv) > 1:
     assert len(sys.argv) == 2
@@ -83,10 +83,11 @@
         elif line[0] == "dumpsmt2":
             assert len(line) == 1
             dumpsmt2 = True
-        
+
         elif line[0] == "mode":
             assert len(line) == 2
-            mode = line[1]
+            if line[1] == "prove":
+                mode = line[1]
 
         else:
             print(line)
@@ -124,7 +125,7 @@ def print_hfmt(f, text, **kwargs):
 hargs["xlen"] = xlen
 hargs["ilen"] = ilen
 hargs["append"] = 0
-hargs["mode"]= mode
+hargs["mode"] = mode
 
 instruction_checks = set()
 consistency_checks = set()
@@ -237,6 +238,9 @@ def check_insn(insn, chanidx, csr_mode=False):
                 : `define RISCV_FORMAL_CHANNEL_IDX @channel@
         """, **hargs)
 
+        if mode == "prove":
+            print("`define RISCV_FORMAL_UNBOUNDED", file=sby_file)
+
         for csr in sorted(csrs):
             print("`define RISCV_FORMAL_CSR_%s" % csr.upper(), file=sby_file)
 
@@ -392,6 +396,9 @@ def check_cons(check, chanidx=None, start=None, trig=None, depth=None, csr_mode=
                 : `define RISCV_FORMAL_CHECK_CYCLE @depth@
         """, **hargs)
 
+        if mode == "prove":
+            print("`define RISCV_FORMAL_UNBOUNDED", file=sby_file)
+
         for csr in sorted(csrs):
             print("`define RISCV_FORMAL_CSR_%s" % csr.upper(), file=sby_file)
 
@@ -439,6 +446,7 @@ def check_cons(check, chanidx=None, start=None, trig=None, depth=None, csr_mode=
     check_cons("unique", chanidx=i, start=0, trig=1, depth=2)
     check_cons("causal", chanidx=i, start=0, depth=1)
     check_cons("ill", chanidx=i, depth=0)
+    check_cons("const_2_time", chanidx=i, start=0, trig=1, depth=2)
 
 check_cons("hang", start=0, depth=1)
 
@@ -473,4 +481,3 @@ def checks_key(check):
         print(".PHONY: %s" % check, file=mkfile)
 
 print("Generated %d checks." % (len(consistency_checks) + len(instruction_checks)))
-

checks/rvfi_testbench.sv

@@ -13,6 +13,14 @@
 // OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 
 module rvfi_testbench (
+	`ifdef RISCV_FORMAL_UNBOUNDED
+	`ifdef RISCV_FORMAL_TRIG_CYCLE
+		input trig,
+	`endif
+	`ifdef RISCV_FORMAL_CHECK_CYCLE
+		input check,
+	`endif
+	`endif
 	input clock, reset
 );
 	`RVFI_WIRES
@@ -32,10 +40,18 @@ module rvfi_testbench (
 		.clock  (clock),
 		.reset  (cycle < `RISCV_FORMAL_RESET_CYCLES),
 `ifdef RISCV_FORMAL_TRIG_CYCLE
+`ifdef RISCV_FORMAL_UNBOUNDED
+		.trig   (trig),
+`else
 		.trig   (cycle == `RISCV_FORMAL_TRIG_CYCLE),
 `endif
+`endif
 `ifdef RISCV_FORMAL_CHECK_CYCLE
+`ifdef RISCV_FORMAL_UNBOUNDED
+		.check   (check),
+`else
 		.check  (cycle == `RISCV_FORMAL_CHECK_CYCLE),
+`endif
 `endif
 		`RVFI_CONN
 	);