While SBY's aiger flow already removes non-assertion driving logic,
there are some uses of write_aiger outside of SBY that could end up with
$scopeinfo cells, so we explicitly ignore them.
The write_btor backend works differently and due to the way it
recursively visits cells, it would never reach isolated cells like
$scopeinfo.
These were previously not being converted correctly leading to yosys
internal cells being written to my netlist.
Signed-off-by: Ethan Mahintorabi <ethanmoon@google.com>
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.
At the moment the only thing it allows is redirecting `$print` cell
output in a context-dependent manner. In the future, it will allow
customizing handling of `$check` cells (where the default is to abort),
of out-of-range memory accesses, and other runtime conditions with
effects.
This context object also allows a suitably written testbench to add
Verilog-compliant `$time`/`$realtime` handling, albeit it involves
the ceremony of defining a `performer` subclass. Most people will
want something like this to customize `$time`:
int64_t time = 0;
struct : public performer {
int64_t *time_ptr;
int64_t time() const override { return *time_ptr; }
} performer = { &time };
p_top.step(&performer);
This approach to tracking simulation time was a mistake that I did not
catch in review. It has several issues:
1. There is absolutely no requirement to call `step()`, as it is
a convenience function. In particular, `steps` will not be
incremented in submodules if `-noflatten` is used.
2. The semantics of `steps` does not match that of the Verilog `$time`
construct.
3. There is no way to make the semantics of `%t` match that of Verilog.
4. The `module` interface is intentionally very barebones. It is little
more than a container for three method pointers, `reset`, `eval`,
and `commit`. Adding ancillary data to it goes against this.
If similar functionality is introduced again it should probably be
a variable that is global per toplevel design using some object that is
unique for an entire hierarchy of modules, and ideally exposed via
the C API. For now, it is being removed (in this commit) and (in next
commit) the capability is being reintroduced through a context object
that can be specified for `eval()`.
This commit achieves three roughly equally important goals:
1. To bring the rendering code in kernel/fmt.cc and in cxxrtl.h as close
together as possible, with an ideal of only having the bigint library
as the difference between the render functions.
2. To make the treatment of `$time` and `$realtime` in CXXRTL closer to
the Verilog semantics, at least in the formatting code.
3. To change the code generator so that all of the `$print`-to-`string`
conversion code is contained inside of a closure.
There are two reasons to aim for goal (3):
a. Because output redirection through definition of a global ostream
object is neither convenient nor useful for environments where
the output is consumed by other code rather than being printed on
a terminal.
b. Because it may be desirable to, in some cases, ignore the `$print`
cells that are present in the netlist based on a runtime decision.
This is doubly true for an upcoming `$check` cell implementing
assertions, since failing a `$check` would by default cause a crash.
This avoids having to devirtualize them later to get performance back,
and simplifies the code a bit.
The change is prompted by the desire to add a similar observer object
to `eval()`, and a repeated consideration of whether the dispatch on
these should be virtual in first place.
The name `on_commit` was terrible since it would not be called, as one
may conclude from the name, on each `commit()`, but only whenever that
method actually updates a value.
This commit adds a reader/writer implementation for a file format
optimized for fast, single-pass storage and retrieval of design state
changes, as well as a recorder/replayer that integrate with the eval
and commit simulation steps to create replay logs and reproduce them
later.
This feature makes it possible to run a simulation once, recording
the stimulus as well as changes to the registers, and navigate to
a past time point in the simulation later without rerunning it.
Both the changes in inputs (stimulus) and changes in state are saved
so that navigation does not require calling `eval()` or `commit()`;
only a series of memory copy operations.
On a representative example of a SoC netlist, saving the replay log
while simulating it takes 150% of the time it would take to simulate
the same design without logging, which is a much lower overhead than
writing an equivalent full view (including memories) VCD waveform dump.
The replay log is also several times smaller than the VCD dump, and
more space savings are available as low hanging fruit.
Replaying the log has not been optimized and currently takes about
the same time as running the simulation in first place. However, it
is still useful since it provides fast navigation to an arbitrary time
point, something that rerunning the simulation does not allow for.
The current file format should be considered preliminary. It is not
very space-efficient, and my testing shows that a lot of time is spent
in the write() syscall in the kernel. Most likely, compression and/or
writing in another thread could improve performance by 10-20%. This
may be done at a later time.
This change only matters for processes that weren't processed by
`proc_rmdead` for which follow-up cases after a default case are treated
differently in Verilog and RTLIL semantics.
The commit observer is a structure containing a callback that is invoked
whenever the `commit()` method changes a wire or a memory. This allows
code external to the compiled netlist to react to changes in the design
state in a very efficient way. One example of how this feature can be
used is an efficient implementation of record/replay.
Note that the VCD writer does not benefit from this feature because it
must be able to react to changes in any debug items and not just those
that contain design state.
While the VCD format separates the timescale and the timestep (likely
to allow representing the timestep with a small integer type), time in
CXXRTL is represented using a uniform 96-bit number, which allows for
a ±100 year range at femtosecond resolution.
The implementation uses `value<96>`, which provides fast arithmetic and
comparison operations, as well as conversion to/from a more common
representation of integer seconds plus femtoseconds.
Prior to this fix, the `CxxrtlBackend` used the entire path for the include
directive when a separated interface file is generated (via the `-header`
option). This commit updates the code to use the base name of the interface
file.
Since the C++11 standard is used by default, we cannot take advantage of
the `std::filesystem` to get the basename.
In preparation for substantial expansion of CXXRTL's runtime, this commit
reorganizes the files used by the implementation. Only minimal changes are
required in a consumer.
First, change:
-I$(yosys-config --datdir)/include
to:
-I$(yosys-config --datdir)/include/backends/cxxrtl/runtime
Second, change:
#include <backends/cxxrtl/cxxrtl.h>
to:
#include <cxxrtl/cxxrtl.h>
(and do the same for cxxrtl_vcd.h, etc.)
The Verilog grammar does not allow an empty case. Most synthesis tools
are quite permissive about this, but Quartus is not. This causes
problems for amaranth with Quartus (see amaranth-lang/amaranth#931).
We add a new flow graph node type, PRINT_SYNC, as they don't get handled
with regular CELL_EVALs. We could probably move this grouping out of
the dump method.
Removing some signed checks and logic where we've already guaranteed the
values to be positive. Indeed, in these cases, if a negative value got
through (per my realisation in the signed fuzz harness), it would cause
an infinite loop due to flooring division.
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.
This include seems to have been copied over from the JSON backend where
AIG models are sometimes inserted into the JSON output, but these other
backends don't do anything with AIG.
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.
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.)
Jannis Harder
Catherine
Martin Povišer
Ethan Mahintorabi
N. Engelhardt
Merry
Henri Nurmi
Wanda
George Rennie
Miodrag Milanović
Asherah Connor
Charlotte
Charlotte
Clifford Wolf
Claire Xenia Wolf
Krystine Sherwin
Benjamin Barzen
AdamHillier
Aki Van Ness
Emil J
KrystalDelusion
Michael Nolan
Kevin Läufer
Jacob Lifshay
Claire Xenia Wolf
R