Added smtbmc longopt support

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 75bc51abb87cb19ce707a84ac5fc7b170fdbcd7a..3ad184190eb9052a95c6c1cc7ec9311128cb9bc8 100644 (file)
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -42,24 +42,24 @@ yosys-smtbmc [options] <yosys_smt2_output>
         assume asserts in skipped steps in BMC
 
     -S <step_size>
-        proof <step_size> time steps at once
-
-    -c <vcd_filename>
-        write counter-example to this VCD file
-        (hint: use 'write_smt2 -wires' for maximum
-        coverage of signals in generated VCD file)
+        prove <step_size> time steps at once
 
     -i
         instead of BMC run temporal induction
 
     -m <module_name>
         name of the top module
+
+    --dump-vcd <vcd_filename>
+        write counter-example to this VCD file
+        (hint: use 'write_smt2 -wires' for maximum
+        coverage of signals in generated VCD file)
 """ + so.helpmsg())
     sys.exit(1)
 
 
 try:
-    opts, args = getopt.getopt(sys.argv[1:], so.optstr + "t:u:S:c:im:")
+    opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:u:S:im:", so.longopts + ["dump-vcd="])
 except:
     usage()
 
@@ -75,7 +75,7 @@ for o, a in opts:
         assume_skipped = int(a)
     elif o == "-S":
         step_size = int(a)
-    elif o == "-c":
+    elif o == "--dump-vcd":
         vcdfile = a
     elif o == "-i":
         tempind = True

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 1b3944ebf3a569b5d68aedd55b27c58b5374deec..8a8033c06a848ad3092ec0f0b64c3ce999504eb1 100644 (file)
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -348,7 +348,8 @@ class smtio:
 
 class smtopts:
     def __init__(self):
-        self.optstr = "s:d:vp"
+        self.shortopts = "s:v"
+        self.longopts = ["no-progress", "dump-smt2="]
         self.solver = "z3"
         self.debug_print = False
         self.debug_file = None
@@ -359,9 +360,9 @@ class smtopts:
             self.solver = a
         elif o == "-v":
             self.debug_print = True
-        elif o == "-p":
+        elif o == "--no-progress":
             self.timeinfo = True
-        elif o == "-d":
+        elif o == "--dump-smt2":
             self.debug_file = open(a, "w")
         else:
             return False
@@ -376,10 +377,10 @@ class smtopts:
     -v
         enable debug output
 
-    -p
-        disable timer display during solving
+    --no-progress
+        disable running timer display during solving
 
-    -d <filename>
+    --dump-smt2 <filename>
         write smt2 statements to file
 """
 

diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile
index 48c81a46383cc614409f7ab3cf84613cf54e6ef2..4a154c2f9c10c204a630135acb3c88f6fbb27971 100644 (file)
--- a/examples/smtbmc/Makefile
+++ b/examples/smtbmc/Makefile
@@ -1,7 +1,7 @@
 
 demo1: demo1.smt2
-       yosys-smtbmc -c demo1.vcd demo1.smt2
-       yosys-smtbmc -i -c demo1.vcd demo1.smt2
+       yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2
+       yosys-smtbmc -i --dump-vcd demo1.vcd demo1.smt2
 
 demo1.smt2: demo1.v
        yosys -p 'read_verilog -formal demo1.v; prep -top demo1; write_smt2 -wires -mem -bv demo1.smt2'