aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Merge pull request #3314 from jix/sva_value_change_logic_wideJannis Harder2022-05-163-9/+72
|\ | | | | verific: Use new value change logic also for $stable of wide signals.
| * verific: Use new value change logic also for $stable of wide signals.Jannis Harder2022-05-113-9/+72
| | | | | | | | I missed this in the previous PR.
* | Bump versiongithub-actions[bot]2022-05-141-1/+1
| |
* | Add opt_ffinv pass.Marcelina Kościelnicka2022-05-134-3/+268
| |
* | Bump versiongithub-actions[bot]2022-05-131-1/+1
| |
* | Add proc_rom pass.Marcelina Kościelnicka2022-05-135-1/+283
|/
* Bump versiongithub-actions[bot]2022-05-101-1/+1
|
* Merge pull request #3305 from jix/sva_value_change_logicJannis Harder2022-05-098-11/+121
|\ | | | | verific: Improve logic generated for SVA value change expressions
| * verific: Improve logic generated for SVA value change expressionsJannis Harder2022-05-098-11/+121
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* | Merge pull request #3297 from jix/sva_nested_clk_elseJannis Harder2022-05-094-5/+27
|\ \ | | | | | | verific: Fix conditions of SVAs with explicit clocks within procedures
| * | verific: Fix conditions of SVAs with explicit clocks within proceduresJannis Harder2022-05-034-5/+27
| | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | Next dev cycleMiodrag Milanovic2022-05-092-2/+5
| | |
* | | Release version 0.17Miodrag Milanovic2022-05-092-3/+3
| | |
* | | Update CHANGELOGMiodrag Milanovic2022-05-091-0/+3
| | |
* | | Update manualMiodrag Milanovic2022-05-091-0/+44
| |/ |/|
* | Merge pull request #3299 from YosysHQ/mmicko/sim_memoryMiodrag Milanović2022-05-094-3/+59
|\ \ | | | | | | sim pass: support for memories
| * | Handle possible non-memory indexed dataMiodrag Milanovic2022-05-061-8/+10
| | |
| * | map memory location to wire value, if memory is converted to FFsMiodrag Milanovic2022-05-041-0/+4
| | |
| * | fix crash when no fst inputMiodrag Milanovic2022-05-041-1/+2
| | |
| * | Start restoring memory state from VCD/FSTMiodrag Milanovic2022-05-043-3/+50
| | |
| * | Add propagated clock signals into btor info fileClaire Xenia Wolf2022-05-041-0/+2
| |/
* | Fix running sva testsMiodrag Milanovic2022-05-091-4/+3
| |
* | Bump versiongithub-actions[bot]2022-05-081-1/+1
| |
* | opt_mem: Remove constant-value bit lanes.Marcelina Kościelnicka2022-05-073-28/+145
| |
* | Bump versiongithub-actions[bot]2022-05-071-1/+1
| |
* | include latest abc changesMiodrag Milanovic2022-05-061-1/+1
| |
* | include latest abc changesMiodrag Milanovic2022-05-061-1/+1
| |
* | Merge pull request #3300 from imhcyx/masterMiodrag Milanović2022-05-061-1/+1
|\ \ | | | | | | memory_share: fix wrong argidx in extra_args
| * | memory_share: fix wrong argidx in extra_argsimhcyx2022-05-051-1/+1
| | |
* | | Include abc change to fix FreeBSD buildMiodrag Milanovic2022-05-061-1/+1
|/ /
* | Bump versiongithub-actions[bot]2022-05-051-1/+1
| |
* | abc: Use dict/pool instead of std::map/std::setMarcelina Kościelnicka2022-05-041-14/+14
|/
* Bump versiongithub-actions[bot]2022-05-031-1/+1
|
* AIM file could have gaps in or between inputs and initsMiodrag Milanovic2022-05-021-3/+6
|
* Bump versiongithub-actions[bot]2022-04-301-1/+1
|
* Merge pull request #3294 from YosysHQ/micko/verific_merge_past_ffMiodrag Milanović2022-04-291-0/+1
|\ | | | | Ignore merging past ffs that we are not properly merging
| * Ignore merging past ffs that we are not properly mergingMiodrag Milanovic2022-04-291-0/+1
|/
* Bump versiongithub-actions[bot]2022-04-261-1/+1
|
* Add missing parameters for ecp5Rick Luiken2022-04-252-1/+2
|
* Merge pull request #3287 from jix/smt2-conditional-storeJannis Harder2022-04-251-2/+4
|\ | | | | smt2: Make write port array stores conditional on nonzero write mask
| * smt2: Make write port array stores conditional on nonzero write maskJannis Harder2022-04-201-2/+4
| |
* | Merge pull request #3257 from jix/tribuf-formalJannis Harder2022-04-251-3/+46
|\ \ | | | | | | tribuf: `-formal` option: convert all to logic and detect conflicts
| * | tribuf: `-formal` option: convert all to logic and detect conflictsJannis Harder2022-04-121-3/+46
| | |
* | | Merge pull request #3290 from mpasternacki/bugfix/freebsd-buildMiodrag Milanović2022-04-251-0/+3
|\ \ \ | | | | | | | | Fix build on FreeBSD, which has no alloca.h
| * | | Fix build on FreeBSD, which has no alloca.hMaciej Pasternacki2022-04-241-0/+3
| | |/ | |/|
* | | Merge pull request #3289 from YosysHQ/micko/sim_improveMiodrag Milanović2022-04-252-29/+74
|\ \ \ | |/ / |/| | Simulation improvements
| * | Match $anyseq input if connected to public wireMiodrag Milanovic2022-04-221-6/+12
| | |
| * | Treat $anyseq as input from FSTMiodrag Milanovic2022-04-221-0/+21
| | |
| * | Ignore change on last edgeMiodrag Milanovic2022-04-221-4/+5
| | |
| * | Last sample from input does not represent changeMiodrag Milanovic2022-04-221-1/+2
| | |
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-22 13:46:24 +0000