aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat
Commit message (Collapse)AuthorAgeFilesLines
* Merge pull request #2173 from whitequark/use-cxx11-final-overridewhitequark2020-06-1915-30/+30
|\ | | | | Use C++11 final/override/[[noreturn]]
| * Use C++11 final/override keywords.whitequark2020-06-1815-30/+30
| |
* | cutpoint: Improve efficiency by iterating over module ports instead of ↵Alberto Gonzalez2020-06-181-9/+10
|/ | | | module wires.
* Drive-by modernization in sat.ccClaire Wolf2020-06-091-4/+4
| | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com>
* smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, ↵Alberto Gonzalez2020-05-251-13/+53
| | | | and CVC4.
* qbfsat: Add support for CVC4.Alberto Gonzalez2020-05-251-2/+6
|
* qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices ↵Alberto Gonzalez2020-05-251-20/+47
| | | | | | 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.
* qbfsat: Remove cruft inadvertently left untouched in commit ↵Alberto Gonzalez2020-05-231-11/+0
| | | | 86fc49a9d60f9ad4cdeec93663e7245a9fdf60c6.
* qbfsat: Add bisection mode and make it the default.Alberto Gonzalez2020-05-231-87/+207
| | | | Also adds `-nooptimize` and reorganizes `qbfsat.cc` a bit.
* Add WASI platform support.whitequark2020-04-301-1/+2
| | | | | | | | | | | | 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.
* Merge pull request #1989 from boqwxp/qbfsat_anyconst_sourcelocsClaire Wolf2020-04-231-5/+2
|\ | | | | qbfsat: Make hole name recovery from source locations more robust.
| * qbfsat: Make hole name recovery more robust. Allow multiple cell types to ↵Alberto Gonzalez2020-04-231-5/+2
| | | | | | | | share the same source location as long as only one `$anyconst` or `$anyseq` has that location.
* | qbfsat: Add `-assume-negative-polarity` option.Alberto Gonzalez2020-04-231-6/+22
|/
* sim: Fix handling of constant-connected cell inputs at startupDavid Shah2020-04-211-1/+5
| | | | Signed-off-by: David Shah <dave@ds0.me>
* qbfsat: Fix illegal use of 'stdout' identifierDavid Shah2020-04-171-3/+3
| | | | Signed-off-by: David Shah <dave@ds0.me>
* Merge pull request #1830 from boqwxp/qbfsatN. Engelhardt2020-04-152-0/+551
|\ | | | | Add `qbfsat` command to integrate exists-forall solving and specialization
| * Use `pool` instead of `std::set`.Alberto Gonzalez2020-04-111-6/+6
| |
| * Use `dict` instead of `std::map`.Alberto Gonzalez2020-04-111-8/+8
| |
| * Clean up `passes/sat/qbfsat.cc`.Alberto Gonzalez2020-04-091-13/+10
| | | | | | | | Makes various cosmetic fixes, removes superfluous `hasPort()` check, and uses `emplace_back()` instead of `push_back()`.
| * Remove `$anyconst` cells before specialization to eliminate warnings and the ↵Alberto Gonzalez2020-04-071-2/+25
| | | | | | | | need to run `opt_clean`.
| * Use newly-renamed `-push-copy` option.Alberto Gonzalez2020-04-041-1/+1
| |
| * Improve style in `passes/sat/qbfsat.cc`.Alberto Gonzalez2020-04-041-4/+2
| |
| * Gracefully report error when module has nothing to prove.Alberto Gonzalez2020-04-041-5/+8
| |
| * Suppress `yosys-smtbmc` output unless the new `-show-smtbmc` option is provided.Alberto Gonzalez2020-04-041-5/+14
| |
| * Fix handling of `-sat` and `-unsat` options when the solver returns `unknown`.Alberto Gonzalez2020-04-041-0/+2
| |
| * Use `log_push()` and `log_pop()` and show the satisfiable model when ↵Alberto Gonzalez2020-04-041-0/+28
| | | | | | | | | | | | `-specialize` is not specified. Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
| * Clean up `qbfsat` command and fix AND-reduction of miter outputs.Alberto Gonzalez2020-04-041-8/+10
| |
| * Use the `-duplicate` option rather than `-save` and `-load` with an explicit ↵Alberto Gonzalez2020-04-041-2/+2
| | | | | | | | | | | | name. Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
| * Use internal `run_command()` API instead of `popen()`.Alberto Gonzalez2020-04-041-49/+15
| | | | | | | | Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
| * Clean up manual casting.Alberto Gonzalez2020-04-041-2/+2
| | | | | | | | Co-Authored-By: David Shah <dave@ds0.me>
| * Remove unimplemented `-timeout` option.Alberto Gonzalez2020-04-041-16/+4
| |
| * Implement the `-assume-outputs`, `-sat`, and -unsat` options for the ↵Alberto Gonzalez2020-04-041-3/+66
| | | | | | | | `qbfsat` command.
| * Add NDEBUG guards to `qbfsat` assertions.Alberto Gonzalez2020-04-041-0/+18
| |
| * Implement `-specialize-from-file` option for the `qbfsat` command.Alberto Gonzalez2020-04-041-23/+56
| |
| * Implement `-write-solution` option for the `qbfsat` command.Alberto Gonzalez2020-04-041-7/+28
| |
| * Clean up `passes/sat/qbfsat.cc`.Alberto Gonzalez2020-04-041-86/+101
| |
| * Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole ↵Alberto Gonzalez2020-04-041-29/+39
| | | | | | | | value recovery using that mode.
| * Hole value recovery and specialization implementation for `qbfsat` command.Alberto Gonzalez2020-04-041-20/+63
| |
| * Barebones implementation of `qbfsat` command.Alberto Gonzalez2020-04-041-32/+157
| |
| * Initial skeleton for `qbfsat` command.Alberto Gonzalez2020-04-042-0/+207
| |
* | kernel: big fat patch to use more ID::*, otherwise ID(*)Eddie Hung2020-04-0212-272/+272
| |
* | kernel: use more ID::*Eddie Hung2020-04-029-60/+60
| |
* | Merge pull request #1845 from YosysHQ/eddie/kernel_speedupEddie Hung2020-04-021-8/+8
|\ \ | |/ |/| kernel: speedup by using more pass-by-const-ref
| * kernel: SigSpec use more const& + overloads to prevent implicit SigSpecEddie Hung2020-03-131-8/+8
| |
* | Merge pull request #1835 from boqwxp/cleanup_sat_exposeEddie Hung2020-03-301-85/+66
|\ \ | | | | | | Clean up pseudo-private member usage in `passes/sat/expose.cc`.
| * | Remove unused function parameter.Alberto Gonzalez2020-03-301-2/+2
| | |
| * | Simplify iterating over selected modules or cells.Alberto Gonzalez2020-03-301-16/+4
| | | | | | | | | | | | Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
| * | Clean up more in `passes/sat/expose.cc`.Alberto Gonzalez2020-03-301-64/+59
| | | | | | | | | | | | Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
| * | Clean up pseudo-private member usage in `passes/sat/expose.cc`.Alberto Gonzalez2020-03-281-11/+9
| | |
* | | Merge pull request #1831 from boqwxp/cleanup_sat_evalEddie Hung2020-03-301-46/+44
|\ \ \ | | | | | | | | Clean up pseudo-private member usage in `passes/sat/eval.cc`.
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-28 14:14:14 +0000