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

12913 Commits

Author SHA1 Message Date
github-actions[bot] 42721b6a12 Bump version 2022-07-01 00:19:06 +00:00
Jannis Harder 5db542742b async2sync: turn FFs with const clks into gclk FFs with feedback 
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.
 2022-06-30 12:09:04 +02:00
Miodrag Milanovic b80976b543 Update to new verific extensions inteface 2022-06-30 11:19:01 +02:00
github-actions[bot] 9d63a90e0e Bump version 2022-06-30 00:17:25 +00:00
Jannis Harder 0d2377c8a6
Merge pull request #3394 from jix/memory_map_rom_keepdc 
memory_map: -keepdc option for formal
 2022-06-29 20:02:12 +02:00
Jannis Harder 930bcf0e75 smt2, btor: Revert calling memory_map -rom-only 
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.)
 2022-06-29 18:28:34 +02:00
Jannis Harder a47254bd10 opt_dff: With -keepdc, never turn undef init vals into const drivers 2022-06-29 15:42:39 +02:00
Jannis Harder a6b440b5c9 memory_map: avoid undriven unused FF inputs for -keepdc 2022-06-28 19:05:35 +02:00
github-actions[bot] 869e6a1b6d Bump version 2022-06-28 00:19:25 +00:00
Jannis Harder d78d807a7f memory_map: -keepdc option for formal 
Use it when invoking memory_map -rom-only from write_{smt2,btor}.
 2022-06-27 15:47:55 +02:00
gatecat 48efc9b75c gatemate: Add test for LUT tree mapping 
Signed-off-by: gatecat <gatecat@ds0.me>
 2022-06-27 10:09:48 +01:00
gatecat 38a24ec5cc gatemate: Add LUT tree library script 
Co-authored-by: Claire Xenia Wolf <claire@clairexen.net>
Signed-off-by: gatecat <gatecat@ds0.me>
 2022-06-27 10:09:48 +01:00
gatecat 7c756c9959 gatemate: Add preliminary sim models for LUT tree structures 
Signed-off-by: gatecat <gatecat@ds0.me>
 2022-06-27 10:09:48 +01:00
George Rennie fbf5d89587 equiv_make: Add -make_assert option 
This adds a -make_assert flag to equiv_make. When used, the pass generates
$eqx and $assert cells to encode equivalence instead of $equiv.
 2022-06-24 00:17:02 +01:00
rockybulwinkle ec2f8796bd
Update tcl doc, yosys does not return data to tcl 
This pull request is to address YosysHQ/yosys#2980.

The documentation, as originally written, does not make it clear that yosys commands, when used within a tcl script, do not return any value to the tcl script.

This pull request notes this and offers a workaround via tee as noted in the issue.
 2022-06-23 13:34:08 -05:00
Jacob Lifshay c16c028831 add hierarchy -smtcheck 
like -simcheck, but allow smtlib2_module modules.
 2022-06-22 20:53:10 -07:00
github-actions[bot] b2408df313 Bump version 2022-06-22 00:19:30 +00:00
Archie f69c2c802c Adding expected error message. 2022-06-22 00:34:49 +01:00
Archie c8cd4f468a Adding testcase for issue 3374 2022-06-22 00:34:49 +01:00
Archie 7eeb656e2a Add check for BLIF with no model name 2022-06-22 00:34:49 +01:00
Miodrag Milanovic 1fdbb42fdd Revert "use new verific extensions library" 
This reverts commit 607e957657.
 2022-06-21 18:07:47 +02:00
Jannis Harder a30b38910c
Merge pull request #3387 from ekiwi/btor-pos-cell 
btor: add support for $pos cell
 2022-06-21 10:30:10 +02:00
github-actions[bot] 0b486c56e8 Bump version 2022-06-21 00:16:10 +00:00
Kevin Läufer de5c4bf523 btor: add support for $pos cell 2022-06-20 16:40:46 -07:00
Archie e7e8e3b0f6 Adding expected error message. 2022-06-20 21:50:26 +01:00
Lofty 34804f3fb6 codeowners: adopt ABC9 and update intel_alm username 2022-06-20 15:02:50 +01:00
George Rennie 5dfad5101d chformal: Rename -coverprecond to -coverenable 2022-06-18 18:28:12 +01:00
Jannis Harder e39c422734 chformal: Test -coverprecond and reuse the src attribute 2022-06-18 18:19:26 +01:00
George Rennie c659bd1878 chformal: Add -coverprecond option 
This inserts $cover cells to cover the enable signal (precondition)
for the selected formal cells.
 2022-06-18 18:19:26 +01:00
github-actions[bot] 90147f5fbf Bump version 2022-06-18 00:17:32 +00:00
Archie 4542d51791 Adding testcase for issue 3374 2022-06-17 20:07:02 +01:00
Jannis Harder e6a5d84149
Merge pull request #3383 from jix/write_formal_map_roms 
smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction
 2022-06-17 19:08:14 +02:00
Jannis Harder 4adef63cd4 smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction 
This avoids provability regressions now that we infer more ROMs.

This fixes #3378
 2022-06-17 17:23:13 +02:00
Marcelina Kościelnicka ab3a9325c3 memory_map: Add -rom-only option. 2022-06-17 16:56:11 +02:00
Miodrag Milanović c23139fd98
Merge pull request #3382 from YosysHQ/micko/verific_extensions 
use new verific extensions library
 2022-06-17 16:20:31 +02:00
Miodrag Milanovic 607e957657 use new verific extensions library 2022-06-17 16:04:22 +02:00
Marcelina Kościelnicka 01daa077a2 memory_map: Use const drivers instead of FFs for ROMs. 2022-06-17 15:17:14 +02:00
github-actions[bot] bb634d39ef Bump version 2022-06-17 00:17:38 +00:00
Marcelina Kościelnicka d69091806a memory_libmap: Fix wrprio handling. 2022-06-17 02:09:37 +02:00
Marcelina Kościelnicka 25a4cd7020 memory_libmap: Fix params emitted for unused ports for consistency. 2022-06-16 08:14:08 +02:00
Archie b604c97b33 Add check for BLIF with no model name 2022-06-14 14:17:00 +01:00
github-actions[bot] 3046a06490 Bump version 2022-06-14 00:18:42 +00:00
Marcelina Kościelnicka 6b7efe12b7 Add a check for packed memory MEMID uniqueness 2022-06-13 19:23:55 +02:00
N. Engelhardt 3eaa9e38e0
Merge pull request #3196 from bfg86/bfg86/rename 
Add -suffix option to rename -wire
 2022-06-13 16:00:04 +02:00
Marcelina Kościelnicka 1ff0e1a58a opt_ffinv: Fix use after free. 2022-06-13 14:04:04 +02:00
Miodrag Milanovic ddc8044655 removed deprecated features code 2022-06-13 10:50:24 +02:00
bfg86 aedd3b7999 Updating help-text with nakengelhardts suggestion. 2022-06-13 09:35:10 +02:00
github-actions[bot] b15a46c2c0 Bump version 2022-06-11 00:17:13 +00:00
Jannis Harder 53b205c41d
Merge pull request #3368 from jix/smtbmc-unroll-noincr-traces-fix 
smtbmc: noincr: keep solver running for post check-sat unrolling
 2022-06-10 15:25:57 +02:00
Miodrag Milanovic 4b423dcfb4 Next dev cycle 2022-06-10 15:05:09 +02:00