Commit Graph

588 Commits

Author SHA1 Message Date
Akash Levy 1b3375d8df Merge upstream in 2025-09-09 05:50:48 -07:00
Akash Levy 3311056d81 Revert "Revert some vhdl stuff"
This reverts commit 6a9102346a.
2025-08-08 01:16:49 -07:00
Akash Levy 6a9102346a Revert some vhdl stuff 2025-08-08 01:05:57 -07:00
Akash Levy 0e50fd3b74 Restricted multiport 2025-08-08 00:37:20 -07:00
Akash Levy 77be4d7be7 Bump Yosys to latest 2025-08-07 17:22:25 -07:00
Jannis Harder 75b62d0164 verificsva: Fix typo in the cover only followed-by operator support 2025-08-04 15:38:19 +02:00
Akash Levy cc733fd11b Merge from upstream 2025-07-30 22:50:14 -07:00
Miodrag Milanovic f92a53ec31 verific: handle nullptr for message_id 2025-07-30 10:51:54 +02:00
Mike Inouye 0314db80ea Correctly reset Verific flags to Yosys defaults after -import and warn this has occurred.
Co-authored-by: Chris Pearce <chris@pearce.org.nz>
Signed-off-by: Mike Inouye <mikeinouye@google.com>
2025-07-25 19:15:01 +00:00
Akash Levy 082adf8684
Merge branch 'YosysHQ:main' into main 2025-07-15 00:04:28 -04:00
N. Engelhardt e47f5369fd verificsva: check -L value is small enough for code to work 2025-07-09 15:58:35 +02:00
N. Engelhardt 642756a9c6
Merge pull request #5178 from jix/sva_cover_only_followed_by 2025-07-07 10:07:06 +02:00
Akash Levy fbc8aa46d4
Merge branch 'YosysHQ:main' into main 2025-07-04 13:37:04 -04:00
Miodrag Milanovic eed3bc243f verific: enable replacing const exprs in static elaboration by default 2025-07-02 11:54:19 +02:00
Jannis Harder f019e44e74 verificsva: Support the followed-by operator in cover mode
The implementation for the implication operator in cover mode actually
implements the followed-by operator, so we can re-use it unchanged.

It is not always the correct behavior for the implication operator in
cover mode, but a) it will only cause false positives not miss anything
so if the behavior is unexpected it will be visible in the produced
traces, b) it is unlikely to make a difference for most properties one
would practically use in cover mode, c) at least one other widely used
SVA implementations behaves the same way and d) it's not clear whether
we can fix this without rewriting most of verificsva.cc
2025-06-13 21:27:31 +02:00
Akash Levy 64d99416c1 Do not downgrade any warnings 2025-06-09 15:11:00 -07:00
Akash Levy 447a73ea86
Merge branch 'YosysHQ:main' into main 2025-06-09 14:51:56 -07:00
N. Engelhardt f22248f056 downgrade verific warnings about common coding styles 2025-06-06 16:30:50 +02:00
Akash Levy e50a5974f7 Get rid of SYNTHESIS redefinition warning 2025-05-28 08:33:56 +02:00
Akash Levy 3a23e772dd
Merge branch 'YosysHQ:main' into main 2025-05-24 12:11:52 -07:00
Emil J. Tywoniak e5171d6aa1 verific: support single_bit_vector 2025-05-12 13:23:29 +02:00
Akash Levy 3bcbfe4dde verific -set_relaxed_file_libext_modes 2025-05-08 23:43:23 -07:00
Akash Levy f3d24aea76 Add spaces in verific 2025-05-08 22:24:10 -07:00
Akash Levy 380850321d Refactor verific -optimization and -no_split_complex_ports into verific pass 2025-05-08 15:59:47 -07:00
Akash Levy 618cf9d372
Merge branch 'YosysHQ:main' into main 2025-04-28 13:57:29 -07:00
Miodrag Milanovic 22e6ce4282 verific: bit blast RAM if using mem2reg attribute 2025-04-14 15:24:11 +02:00
Akash Levy 61715c2c28 Fix memory too large issue 2025-04-04 03:22:22 -07:00
Akash Levy f218b5ba58 Revert "Represent memory size with size_t"
This reverts commit bb5f8415af.
2025-04-04 03:20:07 -07:00
Akash Levy bb5f8415af Represent memory size with size_t 2025-04-04 02:04:34 -07:00
Akash Levy 4bd08ac362
Merge branch 'YosysHQ:main' into main 2025-04-01 22:10:43 -07:00
Miodrag Milanovic 72f2185a94 verific: fix restoring msg state after blackbox import 2025-04-01 17:35:59 +02:00
Akash Levy d2028feefe Set Verific flags via -cfg instead of in Yosys 2025-03-25 22:41:06 -07:00
Akash Levy 95f489beec Merge nice gzip refactor 2025-03-20 16:47:12 -07:00
Emil J. Tywoniak 4f3fdc8457 io: refactor string and file work into new unit 2025-03-19 13:43:42 +01:00
Alain Dargelas 3021dab37d memory limit fix and increased limit 2025-03-17 09:07:33 -07:00
Akash Levy bc3ca6210c Add back operator optimization for Verific frontend 2025-03-17 04:06:28 -07:00
Akash Levy 1c0d4a43b3
Merge branch 'YosysHQ:main' into main 2025-03-14 18:07:55 -07:00
Alain Dargelas 88211310fa code review 2025-03-12 16:32:42 -07:00
Alain Dargelas dcce15207e Memory size check 2025-03-12 16:21:18 -07:00
Jason Xu a5f34d04f8 Address comments 2025-03-11 18:50:44 -04:00
Jason Xu 98eefc5d1a Add file list support to read pass 2025-03-07 20:44:21 -05:00
Akash Levy fd811ddaee Cleanup 2025-02-14 08:48:27 -08:00
Akash Levy f76fd9280b Clean up Verific 2025-02-14 06:56:20 -08:00
Akash Levy c8c97ea00b Revert back to using Verific naming 2025-02-13 19:40:33 -08:00
Akash Levy 47aac95f64 Fix incdir, ydir, libext issues 2025-02-05 05:58:49 -08:00
Akash Levy bd439fc524 Reapply "Merge upstream"
This reverts commit e73d51dbf0.
2025-01-23 13:40:32 -08:00
Akash Levy e73d51dbf0 Revert "Merge upstream"
This reverts commit c58a50f880, reversing
changes made to a1c3c98773.
2025-01-21 05:28:36 -08:00
Akash Levy c58a50f880 Merge upstream 2025-01-21 04:36:34 -08:00
Akash Levy a1c3c98773 Messed up usage of SILIMATE_VERIFIC_EXTENSIONS 2025-01-21 00:12:28 -08:00
Akash Levy da726a4e54 If imported module has parameters it is not a blackbox 2025-01-17 01:14:40 -08:00