yosys/backends/smt2
Jannis Harder 5e82638408 smt2: Fix operation width computation for boolean producing cells
The output width for the boolean value should not influence the
operation width. The previous incorrect width extension would still
produce correct results, but could produce invalid smt2 output for
reduction operators when the output width was larger than the width of
the vector to which the reduction was applied.

This fixes #3654
2023-02-01 12:34:35 +01: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 smt2: Fix operation width computation for boolean producing cells 2023-02-01 12:34:35 +01:00
smtbmc.py smtbmc: Do not assume skipped assertions when loading a witness trace 2022-10-20 13:49:47 +02:00
smtio.py smtbmc: Fix witness handling for k-induction failures 2022-10-18 19:51:36 +02:00
test_cells.sh Various fixes and improvements in "write_smt2 -bv" 2014-12-25 20:28:34 +01:00
witness.py sim: Improvements and fixes for yw cosim 2023-01-11 18:07:16 +01:00
ywio.py Support for BTOR witness to Yosys witness conversion 2023-01-11 18:07:16 +01:00