Commit Graph

254 Commits

Author SHA1 Message Date
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
clairexen b2a0f49371
Merge pull request #2131 from YosysHQ/claire/preserveffs
Do not optimize away FFs in "prep" and Verific front-end
2020-06-10 12:44:23 +02:00
Miodrag Milanovic d6bec3ba1c verific - detect missing memory to prevent crash. 2020-06-10 11:27:44 +02:00
Claire Wolf 3c7122c378 Do not optimize away FFs in "prep" and Verific fron-end
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-06-09 15:54:14 +02:00
Miodrag Milanovic 71072d1945 Support asymmetric memories for verific frontend 2020-06-01 10:30:03 +02:00
Claire Wolf fa8cb3e35d Revert "Add support for non-power-of-two mem chunks in verific importer"
This reverts commit 173aa27ca5.
2020-05-17 11:31:11 +02:00
Eddie Hung 39fa1e160d verific: rewrite initial assume/asserts prior to elaboration 2020-05-15 14:05:28 -07:00
Claire Wolf 173aa27ca5 Add support for non-power-of-two mem chunks in verific importer
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-05-14 14:38:13 +02:00
Eddie Hung 5017ff4a97 verific: ignore anonymous enums 2020-04-30 07:48:47 -07:00
Eddie Hung 97bfe65d3a verific: support VHDL enums too 2020-04-27 15:17:13 -07:00
Eddie Hung dd5f206d9e verific: recover wiretype/enum attr as part of import_attributes() 2020-04-27 08:43:54 -07:00
Eddie Hung b52eccef3a Revert "verific: import enum attributes from verific"
This reverts commit 5028e17f7d.
2020-04-24 11:57:55 -07:00
Eddie Hung d3555c667c verific: do not assert if wire not found; warn instead 2020-04-23 16:28:11 -07:00
Eddie Hung 5028e17f7d verific: import enum attributes from verific 2020-04-22 17:26:56 -07:00
Eddie Hung 956ecd48f7 kernel: big fat patch to use more ID::*, otherwise ID(*) 2020-04-02 09:51:32 -07:00
Eddie Hung fdafb74eb7 kernel: use more ID::* 2020-04-02 07:14:08 -07:00
Claire Wolf 2ce7a0d369
Merge pull request #1667 from YosysHQ/clifford/verificnand
Add Verific support for OPER_REDUCE_NAND
2020-01-30 19:55:53 +01:00
Claire Wolf 60876ce183
Merge pull request #1503 from YosysHQ/eddie/verific_help
`verific` pass to print help message when command syntax error
2020-01-30 18:05:16 +01:00
Claire Wolf 23c44afaed Add Verific support for OPER_REDUCE_NAND
Signed-off-by: Claire Wolf <clifford@clifford.at>
2020-01-30 18:01:13 +01:00
Eddie Hung f443695a38 Merge remote-tracking branch 'origin/master' into eddie/verific_help 2020-01-27 10:34:10 -08:00
Eddie Hung d730bba6d2 verific: no help() when no YOSYS_ENABLE_VERIFIC 2020-01-27 10:32:18 -08:00
Eddie Hung 7b445121cc verific: also unflatten for 'hierarchy' flow as per @cliffordwolf 2020-01-27 10:15:22 -08:00
Eddie Hung cccc0ae112 verific: unflatten struct ports 2020-01-24 10:12:52 -08:00
Clifford Wolf 22dd9f107c Send people to symbioticeda.com instead of verific.com
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-12-18 13:06:34 +01: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 e93e4a7a2c Improve handling of verific primitives in "verific -import -V" mode
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-11-22 16:00:07 +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
Clifford Wolf 55bda2b2c6 Correctly treat empty modules as blackboxes in Verific
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-11-20 12:56:31 +01:00
Clifford Wolf f6ff311a1d Do not rename VHDL entities to "entity(impl)" when they are top modules
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-11-20 12:54:10 +01:00
Eddie Hung e2819ce31c Oops 2019-11-19 13:25:38 -08:00
Eddie Hung 84711f0e8c Print help message for verific pass 2019-11-19 13:24:48 -08:00