3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-22 08:35:32 +00:00
Commit graph

4384 commits

Author SHA1 Message Date
Jannis Harder
c0063288d6 Add the $anyinit cell and the formalff pass
These can be used to protect undefined flip-flop initialization values
from optimizations that are not sound for formal verification and can
help mapping all solver-provided values in witness traces for flows that
use different backends simultaneously.
2022-08-16 13:37:30 +02:00
N. Engelhardt
6f439dc59a
Merge pull request #3425 from YosysHQ/lofty/stat-json 2022-08-11 17:00:54 +02:00
Lofty
59facfa98c stat: add option for machine-readable json output 2022-08-11 13:41:01 +01:00
N. Engelhardt
63fca0dbc2
Merge pull request #3277 from YosysHQ/lofty/rename-scramble_name 2022-08-11 12:06:04 +02:00
Miodrag Milanovic
f4a1906721 support file locations containing spaces 2022-08-08 20:30:50 +02:00
Lofty
a48dcd1d40 rename: add -scramble-name option to randomly rename selections 2022-08-08 16:03:28 +01:00
Marcelina Kościelnicka
f679b756d8 opt_reduce: Fix use-after-free.
Fixes #3418.
2022-07-23 17:27:26 +02:00
Jannis Harder
14ba50908b sim: Fix $anyseq in nested modules 2022-07-22 14:48:30 +02:00
Catherine
502b96fe53 Fix external ABC build after commit 0ca0932b5. 2022-07-07 08:38:30 +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
Jannis Harder
0182b26aba
Merge pull request #3391 from programmerjake/simcheck-allow-smtlib2-blackboxes
add hierarchy -smtcheck
2022-07-01 14:38:45 +02: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
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
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
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
c16c028831 add hierarchy -smtcheck
like -simcheck, but allow smtlib2_module modules.
2022-06-22 20:53:10 -07: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
Marcelina Kościelnicka
ab3a9325c3 memory_map: Add -rom-only option. 2022-06-17 16:56:11 +02:00
Marcelina Kościelnicka
01daa077a2 memory_map: Use const drivers instead of FFs for ROMs. 2022-06-17 15:17:14 +02: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
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
bfg86
aedd3b7999 Updating help-text with nakengelhardts suggestion. 2022-06-13 09:35:10 +02:00
N. Engelhardt
b8ede6162b
Merge pull request #3349 from nakengelhardt/select_count_scratchpad
Make 'stat' and 'select -count' save counts to scratchpad
2022-06-09 17:15:02 +02:00
N. Engelhardt
871b277d35
Merge pull request #3359 from jix/fmcombine-memid
fmcombine: Add _gold/_gate suffix to memids
2022-06-09 17:12:34 +02:00
Henner Zeller
9d41aa8e28 Avoid unnecessary copy of a potential large constant value.
The local variable is used just to iterate through the values, so
a const reference is all we need.
2022-06-09 16:05:51 +01:00
Marcelina Kościelnicka
47efc04a7d wreduce: Introduce -mux_undef option (aligned with opt_expr). 2022-06-08 21:28:58 +02:00
Lofty
aae2c01326 sta: warn on unrecognised cells only once 2022-06-08 09:31:49 +01:00
Marcelina Kościelnicka
d07828b409 opt_ffinv: Harden against simple ff/inv loop. 2022-06-07 08:20:06 +02:00
Marcelina Kościelnicka
9e8a2ac051 iopadmap: Fix z assignment removal.
Fixes #3360.
2022-06-07 04:10:50 +02:00
Jannis Harder
459941c8ff fmcombine: Add _gold/_gate suffix to memids 2022-06-03 21:52:28 +02:00
Miodrag Milanovic
d88a5d26b7 Fix preventing show crashing with newer graphviz 2022-06-03 08:38:16 +02:00
Marcelina Kościelnicka
71dfbf33b2 Add -no-rw-check option to memory_dff + memory + synth_{ice40,ecp5,gowin}. 2022-06-02 23:16:12 +02:00
Marcelina Kościelnicka
3a0aa9c663 memory_dff: Add support for no_rw_check attribute. 2022-06-02 12:49:34 +02:00
N. Engelhardt
61b05051e1 also make 'stat' save counts to scratchpad 2022-06-01 16:01:07 +02:00
N. Engelhardt
a55c3db384 have 'select -count' save the count to scratchpad entry 'select.count' 2022-06-01 14:39:33 +02:00
Mohamed A. Bamakhrama
1822be8792 Observe $TMPDIR variable when creating tmp files
POSIX defines $TMPDIR as containing the pathname of the directory where
programs can create temporary files. On most systems, this variable points to
"/tmp". However, on some systems it can point to a different location.
Without respecting this variable, yosys fails to run on such systems.

Signed-off-by: Mohamed A. Bamakhrama <mohamed@alumni.tum.de>
2022-05-27 15:06:53 +02:00
gatecat
166a175983 abc9_ops: Don't leave unused derived modules lying around
These later become accidentally used for techmap replacements for
blackboxes that we don't actually want.

Signed-off-by: gatecat <gatecat@ds0.me>
2022-05-23 15:02:25 +01:00
Jannis Harder
fc65ea47df select: Fix -assert-none and -assert-any error output and docs
Both of these options consider a selection containing only empty modules
as non-empty. This wasn't mentioned in the documentation nor did the
error message when using `select -assert-none` list those empty modules,
which produced a very confusing error message complaining about a
non-empty selection followed by an empty listing of the selection.

This fixes the documentation and changes the `-assert-none` and
`-assert-any` assertion error messages to also output fully selected
modules (this includes selected empty modules).

It doesn't change the messages for `-assert-count` etc. as they don't
count modules.
2022-05-19 14:07:34 +02:00
Marcelina Kościelnicka
606f1637ae Add memory_bmux2rom pass. 2022-05-18 22:48:55 +02:00
Marcelina Kościelnicka
7c5dba8b77 Add memory_libmap pass. 2022-05-18 17:32:56 +02:00
Marcelina Kościelnicka
9450f308f0 proc_rom: Add special handling of const-0 address bits. 2022-05-18 17:32:30 +02:00
Marcelina Kościelnicka
98c7804b89 opt_ffinv: Use ModIndex instead of ModWalker.
This avoids using out-of-data index information.
2022-05-17 02:52:21 +02:00
Marcelina Kościelnicka
2858bb03cd Add opt_ffinv pass. 2022-05-13 23:02:30 +02:00
Marcelina Kościelnicka
990c9b8e11 Add proc_rom pass. 2022-05-13 00:37:14 +02:00