Alberto Gonzalez
f544a2cc84
qbfsat: Fix name-based hole specialization.
...
Look for unique connections in the containing module with the $anyconst port Y SigBit on the RHS and use those. If no such connection is found, fall back to using the name of the $anyconst port Y SigBit.
2020-06-30 01:53:21 +00:00
Miodrag Milanovic
405b4e97a1
Give error that options are exclusive
2020-06-29 14:45:49 +02:00
Miodrag Milanovic
0545a042f3
cleanup
2020-06-29 14:42:48 +02:00
Miodrag Milanovic
87717d67d1
expose pass fix
2020-06-29 11:56:43 +02:00
Alberto Gonzalez
a564cc806f
log, qbfsat: Include child process time in PerformanceTimer::query() and report the time for each call to the QBF-SAT solver.
2020-06-21 02:16:52 +00:00
Alberto Gonzalez
62a9e62a1b
qbfsat: Simplify solution recovery parsing and tweak the solution regexes.
2020-06-21 02:16:11 +00:00
Alberto Gonzalez
e1fedf054e
qbfsat: Avoid instantiating AttrObjects directly.
...
Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
2020-06-21 02:16:11 +00:00
Alberto Gonzalez
08cede4669
qbfsat: Simplify solution format and replace SigBit::str() with log_signal().
...
Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
2020-06-21 02:16:11 +00:00
Alberto Gonzalez
4ab41c6435
qbfsat: Fixes three bugs.
...
1. Infinite loop in the optimization procedure when the first solution found while maximizing is at zero.
2. A signed-ness issue when maximizing.
3. Erroneously entering bisection mode with no wire to optimize.
2020-06-21 02:16:11 +00:00
Alberto Gonzalez
a3d1f8637a
qbfsat: Use bit precise mapping for hole value wires and a more robust hole spec for writing to and specializing from a solution file.
2020-06-21 02:16:11 +00:00
whitequark
ede4b10da8
Merge pull request #2173 from whitequark/use-cxx11-final-override
...
Use C++11 final/override/[[noreturn]]
2020-06-19 06:15:33 +00:00
whitequark
7191dd16f9
Use C++11 final/override keywords.
2020-06-18 23:34:52 +00:00
Alberto Gonzalez
76dfa81790
cutpoint: Improve efficiency by iterating over module ports instead of module wires.
2020-06-18 17:42:36 +00:00
Claire Wolf
0bd70e8222
Drive-by modernization in sat.cc
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-06-09 22:48:26 +02:00
Alberto Gonzalez
9847a4eea8
smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4.
2020-05-25 20:39:30 +00:00
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
