aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Merge pull request #3398 from jix/mention_smtlib2_moduleMiodrag Milanović2022-07-042-3/+16
|\ | | | | Mention smtlib2_module in README.md and CHANGELOG
| * Mention smtlib2_module in README.md and CHANGELOGJannis Harder2022-07-042-3/+16
|/
* Upadte documentation and changelogMiodrag Milanovic2022-07-043-46/+46
|
* Bump versiongithub-actions[bot]2022-07-021-1/+1
|
* Merge pull request #3395 from jix/opt_dff_keepdc_initivalJannis Harder2022-07-011-5/+17
|\ | | | | opt_dff: With -keepdc, never turn undef init vals into const drivers
| * opt_dff: With -keepdc, never turn undef init vals into const driversJannis Harder2022-06-291-5/+17
| |
* | Merge pull request #3396 from jix/async2sync_const_clocksJannis Harder2022-07-011-0/+3
|\ \ | | | | | | async2sync: turn FFs with const clks into gclk FFs with feedback
| * | async2sync: turn FFs with const clks into gclk FFs with feedbackJannis Harder2022-06-301-0/+3
| | | | | | | | | | | | | | | | | | | | | | | | The formal backends do not support multiple clocks. This includes constant clocks. Constant clocks do appear in what isn't a proper multiclock design, for example when mapping not fully initialized ROMs. As converting FFs with constant clocks to FFs using the global is doable even in a single clock flow, make async2sync do this.
* | | Update abcMiodrag Milanovic2022-07-011-1/+1
| | |
* | | Merge pull request #3391 from programmerjake/simcheck-allow-smtlib2-blackboxesJannis Harder2022-07-012-7/+19
|\ \ \ | | | | | | | | add hierarchy -smtcheck
| * | | add hierarchy -smtcheckJacob Lifshay2022-06-222-7/+19
| | | | | | | | | | | | | | | | like -simcheck, but allow smtlib2_module modules.
* | | | Bump versiongithub-actions[bot]2022-07-011-1/+1
| |/ / |/| |
* | | Update to new verific extensions intefaceMiodrag Milanovic2022-06-301-3/+29
| | |
* | | Bump versiongithub-actions[bot]2022-06-301-1/+1
| | |
* | | Merge pull request #3394 from jix/memory_map_rom_keepdcJannis Harder2022-06-293-5/+17
|\ \ \ | |_|/ |/| | memory_map: -keepdc option for formal
| * | smt2, btor: Revert calling memory_map -rom-onlyJannis Harder2022-06-292-2/+0
| | | | | | | | | | | | | | | | | | | | | | | | This approach had major issues with ROMs whose initialization was not fully defined. If required, memory_map -rom-only -keepdc should be called early in a formal flow instead. (This does require a careful choice of optimization passes though. Sby's scripts will be updated accordingly.)
| * | memory_map: avoid undriven unused FF inputs for -keepdcJannis Harder2022-06-281-0/+3
| | |
| * | memory_map: -keepdc option for formalJannis Harder2022-06-273-5/+16
| | | | | | | | | | | | Use it when invoking memory_map -rom-only from write_{smt2,btor}.
* | | Bump versiongithub-actions[bot]2022-06-281-1/+1
|/ /
* | gatemate: Add test for LUT tree mappinggatecat2022-06-273-0/+813
| | | | | | | | Signed-off-by: gatecat <gatecat@ds0.me>
* | gatemate: Add LUT tree library scriptgatecat2022-06-276-6/+591
| | | | | | | | | | Co-authored-by: Claire Xenia Wolf <claire@clairexen.net> Signed-off-by: gatecat <gatecat@ds0.me>
* | gatemate: Add preliminary sim models for LUT tree structuresgatecat2022-06-271-0/+44
|/ | | | Signed-off-by: gatecat <gatecat@ds0.me>
* Bump versiongithub-actions[bot]2022-06-221-1/+1
|
* Adding expected error message.Archie2022-06-221-0/+1
|
* Adding testcase for issue 3374Archie2022-06-221-0/+3
|
* Add check for BLIF with no model nameArchie2022-06-221-1/+4
|
* Revert "use new verific extensions library"Miodrag Milanovic2022-06-211-70/+54
| | | | This reverts commit 607e957657fc56625de5c28ea9cd43c859017d96.
* Merge pull request #3387 from ekiwi/btor-pos-cellJannis Harder2022-06-211-8/+11
|\ | | | | btor: add support for $pos cell
| * btor: add support for $pos cellKevin Läufer2022-06-201-8/+11
| |
* | Bump versiongithub-actions[bot]2022-06-211-1/+1
|/
* codeowners: adopt ABC9 and update intel_alm usernameLofty2022-06-201-2/+2
|
* Bump versiongithub-actions[bot]2022-06-181-1/+1
|
* Merge pull request #3383 from jix/write_formal_map_romsJannis Harder2022-06-172-0/+2
|\ | | | | smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction
| * smt2, btor: Use memory_map -rom-only to make ROMs usable for k-inductionJannis Harder2022-06-172-0/+2
|/ | | | | | This avoids provability regressions now that we infer more ROMs. This fixes #3378
* memory_map: Add -rom-only option.Marcelina Kościelnicka2022-06-171-4/+18
|
* Merge pull request #3382 from YosysHQ/micko/verific_extensionsMiodrag Milanović2022-06-171-54/+70
|\ | | | | use new verific extensions library
| * use new verific extensions libraryMiodrag Milanovic2022-06-171-54/+70
|/
* memory_map: Use const drivers instead of FFs for ROMs.Marcelina Kościelnicka2022-06-171-52/+59
|
* Bump versiongithub-actions[bot]2022-06-171-1/+1
|
* memory_libmap: Fix wrprio handling.Marcelina Kościelnicka2022-06-171-1/+1
|
* memory_libmap: Fix params emitted for unused ports for consistency.Marcelina Kościelnicka2022-06-161-2/+3
|
* Bump versiongithub-actions[bot]2022-06-141-1/+1
|
* Add a check for packed memory MEMID uniquenessMarcelina Kościelnicka2022-06-131-0/+10
|
* Merge pull request #3196 from bfg86/bfg86/renameN. Engelhardt2022-06-131-4/+13
|\ | | | | Add -suffix option to rename -wire
| * Updating help-text with nakengelhardts suggestion.bfg862022-06-131-2/+2
| |
| * Add -suffix option to rename -wire.bfg862022-02-111-4/+13
| | | | | | | | See #3195
* | opt_ffinv: Fix use after free.Marcelina Kościelnicka2022-06-131-3/+6
| |
* | removed deprecated features codeMiodrag Milanovic2022-06-131-235/+0
| |
* | Bump versiongithub-actions[bot]2022-06-111-1/+1
| |
* | Merge pull request #3368 from jix/smtbmc-unroll-noincr-traces-fixJannis Harder2022-06-101-2/+7
|\ \ | | | | | | smtbmc: noincr: keep solver running for post check-sat unrolling
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-09 19:53:08 +0000