Commit Graph

3836 Commits

Author SHA1 Message Date
Jannis Harder 1c667fab2b
Merge pull request #3672 from jix/yw-cosim-hierarchy-fixes
sim: For yw cosim, drive parent module's signals for input ports
2023-02-15 13:45:00 +01:00
Jannis Harder ec94703619
Merge pull request #2995 from georgerennie/cover_precond
chformal: Add -coverenable option
2023-02-14 17:46:31 +01:00
Jannis Harder 85f611fb23
Merge pull request #3126 from georgerennie/equiv_make_assertions
equiv_make: Add -make_assert option
2023-02-14 17:15:55 +01:00
Jannis Harder b636af9751 chformal: Note about using -coverenable with the Verific frontend 2023-02-14 17:10:43 +01:00
Jannis Harder 1698202ccc sim: For yw cosim, drive parent module's signals for input ports 2023-02-13 12:26:06 +01:00
Miodrag Milanovic 5f33c0e0b2 Updated changelog 2023-02-08 10:11:47 +01:00
N. Engelhardt 417fadbefd
Merge pull request #3625 from povik/show_cleanup 2023-02-06 16:11:26 +01:00
N. Engelhardt 419f91a2b9 add option to fsm_detect to ignore self-resetting 2023-01-30 16:12:53 +01:00
N. Engelhardt ecfa7e9fbc add pmux option to bmuxmap for better fsm detection with verific frontend 2023-01-30 16:12:53 +01:00
Jannis Harder afac3f2c76 formalff: Fix crash with _NOT_ gates in -hierarchy mode 2023-01-25 12:55:29 +01:00
Miodrag Milanović 8180cc4325
Merge pull request #3624 from jix/sim_yw
Changes to support SBY trace generation with the sim command
2023-01-23 16:55:17 +01:00
Miodrag Milanović 245884a101
Merge pull request #3629 from YosysHQ/micko/clang_fixes
Fixes for some of clang scan-build detected issues
2023-01-23 16:24:22 +01:00
gatecat bfacaddca8 show: Remove left-in debug log_warning
Signed-off-by: gatecat <gatecat@ds0.me>
2023-01-23 13:54:07 +01:00
Claire Xenia Wolf bfc3c20cfb Improve splitcells pass
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2023-01-18 00:31:29 +01:00
Miodrag Milanovic 6574553189 Fixes for some of clang scan-build detected issues 2023-01-17 12:58:08 +01:00
Martin Povišer f9e30ee5e0 passes: show: s/pos/bitpos/ for readability
Signed-off-by: Martin Povišer <povik@cutebit.org>
2023-01-13 19:57:24 +01:00
Martin Povišer 314b864205 passes: show: Reuse string parts in generation of portboxes
Signed-off-by: Martin Povišer <povik@cutebit.org>
2023-01-13 19:57:24 +01:00
Martin Povišer 61abca10a3 passes: show: Touch chunk iteration in gen_portbox
Signed-off-by: Martin Povišer <povik@cutebit.org>
2023-01-13 19:57:24 +01:00
Martin Povišer 60318a5cd8 passes: show: Label no_signode flag
Label the flag and rearrange the control flow a bit.

Signed-off-by: Martin Povišer <povik@cutebit.org>
2023-01-13 19:57:24 +01:00
Martin Povišer 8b1f5fba62 passes: show: Simplify wire bit range logic
Signed-off-by: Martin Povišer <povik@cutebit.org>
2023-01-13 19:57:24 +01:00
Martin Povišer ad149cc42a passes: show: Factor out 'join_label_pieces'
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>
2023-01-13 19:57:24 +01:00
Martin Povišer 5848790835 passes: show: Label signed_suffix flag
To make it easier to follow what's going on.

