Commit Graph

284 Commits

Author SHA1 Message Date
Claire Xenia Wolf 2ea757da51 Add "verific -cfg" command
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-11-01 10:41:51 +01:00
Claire Xenia Wolf 83118bfb9e Fix verific gclk handling for async-load FFs
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-10-31 17:12:29 +01:00
Miodrag Milanovic f7cc388bb5 Enable async load dff emit by default in Verific 2021-10-27 15:56:56 +02:00
Miodrag Milanovic 32673edfea Revert "Compile option for enabling async load verific support"
This reverts commit b8624ad2ae.
2021-10-27 15:55:43 +02:00
Miodrag Milanovic b8624ad2ae Compile option for enabling async load verific support 2021-10-25 09:04:43 +02:00
Claire Xenia Wolf 90b440f870 Fix verific.cc PRIM_DLATCH handling
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-10-21 12:13:35 +02:00
Claire Xenia Wolf 16a177560f Initial Verific impoter support for {PRIM,WIDE_OPER}_DLATCH{,RS}
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-10-21 05:42:47 +02:00
Miodrag Milanovic 17269ae59b Option to disable verific VHDL support 2021-10-20 10:02:58 +02:00
Miodrag Milanovic 1aa6896966 Support PRIM_BUFIF1 primitive 2021-10-14 13:04:32 +02:00
Claire Xen 2d3c79458d
Merge pull request #3039 from YosysHQ/claire/verific_aldff
Add support for $aldff flip-flops to verific importer
2021-10-11 10:01:56 +02:00
Claire Xenia Wolf c8074769b0 Add Verific adffe/dffsre/aldffe FIXMEs
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-10-11 10:00:20 +02:00
Miodrag Milanovic 93fbc9fba4 Import module attributes from Verific 2021-10-10 10:01:45 +02:00
Claire Xenia Wolf 34f1df8435 Fixes and add comments for open FIXME items
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-10-08 17:24:45 +02:00
Claire Xenia Wolf 1602a03864 Add support for $aldff flip-flops to verific importer
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-10-08 16:21:25 +02:00
Miodrag Milanovic abc5700628 verific set db_infer_set_reset_registers 2021-10-04 16:48:33 +02:00
Miodrag Milanovic c3d4bb4cc9 update required verific version 2021-09-02 14:59:16 +02:00
Miodrag Milanovic b59c427348 Make Verific extensions optional 2021-08-20 10:19:04 +02:00
Miodrag Milanovic be04d8834e Require latest verific 2021-08-02 10:29:58 +02:00
Miodrag Milanovic 987fca5297 Update to latest verific 2021-07-21 09:46:53 +02:00
Miodrag Milanovic 7a5ac90985 Update to latest Verific with extensions for initial assertions 2021-07-09 09:02:27 +02:00
Miodrag Milanovic 0dbb05a75e Add additional help 2021-07-05 09:16:54 +02:00
Miodrag Milanovic c0d8da20d5 Support command files in Verific 2021-06-16 11:21:44 +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
Claire Xen 6c56c083f8
Update README 2021-03-04 16:43:30 +01:00
Claire Xen 27d7741540
Merge pull request #2574 from dh73/master
Accept disable case for SVA liveness properties.
2021-02-15 17:49:11 +01:00
Miodrag Milanovic 13c2fd7137 Ganulate Verific support 2021-02-12 10:08:43 +01:00
Diego H c96eb2fbd7 Accept disable case for SVA liveness properties. 2021-02-04 15:35:35 -06:00
Miodrag Milanovic d99c032c27 Require latest Verific build 2021-01-30 09:23:46 +01:00
Claire Xenia Wolf acad7a6e40 Switch verific bindings from Symbiotic EDA flavored Verific to YosysHQ flavored Verific
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-01-20 20:48:10 +01:00
Miodrag Milanovic 1c4a18f66f Bump required Verific version 2020-12-02 15:18:04 +01:00
Miodrag Milanovic c228cb74d6 Update verific version 2020-10-30 08:32:59 +01:00
Miodrag Milanovic c8f052bbe0 extend verific library API for formal apps and generators 2020-10-12 14:56:15 +02:00
Miodrag Milanović 1b7ed719a5
Update required Verific version 2020-10-05 13:27:27 +02:00
Miodrag Milanovic a44c5df259 use sha1 for parameter list in case if they contain spaces 2020-09-30 09:16:59 +02:00
Miodrag Milanovic 44705102b5 Better error for unsupported SVA sequence 2020-09-18 17:08:00 +02:00
Miodrag Milanovic 3f27a4ea68 Use latest verific 2020-09-02 10:22:25 +02:00
Miodrag Milanovic 04d5692a85 Reorder to prevent crash 2020-08-31 12:22:26 +02:00
Miodrag Milanovic 3af499c60f ast recognize lower case x and z and verific gives upper case 2020-08-30 13:33:03 +02:00
Miodrag Milanovic 2f93579bd1 Do not check for 1 and 0 only 2020-08-30 13:15:06 +02:00
Miodrag Milanovic b1e3bc059c Fix import of VHDL enums 2020-08-30 12:25:23 +02:00
Miodrag Milanovic fe8226a22d Add formal apps and template generators 2020-08-26 10:39:57 +02:00
Miodrag Milanovic cc02d58194 Clear last error message 2020-07-29 15:28:33 +02:00
clairexen 3d8d98d709
Merge pull request #2132 from YosysHQ/eddie/verific_initial
verific: rewrite initial assume/asserts prior to elaboration
2020-07-02 17:50:22 +02:00
Miodrag Milanovic 561890c4e8 Update verific API version check 2020-06-30 12:13:13 +02:00
Miodrag Milanovic b822beb1b2 Fix crash in verific frontend 2020-06-26 20:11:01 +02:00
clairexen c7d71f436d
Merge pull request #2168 from whitequark/assert-unused-exprs
Use (and ignore) the expression provided to log_assert in NDEBUG builds
2020-06-25 18:21:51 +02:00
Miodrag Milanovic 4aec50a863 optimization, all items should have same attributes 2020-06-25 09:18:53 +02:00
Miodrag Milanovic f993d18755 verific - import attributes for net buses as well 2020-06-24 11:01:06 +02:00
whitequark 118e4caa37 Remove YS_ATTRIBUTE(unused) where present just for log_assert()/log_debug(). 2020-06-19 15:48:58 +00:00
whitequark 7191dd16f9 Use C++11 final/override keywords. 2020-06-18 23:34:52 +00:00