aboutsummaryrefslogtreecommitdiffstats
path: root/backends
Commit message (Collapse)AuthorAgeFilesLines
* 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
|/
* json: Change compat mode to directly emit ints <= 32 bitsR. Ou2020-02-091-3/+3
| | | | | | This increases compatibility with certain older parsers in some cases that worked before commit 15fae357 but do not work with the current compat-int mode
* Merge pull request #1683 from whitequark/write_verilog-memattrswhitequark2020-02-071-0/+1
|\ | | | | write_verilog: dump $mem cell attributes
| * write_verilog: dump $mem cell attributes.whitequark2020-02-061-0/+1
| | | | | | | | | | The Verilog backend already dumps attributes on RTLIL::Memory objects but not on `$mem` cells.
* | edif: more resilience to mismatched port connection sizes.Marcin Kościelnicki2020-02-061-16/+27
|/ | | | Fixes #1653.
* Merge pull request #1661 from YosysHQ/eddie/abc9_requiredEddie Hung2020-02-051-17/+42
|\ | | | | abc9: add support for required times
| * Merge branch 'eddie/abc9_refactor' into eddie/abc9_requiredEddie Hung2020-01-272-3/+5
| |\
| * \ Merge remote-tracking branch 'origin/eddie/abc9_refactor' into ↵Eddie Hung2020-01-151-1/+2
| |\ \ | | | | | | | | | | | | eddie/abc9_required
| * | | abc9_ops: cope with (* abc9_flop *) in place of (* abc9_box_id *)Eddie Hung2020-01-141-1/+1
| | | |
| * | | Merge remote-tracking branch 'origin/eddie/abc9_refactor' into ↵Eddie Hung2020-01-141-2/+6
| |\ \ \ | | | | | | | | | | | | | | | eddie/abc9_required
| * | | | abc9_ops: generate flop box ids, add abc9_required to FD* cellsEddie Hung2020-01-141-1/+5
| | | | |
| * | | | Merge remote-tracking branch 'origin/eddie/abc9_refactor' into ↵Eddie Hung2020-01-141-1/+1
| |\ \ \ \ | | | | | | | | | | | | | | | | | | eddie/abc9_required
| * | | | | write_xaiger: skip if no arrival timesEddie Hung2020-01-141-0/+3
| | | | | |
| * | | | | Merge remote-tracking branch 'origin/eddie/abc9_refactor' into ↵Eddie Hung2020-01-142-94/+145
| |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | eddie/abc9_required
| * \ \ \ \ \ Merge remote-tracking branch 'origin/eddie/abc9_refactor' into ↵Eddie Hung2020-01-121-19/+28
| |\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | eddie/abc9_required
| * | | | | | | log_debug() for abc9_{arrival,required} timesEddie Hung2020-01-101-0/+8
| | | | | | | |
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-08 01:35:35 +0000