riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
12,120 Commits 92 Branches 49 Tags 39 MiB
Commit Graph

12120 Commits

Author SHA1 Message Date
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
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