Commit Graph

623 Commits

Author SHA1 Message Date
Akash Levy 7c70026610 Fix verific issue 2026-02-01 00:16:10 -08:00
Akash Levy bdc9ad9f53 Bump version 2026-01-30 19:29:00 -08:00
Akash Levy a9cf998f9f Merge from upstream 2026-01-29 17:46:44 -08:00
Miodrag Milanovic b70f527c67 verific: fixed -sv2017 option and added ability to set VHDL standard if applicable 2026-01-29 10:32:30 +01:00
Natalia 8d504ecb48 verific: use MFCU for SV file list 2026-01-29 00:03:28 -08:00
Natalia 188082551a verific: only use MFCU when VHDL present 2026-01-28 03:37:08 -08:00
nataliakokoromyti f3c87610f5 verific: allow mixed SV/VHDL in -f files 2026-01-24 23:46:45 -08:00
Akash Levy b11037e6c6 Merge remote-tracking branch 'upstream/main' 2026-01-21 15:13:57 -08:00
Miodrag Milanovic d0fa4781c6 verific: Fix -sv2017 message and formatting 2026-01-20 08:07:26 +01:00
Miodrag Milanovic cc3038f468 verific: Fix -sv2017 message 2026-01-19 16:32:46 +01:00
Miodrag Milanovic d095d2c405 verific: add explicit System Verilog 2017 option 2026-01-16 07:56:53 +01:00
Akash Levy 1941e8f042 Bump yosys and abc to latest 2025-12-25 03:46:16 -05:00
N. Engelhardt 45d654e2d7 avoid merging formal properties 2025-12-17 20:25:24 +01:00
Akash Levy 76c12f8f8c
Merge branch 'YosysHQ:main' into main 2025-11-03 13:38:04 -05:00
Mohamed Gaber dec28f65ae
Merge remote-tracking branch 'donn/pyosys_bugfixes' into merge_pybind11 2025-10-26 02:39:43 +03:00
Robert O'Callahan 25aafab86b Set `port_id` for Verific PortBus wires 2025-10-23 20:51:53 +00:00
Miodrag Milanovic 1f11b2c529 verific: Add src to message missed in #5406 2025-10-13 15:16:17 +02:00
Miodrag Milanovic dc959cdf4a verific: Fix error compiling without VERIFIC_LINEFILE_INCLUDES_COLUMNS 2025-10-13 15:16:17 +02:00
Miodrag Milanovic 9570b39519 verifix: fix bits() deprecation warnings 2025-10-13 09:57:22 +02:00
Miodrag Milanovic 2f8f421dee verifix: fix bits() deprecation warnings 2025-10-13 09:47:18 +02:00
Akash Levy 54653fc82c Reenable Verific opt and comment out clock enable muxing 2025-10-12 07:52:32 -07:00
Akash Levy 6993fc2540 Flush during import 2025-10-12 07:52:12 -07:00
N. Engelhardt 0b6adf832b verific: print source location of problematic object on import error (if available) 2025-10-03 12:57:49 +02:00
Akash Levy 623c54d513 Only do SFCU if has VHDL 2025-10-02 06:02:39 -07:00
Akash Levy 16215b8786 Merge upstream 2025-09-29 20:58:56 -07:00
Akash Levy 507d43a9b8 Fixups 2025-09-28 06:16:07 -07:00
Jannis Harder 4bb4b6c662 verific: Extend -sva-continue-on-err to handle FSM explosion
This also rolls back any added cells and wires, since we might have
added a lot of helper logic by the point we detect this.
2025-09-27 21:13:02 +02:00
Jannis Harder 83dd99efb7 verific: New `-sva-continue-on-error` import option
This option allows you to process a design that includes unsupported
SVA. Unsupported SVA gets imported as formal cells using 'x inputs and
with the `unsupported_sva` attribute set. This allows you to get a
complete list of defined properties or to check only a supported subset
of properties. To ensure no properties are unintentionally skipped for
actual verification, even in cases where `-sva-continue-on-error` is
used by default to read and inspect a design, `hierarchy -simcheck` and
`hierarchy -smtcheck` (run by SBY) now ensure that no `unsupported_sva`
property cells remain in the design.
2025-09-24 18:58:54 +02:00
Akash Levy 60d969530b Bump to latest 2025-09-21 01:10:04 -07:00
Robert O'Callahan a7c46f7b4a Remove .c_str() calls from parameters to log_warning()/log_warning_noprefix() 2025-09-16 23:02:16 +00:00
Robert O'Callahan 5ac6858f26 Remove .c_str() from log_cmd_error() and log_file_error() parameters 2025-09-16 22:59:08 +00:00
Robert O'Callahan 1a367b907c Use fast path for 32-bit Const integer constructor in more places 2025-09-16 03:17:24 +00:00
Akash Levy f5cb0c328f Bump Yosys to latest 2025-09-13 04:35:52 -07:00
Robert O'Callahan e0ae7b7af4 Remove .c_str() calls from log()/log_error()
There are some leftovers, but this is an easy regex-based approach that removes most of them.
2025-09-11 20:59:37 +00:00
Akash Levy 1b3375d8df Merge upstream in 2025-09-09 05:50:48 -07:00
Robert O'Callahan c7df6954b9 Remove .c_str() from stringf parameters 2025-09-01 23:34:42 +00: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