aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2
Commit message (Expand)AuthorAgeFilesLines
* 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
* Added $ff and $_FF_ cell typesClifford Wolf2016-10-121-5/+5
* Merge branch 'master' of github.com:cliffordwolf/yosysClifford Wolf2016-10-112-1/+3
|\
| * Added smtc support for top-level state with [], [N:] syntaxClifford Wolf2016-10-082-1/+3
* | Bugfix in yosys-smtbmc --noincrClifford Wolf2016-10-041-1/+8
|/
* yosys-smtbmc: ABC is a QF_BV solverClifford Wolf2016-10-031-0/+1
* Added "yosys-smtbmc --noincr"Clifford Wolf2016-10-031-10/+39
* yosys-smtbmc: added smtc [...] support for cellsClifford Wolf2016-10-021-0/+2
* Added "yosys-smtbmc -s abc"Clifford Wolf2016-10-011-0/+4
* Minor improvements in yosys-smtbmcClifford Wolf2016-09-242-10/+50
* Added yosys-smtbmc --noinfo and --dummyClifford Wolf2016-09-192-56/+76
* Improved handling of SMT2 logics in yosys-smtbmcClifford Wolf2016-09-183-11/+49
* yosys-smtbmc: added -i support smtc filesClifford Wolf2016-09-181-20/+19
* Work-around for boolector bugClifford Wolf2016-09-131-2/+2
* Added missing :produce-models setting to smtio.pyClifford Wolf2016-09-111-1/+2
* Minor improvements to smtio.py vcd writerClifford Wolf2016-09-101-1/+3
* fixed write_smt2 for (non-combinatorial) loops through hierarchical cellsClifford Wolf2016-09-101-17/+34
* smt2 mem init bugfixClifford Wolf2016-09-081-4/+6
* yosys-smtbmc meminit supportClifford Wolf2016-09-081-3/+23
* Bugfix in "yosys-smtbmc --unroll"Clifford Wolf2016-09-071-1/+1