Alberto Gonzalez
f9eef5e3f7
qbfsat: Add support for CVC4.
2020-05-25 20:39:03 +00:00
Alberto Gonzalez
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
Alberto Gonzalez
ac41f8a9c7
qbfsat: Remove cruft inadvertently left untouched in commit 86fc49a9d6.
2020-05-23 00:53:09 +00:00
Alberto Gonzalez
aea0fd5ed4
qbfsat: Add bisection mode and make it the default.
...
Also adds `-nooptimize` and reorganizes `qbfsat.cc` a bit.
2020-05-23 00:53:09 +00:00
whitequark
b43c282e4e
Add WASI platform support.
...
This includes the following significant changes:
* Patching ezsat and minisat to disable resource limiting code
on WASM/WASI, since the POSIX functions they use are unavailable.
* Adding a new definition, YOSYS_DISABLE_SPAWN, present if platform
does not support spawning subprocesses (i.e. Emscripten or WASI).
This definition hides the definition of `run_command()`.
* Adding a new Makefile flag, DISABLE_SPAWN, present in the same
condition. This flag disables all passes that require spawning
subprocesses for their function.
2020-04-30 18:56:25 +00:00
Claire Wolf
dc9a72bc8d
Merge pull request #1989 from boqwxp/qbfsat_anyconst_sourcelocs
...
qbfsat: Make hole name recovery from source locations more robust.
2020-04-23 11:34:19 +02:00
Alberto Gonzalez
4ee8452d34
qbfsat: Make hole name recovery more robust. Allow multiple cell types to share the same source location as long as only one $anyconst or $anyseq has that location.
2020-04-23 05:45:44 +00:00
Alberto Gonzalez
7369e6b26b
qbfsat: Add -assume-negative-polarity option.
2020-04-23 04:06:15 +00:00
David Shah
abf81c7639
sim: Fix handling of constant-connected cell inputs at startup
...
Signed-off-by: David Shah <dave@ds0.me>
2020-04-21 08:58:52 +01:00
David Shah
586739ecf3
qbfsat: Fix illegal use of 'stdout' identifier
...
Signed-off-by: David Shah <dave@ds0.me>
2020-04-17 08:42:39 +01:00
N. Engelhardt
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
Alberto Gonzalez
e300766fb3
Use pool instead of std::set.
2020-04-11 09:41:09 +00:00
Alberto Gonzalez
73bd7fb01d
Use dict instead of std::map.
2020-04-11 06:53:59 +00:00
Alberto Gonzalez
de5e6fa56a
Clean up passes/sat/qbfsat.cc.
...
Makes various cosmetic fixes, removes superfluous `hasPort()` check, and uses `emplace_back()` instead of `push_back()`.
2020-04-09 07:47:44 +00:00
Alberto Gonzalez
194354e128
Remove $anyconst cells before specialization to eliminate warnings and the need to run opt_clean.
2020-04-07 03:29:54 +00:00
Alberto Gonzalez
5fedd0931c
Use newly-renamed -push-copy option.
2020-04-04 22:22:54 +00:00
Alberto Gonzalez
0ca3a8e94f
Improve style in passes/sat/qbfsat.cc.
2020-04-04 22:13:27 +00:00
Alberto Gonzalez
1db73e8dd2
Gracefully report error when module has nothing to prove.
2020-04-04 22:13:27 +00:00
Alberto Gonzalez
8f0f13cad2
Suppress yosys-smtbmc output unless the new -show-smtbmc option is provided.
2020-04-04 22:13:27 +00:00
Alberto Gonzalez
ce033a8e36
Fix handling of -sat and -unsat options when the solver returns unknown.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
6af8b767b4
Use log_push() and log_pop() and show the satisfiable model when -specialize is not specified.
...
Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
d311a80222
Clean up qbfsat command and fix AND-reduction of miter outputs.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
125a583c57
Use the -duplicate option rather than -save and -load with an explicit name.
...
Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
86fc49a9d6
Use internal run_command() API instead of popen().
...
Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
09b2264837
Clean up manual casting.
...
Co-Authored-By: David Shah <dave@ds0.me>
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
acf96b6b0b
Remove unimplemented -timeout option.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
bb101e0b3a
Implement the -assume-outputs, -sat, and -unsat options for the qbfsat` command.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
5527063f66
Add NDEBUG guards to qbfsat assertions.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
3a4fd4a999
Implement -specialize-from-file option for the qbfsat command.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
b9e79e0bb7
Implement -write-solution option for the qbfsat command.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
d07ac2612b
Clean up passes/sat/qbfsat.cc.
2020-04-04 22:13:26 +00:00
Alberto Gonzalez
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
Alberto Gonzalez
a4598d64ef
Hole value recovery and specialization implementation for qbfsat command.
2020-04-04 22:13:25 +00:00
Alberto Gonzalez
2fff574741
Barebones implementation of qbfsat command.
2020-04-04 22:13:25 +00:00
Alberto Gonzalez
fb878b2a70
Initial skeleton for qbfsat command.
2020-04-04 22:13:25 +00:00
Eddie Hung
956ecd48f7
kernel: big fat patch to use more ID::*, otherwise ID(*)
2020-04-02 09:51:32 -07:00
Eddie Hung
fdafb74eb7
kernel: use more ID::*
2020-04-02 07:14:08 -07:00
Eddie Hung
37f42fe102
Merge pull request #1845 from YosysHQ/eddie/kernel_speedup
...
kernel: speedup by using more pass-by-const-ref
2020-04-02 07:13:33 -07:00
Eddie Hung
3e88ede061
Merge pull request #1835 from boqwxp/cleanup_sat_expose
...
Clean up pseudo-private member usage in `passes/sat/expose.cc`.
2020-03-30 13:05:12 -07:00
Eddie Hung
9f7d20a653
Merge pull request #1831 from boqwxp/cleanup_sat_eval
...
Clean up pseudo-private member usage in `passes/sat/eval.cc`.
2020-03-30 11:13:53 -07:00
Alberto Gonzalez
00544cffab
Remove unused function parameter.
2020-03-30 18:00:19 +00:00
Alberto Gonzalez
5a0f029e23
Simplify iterating over selected modules or cells.
...
Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
2020-03-30 17:56:07 +00:00
Alberto Gonzalez
f4faa1514b
Further clean up passes/sat/eval.cc.
...
Co-Authored-By: Eddie Hung <eddie@fpgeh.com>
2020-03-30 16:38:35 +00:00
Alberto Gonzalez
9f265dfd3f
Further clean up passes/sat/freduce.cc.
...
Co-Authored-By: Eddie Hung <eddie@fpgeh.com>
2020-03-30 16:25:30 +00:00
Alberto Gonzalez
696660351f
Clean up more in passes/sat/expose.cc.
...
Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
2020-03-30 16:16:16 +00:00
Alberto Gonzalez
1197a43380
Clean up pseudo-private member usage in passes/sat/expose.cc.
2020-03-28 06:18:09 +00:00
Alberto Gonzalez
9a0cdc3835
Clean up pseudo-private member usage in passes/sat/freduce.cc.
2020-03-28 06:08:23 +00:00
Alberto Gonzalez
b63b2dbbc3
Clean up pseudo-private member usage in passes/sat/eval.cc.
2020-03-28 03:11:23 +00:00
Alberto Gonzalez
6b626c2b0f
Clean up pseudo-private member usage in passes/sat/miter.cc.
2020-03-19 07:07:22 +00:00
Eddie Hung
432a09af80
kernel: SigSpec use more const& + overloads to prevent implicit SigSpec
2020-03-13 08:17:39 -07:00
