* 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.
This reverts commit 08be796cb8, reversing
changes made to 38dbb44fa0.
This fixes#2728. PR #641 did not actually "fix" #639.
The actual issue in #639 is not equiv_make, but assumptions in equiv_simple
that are not true for the test case provided in #639.
This is a complete rewrite of the FF replacing code.
The previous implementation tried to implement the negative hold time by
wrapping async control signals individually with pulse stretching. This
did not correctly model the interaction between different simultaneously
changing inputs (e.g. a falling ALOAD together with a changing AD would
load the changed AD instead of the value AD had when ALOAD was high; a
falling CLR could mask a raising SET for one cycle; etc.).
The new approach first has the logic for all updates using only sampled
values followed by the logic for all updates using only current values.
That way, e.g., a falling ALOAD will load the sampled AD value but a
still active ALOAD will load the current AD value.
The new code also has deterministic behavior for the initial state: no
operation is active when that operation would depend on a specific
previous signal value. This also means clk2fflogic will no longer
generate any additional uninitialized FFs.
I also documented the negative hold time behavior in the help message,
copying the relevant part from async2sync's help messages.
In 2fcc1ee72e, the following is apparantly added in order to mark any
number of undefined LUT inputs:
lut_a.append(RTLIL::Const(State::Sx, minlut - input_nodes.size()));
However this can only be done if the number of input nodes is less
than minlut.
This fixes#3317
After speaking with the author of ABC he let me know that ifraig is a very old command, and that &get; &fraig -x; &put is over 100x faster than ifraig with improved PPA results.
After making the change I confirmed that this is in fact a major speed up. On our internal designs in O(millions) of standard cells we saw multi hour reductions in runtime.
Also included is an improvement to the dress command. Using AIG based transformations removes the spec it SATs against. Proving the input blif will make sure that no matter what commands are run the dress command can still do its job. I noticed a regression against some LUT mapping jobs that prompted me to fix this.
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.
Verific generates a lot of FFs with an unused async load and we cannot
always optimize that away before running clk2fflogic, so check for that
special case here.
Find FFs with undefined initialization values for which changing the
initialization does not change the observable behavior and initialize
them. For -ff2anyinit, this reduces the number of generated $anyinit
cells that drive wires with private names.
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.
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 formal backends do not support multiple clocks. This includes
constant clocks. Constant clocks do appear in what isn't a proper
multiclock design, for example when mapping not fully initialized ROMs.
As converting FFs with constant clocks to FFs using the global is doable
even in a single clock flow, make async2sync do this.
POSIX defines $TMPDIR as containing the pathname of the directory where
programs can create temporary files. On most systems, this variable points to
"/tmp". However, on some systems it can point to a different location.
Without respecting this variable, yosys fails to run on such systems.
Signed-off-by: Mohamed A. Bamakhrama <mohamed@alumni.tum.de>
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.
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.
Newer GCCs emit the following warning for opt_dff:
passes/opt/opt_dff.cc:560:17: warning: operation on ‘ff.Yosys::FfData::has_clk’ may be undefined [-Wsequence-point]
560 | ff.has_clk = ff.has_ce = ff.has_clk = false;
| ~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Which is correct: the order of whether the read or write of has_clk
occurs first is undefined since there is no sequence point between them.
This is almost certainly just a typo/copy paste error and objectively
wrong, so just fix it.
Signed-off-by: Austin Seipp <aseipp@pobox.com>
- Attempt to lookup a derived module if it potentially contains a port
connection with elaboration ambiguities
- Mark the cell if module has not yet been derived
- This can be extended to implement automatic hierarchical port
connections in a future change
- FfData now keeps track of the module and underlying cell, if any (so
calling emit on FfData created from a cell will replace the existing cell)
- FfData implementation is split off to its own .cc file for faster
compilation
- the "flip FF data sense by inserting inverters in front and after"
functionality that zinit uses is moved onto FfData class and beefed up
to have dffsr support, to support more use cases
- *_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
Mutating the SigMap by adding a new connection will throw off FfInitVals
index. Work around this by removing the relevant init values from index
whenever we connect nets, then re-add the new init value.
Should fix#2920.
Previously, opt_clean would reconnect all ports (including FF Q ports)
to a "canonical" SigBit chosen by complex rules, but would leave the
init attribute on the old wire. This change applies the same
canonicalization rules to the init attributes, ensuring that init moves
to wherever the Q port moved.
Part of another jab at #2920.
This also aligns the functionality:
- in all cases, the onehot attribute is used to create appropriate
constraints (previously, opt_dff didn't do it at all, and share
created one-hot constraints based on $pmux presence alone, which
is unsound)
- in all cases, shift and mul/div/pow cells are now skipped when
importing the SAT problem (previously only memory_share did this)
— this avoids creating clauses for hard cells that are unlikely
to help with proving the UNSATness needed for optimization
If width of a case expression was large, explicit patterns could cause
the existing logic to take an extremely long time, or exhaust the
maximum size of the underlying set. For cases where all of the patterns
are fully defined and there are no constants in the case expression,
this change uses a simple set to track which patterns have been seen.
This adds one simple piece of functionality to opt_expr: when a cell
port is connected to a fully-constant signal (as determined by sigmap),
the port is reconnected directly to the constant value. This is just
enough optimization to fix the "non-constant $meminit input" problem
without requiring a full opt_clean or a separate pass.
I think the code is now a bit easier to follow (and has lost some
levels of indentation!).
The only non-trivial change is that I removed the check for
cell->type[0] != '$' when deciding whether to complain if we couldn't
find a module. This will always be true because of the early exit
earlier in the function.
Spotted during compilation:
passes/proc/proc_init.cc: In function ‘void {anonymous}::proc_init(Yosys::RTLIL::Module*, Yosys::SigMap&, Yosys::RTLIL::Process*)’:
passes/proc/proc_init.cc:31:7: warning: variable ‘found_init’ set but not used [-Wunused-but-set-variable]
There should be no functional change, but this splits up the control
flow across functions, using class fields to hold the state that's
being tracked. The result should be a bit easier to read.
This is part of work to add bind support, but I'm doing some
refactoring in the hierarchy pass to make the code a bit easier to
work with. The idea is that (eventually) the IFExpander object will
hold all the logic for expanding interfaces, and then other code can
do bind insertion.