aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smtio.py
Commit message (Collapse)AuthorAgeFilesLines
* smtbmc: Fix witness handling for k-induction failuresJannis Harder2022-10-181-1/+1
| | | | | The "uninitialized" value is a _list_ of chunks that are part of the initial state for the witness trace.
* smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFsJannis Harder2022-10-121-0/+9
| | | | | | | The witness metadata was missing fine grained FFs completely and for coarse grained FFs where the output connection has multiple chunks it lacked the offset of the chunk within the SMT expression. This fixes both, the later by adding an "smtoffset" field to the metadata.
* smtbmc: Avoid unnecessary string copies when parsing solver outputJannis Harder2022-09-021-12/+9
|
* 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>
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 01:20:30 +0000