aboutsummaryrefslogtreecommitdiffstats
path: root/backends
Commit message (Collapse)AuthorAgeFilesLines
* Merge pull request #1921 from whitequark/write_cxxrtl-separate-compilationwhitequark2020-04-142-10/+82
|\ | | | | write_cxxrtl: enable separate compilation
| * write_verilog: fix precondition check.whitequark2020-04-141-1/+1
| |
| * write_cxxrtl: enable separate compilation.whitequark2020-04-141-9/+81
| | | | | | | | | | | | This commit makes it possible to use several cxxrtl-generated files in one application, as well as compiling cxxrtl-generated code as a separate compilation unit.
* | xaiger: add check for $__ABC9_DELAY modelEddie Hung2020-04-131-0/+4
|/
* Support custom PROGRAM_PREFIXMiodrag Milanovic2020-04-102-9/+8
|
* write_cxxrtl: add basic documentation.whitequark2020-04-091-1/+16
|
* write_cxxrtl: add support for $dlatch and $dlatchsr cells.whitequark2020-04-091-3/+16
| | | | Also, fix codegen for $dffe and $adff.
* write_cxxrtl: add support for $sr cell.whitequark2020-04-091-27/+35
| | | | | | Also, fix the semantics of SET/CLR inputs of the $dffsr cell, and fix the scheduling of async FF cells to consider ARST/SET/CLR->Q as a forward combinatorial arc.
* write_cxxrtl: add support for $slice and $concat cells.whitequark2020-04-091-1/+16
|
* write_cxxrtl: improve writable memory handling.whitequark2020-04-092-65/+87
| | | | | | This commit reduces space and time overhead for writable memories to O(write port count) in both cases; implements handling for write port priorities; and simplifies runtime representation of memories.
* write_cxxrtl: add support for hierarchical designs.whitequark2020-04-091-18/+107
| | | | | | | | | | | Hierarchical design simulations are generally much slower, but this comes with a major increase in flexibility: 1. Since the `flatten` pass currently does not support flattening of designs with processes, this is the only way to simulate such designs with cxxrtl. 2. Support for hierarchy paves way for simulation black boxes, which are necessary for e.g. replacing PHYs with C++ code that integrates with the host system.
* write_cxxrtl: avoid undefined behavior on out-of-bounds memory access.whitequark2020-04-092-46/+78
| | | | | | | | | | After this commit, if NDEBUG is not defined, out-of-bounds accesses cause assertion failures for reads and writes. If NDEBUG is defined, out-of-bounds reads return zeroes, and out-of-bounds writes are ignored. This commit also adds support for memories that start with a non-zero index (`Memory::start_offset` in RTLIL).
* write_cxxrtl: statically schedule comb logic and localize wires.whitequark2020-04-092-68/+368
| | | | | | This results in further massive gains in performance, modest decrease in compile time, and, for designs without feedback arcs, makes it possible to run eval() once per clock edge in certain conditions.
* write_cxxrtl: elide wires for results of comb cells used once.whitequark2020-04-091-35/+359
| | | | | This results in massive gains in performance, equally massive reduction in compile time, and improved readability.
* write_cxxrtl: new backend.whitequark2020-04-093-0/+2010
| | | | | This commit adds a basic implementation that isn't very performant but implements most of the planned features.
* kernel: big fat patch to use more ID::*, otherwise ID(*)Eddie Hung2020-04-029-727/+727
|
* Update backends/btor/btor.cc; credit @boqwxpEddie Hung2020-04-021-2/+1
| | | Co-Authored-By: Alberto Gonzalez <61295559+boqwxp@users.noreply.github.com>
* kernel: use more ID::*Eddie Hung2020-04-0211-280/+280
|
* Merge pull request #1770 from YosysHQ/claire/btor_symbolsClaire Wolf2020-04-021-36/+60
|\ | | | | Improve write_btor symbol handling
| * Improve write_btor symbol handlingClaire Wolf2020-03-141-36/+60
| | | | | | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com>
* | Merge pull request #1765 from YosysHQ/claire/btor_infoClaire Wolf2020-04-021-9/+113
|\| | | | | Add info-file and cover features to write_btor
| * Add info-file and cover features to write_btorClaire Wolf2020-03-131-9/+113
| | | | | | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com>
* | Update `RTLIL::id2cstr()` usage to `log_id`.Alberto Gonzalez2020-04-011-2/+2
| |
* | Clean up pseudo-private member usage in `backends/intersynth/intersynth.cc`.Alberto Gonzalez2020-04-011-22/+19
| |
* | Clean up pseudo-private member usage in `backends/blif/blif.cc`.Alberto Gonzalez2020-04-011-15/+11
| |
* | Clean up pseudo-private member usage in `backends/verilog/verilog_backend.cc`.Alberto Gonzalez2020-04-011-22/+19
| |
* | Clean up pseudo-private member usage in `backends/spice/spice.cc`.Alberto Gonzalez2020-04-011-13/+9
| |
* | Clean up pseudo-private member usage in `backends/edif/edif.cc`.Alberto Gonzalez2020-04-011-23/+18
| |
* | Clean up pseudo-private member usage in `backends/ilang/ilang_backend.cc`.Alberto Gonzalez2020-04-011-6/+6
| |
* | Do not change solver output parsing for non-exists-forall problems.Alberto Gonzalez2020-03-261-2/+6
| |
* | Skip reading stdout from the solver that if it isn't a line reading only ↵Alberto Gonzalez2020-03-261-1/+3
| | | | | | | | "sat", "unsat", or "unknown".
* | Revert part of 0fda8308 from #1746 that broke other smtbmc flowsClaire Wolf2020-03-241-3/+1
| | | | | | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com>
* | fix typo in `write_smt2` helpTeguh Hofstee2020-03-231-1/+1
| |
* | Merge pull request #1768 from boqwxp/smt2_cleanupN. Engelhardt2020-03-161-5/+5
|\ \ | | | | | | Clean up pseudo-private member usage in `backends/smt2/smt2.cc`.
| * | Clean up pseudo-private member usage in `backends/smt2/smt2.cc`.Alberto Gonzalez2020-03-131-5/+5
| |/
* | Merge pull request #1746 from boqwxp/optimizationN. Engelhardt2020-03-163-1/+33
|\ \ | | | | | | Add support for optimizing exists-forall problems.
| * | Add support for optimizing exists-forall problems.Alberto Gonzalez2020-03-133-1/+33
| | | | | | | | | | | | | | | | | | Modifies smt2 backend to recognize `$anyconst` etc. assigned to a wire with the `maximize` or `minimize` attribute and emit `; yosys-smt2-maximize` or `; yosys-smt2-minimize` directives as appropriate. Modifies `backends/smt2/smtbmc.py` and `smtio.py` to recognize those directives and emit a `(maximize ...)` or `(minimize ...)` command at the end of `smt_forall_assert()`, as described in the paper "νZ - An Optimizing SMT Solver" by Nikolaj Bjørner et al. Adds an example `examples/smtbmc/demo9.v` to show how it can be used.
* | | remove include where not usedMiodrag Milanovic2020-03-131-1/+0
| |/ |/|
* | xaiger: remove some unnecessary operations ...Eddie Hung2020-03-061-9/+2
| | | | | | | | | | ... since they can not be triggered by (* keep *) anymore (but could still be triggered by (* abc9_scc *) !?!)
* | abc9: (* keep *) wires to be PO only, not PI as well; fix scc handlingEddie Hung2020-03-061-3/+4
|/
* Make TimingInfo::TimingInfo(SigBit) constructor explicitEddie Hung2020-02-271-1/+1
|
* write_xaiger: add comment about arrival times of flop outputsEddie Hung2020-02-271-0/+1
|
* Get rid of (* abc9_{arrival,required} *) entirelyEddie Hung2020-02-271-29/+15
|
* abc9_ops: ignore (* abc9_flop *) if not '-dff'Eddie Hung2020-02-271-38/+44
|
* xilinx: improve specify functionalityEddie Hung2020-02-271-0/+3
|
* Merge pull request #1703 from YosysHQ/eddie/specify_improveEddie Hung2020-02-211-2/+10
|\ | | | | Improve specify parser
| * specify: system timing checks to accept min:typ:max tripleEddie Hung2020-02-131-2/+10
| |
* | Revert "abc9: fix abc9_arrival for flops"Eddie Hung2020-02-141-5/+2
| | | | | | | | This reverts commit f7c0dbecee7ee8f2e3fc8bc8337e7045fd4aff15.
* | write_xaiger: default value for abc9_initEddie Hung2020-02-131-1/+1
| |
* | abc9: fix abc9_arrival for flopsEddie Hung2020-02-131-2/+5
|/