Clifford Wolf
|
f39b897545
|
Add "read -incdir"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-07-16 15:32:26 +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
|
ebf0f003d3
|
Add "verific -formal" and "read -formal"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-06-29 10:02:27 +02:00 |
Clifford Wolf
|
afedb2d03e
|
Add "read -sv -D" support
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-06-28 23:58:15 +02:00 |
Clifford Wolf
|
07e616900c
|
Add "read -undef"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-06-28 23:43:38 +02:00 |
Clifford Wolf
|
848c3c5c88
|
Add YOSYS_NOVERIFIC env variable for temporarily disabling verific
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-06-22 20:40:22 +02:00 |
Clifford Wolf
|
d412b17259
|
Add simplified "read" command, enable extnets in implicit Verific import
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-06-21 16:56:55 +02:00 |
Clifford Wolf
|
5f2bc1ce76
|
Add automatic verific import in hierarchy command
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-06-20 23:45:01 +02:00 |
Clifford Wolf
|
4372cf690d
|
Add (* gclk *) attribute support
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-06-01 13:25:42 +02:00 |
Clifford Wolf
|
9a946c207f
|
Add comment to VIPER #13453 work-around
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-05-28 13:36:35 +02:00 |
Clifford Wolf
|
001c9f1d45
|
Fix Verific handling of single-bit anyseq/anyconst wires
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-05-25 15:41:45 +02:00 |
Clifford Wolf
|
251562a491
|
Fix VerificClocking for cases where Verific generates chains of PRIM_SVA_POSEDGE
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-05-24 18:13:38 +02:00 |
Clifford Wolf
|
4d645f0fce
|
Fix verific handling of anyconst/anyseq attributes
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-05-24 17:07:06 +02:00 |
Clifford Wolf
|
a7281930c5
|
Fix handling of anyconst/anyseq attrs in VHDL code via Verific
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-05-15 19:27:00 +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
|
617c60cea6
|
Add PRIM_HDL_ASSERTION support to Verific importer
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-04-07 18:38:42 +02:00 |
Clifford Wolf
|
0ac768f9df
|
Fix handling of $global_clocking in Verific
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-04-06 21:23:47 +02:00 |
Clifford Wolf
|
278685b084
|
Add Verific anyseq/anyconst/allseq/allconst attribute support
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-04-06 14:19:55 +02:00 |
Clifford Wolf
|
ab8db2c168
|
Add "verific -autocover"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-04-06 14:10:57 +02:00 |
makaimann
|
0c404b1f63
|
Set RAM runtime flags for Verific frontend
|
2018-04-05 17:38:08 -07: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
|
7cf9d88028
|
Improve import of memories via Verific
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-03-15 18:20:37 +01:00 |
Clifford Wolf
|
bf402a806a
|
Fix handling of SV compilation units in Verific front-end
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-03-14 20:22:11 +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
|
a15208f301
|
Use Verific hier_tree component for elaboration
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-03-08 13:26:33 +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
|
92d5f4db6f
|
Add "verific -import -V"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-03-07 19:40:34 +01:00 |
Clifford Wolf
|
252627fc54
|
Set Verific db_preserve_user_nets flag
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-03-07 18:08:03 +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
|
3c49e3c5b3
|
Add $rose/$fell support to Verific bindings
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-03-01 10:12:15 +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
|
b6fbeb0969
|
Add handling of verific OPER_REDUCE_NOR
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-26 15:26:01 +01:00 |
Clifford Wolf
|
2aeb4d4e12
|
Add handling of verific OPER_SELECTOR and OPER_WIDE_SELECTOR
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-26 15:20:27 +01:00 |
Clifford Wolf
|
9cd9f5fc78
|
Add handling of verific OPER_NTO1MUX and OPER_WIDE_NTO1MUX
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-26 15:02:03 +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 |
Clifford Wolf
|
5c6247dfa6
|
Add support for SVA sequence concatenation ranges via verific
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-18 16:35:06 +01:00 |
Clifford Wolf
|
9d963cd29c
|
Add support for SVA until statements via Verific
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-18 14:57:52 +01:00 |
Clifford Wolf
|
5fa2aa2741
|
Move Verific SVA importer to extra C++ source file
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-18 13:52:49 +01:00 |
Clifford Wolf
|
c4bf34f6ce
|
Merge Verific SVA preprocessor and SVA importer
|
2018-02-18 13:28:08 +01:00 |
Clifford Wolf
|
bc8ab3ab44
|
Fix verific PRIM_SVA_AT handling in properties with PRIM_SVA_DISABLE_IFF
|
2018-02-15 15:26:37 +01:00 |
Clifford Wolf
|
6c00e064e2
|
Fix single-bit $stable handling in verific front-end
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-01 12:51:49 +01:00 |
Clifford Wolf
|
9af40faa0b
|
Add Verific attribute handling for assert/assume/cover/live/fair cells
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-01-31 19:06:51 +01:00 |
Clifford Wolf
|
675f53abbb
|
Fix permissions on verific vdb files
|
2018-01-28 18:52:01 +01:00 |
Clifford Wolf
|
1d8161b432
|
Fixed handling of synchronous and asynchronous assertion/assumption/cover in verific bindings
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-01-23 17:42:40 +01:00 |
Clifford Wolf
|
ba90e08398
|
Add support for Verific PRIM_SVA_NOT properties
|
2017-12-10 01:10:03 +01:00 |
Clifford Wolf
|
e4a4c0e10c
|
Add Verific OPER_SVA_STABLE support
|
2017-12-10 00:59:44 +01:00 |
Clifford Wolf
|
27916105a9
|
Refactoring Verific SVA rewriter
|
2017-12-10 00:26:26 +01:00 |
Clifford Wolf
|
0a31a0b3ae
|
Remove all PSL support code from verific.cc
|
2017-10-20 13:14:04 +02:00 |
Clifford Wolf
|
1954c78ea7
|
Add "verific -vlog-libdir"
|
2017-10-13 20:23:19 +02:00 |
Clifford Wolf
|
e7a3c47cc7
|
Add "verific -vlog-incdir" and "verific -vlog-define"
|
2017-10-13 20:12:51 +02:00 |
Clifford Wolf
|
05068af880
|
Update Verific README
|
2017-10-13 17:11:53 +02:00 |
Clifford Wolf
|
bc5cc4e103
|
Add Verific fairness/liveness support
|
2017-10-12 12:00:09 +02:00 |
Clifford Wolf
|
c10e96c9ec
|
Start work on pre-processor for Verific SVA properties
|
2017-10-10 15:16:39 +02:00 |
Clifford Wolf
|
fc3378916d
|
Improve handling of Verific errors
|
2017-10-05 14:38:32 +02:00 |
Clifford Wolf
|
ee56a887b6
|
Improve Verific error handling, check VHDL static asserts
|
2017-10-04 18:56:28 +02:00 |
Clifford Wolf
|
b92ff2706e
|
Fix nasty bug in Verific bindings
|
2017-10-04 17:23:42 +02:00 |
Clifford Wolf
|
15073790bf
|
Add merging of "past FFs" to verific importer
|
2017-07-29 00:10:38 +02:00 |
Clifford Wolf
|
d4b9602cbd
|
Add minimal support for PSL in VHDL via Verific
|
2017-07-28 17:39:49 +02:00 |
Clifford Wolf
|
5a828fff34
|
Improve Verific HDL language options
|
2017-07-28 15:32:54 +02:00 |
Clifford Wolf
|
acd6cfaf67
|
Fix handling of non-user-declared Verific netbus
|
2017-07-28 11:31:27 +02:00 |
Clifford Wolf
|
c1cfca8f54
|
Improve Verific SVA importer
|
2017-07-27 14:05:09 +02:00 |
Clifford Wolf
|
2336d5508b
|
Add log_warning_noprefix() API, Use for Verific warnings and errors
|
2017-07-27 12:17:04 +02:00 |
Clifford Wolf
|
d9641621d9
|
Add "verific -import -n" and "verific -import -nosva"
|
2017-07-27 11:54:45 +02:00 |
Clifford Wolf
|
90d8329f64
|
Improve Verific SVA import: negedge and $past
|
2017-07-27 11:40:07 +02:00 |
Clifford Wolf
|
147ff96ba3
|
Improve Verific SVA importer
|
2017-07-27 10:39:39 +02:00 |
Clifford Wolf
|
530040ba6f
|
Improve Verific bindings (mostly related to SVA)
|
2017-07-26 18:00:01 +02:00 |
Clifford Wolf
|
abd3b4e8e7
|
Improve "help verific" message
|
2017-07-25 15:13:22 +02:00 |
Clifford Wolf
|
6dbe1d4c92
|
Add "verific -extnets"
|
2017-07-25 14:53:11 +02:00 |
Clifford Wolf
|
c97c92e4ec
|
Improve "verific -all" handling
|
2017-07-25 13:33:25 +02:00 |
Clifford Wolf
|
41be530c4e
|
Add "verific -import -d <dump_file"
|
2017-07-24 13:57:16 +02:00 |
Clifford Wolf
|
92d3aad670
|
Add "verific -import -flatten" and "verific -import -v"
|
2017-07-24 11:29:06 +02:00 |
Clifford Wolf
|
5be535517c
|
Add "verific -import -k"
|
2017-07-22 16:16:44 +02:00 |