Rename passes/cmds from "General passes" to "Design modification".
More `yosys.h` includes.
cmdref: Split passes/status from passes/cmds
Rename passes/cmds from "General passes" to "Design modification".
More `yosys.h` includes.
Give formal index a proper title.
Use `Pass::formatted_help()` to assign the group, but still return `false` because the help text still comes from `Pass::help()`.
Tidy up some of the affected files' includes to make use of the shared `yosys.h` includes.
Content is now added to the `ContentListing` rather than the `PrettyHelp`.
`open_*` methods return the `ContentListing` that was added instead of leaving a hanging continuation.
This allows for (e.g.) options to be added directly to optiongroups, instead of requiring that groups be closed before continuation.
This also means that all `PrettyHelp`s are a listing, with the actual log being called by the default `Pass::help()`; making the mode field redundant.
Added `PrettyHelp::log_help()` which replaces the `PrettyHelp::Mode::LOG` logic.
Added `ContentListing::back()` which just returns the last element of the underlying content vector.
Some of the content tracking was made redundant and removed, in particular `PrettyHelp::_current_listing` and `ContentListing::parent`.
Converted `ContentListing` to a class instead of a struct, adjusting constructors to match.
Added `ContentListing` constructor that accepts a `source_location`.
Update `HelpPass::dump_cmds_json()` for new log_help.
Define `PrettyHelp` class with methods for declaring different parts of help message.
Currently able to produce standard help messages as expected.
Updates chformal to use (only) the new help_v2.
Currently makes use of a global static to track the current help context, allowing register.h to live in blissful ignorance and instead rely on help_v2 implementations calling `auto *help = PrettyHelp::get_current();` and `return true;` to minimise impact on rebuilds (i.e. not requiring every source file to be recompiled).
When building `WITH_PYTHON`, where a global list of modules is maintained, deleting a module also erases the entry in said global list. This can lead to memory corruption if the global list is destructed before the module.
Using `on_shutdown()` instead means the module destructor is explicitly called before the global list can be destructed, preventing the issue.
Also add a comment to `Pass::~Pass()` to suggest the same for future passes that might try to use that (and see this commit in the blame if they need a reason why).
Use `Design::selected_modules()` directly, popping at the end instead of copying the selection.
Also default to a complete selection so that boxes work as before.
Simplify to using `RTLIL::SELECT_WHOLE_CMDERR` instead of doing it manually.
Also add tests for importing selections with boxes.
This adds optional in-memory caching of parsed liberty files to speed up
flows that repeatedly parse the same liberty files. To avoid increasing
the memory overhead by default, the caching is disabled by default. The
caching can be controlled globally or on a per path basis using the new
`libcache` command, which also allows purging cached data.
Currently, the area variables in the stat struct are not initialized.
This caused the area stats occasionally being an erroneous value.
Signed-off-by: Hoa Nguyen <hnpl@google.com>
Rename formal cells in addition to witness signals. This is required to
reliably track individual property states for the non-smtbmc flows.
Also removes a misplced `break` which resulted in only partial witness
renaming.
This allows to control the shape of wire nodes, for example, -wireshape plaintext.
The motivation is to allow the user to reduce visual loads of wires.
This does not change the default behavior of using a diamond shape.
Checks to see if a cell is of type ff in the liberty,
and keeps track of an additional area value.
```
Chip area for module '\addr': 92.280720
Sequential area for module '\addr': 38.814720
```
Signed-off-by: Ethan Mahintorabi <ethanmoon@google.com>
This adds support for `$check` cells in chformal and adds a `-lower`
mode which converts `$check` cells into `$assert` etc. cells with a
`$print` cell to output the `$check` message.
* Speed up the autoname pass by 2x. This is accomplished by only constructing IdString objects for plain strings that have a higher score.
* Defer creating IdStrings even further. This increases the speedup to 3x.
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.
This is still missing a mode to rewrite $overwrite_tag and $original_tag
by injecting $set_tag and $get_tag in the right places. It's also
missing bit-precise propagation models for shifts and arithmetic and
requires the design to be flattened.
* Fixes a non-deterministic polarity error for $eqx/$nex cells
* Fixes a deterministic polarity error for $_NOR_ and $_ORNOT_ cells
* Generates hdlnames when xprop is run after flatten
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.
This was renaming cells while iterating over them which would always
cause an assertion failure. Apparently having to rename cells to make
all witness signals public is rarely required, so this slipped through.
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>
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>
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.