aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2
Commit message (Collapse)AuthorAgeFilesLines
* Hook up $aldff support in various passes.Marcelina Kościelnicka2021-10-021-1/+1
|
* yosys-smtbmc: Fix reused loop variable.Marcelina Kościelnicka2021-09-101-4/+4
| | | | Fixes #2999.
* Add support for the Bitwuzla solverGCHQDeveloper5602021-07-121-5/+5
|
* Fixing old e-mail addresses and deadnamesClaire Xenia Wolf2021-06-083-3/+3
| | | | | | | | s/((Claire|Xen|Xenia|Clifford)\s+)+(Wolf|Xen)\s+<(claire|clifford)@(symbioticeda.com|clifford.at|yosyshq.com)>/Claire Xenia Wolf <claire@yosyshq.com>/gi; s/((Nina|Nak|N\.)\s+)+Engelhardt\s+<nak@(symbioticeda.com|yosyshq.com)>/N. Engelhardt <nak@yosyshq.com>/gi; s/((David)\s+)+Shah\s+<(dave|david)@(symbioticeda.com|yosyshq.com|ds0.me)>/David Shah <dave@ds0.me>/gi; s/((Miodrag)\s+)+Milanovic\s+<(miodrag|micko)@(symbioticeda.com|yosyshq.com)>/Miodrag Milanovic <micko@yosyshq.com>/gi; s,https?://www.clifford.at/yosys/,http://yosyshq.net/yosys/,g;
* Make a few passes auto-call Mem::narrow instead of rejecting wide ports.Marcelina Kościelnicka2021-05-281-6/+1
| | | | | | This essentially adds wide port support for free in passes that don't have a usefully better way of handling wide ports than just breaking them up to narrow ports, avoiding "please run memory_narrow" annoyance.
* Reject wide ports in some passes that will never support them.Marcelina Kościelnicka2021-05-251-0/+6
|
* kernel/rtlil: Extract some helpers for checking memory cell types.Marcelina Kościelnicka2021-05-221-2/+2
| | | | | | There will soon be more (versioned) memory cells, so handle passes that only care if a cell is memory-related by a simple helper call instead of a hardcoded list.
* btor, smt2, smv: Add a hint on how to deal with funny FF types.Marcelina Kościelnicka2021-02-251-0/+12
|
* smt2: Use Mem helper.Marcelina Kościelnicka2020-10-211-186/+244
|
* smtbmc: escape identifiers in verilog testbenchJakob Wenzel2020-10-061-11/+29
|
* use the new isPublic() in a few placesN. Engelhardt2020-09-141-2/+2
|
* write_smt2: fix SMT-LIB tutorial URLwhitequark2020-08-291-1/+1
|
* Ensure smt2 comments are associated with accessorsNoah Moroze2020-08-201-9/+20
|
* smtio: Emit `mode: start` options before `set-logic` command and any other ↵Alberto Gonzalez2020-07-201-1/+8
| | | | | | options after it. Refer to the SMT-LIB specification, section 4.1.7. According to the spec, some options can only be specified in `start` mode. Once the solver sees `set-logic`, it moves to `assert` mode.
* smtio: Add support for parsing `yosys-smt2-solver-option` info statements.Alberto Gonzalez2020-07-201-3/+10
|
* smt2: Add `-solver-option` option.Alberto Gonzalez2020-07-201-0/+13
|
* 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
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-26 07:06:15 +0000