More improvements in smt2-bmc scripts

4 files changed, 128 insertions, 3 deletions

diff --git a/scripts/smt2-bmc/README b/scripts/smt2-bmc/README
new file mode 100644
index 0000000..f947664
--- /dev/null
+++ b/scripts/smt2-bmc/README
@@ -0,0 +1,47 @@
+
+Checking equivalence of different configurations of PicoRV32 using Yosys and
+SMT solvers (Yices, Z3, CVC4, MathSAT).
+
+The PicoRV32 core provides configuration parameters that change the supported
+ISA and/or the timing of the core. This set of scripts uses model checking
+techniques to proof equivalence of cores in different configurations, thus
+transfering the confidence in the cores gained by running test benches on a few
+configurations to the rest of the configurations.
+
+
+async
+-----
+
+The async test compares two cores with different timings (number of clock
+cycles per operation), but same ISA. The SMT problem models the following
+scenario:
+
+The cores start out with identical memory and register file. In cycle 0 the
+reset input is active, in all other cycles the reset input is inactive. The
+trap output must by active in the last cycle for both cores. I.e. whatever
+the program in memory does, it must terminate in a trap and it must do so
+for both cores within the simulated number of clock cycles.
+
+The script searches for a trace that ends in different memory content and/or
+different register file content in the last cycle, i.e. a trace that exposes
+divergent behavior in the two cores.
+
+
+sync
+----
+
+The sync test compares two cores same timings but different ISA. The ISA of the
+2nd code (main_b) must be a superset of the ISA of the first core (main_a), and
+catching illegal instructions and illegal memory transfers must be enabled in
+the first core. The SMT problem models the following scenario:
+
+The cores start out with identical memory and register file. In cycle 0 the
+reset input is active, in all other cycles the reset input is inactive. The
+cores are run in parallel for a number of cycles with the first core not going
+into the trap state. I.e. all traces are limited to the ISA supported by the
+first core.
+
+The script searches for a trace that ends in different memory content and/or
+different register file content in the last cycle, i.e. a trace that exposes
+divergent behavior in the two cores.
+
diff --git a/scripts/smt2-bmc/async.py b/scripts/smt2-bmc/async.py
index 0d13ba6..7606440 100644
--- a/scripts/smt2-bmc/async.py
+++ b/scripts/smt2-bmc/async.py
@@ -13,7 +13,46 @@ initzero = False
 check_mem = True
 check_regs = True
 debug_print = False
-debug_file = open("debug.smt2", "w")
+debug_file = None
+
+def usage():
+    print("""
+python3 async.py [options]
+
+    -s <solver>
+        set SMT solver: yices, z3, cvc4, mathsat
+        default: yices
+
+    -t <steps>
+        default: 12
+
+    -v
+        enable debug output
+
+    -d
+        write smt2 statements to debug.smt2
+""")
+    sys.exit(1)
+
+try:
+    opts, args = getopt.getopt(sys.argv[1:], "s:t:vd")
+except:
+    usage()
+
+for o, a in opts:
+    if o == "-s":
+        solver = a
+    elif o == "-t":
+        steps = int(a)
+    elif o == "-v":
+        debug_print = True
+    elif o == "-d":
+        debug_file = open("debug.smt2", "w")
+    else:
+        usage()
+
+if len(args) > 0:
+    usage()
 
 start_time = time()
 smt = smtio(solver=solver, debug_print=debug_print, debug_file=debug_file)
diff --git a/scripts/smt2-bmc/smtio.py b/scripts/smt2-bmc/smtio.py
index c99c312..1e37eb0 100644
--- a/scripts/smt2-bmc/smtio.py
+++ b/scripts/smt2-bmc/smtio.py
@@ -12,7 +12,7 @@ class smtio:
             popen_vargs = ['z3', '-smt2', '-in']
 
         if solver == "cvc4":
-            popen_vargs = ['cvc4', '--incremental']
+            popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']
 
         if solver == "mathsat":
             popen_vargs = ['mathsat']
diff --git a/scripts/smt2-bmc/sync.py b/scripts/smt2-bmc/sync.py
index f01f0eb..6f35841 100644
--- a/scripts/smt2-bmc/sync.py
+++ b/scripts/smt2-bmc/sync.py
@@ -9,7 +9,46 @@ words = 0
 solver = "yices"
 allmem = False
 debug_print = False
-debug_file = open("debug.smt2", "w")
+debug_file = None
+
+def usage():
+    print("""
+python3 sync.py [options]
+
+    -s <solver>
+        set SMT solver: yices, z3, cvc4, mathsat
+        default: yices
+
+    -t <steps>
+        default: 20
+
+    -v
+        enable debug output
+
+    -d
+        write smt2 statements to debug.smt2
+""")
+    sys.exit(1)
+
+try:
+    opts, args = getopt.getopt(sys.argv[1:], "s:t:vd")
+except:
+    usage()
+
+for o, a in opts:
+    if o == "-s":
+        solver = a
+    elif o == "-t":
+        steps = int(a)
+    elif o == "-v":
+        debug_print = True
+    elif o == "-d":
+        debug_file = open("debug.smt2", "w")
+    else:
+        usage()
+
+if len(args) > 0:
+    usage()
 
 start_time = time()
 smt = smtio(solver=solver, debug_print=debug_print, debug_file=debug_file)