Can now append a user defined number of steps to input traces when joining.
If the number of steps is +ve, inputs are all set to 0.
If -ve then steps are skipped.
If all of steps are skipped (including init step) then the input trace will not be copied.
If more than one input trace is provided, the append option will need to be provided the same number of times as there are input traces.
Intended for use with SCY to combine sequential cover traces.
Arbitrary number of inputs, will load all and attempt to join them. Each trace will be replayed one after the other, in the same order as the files are provided.
Mismatch in init_only fields seems to work fine, with values in subsequent traces being assigned in the initial only if they weren't previously defined.
Uncertain if a mismatch in non init_only fields will cause problems.
Fixes WitnessSig.__eq__().
Adds helper functions to WitnessValues and ReadWitness classes.
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?
This should fix#3648 where when calling `emit_elaborated_extmodules` it
checks to see if a module is a black-box, however there was no
validation that the cell type was actually known, and it just always
assumed that we would get a valid instance, causing a segfault.
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.
Uses the regex below to search (using vscode):
^\t\tlog\("(.{10,}(?<!\\n)|.{81,}\\n)"\);
Finds any log messages double indented (which help messages are)
and checks if *either* there are is no newline character at the end,
*or* the number of characters before the newline is more than 80.
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.)
Before this commit, values, wires, and memories with an initializer
were value-initialized in emitted C++ code. After this commit, all
values, wires, and memories are default-initialized, and the default
constructor of generated modules calls the reset() method, which
assigns the members that have an initializer.
Before this commit, zero width sigspecs were dumped as "" (empty
string). Unfortunately, 1364-2005 5.2.3.3 indicates that an empty
string is equivalent to "\0", and is 8 bits wide, so that's wrong.
After this commit, a replication operation with a count of zero is
used instead, which is explicitly permitted per 1364-2005 5.1.14,
and is defined to have size zero. (Its operand has to have a non-zero
size for it to be legal, though.)
PR #1203 has addressed this issue before, but in an incomplete way.
- *_en is split into *_ce (clock enable) and *_aload (async load aka
latch gate enable), so both can be present at once
- has_d is removed
- has_gclk is added (to have a clear marker for $ff)
- d_is_const and val_d leftovers are removed
- async2sync, clk2fflogic, opt_dff are updated to operate correctly on
FFs with async load
backends/protobuf/protobuf.cc depends on the source and header files
generated by protoc, but this dependency wasn't explicitly declared. Add
a rule to the Makefile to fix intermittent build failures when the
protobuf header/source file isn't built before protobuf.cc.
This mode will be used whenever read port cannot be handled in the
"extract address register" way, ie. whenever it has enable, reset,
init functionality or (in the future) mixed transparency mask.
The following VCD file crashes GTKWave's VCD loader:
$var wire 1 ! x:1 $end
$enddefinitions $end
In practice, a colon can be a part of a variable name that is
translated from a Verilog function, something like:
update$func$.../hdl/hazard3_csr.v:350$2534.$result
Public wires may alias buffered internal wires, so keep BUFFERED
wires in debug information even if they are private. Debug items are
only created for public wires, so this does not otherwise affect how
debug information is emitted.
Fixes#2540.
Fixes#2841.
While this helper is already useful to squash sequential initializations
into one in cxxrtl, its main purpose is to squash overlapping masked memory
initializations (when they land) and avoid having to deal with them in
cxxrtl runtime.
This essentially adds wide port support for free in passes that don't
have a usefully better way of handling wide ports than just breaking
them up to narrow ports, avoiding "please run memory_narrow" annoyance.
Jannis Harder
Krystine Sherwin
Benjamin Barzen
AdamHillier
Catherine
Aki Van Ness
Miodrag Milanović
Emil J
KrystalDelusion
Michael Nolan
Kevin Läufer
Jacob Lifshay
Claire Xenia Wolf
N. Engelhardt
Claire Xenia Wolf
R
Marcelina Kościelnicka
Lofty
the6p4c
GCHQDeveloper560