aboutsummaryrefslogtreecommitdiffstats
path: root/passes
Commit message (Collapse)AuthorAgeFilesLines
* select: do not select inside blackboxesEddie Hung2020-04-161-0/+3
|
* Merge pull request #1928 from YosysHQ/eddie/design_deleteEddie Hung2020-04-161-1/+21
|\ | | | | kernel: add design -delete option
| * kernel: add design -delete optionEddie Hung2020-04-161-1/+21
| |
* | Merge pull request #1927 from YosysHQ/eddie/design_remove_assertEddie Hung2020-04-161-1/+1
|\ \ | |/ |/| kernel: Design::remove(RTLIL::Module *) to check refcount_modules_
| * design: do not delete when iterating over Design::modules() directlyEddie Hung2020-04-141-1/+1
| |
* | opt_expr: Fix X and CO outputs for $alu identity-mapping rules.Marcelina Kościelnicka2020-04-161-2/+17
| |
* | Merge pull request #1933 from YosysHQ/eddie/zinit_moreEddie Hung2020-04-151-7/+27
|\ \ | | | | | | zinit: handle $__DFFS?E?_[NP][NP][01] too
| * | zinit: handle $__DFFS?E?_[NP][NP][01] tooEddie Hung2020-04-141-7/+27
| | |
* | | 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
| | | |
* | | | Merge pull request #1897 from YosysHQ/dave/bram-rejection-fixDavid Shah2020-04-151-3/+3
|\ \ \ \ | | | | | | | | | | memory_bram: Fix ignorance of valid, matched rules
| * | | | memory_bram: Fix ignorance of valid, matched rulesDavid Shah2020-04-101-3/+3
| | | | | | | | | | | | | | | | | | | | Signed-off-by: David Shah <dave@ds0.me>
* | | | | Get rid of dffsr2dff.Marcelina Kościelnicka2020-04-152-214/+0
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This pass is a proper subset of opt_rmdff, which is called by opt, which is called by every synth flow in the coarse part. Thus, it never actually does anything and can be safely removed.
* | | | | opt_clean: Add missing assignments to opt.did_something.Marcelina Kościelnicka2020-04-151-0/+6
| | | | |
* | | | | setundef: Improve error messages.Marcelina Kościelnicka2020-04-151-10/+12
| | | | | | | | | | | | | | | | | | | | Fixes #1092.
* | | | | abc9_ops: Add a check ensuring that connected port actually exists.Marcelina Kościelnicka2020-04-151-0/+3
| | | | |
* | | | | opt_expr: Add more $alu optimizations.Marcelina Kościelnicka2020-04-141-19/+110
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Detect the places in the $alu where the carry bit is constant (due to const A[i] == B[i] ^ BI) and split it into smaller $alu at these points. Also, make the existing const-carry detection for low bits more generic (now handles cases where both BI and CI are constant, but not equal to one another). Fixes #1912.
* | | | dffinit: Avoid setting init parameter to zero-length value.Marcelina Kościelnicka2020-04-141-3/+5
| |_|/ |/| | | | | | | | Fixes #1704.
* | | abc9_exe: verify -> &verify -sEddie Hung2020-04-141-2/+2
| | |
* | | techmap: fix error messageEddie Hung2020-04-141-1/+1
| | |
* | | zinit: resolve one more comment by @mwkmwkmwkEddie Hung2020-04-131-3/+5
| | |
* | | zinit: fix review comments from @mwkmwkmwkEddie Hung2020-04-131-5/+6
| | |
* | | zinit: operate on $adff, erase (* init *) entries on consumptionEddie Hung2020-04-131-22/+20
| | |
* | | Fix S/R comment; thanks @mwkmwkmwkEddie Hung2020-04-131-1/+1
| | |
* | | zinit to transform set/reset value of $_DFF_[NP][NP][01]_Eddie Hung2020-04-131-0/+14
| | |
* | | Supress error for unhandled \init if whole module selectedEddie Hung2020-04-131-3/+4
| | |
* | | opt_expr: Optimize multiplications with low 0 bits in operands.Marcelina Kościelnicka2020-04-131-0/+33
|/ / | | | | | | Fixes #1500.