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
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
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
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
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
Miodrag Milanović
e8ce9442a6
Merge pull request #3452 from ALGCDG/master
...
Add BLIF names command input plane size check
2022-10-10 16:29:27 +02:00
Miodrag Milanović
d68013811f
Merge pull request #3507 from YosysHQ/claire/verificlibopt
...
Fix handling of verific -L options, add implicit "-L work"
2022-10-10 07:50:57 +02:00
Claire Xenia Wolf
090228a6a1
Fix handling of verific -L options, add implicit "-L work"
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-10-10 00:47:42 +02:00
github-actions[bot]
0e13d7e4c7
Bump version
2022-10-08 00:22:25 +00:00
Jannis Harder
ae1a24d0c4
Merge pull request #3503 from jix/abort_on_log_error
...
Add YOSYS_ABORT_ON_LOG_ERROR environment variable for debugging.
2022-10-07 21:30:26 +02:00
Jannis Harder
0113f44faa
Reenable existing equiv_opt tests
2022-10-07 16:04:51 +02:00
Jannis Harder
81906aa627
Fix tests for check in equiv_opt
2022-10-07 16:04:51 +02:00
Claire Xenia Wolf
0516307637
Add "check -assert" to equiv_opt
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-10-07 16:04:51 +02:00
Claire Xenia Wolf
f0478c520d
Re-enable opt_dff_sr equiv_opt checks
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-10-07 16:04:51 +02:00
Claire Xenia Wolf
afa5e6bb53
Exclude primary inputs from quiv_make rewiring
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-10-07 16:04:51 +02:00
Claire Xenia Wolf
381ce66f58
Revert "Merge pull request #641 from tklam/master"
...
This reverts commit 08be796cb8
, reversing
changes made to 38dbb44fa0
.
This fixes #2728 . PR #641 did not actually "fix" #639 .
The actual issue in #639 is not equiv_make, but assumptions in equiv_simple
that are not true for the test case provided in #639 .
2022-10-07 16:04:51 +02:00
Jannis Harder
925f92918a
clk2fflogic: Always correctly handle simultaneously changing signals
...
This is a complete rewrite of the FF replacing code.
The previous implementation tried to implement the negative hold time by
wrapping async control signals individually with pulse stretching. This
did not correctly model the interaction between different simultaneously
changing inputs (e.g. a falling ALOAD together with a changing AD would
load the changed AD instead of the value AD had when ALOAD was high; a
falling CLR could mask a raising SET for one cycle; etc.).
The new approach first has the logic for all updates using only sampled
values followed by the logic for all updates using only current values.
That way, e.g., a falling ALOAD will load the sampled AD value but a
still active ALOAD will load the current AD value.
The new code also has deterministic behavior for the initial state: no
operation is active when that operation would depend on a specific
previous signal value. This also means clk2fflogic will no longer
generate any additional uninitialized FFs.
I also documented the negative hold time behavior in the help message,
copying the relevant part from async2sync's help messages.
2022-10-07 16:04:51 +02:00
Jannis Harder
ac906d15ce
Add YOSYS_ABORT_ON_LOG_ERROR environment variable for debugging.
2022-10-07 15:02:33 +02:00
github-actions[bot]
c4a52b1b02
Bump version
2022-10-06 00:24:43 +00:00
Miodrag Milanovic
a5172df9e9
Next dev cycle
2022-10-05 11:32:11 +02:00
Miodrag Milanovic
f109fa3d4c
Release version 0.22
2022-10-05 11:30:38 +02:00
Miodrag Milanovic
7db26a8e59
Update CHANGELOG
2022-10-05 11:28:48 +02:00
Miodrag Milanović
11203815a8
Merge pull request #3500 from nakengelhardt/mutate_warn_not_enough
...
mutate: warn if less mutations possible than number requested
2022-10-05 11:28:20 +02:00
N. Engelhardt
47e73826e0
mutate: warn if less mutations possible than number requested
2022-10-05 10:59:38 +02:00
Miodrag Milanović
b5d3920bf5
Merge pull request #3499 from YosysHQ/micko/verific_edif
...
Add support for EDIF file reading using Verific
2022-10-05 08:20:03 +02:00
github-actions[bot]
620af8b663
Bump version
2022-10-05 00:26:07 +00:00
Miodrag Milanovic
1a6f10e8ba
Add support for EDIF file reading using Verific
2022-10-04 09:18:44 +02:00
Miodrag Milanović
f5e2c0a498
Merge pull request #3494 from YosysHQ/micko/verific_attributes
...
Handle attributes imported from verific
2022-10-04 08:23:52 +02:00
Archie
d29606532a
Changing error reason string to be based on lut input plane limit constant.
2022-10-02 22:05:51 +02:00
Miodrag Milanovic
43267dec99
support file content redirection for verific frontened
2022-09-28 15:56:46 +02:00
Miodrag Milanovic
b45517f7b7
Add comment for future self
2022-09-28 14:45:39 +02:00
Miodrag Milanovic
f54ac8a6d6
Handle attributes imported from verific
2022-09-28 08:51:26 +02:00
github-actions[bot]
a9795c4fce
Bump version
2022-09-27 00:25:00 +00:00