aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2
Commit message (Expand)AuthorAgeFilesLines
* Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constantsClifford Wolf2018-04-041-0/+3
* Fixed -stbv handling in SMT2 back-endClifford Wolf2018-04-041-1/+1
* Add smtio status msgs when --progress is inactiveClifford Wolf2018-03-291-2/+23
* Bugfix in smtio.py VCD file generatorClifford Wolf2018-03-291-1/+1
* Add $mem support to SMT2 clock taggingClifford Wolf2018-03-271-0/+18
* Improve yosys-smtbmc log output and error handlingClifford Wolf2018-03-171-5/+14
* Improve handling of invalid check-sat result in smtio.pyClifford Wolf2018-03-171-1/+2
* Remove debug prints from yosys-smtbmc VCD writerClifford Wolf2018-03-081-2/+0
* Check results of (check-sat) in yosys-smtbmcClifford Wolf2018-03-071-0/+2
* Imporove yosys-smtbmc error handling, Improve VCD outputClifford Wolf2018-03-052-23/+49
* Improve SMT2 encoding of $reduce_{and,or,bool}Clifford Wolf2018-03-041-1/+9
* Fix a hangup in yosys-smtbmc error handlingClifford Wolf2018-03-041-3/+5
* Improved error handling in yosys-smtbmcClifford Wolf2018-03-031-1/+3
* Terminate running SMT solver when smtbmc is terminatedClifford Wolf2018-03-031-1/+31
* Fix smtbmc smtc/aiw parser for wire names containing []Clifford Wolf2018-03-031-1/+1
* Mangle names with square brackets in VCD files to work around issues in gtkwaveClifford Wolf2018-03-011-2/+8
* Small fixes and improvements in $allconst/$allseq handlingClifford Wolf2018-02-261-12/+18
* Add smtbmc support for exist-forall problemsClifford Wolf2018-02-233-87/+334
* Add support for mockup clock signals in yosys-smtbmc vcd outputClifford Wolf2018-02-203-6/+111
* Fix handling of zero-length cell connections in SMT2 back-endClifford Wolf2018-02-081-0/+8
* Fix smtio.py for large SMT2 S-expressionsClifford Wolf2018-01-291-1/+12
* Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 outputClifford Wolf2018-01-181-3/+3
* Add yosys-smtbmc VCD writer support for memories with async writesClifford Wolf2017-12-143-7/+11
* Add smt2 back-end support for async write memoriesClifford Wolf2017-12-141-14/+53
* Fixed "yosys-smtbmc -g" handling of no solutionClifford Wolf2017-11-271-1/+1
* Fix SMT2 handling of initstate in sub-modulesClifford Wolf2017-10-291-0/+3
* 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 dead...Clifford Wolf2017-10-251-8/+23
* 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 exporti...Clifford Wolf2017-08-251-34/+34
* 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-073-4/+53
* 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