The `has_srst`` case was checking `sig_ce` instead of `sig_srst` due to
a copy and paste error.
This would crash when `has_ce` was false and could incorrectly determine
that an initial value is unused when `has_ce` and `has_srst` are both
set.
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.
This allows tools like SBY to capture the $display output independent
from anything else sim might log. Additionally it provides source and
hierarchy locations for everything printed.
`memory_nordff` has the advantage that it can be called just ahead of
the simulation step no matter whether the clocked read port has been
inferred or was explicitly instantiated in a flow.
This adds the -noinitstate option which is required to simulate
counterexamples to induction with yw-cosim. Also add handling for
$initstate cells for non-co-simulation.
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.
When assigning values to input ports of nested modules in cosimulation,
sim needs to find the actual driver of the signal to perform the
assignment. The existing code didn't handle unconnected inputs in that
scenario.
Writeback of simulation state into initial state was only working for `run()` and `run_cosim_fst()`.
This change moves the writeback into the `write_output_files()` function so that all simulation modes work with the writeback option.
This matches the behavior of smtbmc.
This also updates the sim internal memory API to allow masked writes
where State::Sa bits (internal don't care - not a valid value for a
signal) leave the memory content unchanged.
Emil J. Tywoniak
Emily Schmidt
Miodrag Milanovic
Martin Povišer
Jannis Harder
N. Engelhardt
uis
Dag Lem
Claire Xen
Rasmus Munk Larsen
gatecat
Krystine Sherwin