aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smtbmc.py
Commit message (Expand)AuthorAgeFilesLines
* smtbmc: Add --check-witness modeJannis Harder2022-08-161-1/+22
* smtbmc: Add native json based witness format + smt2 backend supportJannis Harder2022-08-161-108/+292
* smtbmc: fix bmc with no assertionsJannis Harder2022-03-291-0/+2
* Merge pull request #3247 from jix/smtbmc-keepgoingJannis Harder2022-03-281-50/+143
|\
| * 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 sm...Claire Xenia Wolf2022-02-111-1/+4
* yosys-smtbmc: Fix reused loop variable.Marcelina Kościelnicka2021-09-101-4/+4
* Fixing old e-mail addresses and deadnamesClaire Xenia Wolf2021-06-081-1/+1
* 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
* smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, a...Alberto Gonzalez2020-05-251-2/+3
* smtbmc: Fix typo in error message.Alberto Gonzalez2020-05-191-1/+1
* smtbmc: Fix return status handling.Alberto Gonzalez2020-05-141-2/+2
* Merge pull request #1830 from boqwxp/qbfsatN. Engelhardt2020-04-151-3/+15
|\
| * Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole val...Alberto Gonzalez2020-04-041-3/+15
* | Support custom PROGRAM_PREFIXMiodrag Milanovic2020-04-101-2/+1
|/
* Add support for optimizing exists-forall problems.Alberto Gonzalez2020-03-131-0/+14
* Change smtbmc "Warmup failed" status to "PREUNSAT"Clifford Wolf2019-10-031-14/+14
* Fix smtbmc.py handling of zero appended stepsClifford Wolf2019-03-141-5/+5
* Fix typographical and grammatical errors and inconsistencies.whitequark2019-01-021-4/+4
* Add yosys-smtbmc support for btor witnessClifford Wolf2018-12-101-15/+100
* Add "yosys-smtbmc --btorwit" skeletonClifford Wolf2018-12-081-1/+19
* Add proper error message for when smtbmc "append" failsClifford Wolf2018-11-041-2/+10
* Imporove yosys-smtbmc error handling, Improve VCD outputClifford Wolf2018-03-051-3/+6
* Fix smtbmc smtc/aiw parser for wire names containing []Clifford Wolf2018-03-031-1/+1
* Small fixes and improvements in $allconst/$allseq handlingClifford Wolf2018-02-261-12/+18
* Add smtbmc support for exist-forall problemsClifford Wolf2018-02-231-73/+209
* Add support for mockup clock signals in yosys-smtbmc vcd outputClifford Wolf2018-02-201-1/+5
* 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 cons...Clifford Wolf2017-06-071-1/+19
* 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
* Add support for "yosys-smtbmc -c --append"Clifford Wolf2017-02-251-1/+13
* Add "write_smt2 -stbv"Clifford Wolf2017-02-241-4/+4
* Add assert check in "yosys-smtbmc -c"Clifford Wolf2017-02-041-7/+28
* Improve yosys-smtbmc cover() supportClifford Wolf2017-02-041-5/+19
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-25 05:25:35 +0000