Commit Graph

12973 Commits

Author SHA1 Message Date
Emil J c75f12a989
Add missing memory width assert preventing division by zero (#3546) 2022-11-09 10:34:25 +01:00
Miodrag Milanovic 6403bfbd9f Update ABC 2022-11-09 08:48:31 +01:00
github-actions[bot] faa1c2e7fe Bump version 2022-11-09 00:20:01 +00:00
Miodrag Milanovic cb7299c3dc Next dev cycle 2022-11-08 07:57:48 +01:00
Miodrag Milanovic 7ce5011c24 Release version 0.23 2022-11-08 07:55:31 +01:00
Miodrag Milanovic 6758b7babc Update manual 2022-11-08 07:54:14 +01:00
github-actions[bot] 2cdbb85da6 Bump version 2022-11-08 00:20:00 +00:00
Jannis Harder 4cb923a4f5
Merge pull request #3544 from jix/cosim-ffinit
sim: Run a comb-only update step to set past values during FST cosim
2022-11-07 16:04:31 +01:00
Jannis Harder 9b4fba3870 sim: Run a comb-only update step to set past values during FST cosim
The previous approach only initialized past_d and past_ad while for FST
cosim we also need to initialize the other past values like past_clk,
etc. Also to properly initialize them, we need to run a combinational
update step in case any of the wires feeding into the FF are private or
otherwise not part of the FST.
2022-11-07 14:09:33 +01:00
Miodrag Milanovic cff42f0af5 Update CHANGELOG 2022-11-07 13:16:38 +01:00
Miodrag Milanović 96df99dafa
Merge pull request #3536 from YosysHQ/claire/vcdend
Add extra time at the end of a sat VCD trace
2022-11-07 13:15:57 +01:00
Miodrag Milanović bc0e69f5c8
Merge pull request #3543 from jix/fstdata-fixes
fstdata: Fixes and improvements
2022-11-07 13:15:42 +01:00
Jannis Harder 68d52cb1b1 fstdata: Update past_data before end_time callback
Required to make the '-at' parameter work.
2022-11-07 12:32:23 +01:00
Jannis Harder 3477f2d00b fstdata: Handle square/angle bracket replacemnt, change memory handling
When writing VCDs smtbmc replaces square brackets with angle brackets to
avoid the issues with VCD readers misinterpreting such signal names.

For memory addresses it also uses angle brackets and hexadecimal
addresses, while other tools will use square brackets and decimal
addresses.

Previously the code handled both forms of memory addresses, assuming
that any signal that looks like a memory address is a memory address.
This is not the case when the user uses regular signals whose names
include square brackets _or_ when the verific frontend generates such
names to represent various constructs.

With this change all angular brackets are turned into square brackets
when reading the trace _and_ when performing a signal lookup. This means
no matter which kind of brackets are used in the design or in the VCD
signals will be matched. This will not handle multiple signals that are
the same apart from replacing square/angle brackets, but this will cause
issues during the VCD writing of smtbmc already.

It still uses the distinction between square and angle brackets for
memories to decide whether the address is hex or decimal, but even if
something looks like a memory and is added to the `memory_to_handle`
data, the plain signal added to `name_to_handle` is used as-is, without
rewriting the address.

This last change is needed to successfully match verific generated
signal names that look like memory addresses while keeping memories
working at the same time. It may cause regressions when VCD generation
was done with a design that had memories but simulation is done with a
design where the memories were mapped to registers. This seems like an
unusual setup, but could be worked around with some further changes
should this be required.
2022-11-07 12:30:08 +01:00
Miodrag Milanovic 9470ef9efe Update CHANGELOG 2022-11-07 12:13:19 +01:00
github-actions[bot] 14aa485176 Bump version 2022-11-05 00:20:11 +00:00
Miodrag Milanovic 310281a96c Separate deprecated compilers on CI 2022-11-04 14:49:12 +01:00
Claire Xenia Wolf a4eb7e41c0 Add extra time at the end of a sat VCD trace
Otherwise the final values will not show up in gtkwave waveforms
when looking at the generated traces.

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-11-01 17:51:46 +01:00
github-actions[bot] d8ea5ef6e2 Bump version 2022-11-01 00:23:48 +00:00
Miodrag Milanović 8d69220be7
Merge pull request #3533 from YosysHQ/micko/liberty
Liberty file support using verific library
2022-10-31 18:04:53 +01:00
Miodrag Milanovic 59b6ac47c9 Add additional help info 2022-10-31 18:04:34 +01:00
Miodrag Milanović 499390e9ce
Merge pull request #3534 from mmicko/win32_plugins
Plugin support for mingw windows builds
2022-10-31 18:01:30 +01:00
Miodrag Milanovic 6fb80bce15 Enable importing blackbox modules only 2022-10-31 10:51:28 +01:00
Miodrag Milanovic e702f2894a Support for reading liberty files using verific 2022-10-31 10:15:05 +01:00
Miodrag Milanovic d1b3a250db Windows plugin build support 2022-10-31 09:10:46 +01:00
github-actions[bot] 5f209f8be5 Bump version 2022-10-31 00:22:50 +00:00
Claire Xenia Wolf fe438ca1ab Add missing log_dump_val_worker forward declarations
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-10-30 18:57:50 +01:00
github-actions[bot] c0ad6b3bc6 Bump version 2022-10-30 00:23:01 +00:00
Zachary Snow 71e7e09092 verilog: Support module-scoped task/function calls
This is primarily intended to enable the standard-permitted use of
module-scoped identifiers to refer to tasks and non-constant functions.
As a side-effect, this also adds support for the non-standard use of
module-scoped identifiers referring to constant functions, a feature
that is supported in some other tools, including Iverilog.
2022-10-29 15:14:11 -04:00
Jannis Harder 31c15e5fa6
Merge pull request #3530 from jix/simlib-mux-fix
simlib: Simplify recently changed $mux model
2022-10-29 14:54:36 +02:00
Jannis Harder aa7e7df19f simlib: Simplify recently changed $mux model
The use of a procedural continuous assignment introduced in #3526 was
unintended and is completely unnecessary for the actual change of that
PR.
2022-10-28 19:48:00 +02:00
Miodrag Milanovic 05218ec900 Add dlfcn library for win32 2022-10-28 16:15:30 +02:00
github-actions[bot] 518194fac1 Bump version 2022-10-25 00:30:03 +00:00
Claire Xen fdce6c5868
Merge pull request #3528 from YosysHQ/claire/crossbits
Add miter -cross option
2022-10-25 01:18:30 +02:00
Claire Xenia Wolf d04c17fd58 Add miter -cross option 2022-10-24 23:23:33 +02:00
Jannis Harder 408fc60c95
Merge pull request #3526 from jix/mux-simlib-eval
Consistent $mux undef handling
2022-10-24 16:25:33 +02:00
Jannis Harder 3a37597e9f
Merge pull request #3518 from jix/smtmap
Add smtmap.v describing the smt2 backend's behavior for undef bits
2022-10-24 16:12:52 +02:00
Jannis Harder 9f76ff0b6a
Merge pull request #3517 from jix/smtbmc-witness-no-assume-skipped
smtbmc: Do not assume skipped assertions when loading a witness trace
2022-10-24 16:06:52 +02:00
Miodrag Milanović 61440a42d1
Merge pull request #3523 from lparkes/basename
Replace GNU specific invocation of basename(1) with the equivalent POSIX one
2022-10-24 12:13:09 +02:00
Jannis Harder c77b7343d0 Consistent $mux undef handling
* Change simlib's $mux cell to use the ternary operator as $_MUX_
  already does
* Stop opt_expr -keepdc from changing S=x to S=0
* Change const eval of $mux and $pmux to match the updated simlib
  (fixes sim)
* The sat behavior of $mux already matches the updated simlib

The verilog frontend uses $mux for the ternary operators and this
changes all interpreations of the $mux cell (that I found) to match the
verilog simulation behavior for the ternary operator. For 'if' and
'case' expressions the frontend may also use $mux but uses $eqx if the
verilog simulation behavior is requested with the '-ifx' option.

For $pmux there is a remaining mismatch between the sat behavior and the
simlib behavior. Resolving this requires more discussion, as the $pmux
cell does not directly correspond to a specific verilog construct.
2022-10-24 12:03:01 +02:00
Miodrag Milanović c0e4d01aa7
Merge pull request #3512 from lparkes/fstapi
Failure to read FST files on *BSD systems
2022-10-24 11:39:06 +02:00
Miodrag Milanovic 7fcc39abe3 Update CodeQL action 2022-10-24 07:39:34 +02:00
Lloyd Parkes 49945ab1c2 Replace GNU specific invocation of basename(1) with the equivalent
POSIX one. The tests now complete on BSD as well as GNU/Linux.
2022-10-23 11:02:18 +13:00
github-actions[bot] 713d42d25d Bump version 2022-10-22 00:26:01 +00:00
Miodrag Milanović 32808b26c6
Merge pull request #3521 from YosysHQ/ci_upgrade
Update versions of CI actions used
2022-10-21 17:24:03 +02:00
Miodrag Milanovic 61dfc26d74 Update versions of CI actions used 2022-10-21 17:00:46 +02:00
github-actions[bot] 4f4cff0080 Bump version 2022-10-21 00:23:12 +00:00
Jannis Harder 0f96ae5990 Add smtmap.v describing the smt2 backend's behavior for undef bits
Some builtin cells have an undefined (x) output even when all inputs are
defined. This is not natively supported by the formal backends which
will produce a fully defined value instead. This can lead to issues when
combining different backends in a formal flow. To work around these,
this adds a file containing verilog implementation of cells matching the
fully defined behavior implemented by the smt2 backend.
2022-10-20 15:48:18 +02:00
Claire Xenia Wolf be1a12595a Add missing log_dump handler for std::vector<>
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-10-20 13:50:25 +02:00
Jannis Harder 96029400cb smtbmc: Do not assume skipped assertions when loading a witness trace
This is not valid when the prefix of a trace already violates
assertions. This can happen when the trace generating solver doesn't
look for a minimal length counterexample.
2022-10-20 13:49:47 +02:00