Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge pull request #1921 from whitequark/write_cxxrtl-separate-compilation | whitequark | 2020-04-14 | 2 | -10/+82 |
|\ | | | | | write_cxxrtl: enable separate compilation | ||||
| * | write_verilog: fix precondition check. | whitequark | 2020-04-14 | 1 | -1/+1 |
| | | |||||
| * | write_cxxrtl: enable separate compilation. | whitequark | 2020-04-14 | 1 | -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 model | Eddie Hung | 2020-04-13 | 1 | -0/+4 |
|/ | |||||
* | Support custom PROGRAM_PREFIX | Miodrag Milanovic | 2020-04-10 | 2 | -9/+8 |
| | |||||
* | write_cxxrtl: add basic documentation. | whitequark | 2020-04-09 | 1 | -1/+16 |
| | |||||
* | write_cxxrtl: add support for $dlatch and $dlatchsr cells. | whitequark | 2020-04-09 | 1 | -3/+16 |
| | | | | Also, fix codegen for $dffe and $adff. | ||||
* | write_cxxrtl: add support for $sr cell. | whitequark | 2020-04-09 | 1 | -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. | whitequark | 2020-04-09 | 1 | -1/+16 |
| | |||||
* | write_cxxrtl: improve writable memory handling. | whitequark | 2020-04-09 | 2 | -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. | whitequark | 2020-04-09 | 1 | -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. | whitequark | 2020-04-09 | 2 | -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. | whitequark | 2020-04-09 | 2 | -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. | whitequark | 2020-04-09 | 1 | -35/+359 |
| | | | | | This results in massive gains in performance, equally massive reduction in compile time, and improved readability. | ||||
* | write_cxxrtl: new backend. | whitequark | 2020-04-09 | 3 | -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 Hung | 2020-04-02 | 9 | -727/+727 |
| | |||||
* | Update backends/btor/btor.cc; credit @boqwxp | Eddie Hung | 2020-04-02 | 1 | -2/+1 |
| | | | Co-Authored-By: Alberto Gonzalez <61295559+boqwxp@users.noreply.github.com> | ||||
* | kernel: use more ID::* | Eddie Hung | 2020-04-02 | 11 | -280/+280 |
| | |||||
* | Merge pull request #1770 from YosysHQ/claire/btor_symbols | Claire Wolf | 2020-04-02 | 1 | -36/+60 |
|\ | | | | | Improve write_btor symbol handling | ||||
| * | Improve write_btor symbol handling | Claire Wolf | 2020-03-14 | 1 | -36/+60 |
| | | | | | | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com> | ||||
* | | Merge pull request #1765 from YosysHQ/claire/btor_info | Claire Wolf | 2020-04-02 | 1 | -9/+113 |
|\| | | | | | Add info-file and cover features to write_btor | ||||
| * | Add info-file and cover features to write_btor | Claire Wolf | 2020-03-13 | 1 | -9/+113 |
| | | | | | | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com> | ||||
* | | Update `RTLIL::id2cstr()` usage to `log_id`. | Alberto Gonzalez | 2020-04-01 | 1 | -2/+2 |
| | | |||||
* | | Clean up pseudo-private member usage in `backends/intersynth/intersynth.cc`. | Alberto Gonzalez | 2020-04-01 | 1 | -22/+19 |
| | | |||||
* | | Clean up pseudo-private member usage in `backends/blif/blif.cc`. | Alberto Gonzalez | 2020-04-01 | 1 | -15/+11 |
| | | |||||
* | | Clean up pseudo-private member usage in `backends/verilog/verilog_backend.cc`. | Alberto Gonzalez | 2020-04-01 | 1 | -22/+19 |
| | | |||||
* | | Clean up pseudo-private member usage in `backends/spice/spice.cc`. | Alberto Gonzalez | 2020-04-01 | 1 | -13/+9 |
| | | |||||
* | | Clean up pseudo-private member usage in `backends/edif/edif.cc`. | Alberto Gonzalez | 2020-04-01 | 1 | -23/+18 |
| | | |||||
* | | Clean up pseudo-private member usage in `backends/ilang/ilang_backend.cc`. | Alberto Gonzalez | 2020-04-01 | 1 | -6/+6 |
| | | |||||
* | | Do not change solver output parsing for non-exists-forall problems. | Alberto Gonzalez | 2020-03-26 | 1 | -2/+6 |
| | | |||||
* | | Skip reading stdout from the solver that if it isn't a line reading only ↵ | Alberto Gonzalez | 2020-03-26 | 1 | -1/+3 |
| | | | | | | | | "sat", "unsat", or "unknown". | ||||
* | | Revert part of 0fda8308 from #1746 that broke other smtbmc flows | Claire Wolf | 2020-03-24 | 1 | -3/+1 |
| | | | | | | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com> | ||||
* | | fix typo in `write_smt2` help | Teguh Hofstee | 2020-03-23 | 1 | -1/+1 |
| | | |||||
* | | Merge pull request #1768 from boqwxp/smt2_cleanup | N. Engelhardt | 2020-03-16 | 1 | -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 Gonzalez | 2020-03-13 | 1 | -5/+5 |
| |/ | |||||
* | | Merge pull request #1746 from boqwxp/optimization | N. Engelhardt | 2020-03-16 | 3 | -1/+33 |
|\ \ | | | | | | | Add support for optimizing exists-forall problems. | ||||
| * | | Add support for optimizing exists-forall problems. | Alberto Gonzalez | 2020-03-13 | 3 | -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 used | Miodrag Milanovic | 2020-03-13 | 1 | -1/+0 |
| |/ |/| | |||||
* | | xaiger: remove some unnecessary operations ... | Eddie Hung | 2020-03-06 | 1 | -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 handling | Eddie Hung | 2020-03-06 | 1 | -3/+4 |
|/ | |||||
* | Make TimingInfo::TimingInfo(SigBit) constructor explicit | Eddie Hung | 2020-02-27 | 1 | -1/+1 |
| | |||||
* | write_xaiger: add comment about arrival times of flop outputs | Eddie Hung | 2020-02-27 | 1 | -0/+1 |
| | |||||
* | Get rid of (* abc9_{arrival,required} *) entirely | Eddie Hung | 2020-02-27 | 1 | -29/+15 |
| | |||||
* | abc9_ops: ignore (* abc9_flop *) if not '-dff' | Eddie Hung | 2020-02-27 | 1 | -38/+44 |
| | |||||
* | xilinx: improve specify functionality | Eddie Hung | 2020-02-27 | 1 | -0/+3 |
| | |||||
* | Merge pull request #1703 from YosysHQ/eddie/specify_improve | Eddie Hung | 2020-02-21 | 1 | -2/+10 |
|\ | | | | | Improve specify parser | ||||
| * | specify: system timing checks to accept min:typ:max triple | Eddie Hung | 2020-02-13 | 1 | -2/+10 |
| | | |||||
* | | Revert "abc9: fix abc9_arrival for flops" | Eddie Hung | 2020-02-14 | 1 | -5/+2 |
| | | | | | | | | This reverts commit f7c0dbecee7ee8f2e3fc8bc8337e7045fd4aff15. | ||||
* | | write_xaiger: default value for abc9_init | Eddie Hung | 2020-02-13 | 1 | -1/+1 |
| | | |||||
* | | abc9: fix abc9_arrival for flops | Eddie Hung | 2020-02-13 | 1 | -2/+5 |
|/ |