Signed-off-by: Martin Povišer <povik@cutebit.org>
2023-01-13 19:57:24 +01:00
Martin Povišer 13700e12e5 passes: show: s/idx/dot_idx/ for readability
Signed-off-by: Martin Povišer <povik@cutebit.org>
2023-01-13 19:57:24 +01:00
Martin Povišer e3709ce776 passes: show: Fix portbox bit ranges in case of driven signals
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>
2023-01-13 19:57:24 +01:00
Jannis Harder d6c7aa0e3d sim/formalff: Clock handling for yw cosim 2023-01-11 18:07:16 +01:00
Jannis Harder 7ddec5093f sim: Improvements and fixes for yw cosim
* Fixed $cover handling
  * Improved sparse memory handling when writing traces
  * JSON summary output
2023-01-11 18:07:16 +01:00
Jannis Harder dda972a148 sim: New -append option for Yosys witness cosim
This is needed to support SBY's append option.
2023-01-11 18:07:16 +01:00
Jannis Harder 2dd5652215 sim: Add Yosys witness (.yw) cosimulation 2023-01-11 18:07:16 +01:00
Jannis Harder f6458bab70 sim: Only check formal cells during gclk simulation updates
This is required for compatibility with non-multiclock formal semantics.
2023-01-11 18:07:16 +01:00
Jannis Harder 9c6198a827 sim: Internal API to set $initstate
This is not yet added to any of the simulation drivers.
2023-01-11 18:07:16 +01:00
Jannis Harder 44b26d5c6d sim: Emit used memory addresses as signals to output traces
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.
2023-01-11 18:07:16 +01:00
Jannis Harder 5042600c0d xprop, setundef: Mark xprop decoding bwmuxes, exclude them from setundef
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.
2023-01-11 18:07:16 +01:00
N. Engelhardt 4173daa708
Merge pull request #3605 from gadfort/stat-json-area 2023-01-11 16:41:44 +01:00
Claire Xen 843f329b96
Merge branch 'master' into claire/eqystuff 2023-01-11 16:33:08 +01:00
Jannis Harder 5abaa59080
Merge pull request #3537 from jix/xprop
New xprop pass
2023-01-11 16:26:04 +01:00
Miodrag Milanovic 5801152779 Deprecate gcc-4.8 2023-01-11 09:54:19 +01:00
Claire Xenia Wolf 6d56d4ecfc Merge branch 'master' of github.com:YosysHQ/yosys into claire/eqystuff 2023-01-11 04:10:12 +01:00
Miodrag Milanovic e3c0fd8b10 qbfsat support for cvc5, fixes #3608 2023-01-09 16:14:01 +01:00
Peter Gadfort 58cca9592d stat: ensure area is included in json output
Signed-off-by: Peter Gadfort <peter.gadfort@gmail.com>
2022-12-29 21:51:46 -05:00
Claire Xenia Wolf 029b0aac7f Merge branch 'claire/eqystuff' of github.com:YosysHQ/yosys into claire/eqystuff 2022-12-21 14:50:23 +01:00
Claire Xenia Wolf 1bc832a8e1 Allow non-unique modules without state in sim writeback-mode
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-12-21 10:43:02 +01:00
Claire Xenia Wolf a9072dc23c Small bugfix in uniquify pass
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-12-21 10:41:48 +01:00
Jannis Harder 4a0ed35aab xprop: Improve signal splitting code
Avoid splitting output ports twice when combining -split-outputs with
-split-public and clean up the corresponding code.
2022-12-12 17:51:01 +01:00
Claire Xenia Wolf 6a6e1d8424 Improvements in "viz" pass
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-12-09 18:28:17 +01:00
Jannis Harder 967529abb1 formalff: Proper error messages on async inputs for the -clk2ff mode 2022-12-09 15:25:40 +01:00
Claire Xenia Wolf dc14def5f3 Add gold-x handing to miter cross port handling
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-12-08 22:14:16 +01:00
Claire Xenia Wolf 3454bddbe2 Merge branch 'claire/eqystuff' of github.com:YosysHQ/yosys into claire/eqystuff 2022-12-08 20:06:23 +01:00
Jannis Harder 172a8e79f0 xprop: Add -split-public option 2022-12-08 20:00:01 +01:00
Claire Xenia Wolf 068031d2aa Improvements in "viz" command
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-12-07 16:10:58 +01:00
Claire Xenia Wolf aeba966475 Improvements in "viz" pass
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-12-07 12:46:49 +01:00