genrtlil.cc and simplify.cc had inconsistent and slightly broken
handling of signedness for array querying functions. These functions are
defined to return a signed result. Simplify always produced an unsigned
and genrtlil always a signed 32-bit result ignoring the context.
Includes tests for the the relvant edge cases for context dependent
conversions.
The previously generated logic assumed an unconstrained past value in
the initial state and did not handle 'x values. While the current formal
verification flow uses 2-valued logic, SVA value change expressions
require a past value of 'x during the initial state to behave in the
expected way (i.e. to consider both an initial 0 and an initial 1 as
$changed and an initial 1 as $rose and an initial 0 as $fell).
This patch now generates logic that at the same time
a) provides the expected behavior in a 2-valued logic setting, not
depending on any dont-care optimizations, and
b) properly handles 'x values in yosys simulation
For SVAs that have an explicit clock and are contained in a procedure
which conditionally executes the assertion, verific expresses this using
a mux with one input connected to constant 1 and the other output
connected to an SVA_AT. The existing code only handled the case where
the first input is connected to 1. This patch also handles the other
case.
The `-keepdc` option prevents merging flipflops with dont-care bits in
their initial value, as, in general, this is not a valid transform for
formal verification.
The keepdc option of `opt` is passed along to `opt_merge` now.
- Prevent unmatched expected error patterns from self-matching
- Prevent infinite recursion on unmatched expected warnings
- Always print the error message for unmatched error patterns
- Add test coverage for all unmatched message types
- Add test coverage for excess matched logs and warnings
Anlogic FPGAs all have two kinds of BRAMs, one is 9bit*1K when being
true dual port (or 18bit*512 when simple dual port), the other is
16bit*2K.
Supports mapping of these two kinds of BRAMs. 9Kbit BRAM in SDP mode and
32Kbit BRAM with 8bit width are not support yet.
Signed-off-by: Icenowy Zheng <icenowy@aosc.io>
The preprocessor currently destroys double slash containing escaped
identifiers (for example \a//b ). This is due to next_token trying to
convert single line comments (//) into /* */ comments. This then leads
to an unintuitive error message like this:
ERROR: syntax error, unexpected '*'
This patch fixes the error by recognizing escaped identifiers and
returning them as single token. It also adds a testcase.