Miodrag Milanovic
25d50bb2af
VHDL only build support
2024-06-17 13:29:11 +02:00
Jannis Harder
3cbca5064c
verific: Handle non-seq properties with VerificClocking conditions
2023-04-21 17:19:42 +02:00
Miodrag Milanovic
6574553189
Fixes for some of clang scan-build detected issues
2023-01-17 12:58:08 +01: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
Claire Xenia Wolf
72787f52fc
Fixing old e-mail addresses and deadnames
...
s/((Claire|Xen|Xenia|Clifford)\s+)+(Wolf|Xen)\s+<(claire|clifford)@(symbioticeda.com|clifford.at|yosyshq.com)>/Claire Xenia Wolf <claire@yosyshq.com>/gi;
s/((Nina|Nak|N\.)\s+)+Engelhardt\s+<nak@(symbioticeda.com|yosyshq.com)>/N. Engelhardt <nak@yosyshq.com>/gi;
s/((David)\s+)+Shah\s+<(dave|david)@(symbioticeda.com|yosyshq.com|ds0.me)>/David Shah <dave@ds0.me>/gi;
s/((Miodrag)\s+)+Milanovic\s+<(miodrag|micko)@(symbioticeda.com|yosyshq.com)>/Miodrag Milanovic <micko@yosyshq.com>/gi;
s,https?://www.clifford.at/yosys/,http://yosyshq.net/yosys/,g ;
2021-06-08 00:39:36 +02:00
Diego H
c96eb2fbd7
Accept disable case for SVA liveness properties.
2021-02-04 15:35:35 -06:00
Miodrag Milanovic
44705102b5
Better error for unsupported SVA sequence
2020-09-18 17:08:00 +02:00
Clifford Wolf
db323685a4
Add Verific support for SVA nexttime properties
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-11-22 16:11:56 +01:00
Clifford Wolf
6af0d03fae
Add Verific SVA support for "always" properties
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-11-22 15:52:21 +01:00
Eddie Hung
046e1a5214
Use State::S{0,1}
2019-08-06 16:22:47 -07:00
Clifford Wolf
cda37830b0
Add hack for handling SVA labels via Verific
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-07 10:52:44 -08:00
whitequark
efa278e232
Fix typographical and grammatical errors and inconsistencies.
...
The initial list of hits was generated with the codespell command
below, and each hit was evaluated and fixed manually while taking
context into consideration.
DIRS="kernel/ frontends/ backends/ passes/ techlibs/"
DIRS="${DIRS} libs/ezsat/ libs/subcircuit"
codespell $DIRS -S *.o -L upto,iff,thru,synopsys,uint
More hits were found by looking through comments and strings manually.
2019-01-02 13:12:17 +00:00
Clifford Wolf
5d9d22f66d
Add "verific -L <int>" option
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-09-04 20:06:10 +02:00
Clifford Wolf
65234d4b24
Fix handling of eventually properties in verific importer
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-07-17 12:43:30 +02:00
Clifford Wolf
8b92ddb9d2
Fix verific eventually handling
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-06-29 19:24:58 +02:00
Clifford Wolf
0404cf61d5
Add verific support for eventually properties
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-06-29 19:21:04 +02:00
Clifford Wolf
24e6401617
Further improve handling of zero-length SVA consecutive repetition
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-05-05 14:32:04 +02:00
Clifford Wolf
3e67497ec2
Fix handling of zero-length SVA consecutive repetition
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-05-05 13:58:01 +02:00
Clifford Wolf
93985d91b1
Remove left-over log_ping debug commands.. oops.
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-31 14:23:57 +02:00
Clifford Wolf
315d5e32bf
Fix handling of unclocked immediate assertions in Verific front-end
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-26 13:04:10 +02:00
Clifford Wolf
e7862d4f64
Update todo for more features to verificsva.cc
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-16 15:48:48 +01:00
Clifford Wolf
38596ce68f
Update todo for more features to verificsva.cc
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-16 12:16:52 +01:00
Clifford Wolf
462e9f7bd4
Add todo for more features to verificsva.cc
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-16 12:15:36 +01:00
Clifford Wolf
307c16a309
Fix SVA handling of NON_CONSECUTIVE_REPEAT and GOTO_REPEAT
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-10 16:24:01 +01:00
Clifford Wolf
ce37b6d730
Fix variable name typo in verificsva.cc
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-10 14:33:42 +01:00
Clifford Wolf
da216937b1
Add support for trivial SVA sequences and properties
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-10 14:32:01 +01:00
Clifford Wolf
a4bbfd2d15
Fix Verific handling of "assert property (..);" in always block
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-07 20:06:02 +01:00
Clifford Wolf
dcc4a18d5a
Update comment about supported SVA in verificsva.cc
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-06 15:47:33 +01:00
Clifford Wolf
03b49654b1
Add SVA NON_CONSECUTIVE_REPEAT and GOTO_REPEAT support
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-06 15:39:46 +01:00
Clifford Wolf
7bb83ae9f2
Add SVA first_match() support
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-06 15:06:35 +01:00
Clifford Wolf
78f2cca2d9
Add SVA within support
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-06 14:41:27 +01:00
Clifford Wolf
5555292ce2
Add support for SVA sequence intersect
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-06 14:26:57 +01:00
Clifford Wolf
d86e875f0f
Add get_fsm_accept_reject for parsing SVA properties
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-06 11:50:38 +01:00
Clifford Wolf
588ce0e34a
Simplified SVA "until" handling
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-06 01:51:42 +01:00
Clifford Wolf
480e8e676a
Add proper SVA seq.triggered support
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-04 19:29:26 +01:00
Clifford Wolf
8dcf3d0c76
Add Verific SVA support for "seq and seq" expressions
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-04 15:08:21 +01:00
Clifford Wolf
9ab2498c55
Refactor Verific SVA importer property parser
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-04 14:29:48 +01:00
Clifford Wolf
261cf706f4
Add VerificClocking class and refactor Verific DFF handling
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-04 13:48:53 +01:00
Clifford Wolf
707ddb77bc
Add SVA support for sequence OR
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-03 16:34:28 +01:00
Clifford Wolf
cabc3c59e0
Fix handling of SVA "until seq.triggered" properties
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-02 18:17:10 +01:00
Clifford Wolf
ab791e61b3
Update SVA cheat sheet in verificsva.cc
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-02 16:05:56 +01:00
Clifford Wolf
4e5f1f59d6
Fix in Verific SVA importer handling of until_with
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-01 19:37:36 +01:00
Clifford Wolf
9a2a8cd97b
Fixes and improvements in Verific SVA importer
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-01 11:40:43 +01:00
Clifford Wolf
5ac3ee858a
Add support for PRIM_SVA_UNTIL to new SVA importer
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-28 15:32:17 +01:00
Clifford Wolf
8a1d6ccf0c
Add DFSM generator to verific SVA importer
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-28 15:05:33 +01:00
Clifford Wolf
15902d495f
Continue refactoring of Verific SVA importer code
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-28 11:45:04 +01:00
Clifford Wolf
25e33d7ab8
Major redesign of Verific SVA importer
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-27 20:33:15 +01:00
Clifford Wolf
d1cb5150aa
Add "SVA syntax cheat sheet" comment to verificsva.cc
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-26 14:31:58 +01:00
Clifford Wolf
2521ed305e
Add Verific SVA support for ranges in repetition operator
2018-02-22 12:37:30 +01:00
Clifford Wolf
6d12c83d36
Add support for SVA throughout via Verific
2018-02-21 13:09:47 +01:00