aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smtbmc.py
diff options
context:
space:
mode:
authorJim Lawson <ucbjrl@berkeley.edu>2019-02-11 12:43:46 -0800
committerJim Lawson <ucbjrl@berkeley.edu>2019-02-11 12:43:46 -0800
commit311396860b7380e5dc68e66c17d5083d1953fe3f (patch)
treec5146a20e59acc342dfe414e1b35fdfe419b9e81 /backends/smt2/smtbmc.py
parent76696e80041dc5b8f4ba986f4f83d6e7b6854e96 (diff)
parente112d2fbf5a31f00ef19e6d05f28fecc1e9c56b9 (diff)
downloadyosys-311396860b7380e5dc68e66c17d5083d1953fe3f.tar.gz
yosys-311396860b7380e5dc68e66c17d5083d1953fe3f.tar.bz2
yosys-311396860b7380e5dc68e66c17d5083d1953fe3f.zip
Merge remote-tracking branch 'upstream/master'
Diffstat (limited to 'backends/smt2/smtbmc.py')
-rw-r--r--backends/smt2/smtbmc.py8
1 files changed, 4 insertions, 4 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 721a395e3..94a5e2da0 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -87,7 +87,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
--aig <aim_filename>:<aiw_filename>
like above, but for map files and witness files that do not
- share a filename prefix (or use differen file extensions).
+ share a filename prefix (or use different file extensions).
--aig-noheader
the AIGER witness file does not include the status and
@@ -103,8 +103,8 @@ yosys-smtbmc [options] <yosys_smt2_output>
--presat
check if the design with assumptions but without assertions
is SAT before checking if assertions are UNSAT. This will
- detect if there are contradicting assumtions. In some cases
- this will also help to "warmup" the solver, potentially
+ detect if there are contradicting assumptions. In some cases
+ this will also help to "warm up" the solver, potentially
yielding a speedup.
--final-only
@@ -149,7 +149,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
--append <num_steps>
add <num_steps> time steps at the end of the trace
when creating a counter example (this additional time
- steps will still be constrained by assumtions)
+ steps will still be constrained by assumptions)
""" + so.helpmsg())
sys.exit(1)