a95e5d505b
Merge pull request #3186 from nakengelhardt/smtbmc_sby_print_id
...
add argument for printing cell names in yosys-smtbmc
2022-03-04 16:39:12 +01:00
dc739362c7
print cell name for properties in yosys-smtbmc
2022-02-22 17:00:10 +01:00
30eb7f8665
Add a bit of flexibilty re trace length when processing aiger witnesses in smtbmc.py
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-02-11 17:24:49 +01:00
93508d58da
Add $bmux and $demux cells.
2022-01-28 23:34:41 +01:00
e7d89e653c
Hook up $aldff support in various passes.
2021-10-02 21:01:21 +02:00
33749f1e3a
yosys-smtbmc: Fix reused loop variable.
...
Fixes #2999 .
2021-09-10 13:34:58 +02:00
4379375d89
Add support for the Bitwuzla solver
2021-07-12 22:07:58 +02:00
72787f52fc
Fixing old e-mail addresses and deadnames
...
s/((Claire|Xen|Xenia|Clifford)\s+)+(Wolf|Xen)\s+<(claire|clifford)@(symbioticeda.com|clifford.at|yosyshq.com)>/Claire Xenia Wolf <claire@yosyshq.com>/gi;
s/((Nina|Nak|N\.)\s+)+Engelhardt\s+<nak@(symbioticeda.com|yosyshq.com)>/N. Engelhardt <nak@yosyshq.com>/gi;
s/((David)\s+)+Shah\s+<(dave|david)@(symbioticeda.com|yosyshq.com|ds0.me)>/David Shah <dave@ds0.me>/gi;
s/((Miodrag)\s+)+Milanovic\s+<(miodrag|micko)@(symbioticeda.com|yosyshq.com)>/Miodrag Milanovic <micko@yosyshq.com>/gi;
s,https?://www.clifford.at/yosys/,http://yosyshq.net/yosys/,g ;
2021-06-08 00:39:36 +02:00
cbf6b719fe
Make a few passes auto-call Mem::narrow instead of rejecting wide ports.
...
This essentially adds wide port support for free in passes that don't
have a usefully better way of handling wide ports than just breaking
them up to narrow ports, avoiding "please run memory_narrow" annoyance.
2021-05-28 00:40:56 +02:00
69bf5c81c7
Reject wide ports in some passes that will never support them.
2021-05-25 02:07:25 +02:00
c4cc888b2c
kernel/rtlil: Extract some helpers for checking memory cell types.
...
There will soon be more (versioned) memory cells, so handle passes that
only care if a cell is memory-related by a simple helper call instead of
a hardcoded list.
2021-05-22 21:43:00 +02:00
979347999f
btor, smt2, smv: Add a hint on how to deal with funny FF types.
2021-02-25 22:04:04 +01:00
f272c8b407
smt2: Use Mem helper.
2020-10-21 17:51:20 +02:00
54166ae0c5
smtbmc: escape identifiers in verilog testbench
2020-10-06 11:27:14 +02:00
3238190797
use the new isPublic() in a few places
2020-09-14 12:43:18 +02:00
c1fff52477
write_smt2: fix SMT-LIB tutorial URL
2020-08-29 20:02:35 +00:00
91682d189e
Ensure smt2 comments are associated with accessors
2020-08-20 16:00:05 -04:00
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
Miodrag Milanović
N. Engelhardt
Claire Xenia Wolf
Marcelina Kościelnicka
GCHQDeveloper560
Jakob Wenzel
N. Engelhardt
whitequark
Noah Moroze
Alberto Gonzalez
Claire Wolf
Yehowshua Immanuel
Xiretza
Eddie Hung
Teguh Hofstee
Claire Wolf
Sean Cross