Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge pull request #1933 from YosysHQ/eddie/zinit_more | Eddie Hung | 2020-04-15 | 1 | -7/+27 |
|\ | | | | | zinit: handle $__DFFS?E?_[NP][NP][01] too | ||||
| * | zinit: handle $__DFFS?E?_[NP][NP][01] too | Eddie Hung | 2020-04-14 | 1 | -7/+27 |
| | | |||||
* | | Merge pull request #1830 from boqwxp/qbfsat | N. Engelhardt | 2020-04-15 | 2 | -0/+551 |
|\ \ | | | | | | | Add `qbfsat` command to integrate exists-forall solving and specialization | ||||
| * | | Use `pool` instead of `std::set`. | Alberto Gonzalez | 2020-04-11 | 1 | -6/+6 |
| | | | |||||
| * | | Use `dict` instead of `std::map`. | Alberto Gonzalez | 2020-04-11 | 1 | -8/+8 |
| | | | |||||
| * | | Clean up `passes/sat/qbfsat.cc`. | Alberto Gonzalez | 2020-04-09 | 1 | -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 Gonzalez | 2020-04-07 | 1 | -2/+25 |
| | | | | | | | | | | | | need to run `opt_clean`. | ||||
| * | | Use newly-renamed `-push-copy` option. | Alberto Gonzalez | 2020-04-04 | 1 | -1/+1 |
| | | | |||||
| * | | Improve style in `passes/sat/qbfsat.cc`. | Alberto Gonzalez | 2020-04-04 | 1 | -4/+2 |
| | | | |||||
| * | | Gracefully report error when module has nothing to prove. | Alberto Gonzalez | 2020-04-04 | 1 | -5/+8 |
| | | | |||||
| * | | Suppress `yosys-smtbmc` output unless the new `-show-smtbmc` option is provided. | Alberto Gonzalez | 2020-04-04 | 1 | -5/+14 |
| | | | |||||
| * | | Fix handling of `-sat` and `-unsat` options when the solver returns `unknown`. | Alberto Gonzalez | 2020-04-04 | 1 | -0/+2 |
| | | | |||||
| * | | Use `log_push()` and `log_pop()` and show the satisfiable model when ↵ | Alberto Gonzalez | 2020-04-04 | 1 | -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 Gonzalez | 2020-04-04 | 1 | -8/+10 |
| | | | |||||
| * | | Use the `-duplicate` option rather than `-save` and `-load` with an explicit ↵ | Alberto Gonzalez | 2020-04-04 | 1 | -2/+2 |
| | | | | | | | | | | | | | | | | | | name. Co-Authored-By: Claire Wolf <claire@symbioticeda.com> | ||||
| * | | Use internal `run_command()` API instead of `popen()`. | Alberto Gonzalez | 2020-04-04 | 1 | -49/+15 |
| | | | | | | | | | | | | Co-Authored-By: Claire Wolf <claire@symbioticeda.com> | ||||
| * | | Clean up manual casting. | Alberto Gonzalez | 2020-04-04 | 1 | -2/+2 |
| | | | | | | | | | | | | Co-Authored-By: David Shah <dave@ds0.me> | ||||
| * | | Remove unimplemented `-timeout` option. | Alberto Gonzalez | 2020-04-04 | 1 | -16/+4 |
| | | | |||||
| * | | Implement the `-assume-outputs`, `-sat`, and -unsat` options for the ↵ | Alberto Gonzalez | 2020-04-04 | 1 | -3/+66 |
| | | | | | | | | | | | | `qbfsat` command. | ||||
| * | | Add NDEBUG guards to `qbfsat` assertions. | Alberto Gonzalez | 2020-04-04 | 1 | -0/+18 |
| | | | |||||
| * | | Implement `-specialize-from-file` option for the `qbfsat` command. | Alberto Gonzalez | 2020-04-04 | 1 | -23/+56 |
| | | | |||||
| * | | Implement `-write-solution` option for the `qbfsat` command. | Alberto Gonzalez | 2020-04-04 | 1 | -7/+28 |
| | | | |||||
| * | | Clean up `passes/sat/qbfsat.cc`. | Alberto Gonzalez | 2020-04-04 | 1 | -86/+101 |
| | | | |||||
| * | | Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole ↵ | Alberto Gonzalez | 2020-04-04 | 1 | -29/+39 |
| | | | | | | | | | | | | value recovery using that mode. | ||||
| * | | Hole value recovery and specialization implementation for `qbfsat` command. | Alberto Gonzalez | 2020-04-04 | 1 | -20/+63 |
| | | | |||||
| * | | Barebones implementation of `qbfsat` command. | Alberto Gonzalez | 2020-04-04 | 1 | -32/+157 |
| | | | |||||
| * | | Initial skeleton for `qbfsat` command. | Alberto Gonzalez | 2020-04-04 | 2 | -0/+207 |
| | | | |||||
* | | | Merge pull request #1897 from YosysHQ/dave/bram-rejection-fix | David Shah | 2020-04-15 | 1 | -3/+3 |
|\ \ \ | | | | | | | | | memory_bram: Fix ignorance of valid, matched rules | ||||
| * | | | memory_bram: Fix ignorance of valid, matched rules | David Shah | 2020-04-10 | 1 | -3/+3 |
| | | | | | | | | | | | | | | | | Signed-off-by: David Shah <dave@ds0.me> | ||||
* | | | | Get rid of dffsr2dff. | Marcelina Kościelnicka | 2020-04-15 | 2 | -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ścielnicka | 2020-04-15 | 1 | -0/+6 |
| | | | | |||||
* | | | | setundef: Improve error messages. | Marcelina Kościelnicka | 2020-04-15 | 1 | -10/+12 |
| | | | | | | | | | | | | | | | | Fixes #1092. | ||||
* | | | | abc9_ops: Add a check ensuring that connected port actually exists. | Marcelina Kościelnicka | 2020-04-15 | 1 | -0/+3 |
| | | | | |||||
* | | | | opt_expr: Add more $alu optimizations. | Marcelina Kościelnicka | 2020-04-14 | 1 | -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ścielnicka | 2020-04-14 | 1 | -3/+5 |
| | | | | | | | | | | | | Fixes #1704. | ||||
* | | | abc9_exe: verify -> &verify -s | Eddie Hung | 2020-04-14 | 1 | -2/+2 |
| | | | |||||
* | | | techmap: fix error message | Eddie Hung | 2020-04-14 | 1 | -1/+1 |
| | | | |||||
* | | | zinit: resolve one more comment by @mwkmwkmwk | Eddie Hung | 2020-04-13 | 1 | -3/+5 |
| | | | |||||
* | | | zinit: fix review comments from @mwkmwkmwk | Eddie Hung | 2020-04-13 | 1 | -5/+6 |
| | | | |||||
* | | | zinit: operate on $adff, erase (* init *) entries on consumption | Eddie Hung | 2020-04-13 | 1 | -22/+20 |
| | | | |||||
* | | | Fix S/R comment; thanks @mwkmwkmwk | Eddie Hung | 2020-04-13 | 1 | -1/+1 |
| | | | |||||
* | | | zinit to transform set/reset value of $_DFF_[NP][NP][01]_ | Eddie Hung | 2020-04-13 | 1 | -0/+14 |
| | | | |||||
* | | | Supress error for unhandled \init if whole module selected | Eddie Hung | 2020-04-13 | 1 | -3/+4 |
| | | | |||||
* | | | opt_expr: Optimize multiplications with low 0 bits in operands. | Marcelina Kościelnicka | 2020-04-13 | 1 | -0/+33 |
|/ / | | | | | | | Fixes #1500. | ||||
* | | Merge pull request #1603 from whitequark/ice40-ram_style | whitequark | 2020-04-10 | 2 | -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. | whitequark | 2020-04-03 | 1 | -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. | whitequark | 2020-02-06 | 1 | -7/+35 |
| | | | | | | | | | | | | | | | Some vendor toolchains use case insensitive matching for values of attributes that control BRAM inference. | ||||
* | | | Support custom PROGRAM_PREFIX | Miodrag Milanovic | 2020-04-10 | 4 | -14/+14 |
| | | | |||||
* | | | [NFCI] Deduplicate builtin FF cell types list | Marcelina Kościelnicka | 2020-04-09 | 3 | -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_collect | N. Engelhardt | 2020-04-09 | 1 | -6/+3 |
|\ \ \ | | | | | | | | | Clean up `passes/memory/memory_collect.cc`. |