Jannis Harder
a2f9ebe43a
memory_map: Add -formal option
...
This maps memories for a global clock based formal verification flow.
This implies -keepdc, uses $ff cells for ROMs and sets hdlname
attributes.
2022-08-16 13:37:30 +02:00
Jannis Harder
0cdb14df41
setundef: Do not add anyseq / anyconst to unused memory port clocks
...
Instead set those unused clocks to zero.
2022-08-16 13:37:30 +02:00
Jannis Harder
428ad5b9fd
wreduce: Keep more x-bits with -keepdc
2022-08-16 13:37:30 +02:00
Jannis Harder
95db5a9d38
formalff: New -setundef option
...
Find FFs with undefined initialization values for which changing the
initialization does not change the observable behavior and initialize
them. For -ff2anyinit, this reduces the number of generated $anyinit
cells that drive wires with private names.
2022-08-16 13:37:30 +02:00
Jannis Harder
a5e1d3b997
formalff: Set new replaced_by_gclk attribute on removed dff's clks
...
This attribute can be used by formal backends to indicate which clocks
were mapped to the global clock. Update the btor and smt2 backend which
already handle clock inputs to understand this attribute.
2022-08-16 13:37:30 +02:00
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
Jacob Lifshay
c16c028831
add hierarchy -smtcheck
...
like -simcheck, but allow smtlib2_module modules.
2022-06-22 20:53:10 -07: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