| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
|
|
|
| |
Fixes #3418.
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
This avoids using out-of-data index information.
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
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>
|
|
|
|
| |
This is a fixed version of #3072.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- 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.
|
|
|
|
| |
If all of us are wide, then none of us are!
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
Partial #2920 fix.
|
|
|
|
| |
Fixes #2061.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
Signed-off-by: gatecat <gatecat@ds0.me>
|
|
|
|
|
| |
The previous code, in addition to being needlessly limitted to 32 bits
in the first place, also had UB for the 31th bit (doing 1 << 31).
|
|
|
|
|
|
|
|
| |
Turns out the code for div by a power of 2 is already almost capable of
optimizing this to a shift-by-0 or and-with-0, which will be further
folded into nothingness; let's beef it up to handle div by 1 as well.
Fixes #2820.
|
|
|
|
|
|
|
|
| |
s/((Claire|Xen|Xenia|Clifford)\s+)+(Wolf|Xen)\s+<(claire|clifford)@(symbioticeda.com|clifford.at|yosyshq.com)>/Claire Xenia Wolf <claire@yosyshq.com>/gi;
s/((Nina|Nak|N\.)\s+)+Engelhardt\s+<nak@(symbioticeda.com|yosyshq.com)>/N. Engelhardt <nak@yosyshq.com>/gi;
s/((David)\s+)+Shah\s+<(dave|david)@(symbioticeda.com|yosyshq.com|ds0.me)>/David Shah <dave@ds0.me>/gi;
s/((Miodrag)\s+)+Milanovic\s+<(miodrag|micko)@(symbioticeda.com|yosyshq.com)>/Miodrag Milanovic <micko@yosyshq.com>/gi;
s,https?://www.clifford.at/yosys/,http://yosyshq.net/yosys/,g;
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
Fixes #2766.
|
| |
|
|
|
|
|
| |
memory_share is actually three passes in a trenchcoat. Split off the
one that has the least in common with the other two as a separate pass.
|
|
|
|
| |
Fixes #2765.
|