diff --git a/docs/guide/warnings.rst b/docs/guide/warnings.rst index 1f918ed6d..4f730d800 100644 --- a/docs/guide/warnings.rst +++ b/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 diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index e10b43108..58f6d65c0 100644 --- a/src/V3AssertNfa.cpp +++ b/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())) { diff --git a/src/V3Error.h b/src/V3Error.h index dcd419c31..eb5398442 100644 --- a/src/V3Error.h +++ b/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", diff --git a/test_regress/t/t_sequence_intersect_nevermatch.py b/test_regress/t/t_sequence_intersect_nevermatch.py index ddef50cab..a3efd6944 100755 --- a/test_regress/t/t_sequence_intersect_nevermatch.py +++ b/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() diff --git a/test_regress/t/t_sequence_intersect_nevermatch_bad.out b/test_regress/t/t_sequence_intersect_nevermatch_bad.out new file mode 100644 index 000000000..444405282 --- /dev/null +++ b/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 diff --git a/test_regress/t/t_sequence_intersect_nevermatch_bad.py b/test_regress/t/t_sequence_intersect_nevermatch_bad.py new file mode 100755 index 000000000..9dc9e0917 --- /dev/null +++ b/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()