The previous implementation for finding the end of a top-level s-expr
exhibited quadratic behavior as it would re-scan the complete input for
the current expression for every new line. For large designs with
trivial properties this could easily take seconds and dominate the
runtime over the actual solving.
This change remembers the current nesting level between lines, avoiding
the re-scanning.
Python 3.12 emits a SyntaxWarning when encountering invalid escape
sequences. They still parse as expected. Marking these raw produces
the same result without the warnings.
This makes clk2fflogic add an attr to $ff cells that carry the state of
the emulated async FF. The $ff output doesn't have any async updates
that happened in the current cycle, but the $ff input does, so the $ff
input corresponds to the async FF's output in the original design.
Hence this patch also makes the following changes to passes besides
clk2fflogic (but only for FFs with the clk2fflogic attr set):
* opt_clean treats the input as a register name (instead of the
output)
* rename -witness ensures that the input has a public name
* the formal backends (smt2, btor, aiger) will use the input's
name for the initial state of the FF in witness files
* when sim reads a yw witness that assigns an initial value to the
input signal, the state update is redirected to the output
This ensures that yosys witness files for clk2fflogic designs have
useful and stable public signal names. It also makes it possible to
simulate a clk2fflogic witness on the original design (with some
limitations when the original design is already using $ff cells).
It might seem like setting the output of a clk2fflogic FF to update the
input's initial value might not work in general, but it works fine for
these reasons:
* Witnesses for FFs are only present in the initial cycle, so we do
not care about any later cycles.
* The logic that clk2fflogic generates loops the output of the
genreated FF back to the input, with muxes in between to apply any
edge or level sensitive updates. So when there are no active updates
in the current gclk cycle, there is a combinational path from the
output back to the input.
* The logic clk2fflogic generates makes sure that an edge sensitive
update cannot be active in the first cycle (i.e. the past initial
value is assumed to be whatever it needs to be to avoid an edge).
* When a level sensitive update is active in the first gclk cycle, it
is actively driving the output for the whole gclk cycle, so ignoring
any witness initialization is the correct behavior.
While not setting the smtoffset here was clearly a bug, I think using
`chunk.offset` only worked incidentally. The `smtoffset` is an offset
into the `smtname, smtid` pair (here `"", idcounter`) which corresponds
to the smt bitvector `stringf("%s#%d", get_id(module), idcounter)` which
contains all the chunks this loop is iterating over.
Thus using an incrementing `smtoffset` (like the `$ff`/`$dff` case above
already does) should be the correct fix.
Wires weren't being assigned an smtoffset value so when generating a yosys witness trace it would also use an offset of 0.
Not sure if this has any other effects, but it fixes the bug I was having.
@jix could you take a look at this?
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
This is not valid when the prefix of a trace already violates
assertions. This can happen when the trace generating solver doesn't
look for a minimal length counterexample.
I have added an optional flag to smtbmc that causes failed temporal induction counterexample traces to be checked for duplicate states and reported to the user, since loops in the counterexample mean that increasing the induction depth won't help prove a design's safety properties.
The witness metadata was missing fine grained FFs completely and for
coarse grained FFs where the output connection has multiple chunks it
lacked the offset of the chunk within the SMT expression. This fixes
both, the later by adding an "smtoffset" field to the metadata.
This adds a native json based witness trace format. By having a common
format that includes everything we support, and providing a conversion
utility (yosys-witness) we no longer need to implement every format for
every tool that deals with witness traces, avoiding a quadratic
opportunity to introduce subtle bugs.
Included:
* smt2: New yosys-smt2-witness info lines containing full hierarchical
paths without lossy escaping.
* yosys-smtbmc --dump-yw trace.yw: Dump results in the new format.
* yosys-smtbmc --yw trace.yw: Read new format as constraints.
* yosys-witness: New tool to convert witness formats.
Currently this can only display traces in a human-readable-only
format and do a passthrough read/write of the new format.
* ywio.py: Small python lib for reading and writing the new format.
Used by yosys-smtbmc and yosys-witness to avoid duplication.
This attribute can be used by formal backends to indicate which clocks
were mapped to the global clock. Update the btor and smt2 backend which
already handle clock inputs to understand this attribute.
This approach had major issues with ROMs whose initialization was not
fully defined. If required, memory_map -rom-only -keepdc should be
called early in a formal flow instead. (This does require a careful
choice of optimization passes though. Sby's scripts will be updated
accordingly.)
Jannis Harder
Charlotte
Krystine Sherwin
Catherine
Emil J
Miodrag Milanovic
Jacob Lifshay