aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat
Commit message (Expand)AuthorAgeFilesLines
* 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
* Merge pull request #2208 from boqwxp/qbfsat-cleanupclairexen2020-07-022-255/+273
|\
| * 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 direc...Alberto Gonzalez2020-07-011-3/+7
| * 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 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.Alberto Gonzalez2020-06-301-16/+47
| |/
* | Merge pull request #2206 from boqwxp/qbfsat-fix-name-specializationclairexen2020-07-011-2/+24
|\ \
| * | qbfsat: Fix name-based hole specialization.Alberto Gonzalez2020-06-301-2/+24
| |/
* | Merge pull request #2199 from YosysHQ/mmicko/sim_memoryclairexen2020-06-301-1/+4
|\ \ | |/ |/|
| * 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 re...Alberto Gonzalez2020-06-211-1/+6
* 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
* qbfsat: Simplify solution format and replace `SigBit::str()` with `log_signal...Alberto Gonzalez2020-06-211-19/+37
* qbfsat: Fixes three bugs.Alberto Gonzalez2020-06-211-5/+17
* qbfsat: Use bit precise mapping for hole value wires and a more robust hole s...Alberto Gonzalez2020-06-211-80/+113
* Merge pull request #2173 from whitequark/use-cxx11-final-overridewhitequark2020-06-1915-30/+30
|\
| * Use C++11 final/override keywords.whitequark2020-06-1815-30/+30
* | cutpoint: Improve efficiency by iterating over module ports instead of module...Alberto Gonzalez2020-06-181-9/+10
|/
* Drive-by modernization in sat.ccClaire Wolf2020-06-091-4/+4
* smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, a...Alberto Gonzalez2020-05-251-13/+53
* qbfsat: Add support for CVC4.Alberto Gonzalez2020-05-251-2/+6
* qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices th...Alberto Gonzalez2020-05-251-20/+47
* qbfsat: Remove cruft inadvertently left untouched in commit 86fc49a9d60f9ad4c...Alberto Gonzalez2020-05-231-11/+0
* qbfsat: Add bisection mode and make it the default.Alberto Gonzalez2020-05-231-87/+207
* Add WASI platform support.whitequark2020-04-301-1/+2
* Merge pull request #1989 from boqwxp/qbfsat_anyconst_sourcelocsClaire Wolf2020-04-231-5/+2
|\
| * qbfsat: Make hole name recovery more robust. Allow multiple cell types to sha...Alberto Gonzalez2020-04-231-5/+2
* | 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
* qbfsat: Fix illegal use of 'stdout' identifierDavid Shah2020-04-171-3/+3
* Merge pull request #1830 from boqwxp/qbfsatN. Engelhardt2020-04-152-0/+551
|\
| * 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
| * Remove `$anyconst` cells before specialization to eliminate warnings and the ...Alberto Gonzalez2020-04-071-2/+25
| * 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
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-06 14:33:31 +0000