aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2
Commit message (Collapse)AuthorAgeFilesLines
...
* fix typo in `write_smt2` helpTeguh Hofstee2020-03-231-1/+1
|
* Merge pull request #1768 from boqwxp/smt2_cleanupN. Engelhardt2020-03-161-5/+5
|\ | | | | Clean up pseudo-private member usage in `backends/smt2/smt2.cc`.
| * Clean up pseudo-private member usage in `backends/smt2/smt2.cc`.Alberto Gonzalez2020-03-131-5/+5
| |
* | Add support for optimizing exists-forall problems.Alberto Gonzalez2020-03-133-1/+33
|/ | | | | | Modifies smt2 backend to recognize `$anyconst` etc. assigned to a wire with the `maximize` or `minimize` attribute and emit `; yosys-smt2-maximize` or `; yosys-smt2-minimize` directives as appropriate. Modifies `backends/smt2/smtbmc.py` and `smtio.py` to recognize those directives and emit a `(maximize ...)` or `(minimize ...)` command at the end of `smt_forall_assert()`, as described in the paper "νZ - An Optimizing SMT Solver" by Nikolaj Bjørner et al. Adds an example `examples/smtbmc/demo9.v` to show how it can be used.
* Improve yosys-smtbmc "solver not found" handlingClaire Wolf2020-01-271-1/+5
| | | | Signed-off-by: Claire Wolf <clifford@clifford.at>
* Bugfix in smtio vcd handling of $-identifiersClifford Wolf2019-10-231-6/+9
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Change smtbmc "Warmup failed" status to "PREUNSAT"Clifford Wolf2019-10-031-14/+14
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* backends: smt2: use $(CXX) variable for compilerSean Cross2019-09-081-1/+1
| | | | | | | | | | | The Makefile assumes the compiler is called `gcc`, which isn't always true. In fact, if we're building on msys2 or msys2-64, the compiler is called `i686-w64-mingw32-g++` or `x86_64-w64-mingw32-g++`. Use the variable instead of hardcoding the name, to fix building on these systems. Signed-off-by: Sean Cross <sean@xobs.io>
* substr() -> compare()Eddie Hung2019-08-071-1/+1
|
* Make liberal use of IdString.in()Eddie Hung2019-08-061-1/+1
|
* Add $_NMUX_, add "abc -g cmos", add proper cmos cell costsClifford Wolf2019-08-061-0/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* 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
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add timescale and generated-by header to yosys-smtbmc MkVcdClifford Wolf2019-06-161-0/+2
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add "whitebox" attribute, add "read_verilog -wb"Clifford Wolf2019-04-181-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix smtbmc.py handling of zero appended stepsClifford Wolf2019-03-141-5/+5
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Install launcher executable when running yosys-smtbmc on Windows.William D. Jones2019-03-131-1/+17
| | | | Signed-off-by: William D. Jones <thor0505@comcast.net>
* Fix signed $shift/$shiftx handling in write_smt2Clifford Wolf2019-03-091-1/+2
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Use SVA label in smt export if availableClifford Wolf2019-03-071-2/+2
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix smt2 code generation for partially initialized memowy words, fixes #831Clifford Wolf2019-02-281-4/+11
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add missing blackslash-to-slash convertion to smtio.py (matching ↵Clifford Wolf2019-02-061-1/+1
| | | | | | Smt2Worker::get_id() behavior) Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix typographical and grammatical errors and inconsistencies.whitequark2019-01-021-4/+4
| | | | | | | | | | | | The initial list of hits was generated with the codespell command below, and each hit was evaluated and fixed manually while taking context into consideration. DIRS="kernel/ frontends/ backends/ passes/ techlibs/" DIRS="${DIRS} libs/ezsat/ libs/subcircuit" codespell $DIRS -S *.o -L upto,iff,thru,synopsys,uint More hits were found by looking through comments and strings manually.
* 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>
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-05 06:21:17 +0000