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.
This was renaming cells while iterating over them which would always
cause an assertion failure. Apparently having to rename cells to make
all witness signals public is rarely required, so this slipped through.
In two places, we are joining label pieces by a '|' separator. We go
about it by putting the separator behind each entry, then removing the
trailing separator in a final fixup pass on the built string. For easier
reading, replace those occurrences by a new factored-out
'join_label_pieces' function.
Signed-off-by: Martin Povišer <povik@cutebit.org>
When the 'show' pass generates portboxes to detail the connection of
cell ports to wires, it has special handling of signal chunk
repetitions, but those repetitions are not accounted for in the
displayed bit range in case of cell outputs. Fix that, and so bring it
into consistence with the behavior on cell inputs.
So, taking for example the following Verilog snippet,
module DRIVER (Q);
output [7:0] Q;
assign Q = 8'b10101010;
endmodule
module main;
wire w;
DRIVER driver(.Q({8{w}}));
endmodule
make the show pass display '7:0 - 8x 0:0' in the driver-to-w portbox
instead of '7:7 - 8x 0:0' which it displayed formerly.
Signed-off-by: Martin Povišer <povik@cutebit.org>
This adds the xprop_decoder attribute to bwmuxes that drive the original
unencoded signals. Setundef is changed to ignore the x inputs of these
bwmuxes, so that they survive the prep script of SBY's formal flow. This
is required to make simulation (via sim) using the prep model show the
decoded x signals instead of 0/1 values made up by the solver.
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.
These can be used to protect undefined flip-flop initialization values
from optimizations that are not sound for formal verification and can
help mapping all solver-provided values in witness traces for flows that
use different backends simultaneously.
Both of these options consider a selection containing only empty modules
as non-empty. This wasn't mentioned in the documentation nor did the
error message when using `select -assert-none` list those empty modules,
which produced a very confusing error message complaining about a
non-empty selection followed by an empty listing of the selection.
This fixes the documentation and changes the `-assert-none` and
`-assert-any` assertion error messages to also output fully selected
modules (this includes selected empty modules).
It doesn't change the messages for `-assert-count` etc. as they don't
count modules.
There will soon be more (versioned) memory cells, so handle passes that
only care if a cell is memory-related by a simple helper call instead of
a hardcoded list.
Bugpoint's current documentation does specify that the result of a run is stored as the current design,
however it's easy to skim over what that means in practice.
Add a documentation comment to explain specifically that an after bugpoint `write_xyz` pass is required to save
the reduced design.
The only difference between "RTLIL" and "ILANG" is that the latter is
the text representation of the former, as opposed to the in-memory
graph representation. This distinction serves no purpose but confuses
people: it is not obvious that the ILANG backend writes RTLIL graphs.
Passes `write_ilang` and `read_ilang` are provided as aliases to
`write_rtlil` and `read_rtlil` for compatibility.
Rather than assigning specific weights to specific versions of taint tracking logic and summing the weights of all GLIFT cells, sum the following values for each GLIFT cell:
- 0 if the associated hole/$anyconst cell value is non-zero, i.e. reduced-precision taint tracking logic is chosen at this cell
- 1 if the associated hole/$anyconst cell value is zero, i.e. the full-precision taint tracking logic is chosen at this cell
This simplified cost modeling reduces the potential for the QBF-SAT solver to minimize taint tracking logic area but significantly simplifies the QBF-SAT problem.
The new types include:
- FFs with async reset and enable (`$adffe`, `$_DFFE_[NP][NP][01][NP]_`)
- FFs with sync reset (`$sdff`, `$_SDFF_[NP][NP][01]_`)
- FFs with sync reset and enable, reset priority (`$sdffs`, `$_SDFFE_[NP][NP][01][NP]_`)
- FFs with sync reset and enable, enable priority (`$sdffce`, `$_SDFFCE_[NP][NP][01][NP]_`)
- FFs with async reset, set, and enable (`$dffsre`, `$_DFFSRE_[NP][NP][NP][NP]_`)
- latches with reset or set (`$adlatch`, `$_DLATCH_[NP][NP][01]_`)
The new FF types are not actually used anywhere yet (this is left
for future commits).
The $div and $mod cells use truncating division semantics (rounding
towards 0), as defined by e.g. Verilog. Another rounding mode, flooring
(rounding towards negative infinity), can be used in e.g. VHDL. The
new $divfloor cell provides this flooring division.
This commit also fixes the handling of $div in opt_expr, which was
previously optimized as if it was $divfloor.
The $div and $mod cells use truncating division semantics (rounding
towards 0), as defined by e.g. Verilog. Another rounding mode, flooring
(rounding towards negative infinity), can be used in e.g. VHDL. The
new $modfloor cell provides this flooring modulo (also known as "remainder"
in several languages, but this name is ambiguous).
This commit also fixes the handling of $mod in opt_expr, which was
previously optimized as if it was $modfloor.
Before this patch, the code passed around std::string objects by
value. It's probably not a hot-spot, but it can't hurt to avoid the
copying.
Removing the copy and clean-up code means the resulting code is ~6.1kb
smaller when compiled with GCC 9.3 and standard settings.
- Pass a string argument by reference
- Avoid multiple calls to IdString::str and IdString::c_str
- Avoid combining checks for size > 0 and first char (C strings are
null terminated, so foo[0] != '\0' implies that foo has positive
length)
With GCC 9.3, at least, compiling select.cc spits out a warning about
an implausible bound being passed to strncmp. This comes from inlining
IdString::compare(): it turns out that passing std::string::npos as a
bound to strncmp triggers it.
This patch replaces the compare call with a memcmp with the same
effect. The repeated calls to IdString::c_str are slightly
inefficient, but I'll address that in a follow-up commit.
This includes the following significant changes:
* Patching ezsat and minisat to disable resource limiting code
on WASM/WASI, since the POSIX functions they use are unavailable.
* Adding a new definition, YOSYS_DISABLE_SPAWN, present if platform
does not support spawning subprocesses (i.e. Emscripten or WASI).
This definition hides the definition of `run_command()`.
* Adding a new Makefile flag, DISABLE_SPAWN, present in the same
condition. This flag disables all passes that require spawning
subprocesses for their function.
Jannis Harder
Miodrag Milanović
Aki Van Ness
N. Engelhardt
gatecat
Claire Xenia Wolf
Martin Povišer
Peter Gadfort
KrystalDelusion
Kamyar Mohajerani
KrystalDelusion
Aki Van Ness
Lofty
George Rennie
bfg86
Marcelina Kościelnicka
Catherine
Zachary Snow
Iris Johnson
umarcor
N. Engelhardt
Alberto Gonzalez
clairexen
Eddie Hung
Xiretza
Rupert Swarbrick
Claire Wolf