The --track-assumes option makes smtbmc keep track of which assumptions
were used by the solver when reaching an unsat case and to output that
set of assumptions. This is particularly useful to debug PREUNSAT
failures.
The --minimize-assumes option can be used in addition to --track-assumes
which will cause smtbmc to spend additional solving effort to produce a
minimal set of assumptions that are sufficient to cause the unsat
result.
- Use default value of `CXX` instead of forcing override to `clang++`.
- Add base `CXXFLAGS` and `ABCMKARGS` in else condition of `ifeq ($(CONFIG),..)`
block and output the value of `CXX`.
- Change readme to mention `CXX` envvar and that using `make config-clang` etc
will ignore `CXX`.
Note that this functionality is only used by diagnostics emitted by
the C++ testbench; diagnostics emitted by the RTL in `eval()` do not
need to be recorded since they will be emitted again during replay.
This commit is part of a PR that requires corresponding changes in SBY.
To prevent CI failures, detect whether those changes already landed and
skip the SBY using tests until then.
Previously `unroll_stmt` would recurse over the smtlib expressions as
well as recursively follow not-yet-emitted definitions the current
expression depends on. While the depth of smtlib expressions generated
by yosys seems to be reasonably bounded, the dependency chain of
not-yet-emitted definitions can grow linearly with the size of the
design and linearly in the BMC depth.
This makes `unroll_stmt` use a `list` as stack, using python generators
and `recursion_helper` function to keep the overall code structure of
the previous recursive implementation.
Rename formal cells in addition to witness signals. This is required to
reliably track individual property states for the non-smtbmc flows.
Also removes a misplced `break` which resulted in only partial witness
renaming.