aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smtio.py
Commit message (Collapse)AuthorAgeFilesLines
* smtbmc: Add native json based witness format + smt2 backend supportJannis Harder2022-08-161-1/+62
| | | | | | | | | | | | | | | | | | | | This adds a native json based witness trace format. By having a common format that includes everything we support, and providing a conversion utility (yosys-witness) we no longer need to implement every format for every tool that deals with witness traces, avoiding a quadratic opportunity to introduce subtle bugs. Included: * smt2: New yosys-smt2-witness info lines containing full hierarchical paths without lossy escaping. * yosys-smtbmc --dump-yw trace.yw: Dump results in the new format. * yosys-smtbmc --yw trace.yw: Read new format as constraints. * yosys-witness: New tool to convert witness formats. Currently this can only display traces in a human-readable-only format and do a passthrough read/write of the new format. * ywio.py: Small python lib for reading and writing the new format. Used by yosys-smtbmc and yosys-witness to avoid duplication.
* Switched to utf-8 in smtio.pyMiodrag Milanovic2022-08-091-2/+2
|
* smtbmc: noincr: keep solver running for post check-sat unrollingJannis Harder2022-06-081-2/+7
|
* Merge pull request #3357 from jix/smtbmc-cvc5Jannis Harder2022-06-081-3/+13
|\ | | | | smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5
| * smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5Jannis Harder2022-06-031-3/+13
| |
* | smtbmc: Force nonincremental mode when yices is used with forallJannis Harder2022-06-031-1/+4
|/
* smtbmc: Avoid unnecessary deep copies during unrollingJannis Harder2022-03-281-6/+6
|
* print cell name for properties in yosys-smtbmcN. Engelhardt2022-02-221-2/+8
|
* Add support for the Bitwuzla solverGCHQDeveloper5602021-07-121-5/+5
|
* Fixing old e-mail addresses and deadnamesClaire Xenia Wolf2021-06-081-1/+1
| | | | | | | | 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;
* 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
|
* Only allow "sat" and "unsat" smt solver responses in yosys-smtbmcClaire Wolf2020-07-201-2/+2
| | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com>
* 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.
* 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-251-3/+32
| | | | and CVC4.
* 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.
* 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>
* Add support for optimizing exists-forall problems.Alberto Gonzalez2020-03-131-1/+11
| | | | | | 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>
* 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 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>
* 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
|
* Gate POSIX-only signals and resource module to only run on POSIX Python ↵William D. Jones2018-07-061-9/+12
| | | | implementations.
* 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>
* 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>
* 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-051-20/+43
| | | | 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>
* 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>
* Add smtbmc support for exist-forall problemsClifford Wolf2018-02-231-4/+53
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add support for mockup clock signals in yosys-smtbmc vcd outputClifford Wolf2018-02-201-2/+49
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-15 12:39:13 +0000