The previous commit introduced code that optimizes the activation
patterns to be able to generate smaller activation logic. The resulting
supercell was then enqueued as shareable using those optimized
activation patterns. The condition represented by the optimized patterns
is an over-approximation of the actual activiation condition. This means
using it as activiation for the supercell loses precision and pessimises
sharing of the supercell with further cells, breaking the sat/share
test.
This commit fixes that by using the optimized activiation patterns only
for the generation of activation logic and using the original patterns
for enqueuing the supercell.
In case the two sets of activation patterns are mutually exclusive
without considering the logic feeding into the activation signals, an
activation condition can only be relevant if present in both sets with
opposite polarity.
This detects pattern-only mutual exclusion by running an additional SAT
query before importing the input cone logic. If that is already UNSAT,
we remove all non-relevant condition and re-simplify the remaining
patterns.
In cases of pattern-only mutual exclusion, this will often produce much
smaller selection logic and avoid the more costly SAT query that
includes the input cones.
If all the (non-select) inputs of a `$_MUX{4,8,16}_` are undefined, replace it, just like we do for `$mux` and `$_MUX_`.
Add `tests/opt/opt_expr_mux_undef.ys` to verify this.
This doesn't do any const folding on the wide muxes, or shrinking to less wide muxes. It only handles the case where all inputs are 'x and the mux can be completely removed.
- Techlib pmgens are now in relevant techlibs/*.
- `peepopt` pmgens are now in passes/opt.
- `test_pmgen` is still in passes/pmgen.
- Update `Makefile.inc` and `.gitignore` file(s) to match new `*_pm.h` location,
as well as the `#include`s.
- Change default `%_pm.h` make target to `techlibs/%_pm.h` and move it to the
top level Makefile.
- Update pmgen target to use `$(notdir $*)` (where `$*` is the part of the file
name that matched the '%' in the target) instead of `$(subst _pm.h,,$(notdir
$@))`.
The B port is for single-bit summands. These can just as well be
represented as an additional summand on the A port (which supports
summands of arbitrary width). An upcoming `$macc_v2` cell won't be
special-casing single-bit summands in any way.
In preparation, make the following changes:
* remove the `bit_ports` field from the `Macc` helper (instead add any
single-bit summands to `ports` next to other summands)
* leave `B` empty on cells emitted from `Macc::to_cell`
Each call to `handle_clkpol_celltype_swap` has a conversion of the
cell's type ID to an allocated string. This can sum up to a
non-negligible time being spent in the clkpol code even for a design
which doesn't have any flip-flop gates.
Avoid building a cell-to-inbit map when sorting the cells, add a warning
if we are unable to sort, and move the code treating non-combinational
cells ahead of the rest (this means we don't need to pass
non-combinational cells to the TopoSort object at all).
Processes can contain `MemWriteAction` entries which are invisible to
most passes operating on memories but which will be lowered to write
ports later on by `proc_memwr`. For that reason we can get corrupted
RTLIL if we sequence the memory passes before `proc`. Address that by
making the affected memory passes ignore modules with processes.
The main speedup comes from swithing from using a SHA1 hash to std::hash<std::string>. There is no need to use an expensive cryptographic hash for fingerprinting in this context.
This does not correctly handle an `$overwrite_tag` on a module output,
but since we currently require the user to flatten the design for
cross-module dft, this cannot be observed from within the design, only
by manually inspecting the signals in the design.
Group the reconnections, so that instead of producing
connect $auto$wreduce.cc:455:run$24 [0] 1'0
connect $auto$wreduce.cc:455:run$23 [31] 1'0
connect $auto$wreduce.cc:455:run$23 [30] 1'0
... (40 more lines)
we produce
connect $auto$wreduce.cc:461:run$23 [31:11] 21'000000000000000000000
connect $auto$wreduce.cc:461:run$24 [31:10] 22'0000000000000000000000
.
If the `$ge` cell we are replacing has wide output port, the upper bits
on the port should be driven to zero. That's not what a `$not` cell with
a single-bit input does. Instead opt for a `$logic_not` cell, which does
zero-pad its output.
Fixes#3867.
Distinguish between the A, B input ports of `$_ANDNOT_`, `$_ORNOT_`
gates when considering those for sharing. Unlike the input ports of the
other supported single-bit gates, those are not interchangeable.
Fixes#3848.
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.
* Change simlib's $mux cell to use the ternary operator as $_MUX_
already does
* Stop opt_expr -keepdc from changing S=x to S=0
* Change const eval of $mux and $pmux to match the updated simlib
(fixes sim)
* The sat behavior of $mux already matches the updated simlib
The verilog frontend uses $mux for the ternary operators and this
changes all interpreations of the $mux cell (that I found) to match the
verilog simulation behavior for the ternary operator. For 'if' and
'case' expressions the frontend may also use $mux but uses $eqx if the
verilog simulation behavior is requested with the '-ifx' option.
For $pmux there is a remaining mismatch between the sat behavior and the
simlib behavior. Resolving this requires more discussion, as the $pmux
cell does not directly correspond to a specific verilog construct.
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.
The `-keepdc` option prevents merging flipflops with dont-care bits in
their initial value, as, in general, this is not a valid transform for
formal verification.
The keepdc option of `opt` is passed along to `opt_merge` now.
Akash Levy
George Rennie
Jannis Harder
Martin Povišer
Krystine Sherwin
Anhijkt
Emil J
Emil J
Catherine
Miodrag Milanović
N. Engelhardt
Lofty
Rasmus Munk Larsen
KrystalDelusion
Marcelina Kościelnicka