aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat
Commit message (Collapse)AuthorAgeFilesLines
* Add #include needed to build with gcc-11Gabriel Somlo2020-11-261-0/+1
| | | | Suggested by Jeff Law <law@redhat.com>
* Add rewrite_filename for sim -vcd argument.Chris Dailey2020-11-241-1/+3
|
* Merge pull request #2403 from nakengelhardt/sim_timescaleN. Engelhardt2020-10-221-0/+21
|\ | | | | sim -vcd: add date, version, and option for timescale
| * use strftime instead of put_time for gcc 4.8 compatibilityN. Engelhardt2020-10-211-4/+5
| |
| * wild guessing at the problem because it builds fine on my machinesN. Engelhardt2020-10-161-0/+3
| |
| * sim -vcd: add date, version, and option for timescaleN. Engelhardt2020-10-161-0/+17
| |
* | sim: Use Mem helper.Marcelina Kościelnicka2020-10-211-103/+90
| |
* | clk2fflogic: Use Mem helper.Marcelina Kościelnicka2020-10-211-68/+45
|/
* use the new isPublic() in a few placesN. Engelhardt2020-09-142-4/+4
|
* async2sync: Support all FF types.Marcelina Kościelnicka2020-07-302-145/+162
|
* async2sync: Refactor to use FfInitVals.Marcelina Kościelnicka2020-07-241-53/+11
|
* clk2fflogic: Support all FF types.Marcelina Kościelnicka2020-07-241-200/+122
|
* qbfsat: Add `-solver-option` option.Alberto Gonzalez2020-07-202-1/+15
|
* clk2fflogic: Consistently treat async control signals as negative hold.Marcelina Kościelnicka2020-07-091-57/+51
| | | | | | | This fixes some dfflegalize equivalence checks, and breaks others — and I strongly suspect the others are due to bad support for multiple async inputs in `proc` (in particular, lack of proper support for dlatchsr and sketchy circuits on dffsr control inputs).
* Merge pull request #2208 from boqwxp/qbfsat-cleanupclairexen2020-07-022-255/+273
|\ | | | | qbfsat: Cleanup and refactoring
| * qbfsat: Remove useless comment and #ifndef guards.Alberto Gonzalez2020-07-011-5/+0
| |
| * qbfsat: Specify default values for some options in the help message.Alberto Gonzalez2020-07-011-0/+2
| |
| * qbfsat: Clean up external executable command lines and update temporary ↵Alberto Gonzalez2020-07-011-3/+7
| | | | | | | | directory name.
| * qbfsat: Clean up and refactor data structures into `qbfsat.h`.Alberto Gonzalez2020-07-012-248/+265
| |
* | Merge pull request #2211 from YosysHQ/mwk/fix-fmcombine-ffclairexen2020-07-021-2/+1
|\ \ | |/ |/| fmcombine: use the master ff cell type list
| * fmcombine: use the master ff cell type listMarcelina Kościelnicka2020-06-301-2/+1
| |
* | Merge pull request #2138 from boqwxp/qbfsat-oflagclairexen2020-07-011-16/+47
|\ \ | | | | | | qbfsat: Add `-O[012]` options to control pre-solving simplification with ABC
| * | qbfsat: Add `-O[012]` options to control pre-solving simplification with ABC.Alberto Gonzalez2020-06-301-16/+47
| |/ | | | | | | | | | | Thanks to @mwk for the gate mapping part of the ABC scripts. Co-Authored-By: Marcelina Kościelnicka <mwk@0x04.net>
* | Merge pull request #2206 from boqwxp/qbfsat-fix-name-specializationclairexen2020-07-011-2/+24
|\ \ | | | | | | qbfsat: Fix name-based hole specialization
| * | qbfsat: Fix name-based hole specialization.Alberto Gonzalez2020-06-301-2/+24
| |/ | | | | | | 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.
* | Merge pull request #2199 from YosysHQ/mmicko/sim_memoryclairexen2020-06-301-1/+4
|\ \ | |/ |/| sim - error when memrd and memwr detected
| * sim - error when memrd and memwr detectedMiodrag Milanovic2020-06-291-1/+4
| |
* | Give error that options are exclusiveMiodrag Milanovic2020-06-291-2/+6
| |
* | cleanupMiodrag Milanovic2020-06-291-12/+13
| |
* | expose pass fixMiodrag Milanovic2020-06-291-5/+16
|/
* log, qbfsat: Include child process time in `PerformanceTimer::query()` and ↵Alberto Gonzalez2020-06-211-1/+6
| | | | report the time for each call to the QBF-SAT solver.
* qbfsat: Simplify solution recovery parsing and tweak the solution regexes.Alberto Gonzalez2020-06-211-22/+12
|
* qbfsat: Avoid instantiating `AttrObject`s directly.Alberto Gonzalez2020-06-211-9/+6
| | | | Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
* qbfsat: Simplify solution format and replace `SigBit::str()` with ↵Alberto Gonzalez2020-06-211-19/+37
| | | | | | `log_signal()`. Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
* qbfsat: Fixes three bugs.Alberto Gonzalez2020-06-211-5/+17
| | | | | | 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.
* qbfsat: Use bit precise mapping for hole value wires and a more robust hole ↵Alberto Gonzalez2020-06-211-80/+113
| | | | spec for writing to and specializing from a solution file.
* 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>
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-14 11:22:36 +0000