aboutsummaryrefslogtreecommitdiffstats
path: root/passes
Commit message (Collapse)AuthorAgeFilesLines
* 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.
* | Merge pull request #1603 from whitequark/ice40-ram_stylewhitequark2020-04-102-13/+148
|\ \ | | | | | | ice40/ecp5: add support for both 1364.1 and Synplify/LSE RAM/ROM attributes
| * | memory_map: add -attr option, to respect inference attributes.whitequark2020-04-031-6/+113
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Before this commit, memory_map (which is always a part of a synth script) would always pick up any $mem cell that was not processed by a preceding pass and lower it down to $dff/$mux cells. This is undesirable for two reasons: * If there is an explicit inference attribute set on a $mem cell, e.g. (* ram_block *), then it is arguably incorrect to map such a memory to $dff/$mux cells. * If memory_map tries to lower a memory that was intended to be mapped to a large BRAM, it often takes extraordinarily long time to finish, produces an extremely large log file, and outputs an unusable design. After this commit, properly invoked memory_map will not map any memory that has an explicit inference attribute specified, solving the first issue, and alleviating the second. The default behavior is not changed.
| * | memory_bram: add `attr_icase` option.whitequark2020-02-061-7/+35
| | | | | | | | | | | | | | | Some vendor toolchains use case insensitive matching for values of attributes that control BRAM inference.
* | | Support custom PROGRAM_PREFIXMiodrag Milanovic2020-04-104-14/+14
| | |
* | | [NFCI] Deduplicate builtin FF cell types listMarcelina Kościelnicka2020-04-093-73/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | A few passes included the same list of FF cell types. Make it a global const instead. The zinit pass also seems to include a list like that, but given that it seems to be completely broken at the time (see #1568 discussion), I'm going to pretend I didn't see that.
* | | Merge pull request #1890 from boqwxp/cleanup_memory_collectN. Engelhardt2020-04-091-6/+3
|\ \ \ | | | | | | | | Clean up `passes/memory/memory_collect.cc`.