aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smtbmc.py
Commit message (Expand)AuthorAgeFilesLines
* Imporove yosys-smtbmc error handling, Improve VCD outputClifford Wolf2018-03-051-3/+6
* Fix smtbmc smtc/aiw parser for wire names containing []Clifford Wolf2018-03-031-1/+1
* Small fixes and improvements in $allconst/$allseq handlingClifford Wolf2018-02-261-12/+18
* Add smtbmc support for exist-forall problemsClifford Wolf2018-02-231-73/+209
* Add support for mockup clock signals in yosys-smtbmc vcd outputClifford Wolf2018-02-201-1/+5
* Add yosys-smtbmc VCD writer support for memories with async writesClifford Wolf2017-12-141-4/+8
* Fixed "yosys-smtbmc -g" handling of no solutionClifford Wolf2017-11-271-1/+1
* Fix a bug in yosys-smtbmc in ROM handlingClifford Wolf2017-10-251-0/+3
* Add "yosys-smtbmc --smtc-init --smtc-top --noinit"Clifford Wolf2017-08-041-20/+66
* Add verilator support to testbenches generated by yosys-smtbmcClifford Wolf2017-07-211-3/+15
* Generate FSM-style testbenches in smtbmcClifford Wolf2017-07-121-5/+23
* Change s/asserts/assertions/ in yosys-smtbmc log messagesClifford Wolf2017-07-071-2/+2
* Add "yosys-smtbmc --presat"Clifford Wolf2017-07-071-3/+23
* Remove unneeded delays in smtbmc vlogtbClifford Wolf2017-07-031-1/+1
* Add "yosys-smtbmc --vlogtb-top"Clifford Wolf2017-07-011-15/+32
* Fix smtbmc vlogtb bug in $anyseq handlingClifford Wolf2017-07-011-3/+3
* Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand cons...Clifford Wolf2017-06-071-1/+19
* Use hex addresses in smtbmc vcd mem tracesClifford Wolf2017-02-281-1/+1
* Add smtbmc support for memory vcd dumpingClifford Wolf2017-02-261-0/+98
* Fix assert checking in "yosys-smtbmc -c --append"Clifford Wolf2017-02-261-1/+1
* Improve (and fix for stbv mode) SMT2 memory APIClifford Wolf2017-02-261-19/+24
* Add support for "yosys-smtbmc -c --append"Clifford Wolf2017-02-251-1/+13
* Add "write_smt2 -stbv"Clifford Wolf2017-02-241-4/+4
* Add assert check in "yosys-smtbmc -c"Clifford Wolf2017-02-041-7/+28
* Improve yosys-smtbmc cover() supportClifford Wolf2017-02-041-5/+19
* Partially implement cover() support in yosys-smtbmcClifford Wolf2017-02-041-2/+87
* Add "yosys-smtbmc --aig <aim_filename>:<aiw_filename>" supportClifford Wolf2017-01-301-5/+14
* Add "yosys-smtbmc --aig-noheader" and AIGER mem init supportClifford Wolf2017-01-281-6/+33
* Fix $initstate handling bug in yosys-smtbmcClifford Wolf2017-01-111-0/+2
* Handle "always 1" like "always -1" in .smtc filesClifford Wolf2017-01-021-7/+5
* Improved yosys-smtbmc default -t/--assume-skipped for --cex and --aigClifford Wolf2016-12-031-2/+15
* Added "yosys-smtbmc --aig"Clifford Wolf2016-12-011-6/+127
* Added "yosys-smtbmc --append"Clifford Wolf2016-11-221-2/+20
* Ignore L_pi nets in "yosys-smtbmc --cex"Clifford Wolf2016-10-181-2/+5
* Added "yosys-smtbmc --cex <filename>"Clifford Wolf2016-10-171-1/+35
* Added smtc support for top-level state with [], [N:] syntaxClifford Wolf2016-10-081-1/+1
* Minor improvements in yosys-smtbmcClifford Wolf2016-09-241-3/+19
* Added yosys-smtbmc --noinfo and --dummyClifford Wolf2016-09-191-1/+10
* Improved handling of SMT2 logics in yosys-smtbmcClifford Wolf2016-09-181-2/+0
* yosys-smtbmc: added -i support smtc filesClifford Wolf2016-09-181-20/+19
* Work-around for boolector bugClifford Wolf2016-09-131-2/+2
* yosys-smtbmc: flush stdout after each log msgClifford Wolf2016-09-061-17/+21
* Added boolector support to yosys-smtbmcClifford Wolf2016-09-031-22/+22
* More PEP 8 fixes.Kaj Tuomi2016-09-021-5/+2
* Indentation and PEP 8 fixes. CamelCase and white space after semicolon.Kaj Tuomi2016-09-021-4/+4
* Some syntax fixes. Generator and comma separated list modifications.Kaj Tuomi2016-09-021-14/+8
* Added $anyconst support to yosys-smtbmcClifford Wolf2016-08-301-0/+20
* Added "yosys-smtbmc --dump-all"Clifford Wolf2016-08-291-45/+67
* More yosys-smtbmc bugfixesClifford Wolf2016-08-291-6/+6
* Various fixes and improvements in yosys-smtbmcClifford Wolf2016-08-291-42/+66