Commit Graph

11524 Commits

Author SHA1 Message Date
Marcelina Kościelnicka 0a8eaca322 nexus: Use `memory_libmap` pass. 2022-05-18 17:32:56 +02:00
Marcelina Kościelnicka a04b025abf ecp5: Use `memory_libmap` pass. 2022-05-18 17:32:56 +02:00
Marcelina Kościelnicka 7c5dba8b77 Add memory_libmap pass. 2022-05-18 17:32:56 +02:00
Marcelina Kościelnicka 9450f308f0 proc_rom: Add special handling of const-0 address bits. 2022-05-18 17:32:30 +02:00
github-actions[bot] 06ef3f264a Bump version 2022-05-18 00:16:27 +00:00
Miodrag Milanović 7c64c70727
Merge pull request #3310 from robinsonb5-PRs/master
Now calls Tcl_Init after creating the interp, fixes clock format.
2022-05-17 09:33:20 +02:00
Marcelina Kościelnicka 98c7804b89 opt_ffinv: Use ModIndex instead of ModWalker.
This avoids using out-of-data index information.
2022-05-17 02:52:21 +02:00
Alastair M. Robinson 6c6017c973 Use log_warning when Tcl_Init fails, report error with Tcl_ErrnoMsg. 2022-05-16 20:22:28 +01:00
Jannis Harder 2864f2826a
Merge pull request #3314 from jix/sva_value_change_logic_wide
verific: Use new value change logic also for $stable of wide signals.
2022-05-16 16:15:04 +02:00
github-actions[bot] 3f8fb28cd2 Bump version 2022-05-14 00:19:50 +00:00
Marcelina Kościelnicka 2858bb03cd Add opt_ffinv pass. 2022-05-13 23:02:30 +02:00
github-actions[bot] f56a3bd48f Bump version 2022-05-13 00:19:56 +00:00
Marcelina Kościelnicka 990c9b8e11 Add proc_rom pass. 2022-05-13 00:37:14 +02:00
Jannis Harder fada77b8cf verific: Use new value change logic also for $stable of wide signals.
I missed this in the previous PR.
2022-05-11 13:05:27 +02:00
Alastair M. Robinson 83dbea1689 Now calls Tcl_Init after creating the interp, fixes clock format. 2022-05-10 18:48:54 +01:00
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