diff options
| -rw-r--r-- | backends/smt2/smtbmc.py | 16 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 13 | ||||
| -rw-r--r-- | examples/smtbmc/Makefile | 4 |
3 files changed, 17 insertions, 16 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 75bc51abb..3ad184190 100644 --- 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 1b3944ebf..8a8033c06 100644 --- 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 48c81a463..4a154c2f9 100644 --- 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' |