| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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>
|
| |
|
|\
| |
| | |
muxcover: do not add decode muxes with x inputs
|
| | |
|
|\ \
| | |
| | | |
sim: For yw cosim, drive parent module's signals for input ports
|
| | | |
|
|\ \ \
| | | |
| | | | |
chformal: Add -coverenable option
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
This inserts $cover cells to cover the enable signal (precondition)
for the selected formal cells.
|
|\ \ \ \
| |_|/ /
|/| | | |
equiv_make: Add -make_assert option
|
| |/ /
| | |
| | |
| | |
| | | |
This adds a -make_assert flag to equiv_make. When used, the pass generates
$eqx and $assert cells to encode equivalence instead of $equiv.
|
| | | |
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | | |
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
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
* Fixed $cover handling
* Improved sparse memory handling when writing traces
* JSON summary output
|
| | | | |
| | | | |
| | | | |
| | | | | |
This is needed to support SBY's append option.
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
This is required for compatibility with non-multiclock formal semantics.
|
| | | | |
| | | | |
| | | | |
| | | | | |
This is not yet added to any of the simulation drivers.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| |/ / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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
|
| | | | | |
|
|\| | | | |
|
| | |/ /
| |/| | |
|
| | | | |
|
| | | | |
|
| | | | |
|