aboutsummaryrefslogtreecommitdiffstats
path: root/passes
Commit message (Collapse)AuthorAgeFilesLines
* ABC9: Cell Port Bug Patch (#3670)Benjamin Barzen2023-04-221-1/+5
| | | | | | | | | | | | | | | | | * ABC9: RAMB36E1 Bug Patch * Add simplified testcase * Also fix xaiger writer for under-width output ports * Remove old testcase * Missing top-level input port * Fix tabs --------- Co-authored-by: Eddie Hung <eddie@fpgeh.com>
* stat: pass down quiet argN. Engelhardt2023-02-281-1/+1
|
* Merge pull request #3646 from YosysHQ/lofty/fix-3591Miodrag Milanović2023-02-271-4/+1
|\ | | | | muxcover: do not add decode muxes with x inputs
| * muxcover: do not add decode muxes with x inputsLofty2023-01-261-4/+1
| |
* | Merge pull request #3672 from jix/yw-cosim-hierarchy-fixesJannis Harder2023-02-151-1/+25
|\ \ | | | | | | sim: For yw cosim, drive parent module's signals for input ports
| * | sim: For yw cosim, drive parent module's signals for input portsJannis Harder2023-02-131-1/+25
| | |
* | | Merge pull request #2995 from georgerennie/cover_precondJannis Harder2023-02-141-0/+19
|\ \ \ | | | | | | | | chformal: Add -coverenable option
| * | | chformal: Note about using -coverenable with the Verific frontendJannis Harder2023-02-141-0/+5
| | | |
| * | | chformal: Rename -coverprecond to -coverenableGeorge Rennie2022-06-181-4/+4
| | | |
| * | | chformal: Test -coverprecond and reuse the src attributeJannis Harder2022-06-181-2/+2
| | | |
| * | | chformal: Add -coverprecond optionGeorge Rennie2022-06-181-0/+14
| | | | | | | | | | | | | | | | | | | | This inserts $cover cells to cover the enable signal (precondition) for the selected formal cells.
* | | | Merge pull request #3126 from georgerennie/equiv_make_assertionsJannis Harder2023-02-141-27/+65
|\ \ \ \ | |_|/ / |/| | | equiv_make: Add -make_assert option
| * | | equiv_make: Add -make_assert optionGeorge Rennie2022-06-241-27/+65
| |/ / | | | | | | | | | | | | This adds a -make_assert flag to equiv_make. When used, the pass generates $eqx and $assert cells to encode equivalence instead of $equiv.
* | | Updated changelogMiodrag Milanovic2023-02-081-0/+3
| | |
* | | Merge pull request #3625 from povik/show_cleanupN. Engelhardt2023-02-061-56/+82
|\ \ \
| * | | passes: show: s/pos/bitpos/ for readabilityMartin Povišer2023-01-131-4/+5
| | | | | | | | | | | | | | | | Signed-off-by: Martin Povišer <povik@cutebit.org>
| * | | passes: show: Reuse string parts in generation of portboxesMartin Povišer2023-01-131-2/+5
| | | | | | | | | | | | | | | | Signed-off-by: Martin Povišer <povik@cutebit.org>
| * | | passes: show: Touch chunk iteration in gen_portboxMartin Povišer2023-01-131-8/+11
| | | | | | | | | | | | | | | | Signed-off-by: Martin Povišer <povik@cutebit.org>
| * | | passes: show: Label no_signode flagMartin Povišer2023-01-131-20/+19
| | | | | | | | | | | | | | | | | | | | | | | | Label the flag and rearrange the control flow a bit. Signed-off-by: Martin Povišer <povik@cutebit.org>
| * | | passes: show: Simplify wire bit range logicMartin Povišer2023-01-131-8/+10
| | | | | | | | | | | | | | | | Signed-off-by: Martin Povišer <povik@cutebit.org>
| * | | passes: show: Factor out 'join_label_pieces'Martin Povišer2023-01-131-20/+35
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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>
| * | | passes: show: Label signed_suffix flagMartin Povišer2023-01-131-3/+6
| | | | | | | | | | | | | | | | | | | | | | | | To make it easier to follow what's going on. Signed-off-by: Martin Povišer <povik@cutebit.org>
| * | | passes: show: s/idx/dot_idx/ for readabilityMartin Povišer2023-01-131-7/+7
| | | | | | | | | | | | | | | | Signed-off-by: Martin Povišer <povik@cutebit.org>
| * | | passes: show: Fix portbox bit ranges in case of driven signalsMartin Povišer2023-01-131-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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>
* | | | add option to fsm_detect to ignore self-resettingN. Engelhardt2023-01-301-7/+22
| | | |
* | | | add pmux option to bmuxmap for better fsm detection with verific frontendN. Engelhardt2023-01-301-6/+30
| | | |
* | | | formalff: Fix crash with _NOT_ gates in -hierarchy modeJannis Harder2023-01-251-1/+1
| | | |
* | | | Merge pull request #3624 from jix/sim_ywMiodrag Milanović2023-01-234-40/+680
|\ \ \ \ | | | | | | | | | | Changes to support SBY trace generation with the sim command
| * | | | sim/formalff: Clock handling for yw cosimJannis Harder2023-01-112-21/+246
| | | | |
| * | | | sim: Improvements and fixes for yw cosimJannis Harder2023-01-111-4/+91
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Fixed $cover handling * Improved sparse memory handling when writing traces * JSON summary output
| * | | | sim: New -append option for Yosys witness cosimJannis Harder2023-01-111-5/+14
| | | | | | | | | | | | | | | | | | | | This is needed to support SBY's append option.
| * | | | sim: Add Yosys witness (.yw) cosimulationJannis Harder2023-01-111-3/+194
| | | | |
| * | | | sim: Only check formal cells during gclk simulation updatesJannis Harder2023-01-111-16/+19
| | | | | | | | | | | | | | | | | | | | This is required for compatibility with non-multiclock formal semantics.
| * | | | sim: Internal API to set $initstateJannis Harder2023-01-111-0/+11
| | | | | | | | | | | | | | | | | | | | This is not yet added to any of the simulation drivers.
| * | | | sim: Emit used memory addresses as signals to output tracesJannis Harder2023-01-111-17/+122
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This matches the behavior of smtbmc. This also updates the sim internal memory API to allow masked writes where State::Sa bits (internal don't care - not a valid value for a signal) leave the memory content unchanged.
| * | | | xprop, setundef: Mark xprop decoding bwmuxes, exclude them from setundefJannis Harder2023-01-112-2/+11
| |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | Merge pull request #3629 from YosysHQ/micko/clang_fixesMiodrag Milanović2023-01-234-2/+9
|\ \ \ \ | | | | | | | | | | Fixes for some of clang scan-build detected issues
| * | | | Fixes for some of clang scan-build detected issuesMiodrag Milanovic2023-01-174-2/+9
| |/ / /
* | | | show: Remove left-in debug log_warninggatecat2023-01-231-1/+0
| | | | | | | | | | | | | | | | Signed-off-by: gatecat <gatecat@ds0.me>
* | | | Improve splitcells passClaire Xenia Wolf2023-01-181-52/+120
|/ / / | | | | | | | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* | | Merge pull request #3605 from gadfort/stat-json-areaN. Engelhardt2023-01-111-0/+3
|\ \ \ | |_|/ |/| |
| * | stat: ensure area is included in json outputPeter Gadfort2022-12-291-0/+3
| | | | | | | | | | | | Signed-off-by: Peter Gadfort <peter.gadfort@gmail.com>
* | | Merge branch 'master' into claire/eqystuffClaire Xen2023-01-114-36/+36
|\ \ \
| * \ \ Merge pull request #3537 from jix/xpropJannis Harder2023-01-1110-35/+1508
| |\ \ \ | | | | | | | | | | New xprop pass
| * | | | Deprecate gcc-4.8Miodrag Milanovic2023-01-114-36/+36
| | | | |
* | | | | Merge branch 'master' of github.com:YosysHQ/yosys into claire/eqystuffClaire Xenia Wolf2023-01-115-5/+25
|\| | | |
| * | | | qbfsat support for cvc5, fixes #3608Miodrag Milanovic2023-01-092-3/+7
| | |/ / | |/| |
| * | | formalff: Proper error messages on async inputs for the -clk2ff modeJannis Harder2022-12-091-0/+3
| | | |
| * | | stat: Fix JSON output for empty designsJannis Harder2022-12-021-2/+2
| | | |
| * | | tee: Allow logging command output to a given scratchpad valueJannis Harder2022-12-021-0/+13
| | | |