| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
|\
| |
| | |
chformal: Add -coverenable option
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
This inserts $cover cells to cover the enable signal (precondition)
for the selected formal cells.
|
|\ \ |
|
| | |
| | |
| | |
| | | |
Signed-off-by: Martin Povišer <povik@cutebit.org>
|
| | |
| | |
| | |
| | | |
Signed-off-by: Martin Povišer <povik@cutebit.org>
|
| | |
| | |
| | |
| | | |
Signed-off-by: Martin Povišer <povik@cutebit.org>
|
| | |
| | |
| | |
| | |
| | |
| | | |
Label the flag and rearrange the control flow a bit.
Signed-off-by: Martin Povišer <povik@cutebit.org>
|
| | |
| | |
| | |
| | | |
Signed-off-by: Martin Povišer <povik@cutebit.org>
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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>
|
| | |
| | |
| | |
| | |
| | |
| | | |
To make it easier to follow what's going on.
Signed-off-by: Martin Povišer <povik@cutebit.org>
|
| | |
| | |
| | |
| | | |
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>
|
|\ \ \
| | | |
| | | | |
Changes to support SBY trace generation with the sim command
|
| |/ /
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
|\ \ \
| | | |
| | | | |
Fixes for some of clang scan-build detected issues
|
| |/ / |
|
| | |
| | |
| | |
| | | |
Signed-off-by: gatecat <gatecat@ds0.me>
|
|/ /
| |
| |
| | |
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
|
|\ \ |
|
| | |
| | |
| | |
| | | |
Signed-off-by: Peter Gadfort <peter.gadfort@gmail.com>
|
|\ \ \ |
|
| |\ \ \
| | | | |
| | | | | |
New xprop pass
|
| | |/ /
| |/| | |
|
|\| | | |
|
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
Avoid splitting output ports twice when combining -split-outputs with
-split-public and clean up the corresponding code.
|
| | | |
| | | |
| | | |
| | | | |
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
|
|\ \ \ \ |
|
| | | | | |
|
|/ / / /
| | | |
| | | |
| | | | |
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
|
| | | |
| | | |
| | | |
| | | | |
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
|
| | | |
| | | |
| | | |
| | | | |
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
|
| | | |
| | | |
| | | |
| | | | |
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
|
| | | |
| | | |
| | | |
| | | | |
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
|
| | | |
| | | |
| | | |
| | | | |
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
|
| |/ /
|/| |
| | |
| | | |
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
|
|/ / |
|
| |
| |
| | |
Rst docs conversion
|
| | |
|
| |
| |
| |
| |
| | |
- refactor resource util. estimation/calculations for Xilinx and CMOS
- don't print log_header if "-json" is set
|
|\ \ |
|
| | | |
|
|/ /
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
| |
| |
| |
| | |
Instead set those unused clocks to zero.
|