github-actions[bot]
c862b1dbfb
Bump version
2022-05-10 00:16:26 +00:00
Jannis Harder
587e09d551
Merge pull request #3305 from jix/sva_value_change_logic
...
verific: Improve logic generated for SVA value change expressions
2022-05-09 16:40:34 +02:00
Jannis Harder
5ca2ee0c31
Merge pull request #3297 from jix/sva_nested_clk_else
...
verific: Fix conditions of SVAs with explicit clocks within procedures
2022-05-09 16:07:39 +02:00
Jannis Harder
a855d62b42
verific: Improve logic generated for SVA value change expressions
...
The previously generated logic assumed an unconstrained past value in
the initial state and did not handle 'x values. While the current formal
verification flow uses 2-valued logic, SVA value change expressions
require a past value of 'x during the initial state to behave in the
expected way (i.e. to consider both an initial 0 and an initial 1 as
$changed and an initial 1 as $rose and an initial 0 as $fell).
This patch now generates logic that at the same time
a) provides the expected behavior in a 2-valued logic setting, not
depending on any dont-care optimizations, and
b) properly handles 'x values in yosys simulation
2022-05-09 15:04:01 +02:00
Miodrag Milanovic
d562bfd165
Next dev cycle
2022-05-09 10:12:32 +02:00
Miodrag Milanovic
6f9602b4cf
Release version 0.17
2022-05-09 10:11:04 +02:00
Miodrag Milanovic
72d2efeb32
Update CHANGELOG
2022-05-09 10:06:15 +02:00
Miodrag Milanovic
65f70b9d50
Update manual
2022-05-09 09:53:01 +02:00
Miodrag Milanović
58b23954e8
Merge pull request #3299 from YosysHQ/mmicko/sim_memory
...
sim pass: support for memories
2022-05-09 09:28:09 +02:00
Miodrag Milanovic
600079e281
Fix running sva tests
2022-05-09 09:01:57 +02:00
github-actions[bot]
9c69e9f8a6
Bump version
2022-05-08 00:16:45 +00:00
Marcelina Kościelnicka
77b1dfd8c3
opt_mem: Remove constant-value bit lanes.
2022-05-07 23:13:16 +02:00
github-actions[bot]
048170d376
Bump version
2022-05-07 00:15:38 +00:00
Miodrag Milanovic
37b6614718
include latest abc changes
2022-05-06 15:52:24 +02:00
Miodrag Milanovic
7fcf976f9e
include latest abc changes
2022-05-06 15:42:39 +02:00
Miodrag Milanović
384d2120ee
Merge pull request #3300 from imhcyx/master
...
memory_share: fix wrong argidx in extra_args
2022-05-06 09:17:59 +02:00
Miodrag Milanovic
52d8ddee0c
Include abc change to fix FreeBSD build
2022-05-06 08:08:06 +02:00
Miodrag Milanovic
d8adbff72f
Handle possible non-memory indexed data
2022-05-06 08:05:23 +02:00
imhcyx
71166eeecf
memory_share: fix wrong argidx in extra_args
2022-05-05 16:58:39 +08:00
github-actions[bot]
a8cc0c3930
Bump version
2022-05-05 00:15:34 +00:00
Marcelina Kościelnicka
18a48b1337
abc: Use dict/pool instead of std::map/std::set
2022-05-04 22:04:50 +02:00
Miodrag Milanovic
8b3657454b
map memory location to wire value, if memory is converted to FFs
2022-05-04 13:08:16 +02:00
Miodrag Milanovic
8e02b3ca30
fix crash when no fst input
2022-05-04 11:21:39 +02:00
Miodrag Milanovic
ad48639cdd
Start restoring memory state from VCD/FST
2022-05-04 10:41:04 +02:00
Claire Xenia Wolf
3fb32540ea
Add propagated clock signals into btor info file
2022-05-04 08:10:18 +02:00
Jannis Harder
96f64f4788
verific: Fix conditions of SVAs with explicit clocks within procedures
...
For SVAs that have an explicit clock and are contained in a procedure
which conditionally executes the assertion, verific expresses this using
a mux with one input connected to constant 1 and the other output
connected to an SVA_AT. The existing code only handled the case where
the first input is connected to 1. This patch also handles the other
case.
2022-05-03 14:13:08 +02:00
github-actions[bot]
11e75bc27c
Bump version
2022-05-03 00:16:24 +00:00
Miodrag Milanovic
3730db4b98
AIM file could have gaps in or between inputs and inits
2022-05-02 11:18:30 +02:00
github-actions[bot]
c785cb7fe3
Bump version
2022-04-30 00:18:55 +00:00
Miodrag Milanović
7bdf7365e7
Merge pull request #3294 from YosysHQ/micko/verific_merge_past_ff
...
Ignore merging past ffs that we are not properly merging
2022-04-29 14:35:46 +02:00
Miodrag Milanovic
422db937d4
Ignore merging past ffs that we are not properly merging
2022-04-29 14:35:02 +02:00
github-actions[bot]
b30d90a14a
Bump version
2022-04-26 00:18:47 +00:00
Rick Luiken
414dc25a96
Add missing parameters for ecp5
2022-04-25 15:31:41 +01:00
Jannis Harder
6ae0b51c76
Merge pull request #3287 from jix/smt2-conditional-store
...
smt2: Make write port array stores conditional on nonzero write mask
2022-04-25 16:23:21 +02:00
Jannis Harder
e0e31bfc5c
Merge pull request #3257 from jix/tribuf-formal
...
tribuf: `-formal` option: convert all to logic and detect conflicts
2022-04-25 16:23:06 +02:00
Miodrag Milanović
3c0f3504c6
Merge pull request #3290 from mpasternacki/bugfix/freebsd-build
...
Fix build on FreeBSD, which has no alloca.h
2022-04-25 10:16:50 +02:00
Miodrag Milanović
a511c27eb7
Merge pull request #3289 from YosysHQ/micko/sim_improve
...
Simulation improvements
2022-04-25 10:16:25 +02:00
Maciej Pasternacki
0302e97ebc
Fix build on FreeBSD, which has no alloca.h
2022-04-24 19:35:50 +02:00
Miodrag Milanovic
bbfdea2f8a
Match $anyseq input if connected to public wire
2022-04-22 17:20:17 +02:00
Miodrag Milanovic
4d80bc24c7
Treat $anyseq as input from FST
2022-04-22 16:23:39 +02:00
Miodrag Milanovic
9c7deabf94
Ignore change on last edge
2022-04-22 15:24:02 +02:00
Miodrag Milanovic
33f4009bb5
Last sample from input does not represent change
2022-04-22 13:46:11 +02:00
Miodrag Milanovic
83cad82b29
latches are always set to zero
2022-04-22 12:04:05 +02:00
Miodrag Milanovic
c989adcc2d
If not multiclock, output only on clock edges
2022-04-22 12:03:39 +02:00
Miodrag Milanovic
75032a565d
Set init state for all wires from FST and set past
2022-04-22 11:57:39 +02:00
Miodrag Milanovic
8fa2f3b260
Fix multiclock for btor2 witness
2022-04-22 11:53:41 +02:00
Jannis Harder
c7ef0f2932
smt2: Make write port array stores conditional on nonzero write mask
2022-04-20 17:49:48 +02:00
github-actions[bot]
29c0a59589
Bump version
2022-04-19 00:14:02 +00:00
Miodrag Milanović
c3a3f68b4d
Merge pull request #3280 from YosysHQ/micko/fix_readaiw
...
Fix reading aiw from other solvers
2022-04-18 09:49:21 +02:00
Miodrag Milanovic
2610b04033
Update abc
2022-04-18 09:27:00 +02:00
