Commit Graph

12100 Commits

Author SHA1 Message Date
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
github-actions[bot] 6781746872 Bump version 2022-10-20 00:25:10 +00:00
Emil J 8859d801c8
Temporal induction counterexample loop detection (#3504)
I have added an optional flag to smtbmc that causes failed temporal induction counterexample traces to be checked for duplicate states and reported to the user, since loops in the counterexample mean that increasing the induction depth won't help prove a design's safety properties.
2022-10-19 12:20:12 +02:00
Jannis Harder f4ede15d68
Merge pull request #3514 from jix/smtbmc-kind-witness-fix
smtbmc: Fix witness handling for k-induction failures
2022-10-19 11:28:12 +02:00
Jannis Harder 8838b1eaa4 smtbmc: Fix witness handling for k-induction failures
The "uninitialized" value is a _list_ of chunks that are part of the
initial state for the witness trace.
2022-10-18 19:51:36 +02:00
Lloyd Parkes 7dcc9c664e And another place we need to lseek() after dup(). 2022-10-16 12:50:49 +13:00
Lloyd Parkes 635aa2a3fc Forcibly set the current seek location of gz files that we are accessing
via dup(fileno());gzdopen() because stdio might have buffered data from
the underlying file meaning that the underlying seek position isn't what
we think it is.
2022-10-16 12:36:00 +13:00
github-actions[bot] d02ae8f2fc Bump version 2022-10-15 00:24:26 +00:00
Miodrag Milanović fc53a0a5c2
Merge pull request #3511 from YosysHQ/improve_edif
verific: enable import all cells
2022-10-14 17:53:56 +02:00
Miodrag Milanovic 48628fbf5a Skip verific primitives and operators import by default 2022-10-14 17:41:24 +02:00
Miodrag Milanovic 922f8b614a Add option to import all cells from all libraries 2022-10-14 16:54:57 +02:00
github-actions[bot] 2e837956dc Bump version 2022-10-13 00:25:23 +00:00
Jannis Harder 33a2773de0
Merge pull request #3510 from jix/ff_witness_fixes
smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs
2022-10-12 20:50:00 +02:00
Jannis Harder 4d334fd3e3 smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs
The witness metadata was missing fine grained FFs completely and for
coarse grained FFs where the output connection has multiple chunks it
lacked the offset of the chunk within the SMT expression. This fixes
both, the later by adding an "smtoffset" field to the metadata.
2022-10-12 19:48:36 +02:00
Aki Van Ness f35c062354 github: issues: added an OS dropdown to the issue template 2022-10-12 09:31:32 -04:00
Jannis Harder fcf742837e
Merge pull request #3502 from jix/equiv_opt_fixes
equiv_opt and clk2fflogic fixes
2022-10-11 12:02:16 +02:00
github-actions[bot] 5c7a1eda92 Bump version 2022-10-11 00:24:29 +00:00
Miodrag Milanović 00bef0b534
Merge pull request #3508 from YosysHQ/aki/rm_protobuf
backends: protobuf: removed protobuf backend
2022-10-10 18:08:51 +02:00
Aki Van Ness 7a73133c9f
backends: protobuf: removed protobuf backend 2022-10-10 10:41:11 -04:00
Miodrag Milanovic 03df1ac72b fix whitespace 2022-10-10 16:31:29 +02:00