| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs | Jannis Harder | 2022-10-12 | 1 | -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-witness | Jannis Harder | 2022-08-16 | 1 | -2/+14 |
| | | |||||
| * | smtbmc: Add --check-witness mode | Jannis Harder | 2022-08-16 | 1 | -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 support | Jannis Harder | 2022-08-16 | 1 | -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 assertions | Jannis Harder | 2022-03-29 | 1 | -0/+2 |
| | | | | | this was broken by the `--keep-going` changes | ||||
| * | Merge pull request #3247 from jix/smtbmc-keepgoing | Jannis Harder | 2022-03-28 | 1 | -50/+143 |
| |\ | | | | | smtbmc `--keep-going` | ||||
| | * | yosys-smtbmc: Option to keep going after failed assertions in BMC mode | Jannis Harder | 2022-03-24 | 1 | -48/+141 |
| | | | |||||
| | * | yosys-smtbmc: Fix typo in help text, remove trailing whitespace | Jannis Harder | 2022-03-24 | 1 | -2/+2 |
| | | | |||||
| * | | ignore # comment lines | N. Engelhardt | 2022-03-24 | 1 | -1/+1 |
| |/ | |||||
| * | Add a bit of flexibilty re trace length when processing aiger witnesses in ↵ | Claire Xenia Wolf | 2022-02-11 | 1 | -1/+4 |
| | | | | | | | smtbmc.py Signed-off-by: Claire Xenia Wolf <claire@clairexen.net> | ||||
| * | yosys-smtbmc: Fix reused loop variable. | Marcelina Kościelnicka | 2021-09-10 | 1 | -4/+4 |
| | | | | | Fixes #2999. | ||||
| * | Fixing old e-mail addresses and deadnames | Claire Xenia Wolf | 2021-06-08 | 1 | -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 testbench | Jakob Wenzel | 2020-10-06 | 1 | -11/+29 |
| | | |||||
| * | Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc | Claire Wolf | 2020-07-20 | 1 | -2/+2 |
| | | | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com> | ||||
| * | smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, ↵ | Alberto Gonzalez | 2020-05-25 | 1 | -2/+3 |
| | | | | | and CVC4. | ||||
| * | smtbmc: Fix typo in error message. | Alberto Gonzalez | 2020-05-19 | 1 | -1/+1 |
| | | | | | Co-Authored-By: N. Engelhardt <nak@symbioticeda.com> | ||||
| * | smtbmc: Fix return status handling. | Alberto Gonzalez | 2020-05-14 | 1 | -2/+2 |
| | | |||||
| * | Merge pull request #1830 from boqwxp/qbfsat | N. Engelhardt | 2020-04-15 | 1 | -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 Gonzalez | 2020-04-04 | 1 | -3/+15 |
| | | | | | | | | | value recovery using that mode. | ||||
| * | | Support custom PROGRAM_PREFIX | Miodrag Milanovic | 2020-04-10 | 1 | -2/+1 |
| |/ | |||||
| * | Add support for optimizing exists-forall problems. | Alberto Gonzalez | 2020-03-13 | 1 | -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 Wolf | 2019-10-03 | 1 | -14/+14 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Fix smtbmc.py handling of zero appended steps | Clifford Wolf | 2019-03-14 | 1 | -5/+5 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Fix typographical and grammatical errors and inconsistencies. | whitequark | 2019-01-02 | 1 | -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 witness | Clifford Wolf | 2018-12-10 | 1 | -15/+100 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add "yosys-smtbmc --btorwit" skeleton | Clifford Wolf | 2018-12-08 | 1 | -1/+19 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add proper error message for when smtbmc "append" fails | Clifford Wolf | 2018-11-04 | 1 | -2/+10 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Imporove yosys-smtbmc error handling, Improve VCD output | Clifford Wolf | 2018-03-05 | 1 | -3/+6 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Fix smtbmc smtc/aiw parser for wire names containing [] | Clifford Wolf | 2018-03-03 | 1 | -1/+1 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Small fixes and improvements in $allconst/$allseq handling | Clifford Wolf | 2018-02-26 | 1 | -12/+18 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add smtbmc support for exist-forall problems | Clifford Wolf | 2018-02-23 | 1 | -73/+209 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add support for mockup clock signals in yosys-smtbmc vcd output | Clifford Wolf | 2018-02-20 | 1 | -1/+5 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add yosys-smtbmc VCD writer support for memories with async writes | Clifford Wolf | 2017-12-14 | 1 | -4/+8 |
| | | |||||
| * | Fixed "yosys-smtbmc -g" handling of no solution | Clifford Wolf | 2017-11-27 | 1 | -1/+1 |
| | | |||||
| * | Fix a bug in yosys-smtbmc in ROM handling | Clifford Wolf | 2017-10-25 | 1 | -0/+3 |
| | | |||||
| * | Add "yosys-smtbmc --smtc-init --smtc-top --noinit" | Clifford Wolf | 2017-08-04 | 1 | -20/+66 |
| | | |||||
| * | Add verilator support to testbenches generated by yosys-smtbmc | Clifford Wolf | 2017-07-21 | 1 | -3/+15 |
| | | |||||
| * | Generate FSM-style testbenches in smtbmc | Clifford Wolf | 2017-07-12 | 1 | -5/+23 |
| | | |||||
| * | Change s/asserts/assertions/ in yosys-smtbmc log messages | Clifford Wolf | 2017-07-07 | 1 | -2/+2 |
| | | |||||
| * | Add "yosys-smtbmc --presat" | Clifford Wolf | 2017-07-07 | 1 | -3/+23 |
| | | |||||
| * | Remove unneeded delays in smtbmc vlogtb | Clifford Wolf | 2017-07-03 | 1 | -1/+1 |
| | | |||||
| * | Add "yosys-smtbmc --vlogtb-top" | Clifford Wolf | 2017-07-01 | 1 | -15/+32 |
| | | |||||
| * | Fix smtbmc vlogtb bug in $anyseq handling | Clifford Wolf | 2017-07-01 | 1 | -3/+3 |
| | | |||||
| * | Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand ↵ | Clifford Wolf | 2017-06-07 | 1 | -1/+19 |
| | | | | | const reg" | ||||
| * | Use hex addresses in smtbmc vcd mem traces | Clifford Wolf | 2017-02-28 | 1 | -1/+1 |
| | | |||||
| * | Add smtbmc support for memory vcd dumping | Clifford Wolf | 2017-02-26 | 1 | -0/+98 |
| | | |||||
| * | Fix assert checking in "yosys-smtbmc -c --append" | Clifford Wolf | 2017-02-26 | 1 | -1/+1 |
| | | |||||
| * | Improve (and fix for stbv mode) SMT2 memory API | Clifford Wolf | 2017-02-26 | 1 | -19/+24 |
| | | |||||
| * | Add support for "yosys-smtbmc -c --append" | Clifford Wolf | 2017-02-25 | 1 | -1/+13 |
| | | |||||
| * | Add "write_smt2 -stbv" | Clifford Wolf | 2017-02-24 | 1 | -4/+4 |
| | | |||||
 |
index : iCE40/yosys | |
| [no description] |
| aboutsummaryrefslogtreecommitdiffstats |