Jannis Harder
390d1c583a
verific: Fix enum_values support and signed attribute values
...
This uses the same constant parsing for enum_values and for attributes
and extends it to handle signed values as those are used for enums that
implicitly use the int type.
2023-03-15 09:51:36 +01:00
Miodrag Milanovic
a30894e5fa
Handle more wide case selector types
2023-02-27 09:24:04 +01:00
Miodrag Milanovic
109b88c379
For case select values use Sa instead of Sx and Sz
2023-02-08 09:22:48 +01:00
Miodrag Milanovic
e7e37df91b
Add verific import support for OPER_WIDE_CASE_SELECT_BOX
2023-02-06 09:28:23 +01:00
Miodrag Milanovic
6574553189
Fixes for some of clang scan-build detected issues
2023-01-17 12:58:08 +01:00
Miodrag Milanovic
b867dee241
respect noblackbox attribute in verific
2022-12-15 08:17:53 +01:00
Miodrag Milanović
9362fdb4c6
Merge pull request #3568 from YosysHQ/verific_msg
...
Set all Verific messages of certain type to other
2022-12-05 16:22:44 +01:00
Miodrag Milanovic
34a64aa322
set VERI-1063 explicitly
2022-12-02 17:11:17 +01:00
Miodrag Milanovic
2dd55d73a0
reset elaboration error after rewriter
2022-11-30 17:26:48 +01:00
Miodrag Milanovic
bfd79845b6
Set all verific messages of certain type to other
2022-11-30 16:42:37 +01:00
Miodrag Milanovic
f764cd1655
update documentation
2022-11-25 14:27:30 +01:00
Miodrag Milanovic
b0be19c126
Support importing verilog configurations using Verific
2022-11-25 13:02:11 +01:00
Miodrag Milanovic
59b6ac47c9
Add additional help info
2022-10-31 18:04:34 +01:00
Miodrag Milanovic
6fb80bce15
Enable importing blackbox modules only
2022-10-31 10:51:28 +01:00
Miodrag Milanovic
e702f2894a
Support for reading liberty files using verific
2022-10-31 10:15:05 +01:00
Miodrag Milanovic
48628fbf5a
Skip verific primitives and operators import by default
2022-10-14 17:41:24 +02:00
Miodrag Milanovic
922f8b614a
Add option to import all cells from all libraries
2022-10-14 16:54:57 +02:00
Claire Xenia Wolf
090228a6a1
Fix handling of verific -L options, add implicit "-L work"
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-10-10 00:47:42 +02:00
Miodrag Milanovic
1a6f10e8ba
Add support for EDIF file reading using Verific
2022-10-04 09:18:44 +02:00
Miodrag Milanovic
43267dec99
support file content redirection for verific frontened
2022-09-28 15:56:46 +02:00
Miodrag Milanovic
b45517f7b7
Add comment for future self
2022-09-28 14:45:39 +02:00
Miodrag Milanovic
f54ac8a6d6
Handle attributes imported from verific
2022-09-28 08:51:26 +02:00
Miodrag Milanovic
8fb498744f
Import memory attributes
2022-09-21 15:48:40 +02:00
Miodrag Milanovic
3f94f9313a
verific: better fix for read callback
2022-09-07 09:48:19 +02:00
Miodrag Milanovic
06a9c7499a
verific: fix crash when using prep right after read
2022-09-07 09:40:14 +02:00
Miodrag Milanovic
6c65ca4e50
Encode filename unprintable chars
2022-08-08 16:13:33 +02:00
Miodrag Milanovic
2b1aeb44d9
verific - make filepath handling compatible with verilog frontend
2022-08-08 11:57:28 +02:00
Miodrag Milanovic
52a4a89265
Setting wire upto in verific import
2022-07-29 17:10:31 +02:00
Miodrag Milanović
d19f9d0b66
Update README
2022-07-28 12:32:19 +02:00
Miodrag Milanovic
59b96bb1f8
Upadte documentation and changelog
2022-07-04 11:09:06 +02:00
Miodrag Milanovic
b80976b543
Update to new verific extensions inteface
2022-06-30 11:19:01 +02:00
Miodrag Milanovic
1fdbb42fdd
Revert "use new verific extensions library"
...
This reverts commit 607e957657
2022-06-21 18:07:47 +02:00
Miodrag Milanovic
607e957657
use new verific extensions library
2022-06-17 16:04:22 +02:00
Miodrag Milanovic
ddc8044655
removed deprecated features code
2022-06-13 10:50:24 +02:00
Miodrag Milanovic
6e8e4b4550
verific: Added "-vlog-libext" option to specify search extension for libraries
2022-06-09 08:57:48 +02:00
Miodrag Milanovic
e35a166353
verific: proper file location for readmem commands
2022-06-04 08:39:50 +02:00
Miodrag Milanovic
fdb393b6ce
fix text to fit 80 columns
2022-05-23 19:57:21 +02:00
Miodrag Milanovic
4a5790d404
Update verific command file documentation
2022-05-23 19:35:14 +02:00
Miodrag Milanovic
a6ec5754c6
Use analysis mode if set in file
2022-05-23 19:13:45 +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
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
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
Miodrag Milanovic
422db937d4
Ignore merging past ffs that we are not properly merging
2022-04-29 14:35:02 +02:00
Miodrag Milanovic
1cc281ca6f
verific: allow memories to be inferred in loops (vhdl)
2022-04-18 09:10:28 +02:00
N. Engelhardt
57bc29c64a
verific: allow memories to be inferred in loops
2022-04-15 15:10:48 +02:00
Miodrag Milanovic
1a1f529099
Preserve internal wires for external nets
2022-04-01 12:07:15 +02:00
Miodrag Milanovic
bbf65702a1
Fix valgrind tests when using verific
2022-03-30 17:25:53 +02:00
Miodrag Milanovic
703769e494
Properly mark modules imported
2022-03-26 09:43:51 +01:00
Miodrag Milanovic
245ecb0529
Import verific netlist in consistent order
2022-03-25 13:44:16 +01:00
