aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smtbmc.py
Commit message (Collapse)AuthorAgeFilesLines
* smtbmc: Do not assume skipped assertions when loading a witness traceJannis Harder2022-10-201-3/+0
| | | | | | This is not valid when the prefix of a trace already violates assertions. This can happen when the trace generating solver doesn't look for a minimal length counterexample.
* Temporal induction counterexample loop detection (#3504)Emil J2022-10-191-1/+36
| | | I have added an optional flag to smtbmc that causes failed temporal induction counterexample traces to be checked for duplicate states and reported to the user, since loops in the counterexample mean that increasing the induction depth won't help prove a design's safety properties.
* smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFsJannis Harder2022-10-121-2/+3
| | | | | | | 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: Set step range for --yw and dont skip steps for --check-witnessJannis Harder2022-08-161-2/+14
|
* smtbmc: Add --check-witness modeJannis Harder2022-08-161-1/+22
| | | | | This verifies that the given constraints force an assertion failure. This is useful to debug witness trace conversion (and minimization).
* smtbmc: Add native json based witness format + smt2 backend supportJannis Harder2022-08-161-108/+292
| | | | | | | | | | | | | | | | | | | | 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.
* smtbmc: fix bmc with no assertionsJannis Harder2022-03-291-0/+2
| | | | this was broken by the `--keep-going` changes
* Merge pull request #3247 from jix/smtbmc-keepgoingJannis Harder2022-03-281-50/+143
|\ | | | | smtbmc `--keep-going`
| * yosys-smtbmc: Option to keep going after failed assertions in BMC modeJannis Harder2022-03-241-48/+141
| |
| * yosys-smtbmc: Fix typo in help text, remove trailing whitespaceJannis Harder2022-03-241-2/+2
| |
* | ignore # comment linesN. Engelhardt2022-03-241-1/+1
|/
* Add a bit of flexibilty re trace length when processing aiger witnesses in ↵Claire Xenia Wolf2022-02-111-1/+4
| | | | | | smtbmc.py Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* yosys-smtbmc: Fix reused loop variable.Marcelina Kościelnicka2021-09-101-4/+4
| | | | Fixes #2999.
* 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;
* smtbmc: escape identifiers in verilog testbenchJakob Wenzel2020-10-061-11/+29
|
* Only allow "sat" and "unsat" smt solver responses in yosys-smtbmcClaire Wolf2020-07-201-2/+2
| | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com>
* smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, ↵Alberto Gonzalez2020-05-251-2/+3
| | | | and CVC4.
* 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-101-2/+1
|/
* Add support for optimizing exists-forall problems.Alberto Gonzalez2020-03-131-0/+14
| | | | | | 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.
* Change smtbmc "Warmup failed" status to "PREUNSAT"Clifford Wolf2019-10-031-14/+14
| | | | 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>
* 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>
* Add proper error message for when smtbmc "append" failsClifford Wolf2018-11-041-2/+10
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Imporove yosys-smtbmc error handling, Improve VCD outputClifford Wolf2018-03-051-3/+6
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix smtbmc smtc/aiw parser for wire names containing []Clifford Wolf2018-03-031-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Small fixes and improvements in $allconst/$allseq handlingClifford Wolf2018-02-261-12/+18
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add smtbmc support for exist-forall problemsClifford Wolf2018-02-231-73/+209
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add support for mockup clock signals in yosys-smtbmc vcd outputClifford Wolf2018-02-201-1/+5
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add yosys-smtbmc VCD writer support for memories with async writesClifford Wolf2017-12-141-4/+8
|
* Fixed "yosys-smtbmc -g" handling of no solutionClifford Wolf2017-11-271-1/+1
|
* Fix a bug in yosys-smtbmc in ROM handlingClifford Wolf2017-10-251-0/+3
|
* Add "yosys-smtbmc --smtc-init --smtc-top --noinit"Clifford Wolf2017-08-041-20/+66
|
* Add verilator support to testbenches generated by yosys-smtbmcClifford Wolf2017-07-211-3/+15
|
* Generate FSM-style testbenches in smtbmcClifford Wolf2017-07-121-5/+23
|
* Change s/asserts/assertions/ in yosys-smtbmc log messagesClifford Wolf2017-07-071-2/+2
|
* Add "yosys-smtbmc --presat"Clifford Wolf2017-07-071-3/+23
|
* Remove unneeded delays in smtbmc vlogtbClifford Wolf2017-07-031-1/+1
|
* Add "yosys-smtbmc --vlogtb-top"Clifford Wolf2017-07-011-15/+32
|
* Fix smtbmc vlogtb bug in $anyseq handlingClifford Wolf2017-07-011-3/+3
|
* Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand ↵Clifford Wolf2017-06-071-1/+19
| | | | const reg"
* Use hex addresses in smtbmc vcd mem tracesClifford Wolf2017-02-281-1/+1
|
* Add smtbmc support for memory vcd dumpingClifford Wolf2017-02-261-0/+98
|
* Fix assert checking in "yosys-smtbmc -c --append"Clifford Wolf2017-02-261-1/+1
|
* Improve (and fix for stbv mode) SMT2 memory APIClifford Wolf2017-02-261-19/+24
|
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 09:56:28 +0000