yosys/backends/smt2
Jannis Harder a52088b6af smtbmc: Improvements for --incremental and .yw fixes
This extends the experimental incremental JSON API to allow arbitrary
smtlib subexpressions, defining smtlib constants and to allow access of
signals by their .yw path.

It also fixes a bug during .yw writing where values would be re-emitted
in later cycles if they have no newer defined value and a potential
crash when using --track-assumes.
2024-05-07 17:57:37 +02:00
..
.gitignore Various fixes and improvements in "write_smt2 -bv" 2014-12-25 20:28:34 +01:00
Makefile.inc smtbmc: Add native json based witness format + smt2 backend support 2022-08-16 13:37:30 +02:00
example.v Added smtbmc.py 2015-10-13 17:17:23 +02:00
example.ys Added smtbmc.py 2015-10-13 17:17:23 +02:00
smt2.cc rename -witness: Bug fix and rename formal cells 2024-03-04 16:53:03 +01:00
smtbmc.py smtbmc: Improvements for --incremental and .yw fixes 2024-05-07 17:57:37 +02:00
smtbmc_incremental.py smtbmc: Improvements for --incremental and .yw fixes 2024-05-07 17:57:37 +02:00
smtio.py smtbmc: Improvements for --incremental and .yw fixes 2024-05-07 17:57:37 +02:00
test_cells.sh tests: use /usr/bin/env for bash. 2023-08-12 11:59:39 +10:00
witness.py yosys-witness: Add aiw2yw --present-only to omit unused signals 2023-12-14 16:45:19 +01:00
ywio.py smtbmc: Add --incremental mode 2023-11-16 13:22:17 +01:00