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.
This is an alternative to setting the dont_use property in lib. This brings
dfflibmap in parity with the abc pass for dont_use.
Signed-off-by: Austin Rovinski <rovinski@nyu.edu>
See the test case. PROC_ROM will consider this for evaluation, even
though -- without any actions -- lhs is empty (but still "uniform").
A zero-width memory is constructed, which later fails check with:
ERROR: Assert `width != 0' failed in kernel/mem.cc:518.
Ensure we don't proceed if there's nothing to encode.
Fixes a bug in the handling of the recently introduced $check cells.
Both $check and $print cells in clk2fflogic are handled by the same code
and the existing tests for that were only using $print cells. This
missed a bug where the additional A signal of $check cells that is not
present on $print cells was dropped due to a typo, rendering $check
cells non-functional.
Also updates the tests to explicitly cover both cell types such that
they would have detected the now fixed bug.
The purpose of memtest02 in tests/simple/memory.v is to test bit
select on both memory (mem1) and memory converted to registers (mem2).
After 7cfae2c52, mem1 was automatically converted to registers,
and the test no longer worked as intended. This is fixed by
adding (* nomem2reg *) to mem1.
This fixes hierarchy when used with cell libraries that were loaded with
-defer and also makes more of the hierarchy visible to the auto-top
heuristic.
Right now neither `sat` nor `sim` have support for the `$check` cell.
For formal verification it is a good idea to always run either
async2sync or clk2fflogic which will (in a future commit) lower `$check`
to `$assert`, etc.
While `sim` should eventually support `$check` directly, using
`async2sync` is ok for the current tests that use `sim`, so this commit
also runs `async2sync` before running sim on designs containing
assertions.
This compares the write_smt2 output pretty much verbatim, which contains
auto generated private names and fixes an arbitrary ordering. The tested
functionality is also covered by SBY tests which actually interpret the
write_smt2 output using an SMT solver and thus are much more robust, so
we can safely remove this test.
This is mostly useful for collecting coverage for the future `$check`
cell, where, depending on the flavor, formatting a message may not be
wanted even for a failed assertion.
The behavior of these format specifiers is highly specific to Verilog
(`$time` and `$realtime` are only defined relative to `$timescale`)
and may not fit other languages well, if at all. If they choose to use
it, it is now clear what they are opting into.
This commit also simplifies the CXXRTL code generation for these format
specifiers.
Miodrag Milanovic
Martin Povišer
N. Engelhardt
Catherine
Merry
Jannis Harder
Roland Coeurjoly
Austin Rovinski
Amelia Cuss
Dag Lem
Thomas Watson