aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smtio.py
Commit message (Expand)AuthorAgeFilesLines
* smt: handle failure of setrlimit syscallN. Engelhardt2019-07-151-1/+5
* Escape scope names starting with dollar sign in smtio.pyClifford Wolf2019-06-261-1/+4
* Add timescale and generated-by header to yosys-smtbmc MkVcdClifford Wolf2019-06-161-0/+2
* Add missing blackslash-to-slash convertion to smtio.py (matching Smt2Worker::...Clifford Wolf2019-02-061-1/+1
* Merge pull request #693 from YosysHQ/rlimitClifford Wolf2018-11-071-8/+11
|\
| * Limit stack size to 16 MB on DarwinClifford Wolf2018-11-071-1/+4
| * Fix for improved smtio.py rlimit codeClifford Wolf2018-11-061-1/+1
| * Improve stack rlimit code in smtio.pyClifford Wolf2018-11-061-8/+8
* | Run solver in non-incremental mode whem smtio.py is configured for non-increm...Clifford Wolf2018-11-061-3/+12
|/
* Use conservative stack size for SMT2 on MacOSArjen Roodselaar2018-11-041-1/+6
* Gate POSIX-only signals and resource module to only run on POSIX Python imple...William D. Jones2018-07-061-9/+12
* Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constantsClifford Wolf2018-04-041-0/+3
* 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
* 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-051-20/+43
* 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
* Mangle names with square brackets in VCD files to work around issues in gtkwaveClifford Wolf2018-03-011-2/+8
* Add smtbmc support for exist-forall problemsClifford Wolf2018-02-231-4/+53
* Add support for mockup clock signals in yosys-smtbmc vcd outputClifford Wolf2018-02-201-2/+49
* 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-141-1/+1
* 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 generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand cons...Clifford Wolf2017-06-071-1/+30
* Change default smt2 solver to yices (Yices 2 has switched its license to GPL)Clifford Wolf2017-05-271-4/+4
* Fix boolector support in yosys-smtbmcClifford Wolf2017-05-081-18/+18
* Add "write_smt2 -stdt" modeClifford Wolf2017-03-201-28/+37
* Improve smt2 encodings of assert/assume/cover, better wire_smt2 help msgClifford Wolf2017-03-041-2/+2
* Fix bug in smtio unroll codeClifford Wolf2017-02-261-3/+2
* Improve (and fix for stbv mode) SMT2 memory APIClifford Wolf2017-02-261-3/+3
* Add "write_smt2 -stbv"Clifford Wolf2017-02-241-1/+1
* Add "yosys-smtbmc -S <opt>"Clifford Wolf2017-02-191-7/+18
* Partially implement cover() support in yosys-smtbmcClifford Wolf2017-02-041-0/+4
* Add "yosys-smtbmc --aig-noheader" and AIGER mem init supportClifford Wolf2017-01-281-2/+22
* Implicitly set "yosys-smtbmc --noprogress" on windowsClifford Wolf2017-01-041-3/+4
* Fixed "yosys-smtbmc --noprogress"Clifford Wolf2017-01-041-1/+1
* Removed shebang line from smtio.py, fixes #279Clifford Wolf2016-11-271-1/+0
* Merge branch 'master' of github.com:cliffordwolf/yosysClifford Wolf2016-10-111-0/+2
|\
| * Added smtc support for top-level state with [], [N:] syntaxClifford Wolf2016-10-081-0/+2
* | Bugfix in yosys-smtbmc --noincrClifford Wolf2016-10-041-1/+8
|/
* yosys-smtbmc: ABC is a QF_BV solverClifford Wolf2016-10-031-0/+1