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
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
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
Jannis Harder
ac22f1764d
smt2: emit smtlib2_comb_expr outputs after all inputs
2022-06-07 19:06:45 +02:00
0b0123e003
don't use sed -i because it won't work on macos
2022-06-03 01:09:57 -07:00
b7c19b1c88
smtlib2_module: try to fix test on macos
2022-06-02 23:12:07 -07:00
cd57c5adb3
smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressions
2022-06-02 22:37:29 -07:00
Zachary Snow
a650d9079f
verilog: fix width/sign detection for functions
2022-05-30 16:45:39 -04:00
Jannis Harder
4bfaaea0d5
verilog: fix size and signedness of array querying functions
...
genrtlil.cc and simplify.cc had inconsistent and slightly broken
handling of signedness for array querying functions. These functions are
defined to return a signed result. Simplify always produced an unsigned
and genrtlil always a signed 32-bit result ignoring the context.
Includes tests for the the relvant edge cases for context dependent
conversions.
2022-05-30 09:11:31 -04:00
Jannis Harder
b75fa62e9b
verilog: fix $past's signedness
2022-05-25 16:32:08 -04:00
Jannis Harder
cffec1f95f
verilog: fix signedness when removing unreachable cases
2022-05-24 23:03:31 -04:00
Marcelina Kościelnicka
606f1637ae
Add memory_bmux2rom pass.
2022-05-18 22:48:55 +02:00
Marcelina Kościelnicka
982a11c709
Add memory_libmap tests.
2022-05-18 17:32:56 +02:00
Marcelina Kościelnicka
9d11575856
efinix: Use memory_libmap pass.
2022-05-18 17:32:56 +02:00
Marcelina Kościelnicka
d7dc2313b9
ice40: Use memory_libmap pass.
2022-05-18 17:32:56 +02:00
Marcelina Kościelnicka
3b2f95953c
xilinx: Use memory_libmap pass.
2022-05-18 17:32:56 +02:00
Marcelina Kościelnicka
0a8eaca322
nexus: Use memory_libmap pass.
2022-05-18 17:32:56 +02:00
Marcelina Kościelnicka
a04b025abf
ecp5: Use 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
Jannis Harder
2864f2826a
Merge pull request #3314 from jix/sva_value_change_logic_wide
...
verific: Use new value change logic also for $stable of wide signals.
2022-05-16 16:15:04 +02:00
Marcelina Kościelnicka
990c9b8e11
Add proc_rom pass.
2022-05-13 00:37:14 +02:00
Jannis Harder
fada77b8cf
verific: Use new value change logic also for $stable of wide signals.
...
I missed this in the previous PR.
2022-05-11 13:05:27 +02:00
Jannis Harder
587e09d551
Merge pull request #3305 from jix/sva_value_change_logic
...
verific: Improve logic generated for SVA value change expressions
2022-05-09 16:40:34 +02:00
Jannis Harder
5ca2ee0c31
Merge pull request #3297 from jix/sva_nested_clk_else
...
verific: Fix conditions of SVAs with explicit clocks within procedures
2022-05-09 16:07:39 +02:00
Jannis Harder
a855d62b42
verific: Improve logic generated for SVA value change expressions
...
The previously generated logic assumed an unconstrained past value in
the initial state and did not handle 'x values. While the current formal
verification flow uses 2-valued logic, SVA value change expressions
require a past value of 'x during the initial state to behave in the
expected way (i.e. to consider both an initial 0 and an initial 1 as
$changed and an initial 1 as $rose and an initial 0 as $fell).
This patch now generates logic that at the same time
a) provides the expected behavior in a 2-valued logic setting, not
depending on any dont-care optimizations, and
b) properly handles 'x values in yosys simulation
2022-05-09 15:04:01 +02:00
Miodrag Milanovic
600079e281
Fix running sva tests
2022-05-09 09:01:57 +02:00
Marcelina Kościelnicka
77b1dfd8c3
opt_mem: Remove constant-value bit lanes.
2022-05-07 23:13:16 +02:00
Jannis Harder
96f64f4788
verific: Fix conditions of SVAs with explicit clocks within procedures
...
For SVAs that have an explicit clock and are contained in a procedure
which conditionally executes the assertion, verific expresses this using
a mux with one input connected to constant 1 and the other output
connected to an SVA_AT. The existing code only handled the case where
the first input is connected to 1. This patch also handles the other
case.
2022-05-03 14:13:08 +02:00
Zachary Snow
bf15dbd0f7
sv: fix always_comb auto nosync for nested and function blocks
2022-04-05 14:43:48 -06:00
Jannis Harder
ca5b910296
opt_merge: Add -keepdc option required for formal verification
...
The `-keepdc` option prevents merging flipflops with dont-care bits in
their initial value, as, in general, this is not a valid transform for
formal verification.
The keepdc option of `opt` is passed along to `opt_merge` now.
2022-04-01 21:03:20 +02:00
Miodrag Milanovic
bbf65702a1
Fix valgrind tests when using verific
2022-03-30 17:25:53 +02:00
Miodrag Milanovic
27c5bafc95
Proper example code
2022-03-14 15:39:11 +01:00
Lofty
9f7a55c99f
intel_alm: M10K write-enable is negative-true
2022-03-09 20:18:06 +00:00
Miodrag Milanović
c3124023e4
Merge pull request #3207 from nakengelhardt/json_escape_quotes
...
fix handling of escaped chars in json backend and frontend (mostly)
2022-03-04 13:57:32 +01:00
N. Engelhardt
8fd1b06249
fix handling of escaped chars in json backend and frontend
2022-02-18 17:13:09 +01:00
Miodrag Milanovic
21baf48e04
test dlatchsr and adlatch
2022-02-16 13:58:51 +01:00
Miodrag Milanovic
271ac28b41
Added test cases
2022-02-16 13:27:59 +01:00
Zachary Snow
15a4e900b2
verilog: support for time scale delay values
2022-02-14 15:58:31 +01:00
Kamil Rakoczy
68c67c40ec
Fix access to whole sub-structs ( #3086 )
...
* Add support for accessing whole struct
* Update tests
Signed-off-by: Kamil Rakoczy <krakoczy@antmicro.com>
2022-02-14 14:34:20 +01:00
Zachary Snow
15eb66b99d
verilog: fix dynamic dynamic range asgn elab
2022-02-11 22:54:55 +01:00
Zachary Snow
90bb47d181
verilog: fix const func eval with upto variables
2022-02-11 21:01:51 +01:00
Marcelina Kościelnicka
f61f2a4078
gowin: Fix LUT RAM inference, add more models.
2022-02-09 09:04:34 +01:00
Miodrag Milanović
d7f7227ce8
Merge pull request #3185 from YosysHQ/micko/co_sim
...
Add co-simulation in sim pass
2022-02-07 16:36:43 +01:00
Miodrag Milanovic
6db23de7b1
bug fix and cleanups
2022-02-04 10:01:06 +01:00
Miodrag Milanovic
7ef6da4c7d
Add test cases for co-simulation
2022-02-02 13:22:44 +01:00
Marcelina Kościelnicka
07a657fb0c
opt_reduce: Add $bmux and $demux optimization patterns.
2022-01-30 03:37:52 +01:00
Miodrag Milanović
4525e419f6
Merge pull request #3120 from Icenowy/anlogic-bram
...
anlogic: support BRAM mapping
2022-01-19 08:49:58 +01:00
Zachary Snow
aa35f24290
sv: auto add nosync to certain always_comb local vars
...
If a local variable is always assigned before it is used, then adding
nosync prevents latches from being needlessly generated.
2022-01-07 22:53:22 -07:00
