aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2
Commit message (Collapse)AuthorAgeFilesLines
* Add yosys-smtbmc support for btor witnessClifford Wolf2018-12-101-15/+100
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add "yosys-smtbmc --btorwit" skeletonClifford Wolf2018-12-081-1/+19
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Merge pull request #693 from YosysHQ/rlimitClifford Wolf2018-11-071-8/+11
|\ | | | | improve rlimit handling in smtio.py
| * Limit stack size to 16 MB on DarwinClifford Wolf2018-11-071-1/+4
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * Fix for improved smtio.py rlimit codeClifford Wolf2018-11-061-1/+1
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * Improve stack rlimit code in smtio.pyClifford Wolf2018-11-061-8/+8
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Run solver in non-incremental mode whem smtio.py is configured for ↵Clifford Wolf2018-11-061-3/+12
|/ | | | | | non-incremental solving Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Use conservative stack size for SMT2 on MacOSArjen Roodselaar2018-11-041-1/+6
|
* Add proper error message for when smtbmc "append" failsClifford Wolf2018-11-041-2/+10
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add support for signed $shift/$shiftx in smt2 back-endClifford Wolf2018-11-011-1/+3
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Merge pull request #591 from hzeller/virtual-overrideClifford Wolf2018-08-151-2/+2
|\ | | | | Consistent use of 'override' for virtual methods in derived classes.
| * Consistent use of 'override' for virtual methods in derived classes.Henner Zeller2018-07-201-2/+2
| | | | | | | | | | | | | | | | | | o Not all derived methods were marked 'override', but it is a great feature of C++11 that we should make use of. o While at it: touched header files got a -*- c++ -*- for emacs to provide support for that language. o use YS_OVERRIDE for all override keywords (though we should probably use the plain keyword going forward now that C++11 is established)
* | Merge pull request #576 from cr1901/no-resourceClifford Wolf2018-08-151-9/+12
|\ \ | | | | | | Gate POSIX-only signals and resource module to only run on POSIX Pyth…
| * | Gate POSIX-only signals and resource module to only run on POSIX Python ↵William D. Jones2018-07-061-9/+12
| |/ | | | | | | implementations.
* / Use `realpath` jpathy2018-08-061-1/+1
|/ | | Use `os.path.realpath` instead to make sure symlinks are followed. This is also required to work for nix package manager.
* Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constantsClifford Wolf2018-04-041-0/+3
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* 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
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Bugfix in smtio.py VCD file generatorClifford Wolf2018-03-291-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add $mem support to SMT2 clock taggingClifford Wolf2018-03-271-0/+18
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Improve yosys-smtbmc log output and error handlingClifford Wolf2018-03-171-5/+14
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Improve handling of invalid check-sat result in smtio.pyClifford Wolf2018-03-171-1/+2
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Remove debug prints from yosys-smtbmc VCD writerClifford Wolf2018-03-081-2/+0
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Check results of (check-sat) in yosys-smtbmcClifford Wolf2018-03-071-0/+2
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Imporove yosys-smtbmc error handling, Improve VCD outputClifford Wolf2018-03-052-23/+49
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Improve SMT2 encoding of $reduce_{and,or,bool}Clifford Wolf2018-03-041-1/+9
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix a hangup in yosys-smtbmc error handlingClifford Wolf2018-03-041-3/+5
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Improved error handling in yosys-smtbmcClifford Wolf2018-03-031-1/+3
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Terminate running SMT solver when smtbmc is terminatedClifford Wolf2018-03-031-1/+31
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix smtbmc smtc/aiw parser for wire names containing []Clifford Wolf2018-03-031-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Mangle names with square brackets in VCD files to work around issues in gtkwaveClifford Wolf2018-03-011-2/+8
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Small fixes and improvements in $allconst/$allseq handlingClifford Wolf2018-02-261-12/+18
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add smtbmc support for exist-forall problemsClifford Wolf2018-02-233-87/+334
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add support for mockup clock signals in yosys-smtbmc vcd outputClifford Wolf2018-02-203-6/+111
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix handling of zero-length cell connections in SMT2 back-endClifford Wolf2018-02-081-0/+8
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* 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 ↵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
|
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-30 10:26:00 +0000