aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2
Commit message (Collapse)AuthorAgeFilesLines
...
* Improve smtio performance by using reader thread, not writer threadClifford Wolf2017-10-261-10/+30
|
* Use separate writer thread for talking to SMT solver to avoid read/write ↵Clifford Wolf2017-10-251-8/+23
| | | | deadlock
* Improve p_* functions in smtio.pyClifford Wolf2017-10-251-21/+19
|
* Capsulate smt-solver read/write in separate functionsClifford Wolf2017-10-251-8/+24
|
* Fix a bug in yosys-smtbmc in ROM handlingClifford Wolf2017-10-251-0/+3
|
* Fix bug in write_smt2 (export logic driving hierarchical cells before ↵Clifford Wolf2017-08-251-34/+34
| | | | exporting regs)
* 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 ↵Clifford Wolf2017-06-073-4/+53
| | | | const reg"
* Change default smt2 solver to yices (Yices 2 has switched its license to GPL)Clifford Wolf2017-05-271-4/+4
|
* Add $_ANDNOT_ and $_ORNOT_ gatesClifford Wolf2017-05-171-0/+2
|
* Fix boolector support in yosys-smtbmcClifford Wolf2017-05-081-18/+18
|
* Add "write_smt2 -stdt" modeClifford Wolf2017-03-202-37/+84
|
* Improve smt2 encodings of assert/assume/cover, better wire_smt2 help msgClifford Wolf2017-03-042-33/+87
|
* 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 extra newline bug in write_smt2Clifford Wolf2017-02-261-1/+1
|
* Fix bug in smtio unroll codeClifford Wolf2017-02-261-3/+2
|
* 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-263-47/+51
|
* Add support for "yosys-smtbmc -c --append"Clifford Wolf2017-02-251-1/+13
|
* Add "write_smt2 -stbv"Clifford Wolf2017-02-243-49/+179
|
* Add SMT2 statebv mode (inactive for now)Clifford Wolf2017-02-241-20/+47
|
* Add "yosys-smtbmc -S <opt>"Clifford Wolf2017-02-191-7/+18
|
* 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-043-4/+97
|
* Further improve cover() supportClifford Wolf2017-02-041-3/+5
|
* 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-282-8/+55
|
* Fix $initstate handling bug in yosys-smtbmcClifford Wolf2017-01-111-0/+2
|
* Implicitly set "yosys-smtbmc --noprogress" on windowsClifford Wolf2017-01-041-3/+4
|
* Fixed "yosys-smtbmc --noprogress"Clifford Wolf2017-01-041-1/+1
|
* 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 support for partially initialized regs to smt2 back-endClifford Wolf2016-12-011-3/+15
|
* Bugfix in smt2 back-end for pure checker modulesClifford Wolf2016-11-281-0/+4
|
* Removed shebang line from smtio.py, fixes #279Clifford Wolf2016-11-271-1/+0
|
* 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
|
* cleanup in write_smt2 log messages (-bv and -mem are now default)Clifford Wolf2016-10-161-1/+1
|
* Added $anyseq cell typeClifford Wolf2016-10-141-1/+1
|