aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smtbmc.py
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2016-08-20 16:07:59 +0200
committerClifford Wolf <clifford@clifford.at>2016-08-20 16:07:59 +0200
commita889acb897b742f8d17ebccb0fb0d0a8e622fb70 (patch)
treef0734a47d9d468bcc61527a1a99de532485f8526 /backends/smt2/smtbmc.py
parentfe9315b7a19bcb6dcde1a1ce49dd23f999bda7eb (diff)
downloadyosys-a889acb897b742f8d17ebccb0fb0d0a8e622fb70.tar.gz
yosys-a889acb897b742f8d17ebccb0fb0d0a8e622fb70.tar.bz2
yosys-a889acb897b742f8d17ebccb0fb0d0a8e622fb70.zip
Added smtbmc longopt support
Diffstat (limited to 'backends/smt2/smtbmc.py')
-rw-r--r--backends/smt2/smtbmc.py16
1 files changed, 8 insertions, 8 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