mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-27 01:39:23 +00:00
Code Activity
12575 commits 122 branches 59 tags 72 MiB
Commit graph

12575 commits

This branch
This branch
All branches
Author SHA1 Message Date
Miodrag Milanovic
0ca0932b52 Update abc and build as C++ 2022-07-04 16:52:28 +02:00
Miodrag Milanovic
da0682b99a Next dev cycle 2022-07-04 14:08:53 +02:00
Miodrag Milanovic
a45c131b37 Release version 0.19 2022-07-04 14:07:01 +02:00
Miodrag Milanović
0b44bff182
Merge pull request #3398 from jix/mention_smtlib2_module 
Mention smtlib2_module in README.md and CHANGELOG
 2022-07-04 14:05:00 +02:00
Jannis Harder
5343911263 Mention smtlib2_module in README.md and CHANGELOG 2022-07-04 13:54:49 +02:00
Miodrag Milanovic
59b96bb1f8 Upadte documentation and changelog 2022-07-04 11:09:06 +02:00
Pepijn de Vos
de07eb11c1
Apicula now supports lutram 2022-07-03 12:45:03 +02:00
github-actions[bot]
c39bade1a7 Bump version 2022-07-02 00:18:03 +00:00
Jannis Harder
4a1e54bf70
Merge pull request #3395 from jix/opt_dff_keepdc_initival 
opt_dff: With -keepdc, never turn undef init vals into const drivers
 2022-07-01 16:52:32 +02:00
Jannis Harder
876ef59f4f
Merge pull request #3396 from jix/async2sync_const_clocks 
async2sync: turn FFs with const clks into gclk FFs with feedback
 2022-07-01 16:47:31 +02:00
Miodrag Milanovic
fda3a537e1 Update abc 2022-07-01 16:23:24 +02:00
Jannis Harder
0182b26aba
Merge pull request #3391 from programmerjake/simcheck-allow-smtlib2-blackboxes 
add hierarchy -smtcheck
 2022-07-01 14:38:45 +02:00
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