| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | 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 |
| | | |||||
| * | Add assert check in "yosys-smtbmc -c" | Clifford Wolf | 2017-02-04 | 1 | -7/+28 |
| | | |||||
| * | Improve yosys-smtbmc cover() support | Clifford Wolf | 2017-02-04 | 1 | -5/+19 |
| | | |||||
| * | Partially implement cover() support in yosys-smtbmc | Clifford Wolf | 2017-02-04 | 1 | -2/+87 |
| | | |||||
| * | Add "yosys-smtbmc --aig <aim_filename>:<aiw_filename>" support | Clifford Wolf | 2017-01-30 | 1 | -5/+14 |
| | | |||||
 |
index : iCE40/yosys | |
| [no description] |
| aboutsummaryrefslogtreecommitdiffstats |