42fb75c570
smtio: Emit `mode: start` options before `set-logic` command and any other options after it.
...
Refer to the SMT-LIB specification, section 4.1.7. According to the spec, some options can only be specified in `start` mode. Once the solver sees `set-logic`, it moves to `assert` mode.
2020-07-20 22:09:44 +00:00
654864658f
smtio: Add support for parsing `yosys-smt2-solver-option` info statements.
2020-07-20 21:54:56 +00:00
f037985337
smt2: Add `-solver-option` option.
2020-07-20 21:54:56 +00:00
a207cb362c
Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-07-20 19:35:32 +02:00
7191dd16f9
Use C++11 final/override keywords.
2020-06-18 23:34:52 +00:00
da0778350b
more reasonable numbers for memory
2020-06-04 17:00:04 -04:00
5d29a9f633
MacOS has even stricter stack limits in catalina.
...
Invoking sby in macOS Catalina fails because of bizarre stack limits in Catalina.
2020-06-04 14:01:56 -04:00
ea46ed81f9
Merge pull request #2018 from boqwxp/qbfsat-timeout
...
smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4.
2020-05-30 15:04:51 +02:00
ea30465107
smtbmc: Remove superfluous `yosys-smt2-timeout` file macro.
...
Co-Authored-By: clairexen <claire@symbioticeda.com>
2020-05-29 21:33:00 +00:00
94c1035389
Merge pull request #1885 from Xiretza/mod-rem-cells
...
Fix modulo/remainder semantics
2020-05-29 16:37:23 +02:00
17163cf43a
Add flooring modulo operator
...
The $div and $mod cells use truncating division semantics (rounding
towards 0), as defined by e.g. Verilog. Another rounding mode, flooring
(rounding towards negative infinity), can be used in e.g. VHDL. The
new $modfloor cell provides this flooring modulo (also known as "remainder"
in several languages, but this name is ambiguous).
This commit also fixes the handling of $mod in opt_expr, which was
previously optimized as if it was $modfloor.
2020-05-28 22:59:03 +02:00
9847a4eea8
smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4.
2020-05-25 20:39:30 +00:00
54570a3978
qbfsat: Move SMT2 info statements back to the top of the file.
2020-05-25 20:38:29 +00:00
903456c267
qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices the default.
...
Ensures that "BV" is the logic whenever solving an exists-forall problem with Yices, moves the "(set-logic ...)" directive above any non-info line, sets the `ef-max-iters` parameter to a very high number when using Yices in exists-forall mode so as not to prematurely abandon difficult problems, and does not provide the incompatible "--incremental" Yices argument when in exists-forall mode.
2020-05-25 20:38:29 +00:00
1053032a81
smtbmc: Fix typo in error message.
...
Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
2020-05-19 16:13:44 +00:00
299ab76a09
smtbmc: Fix return status handling.
2020-05-14 17:07:59 +00:00
0b7a5879e5
Merge pull request #1830 from boqwxp/qbfsat
...
Add `qbfsat` command to integrate exists-forall solving and specialization
2020-04-15 17:33:50 +02:00
0d789c5a3b
Support custom PROGRAM_PREFIX
2020-04-10 10:38:40 +02:00
437afa1f0c
Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole value recovery using that mode.
2020-04-04 22:13:25 +00:00
956ecd48f7
kernel: big fat patch to use more ID::*, otherwise ID(*)
2020-04-02 09:51:32 -07:00
fdafb74eb7
kernel: use more ID::*
2020-04-02 07:14:08 -07:00
c23c2c59c1
Update `RTLIL::id2cstr()` usage to `log_id`.
2020-04-01 06:53:28 +00:00
d72cb8ea2a
Do not change solver output parsing for non-exists-forall problems.
2020-03-26 23:00:00 +00:00
5accf08ef9
Skip reading stdout from the solver that if it isn't a line reading only "sat", "unsat", or "unknown".
2020-03-26 01:21:01 +00:00
c9555c9ade
Revert part of 0fda8308 from #1746 that broke other smtbmc flows
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-03-24 17:33:46 +01:00
b08932cb81
fix typo in `write_smt2` help
2020-03-23 02:14:26 -07:00
020f6d167a
Merge pull request #1768 from boqwxp/smt2_cleanup
...
Clean up pseudo-private member usage in `backends/smt2/smt2.cc`.
2020-03-16 13:49:10 +01:00
07f0874779
Clean up pseudo-private member usage in `backends/smt2/smt2.cc`.
2020-03-13 21:49:12 +00:00
0fda8308bc
Add support for optimizing exists-forall problems.
...
Modifies smt2 backend to recognize `$anyconst` etc. assigned to a wire with the `maximize` or `minimize` attribute and emit `; yosys-smt2-maximize` or `; yosys-smt2-minimize` directives as appropriate.
Modifies `backends/smt2/smtbmc.py` and `smtio.py` to recognize those directives and emit a `(maximize ...)` or `(minimize ...)` command at the end of `smt_forall_assert()`, as described in the paper "νZ - An Optimizing SMT Solver" by Nikolaj Bjørner et al.
Adds an example `examples/smtbmc/demo9.v` to show how it can be used.
2020-03-13 17:10:29 +00:00
485f31f681
Improve yosys-smtbmc "solver not found" handling
...
Signed-off-by: Claire Wolf <clifford@clifford.at>
2020-01-27 17:48:56 +01:00
f02623abb5
Bugfix in smtio vcd handling of $-identifiers
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-10-23 00:04:34 +02:00
2ed2e9c3e8
Change smtbmc "Warmup failed" status to "PREUNSAT"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-10-03 14:59:07 +02:00
c1b628508d
backends: smt2: use $(CXX) variable for compiler
...
The Makefile assumes the compiler is called `gcc`, which isn't always
true. In fact, if we're building on msys2 or msys2-64, the compiler
is called `i686-w64-mingw32-g++` or `x86_64-w64-mingw32-g++`.
Use the variable instead of hardcoding the name, to fix building on
these systems.
Signed-off-by: Sean Cross <sean@xobs.io>
2019-09-08 15:47:09 +08:00
6d77236f38
substr() -> compare()
2019-08-07 12:20:08 -07:00
3486235338
Make liberal use of IdString.in()
2019-08-06 16:18:18 -07:00
023086bd46
Add $_NMUX_, add "abc -g cmos", add proper cmos cell costs
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-08-06 04:47:55 +02:00
ab4b9e8db4
smt: handle failure of setrlimit syscall
2019-07-15 23:33:18 +08:00
b3c36b4448
Escape scope names starting with dollar sign in smtio.py
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-06-26 10:58:39 +02:00
c23bbc4291
Add timescale and generated-by header to yosys-smtbmc MkVcd
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-06-16 23:12:03 +02:00
f4abc21d8a
Add "whitebox" attribute, add "read_verilog -wb"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-04-18 17:45:47 +02:00
bacca57537
Fix smtbmc.py handling of zero appended steps
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-14 22:04:42 +01:00
ff15cf9b1f
Install launcher executable when running yosys-smtbmc on Windows.
...
Signed-off-by: William D. Jones <thor0505@comcast.net>
2019-03-13 13:49:16 -04:00
94f995ee37
Fix signed $shift/$shiftx handling in write_smt2
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-09 13:19:41 -08:00
5dfc7becca
Use SVA label in smt export if available
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-07 11:31:46 -08:00
f570aa5e1d
Fix smt2 code generation for partially initialized memowy words, fixes #831
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-02-28 12:15:58 -08:00
e112d2fbf5
Add missing blackslash-to-slash convertion to smtio.py (matching Smt2Worker::get_id() behavior)
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-02-06 16:35:59 +01:00
efa278e232
Fix typographical and grammatical errors and inconsistencies.
...
The initial list of hits was generated with the codespell command
below, and each hit was evaluated and fixed manually while taking
context into consideration.
DIRS="kernel/ frontends/ backends/ passes/ techlibs/"
DIRS="${DIRS} libs/ezsat/ libs/subcircuit"
codespell $DIRS -S *.o -L upto,iff,thru,synopsys,uint
More hits were found by looking through comments and strings manually.
2019-01-02 13:12:17 +00:00
0b9bb852c6
Add yosys-smtbmc support for btor witness
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-10 03:43:07 +01:00
47a5dfdaa4
Add "yosys-smtbmc --btorwit" skeleton
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-08 06:59:27 +01:00
825b4c1aa9
Merge pull request #693 from YosysHQ/rlimit
...
improve rlimit handling in smtio.py
2018-11-07 20:16:40 +01:00
Alberto Gonzalez
Claire Wolf
whitequark
Yehowshua Immanuel
Xiretza
N. Engelhardt
Miodrag Milanovic
Eddie Hung
Teguh Hofstee
Claire Wolf
Sean Cross
N. Engelhardt
William D. Jones