aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* proc_rom: Add special handling of const-0 address bits.Marcelina Kościelnicka2022-05-182-15/+186
|
* Bump versiongithub-actions[bot]2022-05-181-1/+1
|
* Merge pull request #3310 from robinsonb5-PRs/masterMiodrag Milanović2022-05-171-0/+2
|\ | | | | Now calls Tcl_Init after creating the interp, fixes clock format.
| * Use log_warning when Tcl_Init fails, report error with Tcl_ErrnoMsg.Alastair M. Robinson2022-05-161-1/+1
| |
| * Now calls Tcl_Init after creating the interp, fixes clock format.Alastair M. Robinson2022-05-101-0/+2
| |
* | opt_ffinv: Use ModIndex instead of ModWalker.Marcelina Kościelnicka2022-05-171-50/+53
| | | | | | | | This avoids using out-of-data index information.
* | 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
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-26 02:28:50 +0000