Add NEVERMATCH warning when an SVA sequence can never match (#8176) (#8183)

Signed-off-by: Artur Bieniek <[email protected]>

docs/guide/warnings.rst

@@ -1556,6 +1556,19 @@ List Of Warnings
    (neither :vlopt:`--timing` nor :vlopt:`--no-timing` option was provided).
 
 
+.. option:: NEVERMATCH
+
+   Warns that an SVA sequence is statically known to never match. Such a
+   sequence is legal SystemVerilog and is fully supported, the warning
+   only highlights a potential problem. For example, using the sequence as
+   the antecedent of an implication causes the implication to pass
+   vacuously. For an intersect sequence, ensure its operands can match
+   over a common length (IEEE 1800-2023 16.9.6).
+
+   Ignoring this warning will only suppress the lint check; it will
+   simulate correctly.
+
+
 .. option:: NEWERSTD
 
    Warns that a feature requires a newer standard of Verilog or SystemVerilog

src/V3AssertNfa.cpp

@@ -1087,7 +1087,11 @@ class SvaNfaBuilder final {
             nodep->v3warn(E_UNSUPPORTED, "Unsupported: within with ranged cycle-delay operand");
             return BuildResult::failWithError();
         }
-        if (innerLen > outerLen) return buildNeverMatchIntersect(nodep, entryVtxp, isTopLevelStep);
+        if (innerLen > outerLen) {
+            return buildNeverMatchIntersect(
+                nodep, entryVtxp, isTopLevelStep,
+                "the inner sequence is longer than the outer sequence");
+        }
         FileLine* const flp = nodep->fileline();
         const int slack = outerLen - innerLen;
         AstNodeExpr* innerOrp = nullptr;
@@ -1238,7 +1242,8 @@ class SvaNfaBuilder final {
     // simply never matches. This is legal (matching nothing), not an error, so
     // lower to a constant false rather than rejecting legal code.
     BuildResult buildNeverMatchIntersect(AstNodeExpr* nodep, SvaStateVertex* entryVtxp,
-                                         bool isTopLevelStep) {
+                                         bool isTopLevelStep, const char* reason) {
+        nodep->v3warn(NEVERMATCH, "Sequence can never match because " << reason << ".");
         AstNodeExpr* const falsep = new AstConst{nodep->fileline(), AstConst::BitFalse{}};
         return buildFromLoweringTree(falsep, entryVtxp, isTopLevelStep);
     }
@@ -1269,7 +1274,8 @@ class SvaNfaBuilder final {
         const int hi = std::min(lhsRange.second, rhsRange.second);
         if (lo > hi) {
             // Disjoint length ranges share no common length -> never matches.
-            return buildNeverMatchIntersect(nodep, entryVtxp, isTopLevelStep);
+            return buildNeverMatchIntersect(nodep, entryVtxp, isTopLevelStep,
+                                            "intersect operands have no common length");
         }
         FileLine* const flp = nodep->fileline();
         if (lo == hi) {
@@ -1599,7 +1605,8 @@ public:
             if (lhsLen >= 0 && rhsLen >= 0) {
                 if (lhsLen != rhsLen) {
                     // Unequal fixed lengths share no common length -> never matches.
-                    return buildNeverMatchIntersect(intp, entryVtxp, isTopLevelStep);
+                    return buildNeverMatchIntersect(intp, entryVtxp, isTopLevelStep,
+                                                    "intersect operands have no common length");
                 }
                 if (AstNodeExpr* const conjp
                     = conjoinFixedSeqs(intp->lhsp(), intp->rhsp(), intp->fileline())) {

src/V3Error.h

@@ -137,6 +137,7 @@ public:
         MULTIDRIVEN,    // Driven from multiple blocks
         MULTIDRIVENPROC,  // Driven from multiple plain always blocks
         MULTITOP,       // Multiple top level modules
+        NEVERMATCH,     // Sequence can never match
         NEWERSTD,       // Newer language standard required
         NOEFFECT,       // Statement has no effect
         NOLATCH,        // No latch detected in always_latch block
@@ -235,8 +236,8 @@ public:
             "IEEEMAYDEPRECATE", "IFDEPTH", "IGNOREDRETURN", "IMPERFECTSCH", "IMPLICIT",
             "IMPLICITSTATIC", "IMPORTSTAR", "IMPURE", "INCABSPATH", "INFINITELOOP", "INITIALDLY",
             "INSECURE", "INSIDETRUE", "LATCH", "LITENDIAN", "MINTYPMAXDLY", "MISINDENT", "MODDUP",
-            "MODMISSING", "MULTIDRIVEN", "MULTIDRIVENPROC", "MULTITOP", "NEWERSTD", "NOEFFECT",
-            "NOLATCH", "NONSTD", "NORETURN", "NOTREDOP", "NULLPORT", "PARAMNODEFAULT",
+            "MODMISSING", "MULTIDRIVEN", "MULTIDRIVENPROC", "MULTITOP", "NEVERMATCH", "NEWERSTD",
+            "NOEFFECT", "NOLATCH", "NONSTD", "NORETURN", "NOTREDOP", "NULLPORT", "PARAMNODEFAULT",
             "PINCONNECTEMPTY", "PINMISSING", "PINNOCONNECT", "PINNOTFOUND", "PKGNODECL",
             "PREPROCZERO", "PROCASSINIT", "PROCASSWIRE", "PROFOUTOFDATE", "PROTECTED",
             "PROTOTYPEMIS", "RANDC", "REALCVT", "REDEFMACRO", "RISEFALLDLY", "SELRANGE",

test_regress/t/t_sequence_intersect_nevermatch.py

@@ -11,7 +11,7 @@ import vltest_bootstrap
 
 test.scenarios('simulator')
 
-test.compile(verilator_flags2=['--assert --timing'])
+test.compile(verilator_flags2=['--assert --timing -Wno-NEVERMATCH'])
 
 test.execute()
 

test_regress/t/t_sequence_intersect_nevermatch_bad.out

@@ -0,0 +1,15 @@
+%Warning-NEVERMATCH: t/t_sequence_intersect_nevermatch.v:47:53: Sequence can never match because intersect operands have no common length.
+                                                              : ... note: In instance 't'
+   47 |   assert property (disable iff (cyc < 2) ((a ##2 b) intersect (c ##3 d)) |-> 1'b0)
+      |                                                     ^~~~~~~~~
+                     ... For warning description see https://verilator.org/warn/NEVERMATCH?v=latest
+                     ... Use "/* verilator lint_off NEVERMATCH */" and lint_on around source to disable this message.
+%Warning-NEVERMATCH: t/t_sequence_intersect_nevermatch.v:52:57: Sequence can never match because intersect operands have no common length.
+                                                              : ... note: In instance 't'
+   52 |   assert property (disable iff (cyc < 2) ((a ##[1:2] b) intersect (c ##[4:5] d)) |-> 1'b0)
+      |                                                         ^~~~~~~~~
+%Warning-NEVERMATCH: t/t_sequence_intersect_nevermatch.v:57:53: Sequence can never match because the inner sequence is longer than the outer sequence.
+                                                              : ... note: In instance 't'
+   57 |   assert property (disable iff (cyc < 2) ((a ##3 b) within (c ##1 d)) |-> 1'b0)
+      |                                                     ^~~~~~
+%Error: Exiting due to

test_regress/t/t_sequence_intersect_nevermatch_bad.py

@@ -0,0 +1,19 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# This program is free software; you can redistribute it and/or modify it
+# under the terms of either the GNU Lesser General Public License Version 3
+# or the Perl Artistic License Version 2.0.
+# SPDX-FileCopyrightText: 2026 Wilson Snyder
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('vlt')
+test.top_filename = 't/t_sequence_intersect_nevermatch.v'
+
+test.compile(verilator_flags2=['--assert --timing'],
+             fails=True,
+             expect_filename=test.golden_filename)
+
+test.passes()