Commit Graph

573 Commits

Author SHA1 Message Date
Martin Povišer f8325f66b7 opt_expr: Fix 'signed X>=0' replacement for wide output ports
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.
2023-08-01 13:50:12 +01:00
Martin Povišer f0ae046c5a opt_share: Fix input confusion with ANDNOT, ORNOT gates
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.
2023-07-20 20:58:52 +01:00
Jannis Harder e36c71b5b7 Use clk2fflogic attr on cells to track original FF names in witnesses
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.
2023-05-25 12:48:02 +02:00
Miodrag Milanovic 6574553189 Fixes for some of clang scan-build detected issues 2023-01-17 12:58:08 +01:00
Jannis Harder 3ecf85e32c opt_expr: Optimizations for `$bweqx` and `$bwmux` 2022-11-30 18:50:53 +01:00
Jannis Harder 1e67c3a3c2 opt_expr: Fix shift/shiftx optimizations 2022-11-30 18:24:25 +01:00
Jannis Harder fd56d1f79e opt_expr: Constant fold mux, pmux, bmux, demux, eqx, nex cells 2022-11-29 19:06:45 +01:00
Jannis Harder c08242ba41 opt_expr: Optimize bitwise logic ops with one fully const input 2022-11-29 19:06:45 +01:00
Jannis Harder c77b7343d0 Consistent $mux undef handling
* 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.
2022-10-24 12:03:01 +02:00
KrystalDelusion 9465b2af95 Fitting help messages to 80 character width
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.
2022-08-24 10:40:57 +12:00
Jannis Harder 428ad5b9fd wreduce: Keep more x-bits with -keepdc 2022-08-16 13:37:30 +02:00
Jannis Harder c0063288d6 Add the $anyinit cell and the formalff pass
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.
2022-08-16 13:37:30 +02:00
Marcelina Kościelnicka f679b756d8 opt_reduce: Fix use-after-free.
Fixes #3418.
2022-07-23 17:27:26 +02:00
Jannis Harder a47254bd10 opt_dff: With -keepdc, never turn undef init vals into const drivers 2022-06-29 15:42:39 +02:00
Marcelina Kościelnicka 1ff0e1a58a opt_ffinv: Fix use after free. 2022-06-13 14:04:04 +02:00
Marcelina Kościelnicka 47efc04a7d wreduce: Introduce -mux_undef option (aligned with opt_expr). 2022-06-08 21:28:58 +02:00
Marcelina Kościelnicka d07828b409 opt_ffinv: Harden against simple ff/inv loop. 2022-06-07 08:20:06 +02:00
Marcelina Kościelnicka 98c7804b89 opt_ffinv: Use ModIndex instead of ModWalker.
This avoids using out-of-data index information.
2022-05-17 02:52:21 +02:00
Marcelina Kościelnicka 2858bb03cd Add opt_ffinv pass. 2022-05-13 23:02:30 +02:00
Marcelina Kościelnicka 77b1dfd8c3 opt_mem: Remove constant-value bit lanes. 2022-05-07 23:13:16 +02:00
Marcelina Kościelnicka 48eea3efcf opt_dff: Fix behavior on $ff with D == Q. 2022-04-15 22:00:32 +02:00
Jannis Harder ca5b910296 opt_merge: Add `-keepdc` option required for formal verification
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.
2022-04-01 21:03:20 +02:00
Marcelina Kościelnicka 07a657fb0c opt_reduce: Add $bmux and $demux optimization patterns. 2022-01-30 03:37:52 +01:00
Marcelina Kościelnicka db33b1e535 opt_dff: Don't mutate muxes while ModWalker is active. 2022-01-28 08:55:56 +01:00
Austin Seipp b022fe61a7 opt_dff: fix sequence point copy paste bug
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>
2022-01-04 18:18:08 +01:00
Marcelina Kościelnicka 1184a7f3b4 opt_mem_priority: Fix non-ascii char in help message.
This is a fixed version of #3072.
2021-12-09 00:56:14 +01:00
Pepijn de Vos 0c7461fe5e
gowin: widelut support (#3042) 2021-11-06 16:09:30 +01:00
Marcelina Kościelnicka 4e70c30775 FfData: some refactoring.
- 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
2021-10-07 04:24:06 +02:00
Marcelina Kościelnicka e7d89e653c Hook up $aldff support in various passes. 2021-10-02 21:01:21 +02:00
Marcelina Kościelnicka 63b9df8693 kernel/ff: Refactor FfData to enable FFs with async load.
- *_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
2021-10-02 20:19:48 +02:00
Marcelina Kościelnicka 9cbff3a4a9 opt_merge: Remove and reinsert init when connecting nets.
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.
2021-08-22 18:34:11 +02:00
Marcelina Kościelnicka 62d41d4639 opt_clean: Make the init attribute follow the FF's Q.
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.
2021-08-22 15:38:29 +02:00
Marcelina Kościelnicka f791328506 Add opt_mem_widen pass.
If all of us are wide, then none of us are!
2021-08-14 01:06:23 +02:00
Marcelina Kościelnicka 616ace2d92 Add new opt_mem_priority pass. 2021-08-13 11:58:52 +02:00
Marcelina Kościelnicka fd79217763 Add v2 memory cells. 2021-08-11 13:34:10 +02:00
Marcelina Kościelnicka e6f3d1c225 kernel/mem: Introduce transparency masks. 2021-08-11 00:04:16 +02:00
Marcelina Kościelnicka d25b9088c8 Refactor common parts of SAT-using optimizations into a helper.
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
2021-08-09 16:54:35 +02:00
Marcelina Kościelnicka 98003430d6 opt_merge: Use FfInitVals.
Partial #2920 fix.
2021-08-08 01:19:22 +02:00
Marcelina Kościelnicka 54e75129e5 opt_lut: Allow more than one -dlogic per cell type.
Fixes #2061.
2021-07-29 17:30:07 +02:00
Marcelina Kościelnicka 19720b970d memory: Introduce $meminit_v2 cell, with EN input. 2021-07-28 23:18:38 +02:00
Marcelina Kościelnicka 436d42c00c opt_expr: Propagate constants to port connections.
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.
2021-07-27 20:44:26 +02:00
gatecat 6a6d049f1c opt_muxtree: Update port_off and port_idx even for constant bits
Signed-off-by: gatecat <gatecat@ds0.me>
2021-06-11 12:06:35 +01:00
Marcelina Kościelnicka 1667ad658b opt_expr: Fix mul/div/mod by POT patterns to support >= 32 bits.
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).
2021-06-09 19:53:44 +02:00
Marcelina Kościelnicka 12b3a9765d opt_expr: Optimize div/mod by const 1.
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.
2021-06-09 17:42:30 +02:00
Claire Xenia Wolf 72787f52fc Fixing old e-mail addresses and deadnames
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;
2021-06-08 00:39:36 +02:00
Marcelina Kościelnicka 83a218141c kernel/mem: Add sub_addr helpers. 2021-05-26 03:34:02 +02:00
Marcelina Kościelnicka e6b078d156 opt_mem: Add reset/init value support. 2021-05-25 20:06:00 +02:00
Marcelina Kościelnicka 5628f5a88f opt_mem_feedback: Respect write port priority. 2021-05-25 15:59:41 +02:00
Marcelina Kościelnicka 9d5d5a48b1 opt_mem_feedback: Add wide port support. 2021-05-25 02:57:32 +02:00
Marcelina Kościelnicka 835688bf80 opt_mem_feedback: Rewrite feedback path finding logic.
Fixes #2766.
2021-05-24 23:20:30 +02:00