aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2
Commit message (Collapse)AuthorAgeFilesLines
...
* Only allow "sat" and "unsat" smt solver responses in yosys-smtbmcClaire Wolf2020-07-202-4/+4
| | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com>
* Use C++11 final/override keywords.whitequark2020-06-181-2/+2
|
* more reasonable numbers for memoryYehowshua Immanuel2020-06-041-1/+1
|
* MacOS has even stricter stack limits in catalina.Yehowshua Immanuel2020-06-041-1/+1
| | | Invoking sby in macOS Catalina fails because of bizarre stack limits in Catalina.
* Merge pull request #2018 from boqwxp/qbfsat-timeoutclairexen2020-05-302-5/+31
|\ | | | | smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4.
| * smtbmc: Remove superfluous `yosys-smt2-timeout` file macro.Alberto Gonzalez2020-05-291-4/+0
| | | | | | | | Co-Authored-By: clairexen <claire@symbioticeda.com>
| * smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, ↵Alberto Gonzalez2020-05-252-5/+35
| | | | | | | | and CVC4.
* | Merge pull request #1885 from Xiretza/mod-rem-cellsclairexen2020-05-291-0/+10
|\ \ | |/ |/| Fix modulo/remainder semantics
| * Add flooring modulo operatorXiretza2020-05-281-0/+10
| | | | | | | | | | | | | | | | | | | | | | The $div and $mod cells use truncating division semantics (rounding towards 0), as defined by e.g. Verilog. Another rounding mode, flooring (rounding towards negative infinity), can be used in e.g. VHDL. The new $modfloor cell provides this flooring modulo (also known as "remainder" in several languages, but this name is ambiguous). This commit also fixes the handling of $mod in opt_expr, which was previously optimized as if it was $modfloor.
* | qbfsat: Move SMT2 info statements back to the top of the file.Alberto Gonzalez2020-05-251-3/+3
| |
* | qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices ↵Alberto Gonzalez2020-05-251-3/+7
|/ | | | | | the default. Ensures that "BV" is the logic whenever solving an exists-forall problem with Yices, moves the "(set-logic ...)" directive above any non-info line, sets the `ef-max-iters` parameter to a very high number when using Yices in exists-forall mode so as not to prematurely abandon difficult problems, and does not provide the incompatible "--incremental" Yices argument when in exists-forall mode.
* smtbmc: Fix typo in error message.Alberto Gonzalez2020-05-191-1/+1
| | | | Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
* smtbmc: Fix return status handling.Alberto Gonzalez2020-05-141-2/+2
|
* Merge pull request #1830 from boqwxp/qbfsatN. Engelhardt2020-04-151-3/+15
|\ | | | | Add `qbfsat` command to integrate exists-forall solving and specialization
| * Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole ↵Alberto Gonzalez2020-04-041-3/+15
| | | | | | | | value recovery using that mode.
* | Support custom PROGRAM_PREFIXMiodrag Milanovic2020-04-102-9/+8
| |
* | kernel: big fat patch to use more ID::*, otherwise ID(*)Eddie Hung2020-04-021-135/+135
| |
* | kernel: use more ID::*Eddie Hung2020-04-021-37/+37
| |
* | Update `RTLIL::id2cstr()` usage to `log_id`.Alberto Gonzalez2020-04-011-2/+2
|/
* Do not change solver output parsing for non-exists-forall problems.Alberto Gonzalez2020-03-261-2/+6
|
* Skip reading stdout from the solver that if it isn't a line reading only ↵Alberto Gonzalez2020-03-261-1/+3
| | | | "sat", "unsat", or "unknown".
* Revert part of 0fda8308 from #1746 that broke other smtbmc flowsClaire Wolf2020-03-241-3/+1
| | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com>
* 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>
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 03:22:09 +0000