aboutsummaryrefslogtreecommitdiffstats
path: root/backends
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'master' of github.com:YosysHQ/yosys into firrtl_backend_fileinfoSahand Kashani2020-04-0814-1131/+1243
|\
| * 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
| | |
* | | Remove unnecessary pruning of double-quotingSahand Kashani2020-04-081-5/+0
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In the past I was calling the ILANG_BACKEND::dump_const() to dump values to an output stream. When these values were strings, the function used to add quotes around them. The firrtl compiler, in turn, escaped these quotes and the result was double-quoted strings which were hard to read. However I'm now calling design_entity->get_src_attribute() directly and there is no additional quote being put around it, so we can safely remove the unnecessary call to str.erase() here.
* | | Remove use of auto for simple types + simplify src attribute computationSahand Kashani2020-03-241-10/+5
| | |
* | | Refactor to directly call ILANG_BACKEND::dump_const() + directly lookup src ↵Sahand Kashani2020-03-241-68/+15
| | | | | | | | | | | | attribute
* | | Indentation conventionsSahand Kashani2020-03-231-5/+6
| | |
* | | Const parameter in function (backends/firrtl/firrtl.cc)Sahand Kashani-Akhavan2020-03-231-1/+1
| | | | | | | | | Co-Authored-By: Alberto Gonzalez <61295559+boqwxp@users.noreply.github.com>
* | | Strip quotes around fileinfo stringsSahand Kashani2020-03-211-1/+5
| | | | | | | | | | | | | | | | | | Yosys puts quotes around the string that represents the fileinfo whereas firrtl does not. So when firrtl sees quotes, it escapes them with an extra backslash which makes it hard to read afterwards.
* | | Add fileinfo to firrtl backend for assignments and non-instance cellsSahand Kashani2020-03-211-21/+30
| | |
* | | Refactor fileinfo emission characters to single locationSahand Kashani2020-03-201-6/+8
| | |
* | | Add fileinfo to firrtl backend for instancesSahand Kashani2020-03-191-2/+3
| | |
* | | Add fileinfo to firrtl backend for modules and wiresSahand Kashani2020-03-191-12/+20
| | |
* | | Add fileinfo to firrtl backend for top-level circuitSahand Kashani2020-03-191-1/+62
|/ /
* | 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.