diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index bf50e97a1..7dfdaaca8 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -77,6 +77,10 @@ public: AstNodeExpr* m_andRhsCondp = nullptr; // OWNED; RHS final condition (may be nullptr) // Reject sink for SAnd rejectOnFail wiring; not a state-signal source bool m_isRejectSink = false; + // In-window vertex of a strong s_always[m:n]: if its state is still set at + // end-of-simulation the universal-quantifier window never completed, which is + // a liveness failure (IEEE 1800-2023 16.12.11 strong semantics). + bool m_strongPending = false; // CONSTRUCTORS explicit SvaStateVertex(V3Graph* graphp) @@ -198,6 +202,7 @@ class SvaNfaBuilder final { // (IEEE 1800-2023 16.12.14 outer-wraps-inner). std::vector m_outerAbortStack; bool m_inUnboundedScope = false; // Sticky: nodes created after inherit liveness + bool m_markStrongPending = false; // Mark new vertices as strong s_always in-window AstNodeExpr* throughoutCond(AstNodeExpr* baseCondp, FileLine* flp) { if (m_throughoutStack.empty()) return baseCondp; @@ -330,6 +335,7 @@ class SvaNfaBuilder final { vtxp->m_throughoutConds.push_back(cp->cloneTreePure(false)); } if (m_inUnboundedScope) vtxp->m_isUnbounded = true; + if (m_markStrongPending) vtxp->m_strongPending = true; return vtxp; } @@ -577,10 +583,37 @@ class SvaNfaBuilder final { FileLine* const flp = nodep->fileline(); AstNodeExpr* const propp = nodep->propp(); const int lo = getConstInt(nodep->loBoundp()); + if (VN_IS(nodep->hiBoundp(), Unbounded)) { + // Weak always [lo:$]: unbounded upper bound (IEEE 1800-2023 16.12.11). + // p must hold at every clock tick at least lo cycles after the attempt + // start; those ticks are not required to exist, so there is no + // end-of-trace obligation (weak). The self-loop keeps the attempt live + // every cycle; each observed cycle is a safety obligation, so a false p + // rejects immediately. + UASSERT_OBJ(!nodep->isStrong() && lo >= 0, nodep, + "Unbounded always must be weak with non-negative lo (V3Width)"); + SvaStateVertex* const livep = addDelayChain(entryVtxp, lo, flp); + livep->m_isUnbounded = true; + guardedEdge(livep, livep, flp); // stay active every subsequent cycle + SvaStateVertex* const sinkp = m_graph.createStateVertex(); + sinkp->m_isRejectSink = true; + SvaTransEdge* const rejEdgep + = guardedLink(livep, sinkp, sampled(propp->cloneTreePure(false)), flp); + if (isTopLevelStep) rejEdgep->m_rejectOnFail = true; + return {livep, nullptr, {}}; + } const int hi = getConstInt(nodep->hiBoundp()); UASSERT_OBJ(lo >= 0 && hi >= lo, nodep, "PropAlways bounds invariant (V3Width)"); if (exceedsAssertUnrollLimit(nodep, hi - lo + 1)) return BuildResult::failWithError(); AstVar* const hoistVarp = tryHoistSampled(propp, flp, hi - lo + 1); + // Strong s_always[m:n]: mark every in-window registered vertex so an + // attempt still mid-window at end-of-simulation is reported as a liveness + // failure (IEEE strong: the n+1 ticks must exist). An attempt that has + // completed earlier in the trace has already cleared its state, so it is + // not flagged; an attempt whose final tick coincides with $finish is still + // flagged, matching the strong reference. Weak always[m:n] is not marked. + VL_RESTORER(m_markStrongPending); + m_markStrongPending = nodep->isStrong(); SvaStateVertex* currentp = addDelayChain(entryVtxp, lo, flp); for (int k = 0; k <= hi - lo; ++k) { if (k > 0) { @@ -1740,6 +1773,36 @@ public: flp, isCover, negated, matchCondp, sigs.terminalActivep, sigs.rejectBasep, sigs.throughoutRejectp, sigs.requiredStepRejectp, outMatchpp); + // Strong s_always[m:n] end-of-simulation liveness: if any in-window state + // is still set at $finish, the universal-quantifier window never completed + // (IEEE 1800-2023 16.12.11 strong semantics). Fire the assertion failure + // from a final block; V3Assert turns the DT_ERROR display into the standard + // "Assertion failed in %m" message. + AstNodeExpr* pendingp = nullptr; + for (int i = 0; i < N; ++i) { + if (!vtx[i]->m_strongPending || !vtx[i]->datap()->stateVarp) continue; + AstNodeExpr* const svp = new AstVarRef{flp, vtx[i]->datap()->stateVarp, VAccess::READ}; + if (!pendingp) { + pendingp = svp; + } else { + pendingp = new AstLogOr{flp, pendingp, svp}; + pendingp->dtypeSetBit(); + } + } + if (pendingp) { + AstCExpr* const assertOnp + = new AstCExpr{flp, AstCExpr::Pure{}, "vlSymsp->_vm_contextp__->assertOn()", 1}; + assertOnp->dtypeSetBit(); + AstNodeExpr* const condp = new AstLogAnd{flp, assertOnp, pendingp}; + condp->dtypeSetBit(); + AstDisplay* const dispp + = new AstDisplay{flp, VDisplayType::DT_ERROR, "", nullptr, nullptr}; + dispp->fmtp()->timeunit(m_modp->timeunit()); + AstNodeStmt* firep = dispp; + if (v3Global.opt.stopFail()) firep->addNext(new AstStop{flp, false}); + m_modp->addStmtsp(new AstFinal{flp, new AstIf{flp, condp, firep}}); + } + // Clear userp on every vertex before vertexData unique_ptrs are destroyed. for (int i = 0; i < N; ++i) vtx[i]->userp(nullptr); return resultp; diff --git a/src/V3Width.cpp b/src/V3Width.cpp index 861714e34..876ea7454 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -1564,13 +1564,18 @@ class WidthVisitor final : public VNVisitor { } const bool loUnbounded = VN_IS(nodep->loBoundp(), Unbounded); const bool hiUnbounded = VN_IS(nodep->hiBoundp(), Unbounded); - if (loUnbounded || hiUnbounded) { - if (nodep->isStrong()) { - nodep->v3error("s_always range must be bounded (IEEE 1800-2023 16.12.11)"); - } else { - nodep->v3warn(E_UNSUPPORTED, - "Unsupported: unbounded always range (always [m:$])"); - } + // Strong always must be bounded (IEEE 1800-2023 16.12.11: "the range + // for a strong always shall be bounded"). Weak always [m:$] is legal: + // an unbounded upper bound imposes no end-of-trace obligation. + if (nodep->isStrong() && (loUnbounded || hiUnbounded)) { + nodep->v3error("s_always range must be bounded (IEEE 1800-2023 16.12.11)"); + nodep->dtypeSetBit(); + return; + } + if (loUnbounded) { + // Only the high bound may be $ (cycle_delay_const_range_expression). + nodep->v3error("always range low bound must be a constant expression" + " (IEEE 1800-2023 16.12.11)"); nodep->dtypeSetBit(); return; } @@ -1580,7 +1585,7 @@ class WidthVisitor final : public VNVisitor { nodep->v3error("always range low bound must be a constant expression" " (IEEE 1800-2023 16.12.11)"); } - if (!hiConstp) { + if (!hiUnbounded && !hiConstp) { nodep->v3error("always range high bound must be a constant expression" " (IEEE 1800-2023 16.12.11)"); } @@ -1588,7 +1593,7 @@ class WidthVisitor final : public VNVisitor { nodep->v3error("always range low bound must be non-negative" " (IEEE 1800-2023 16.12.11)"); } - if (loConstp && hiConstp && hiConstp->toSInt() < loConstp->toSInt()) { + if (!hiUnbounded && loConstp && hiConstp && hiConstp->toSInt() < loConstp->toSInt()) { nodep->v3error("always range high bound must be >= low bound" " (IEEE 1800-2023 16.12.11)"); } diff --git a/test_regress/t/t_assert_always_unbounded.py b/test_regress/t/t_assert_always_unbounded.py new file mode 100755 index 000000000..2351d6963 --- /dev/null +++ b/test_regress/t/t_assert_always_unbounded.py @@ -0,0 +1,18 @@ +#!/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.compile() + +test.execute() + +test.passes() diff --git a/test_regress/t/t_assert_always_unbounded.v b/test_regress/t/t_assert_always_unbounded.v new file mode 100644 index 000000000..9f41a2627 --- /dev/null +++ b/test_regress/t/t_assert_always_unbounded.v @@ -0,0 +1,57 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 PlanV GmbH +// SPDX-License-Identifier: CC0-1.0 + +// verilog_format: off +`define stop $stop +`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); +// verilog_format: on + +module t ( + input clk +); + + int cyc = 0; + logic a_high = 1'b1; + logic a_low = 1'b0; + logic a_drop = 1'b1; + + // Weak always [m:$] is a pure safety property: it has no end-of-trace + // obligation, so it can only fail (else fires), once per failing tick. + int high_fail_q[$]; + int low0_fail_q[$]; + int low2_fail_q[$]; + int drop_fail_q[$]; + + // Constant-true input: never fails at any tick. + assert property (@(posedge clk) always [2:$] a_high) else high_fail_q.push_back(cyc); + + // Constant-false input, m=0: fails at every observed tick. + assert property (@(posedge clk) always [0:$] a_low) else low0_fail_q.push_back(cyc); + + // Constant-false input, m=2: fails at every tick once the window is live. + assert property (@(posedge clk) always [2:$] a_low) else low2_fail_q.push_back(cyc); + + // a_drop is high then drops at cyc 5 and stays low: deterministic single + // transition, so Verilator and Questa agree on the failing ticks exactly. + assert property (@(posedge clk) always [2:$] a_drop) else drop_fail_q.push_back(cyc); + + always @(posedge clk) begin + cyc <= cyc + 1; + if (cyc >= 4) a_drop <= 1'b0; + if (cyc == 19) begin + // Counts pinned to Verilator (NFA per-cycle reject). For all-fail windows + // Questa is one lower (it does not fire the end-of-sim tick); see the sva + // lessons "multi-cycle end-of-simulation offset" note. + `checkd(high_fail_q.size(), 0); // Questa: 0 + `checkd(low0_fail_q.size(), 20); // Questa: 19 + `checkd(low2_fail_q.size(), 18); // Questa: 17 + `checkd(drop_fail_q[0], 5); // first fail tick: a_drop sampled low from cyc 5 + $write("*-* All Finished *-*\n"); + $finish; + end + end + +endmodule diff --git a/test_regress/t/t_assert_always_unbounded_bad.out b/test_regress/t/t_assert_always_unbounded_bad.out new file mode 100644 index 000000000..39f1983cf --- /dev/null +++ b/test_regress/t/t_assert_always_unbounded_bad.out @@ -0,0 +1,10 @@ +%Error: t/t_assert_always_unbounded_bad.v:13:35: s_always range must be bounded (IEEE 1800-2023 16.12.11) + : ... note: In instance 't' + 13 | assert property (@(posedge clk) s_always a); + | ^~~~~~~~ + ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. +%Error: t/t_assert_always_unbounded_bad.v:14:35: s_always range must be bounded (IEEE 1800-2023 16.12.11) + : ... note: In instance 't' + 14 | assert property (@(posedge clk) s_always [2:$] a); + | ^~~~~~~~ +%Error: Exiting due to diff --git a/test_regress/t/t_assert_always_unbounded_bad.py b/test_regress/t/t_assert_always_unbounded_bad.py new file mode 100755 index 000000000..77a0ac64b --- /dev/null +++ b/test_regress/t/t_assert_always_unbounded_bad.py @@ -0,0 +1,16 @@ +#!/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.lint(expect_filename=test.golden_filename, fails=True) + +test.passes() diff --git a/test_regress/t/t_assert_always_unbounded_bad.v b/test_regress/t/t_assert_always_unbounded_bad.v new file mode 100644 index 000000000..e07e7a3bc --- /dev/null +++ b/test_regress/t/t_assert_always_unbounded_bad.v @@ -0,0 +1,16 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 PlanV GmbH +// SPDX-License-Identifier: CC0-1.0 + +module t (input clk); + logic a; + + // A strong always must be bounded (IEEE 1800-2023 16.12.11): there is no bare + // s_always grammar production, and s_always [m:$] is the explicit "// Illegal" + // example (p5). Both forms are rejected. + assert property (@(posedge clk) s_always a); + assert property (@(posedge clk) s_always [2:$] a); + +endmodule diff --git a/test_regress/t/t_prop_always.v b/test_regress/t/t_prop_always.v index 3f54b1023..6e9fef867 100644 --- a/test_regress/t/t_prop_always.v +++ b/test_regress/t/t_prop_always.v @@ -24,7 +24,6 @@ module t ( // For "always [m:n] P" the action runs at cyc=K+n on success and at the // detected-violation cyc on failure -- both deterministic given the inputs. int high_bounded_pass_q[$]; - int high_sbounded_pass_q[$]; int high_degenerate_pass_q[$]; int low_bounded_fail_q[$]; int low_degenerate_fail_q[$]; @@ -39,8 +38,8 @@ module t ( // Bounded weak always over constant-true input. assert property (@(posedge clk) always [0:3] a_high) high_bounded_pass_q.push_back(cyc); - // Bounded strong s_always over constant-true input. - assert property (@(posedge clk) s_always [1:2] a_high) high_sbounded_pass_q.push_back(cyc); + // Strong s_always[m:n] (including its end-of-simulation liveness) is covered + // by t_prop_s_always_liveness; this file stays a pure pass/fail suite. // Degenerate [0:0]: equivalent to immediate sample. assert property (@(posedge clk) always [0:0] a_high) high_degenerate_pass_q.push_back(cyc); @@ -83,10 +82,6 @@ module t ( `checkd(high_bounded_pass_q.size(), 17); `checkd(high_bounded_pass_q[0], 3); `checkd(high_bounded_pass_q[$], 19); - // Strong [1:2]: K=0..17 succeed at cyc K+2 = 2..19. - `checkd(high_sbounded_pass_q.size(), 18); - `checkd(high_sbounded_pass_q[0], 2); - `checkd(high_sbounded_pass_q[$], 19); // Degenerate [0:0]: K=0..19 succeed at cyc K = 0..19. `checkd(high_degenerate_pass_q.size(), 20); `checkd(high_degenerate_pass_q[0], 0); diff --git a/test_regress/t/t_prop_always_unsup.out b/test_regress/t/t_prop_always_unsup.out index 52bd14918..3bc897181 100644 --- a/test_regress/t/t_prop_always_unsup.out +++ b/test_regress/t/t_prop_always_unsup.out @@ -1,18 +1,14 @@ -%Error-UNSUPPORTED: t/t_prop_always_unsup.v:12:35: Unsupported: unbounded always range (always [m:$]) +%Error-UNSUPPORTED: t/t_prop_always_unsup.v:12:35: Unsupported: property/sequence operator inside bounded always (IEEE 1800-2023 16.12.11) : ... note: In instance 't' - 12 | assert property (@(posedge clk) always [2:$] a); + 12 | assert property (@(posedge clk) always [0:3] (a |-> b)); | ^~~~~~ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error-UNSUPPORTED: t/t_prop_always_unsup.v:15:35: Unsupported: property/sequence operator inside bounded always (IEEE 1800-2023 16.12.11) +%Error-UNSUPPORTED: t/t_prop_always_unsup.v:13:35: Unsupported: property/sequence operator inside bounded always (IEEE 1800-2023 16.12.11) : ... note: In instance 't' - 15 | assert property (@(posedge clk) always [0:3] (a |-> b)); + 13 | assert property (@(posedge clk) always [0:3] (a |=> b)); | ^~~~~~ -%Error-UNSUPPORTED: t/t_prop_always_unsup.v:16:35: Unsupported: property/sequence operator inside bounded always (IEEE 1800-2023 16.12.11) +%Error-UNSUPPORTED: t/t_prop_always_unsup.v:14:35: Unsupported: property/sequence operator inside bounded always (IEEE 1800-2023 16.12.11) : ... note: In instance 't' - 16 | assert property (@(posedge clk) always [0:3] (a |=> b)); - | ^~~~~~ -%Error-UNSUPPORTED: t/t_prop_always_unsup.v:17:35: Unsupported: property/sequence operator inside bounded always (IEEE 1800-2023 16.12.11) - : ... note: In instance 't' - 17 | assert property (@(posedge clk) always [0:3] (a ##1 b)); + 14 | assert property (@(posedge clk) always [0:3] (a ##1 b)); | ^~~~~~ %Error: Exiting due to diff --git a/test_regress/t/t_prop_always_unsup.v b/test_regress/t/t_prop_always_unsup.v index 7013c9fff..998516d7d 100644 --- a/test_regress/t/t_prop_always_unsup.v +++ b/test_regress/t/t_prop_always_unsup.v @@ -8,9 +8,6 @@ module t (input clk); logic a; logic b; - // IEEE-legal but engine has no sim-end liveness. - assert property (@(posedge clk) always [2:$] a); - // Nested sequence/property operators inside bounded always. assert property (@(posedge clk) always [0:3] (a |-> b)); assert property (@(posedge clk) always [0:3] (a |=> b)); diff --git a/test_regress/t/t_prop_always_wide.v b/test_regress/t/t_prop_always_wide.v index a0e297293..d631ffa6b 100644 --- a/test_regress/t/t_prop_always_wide.v +++ b/test_regress/t/t_prop_always_wide.v @@ -15,16 +15,15 @@ module t ( int cyc = 0; logic a_high = 1'b1, b_high = 1'b1, c_high = 1'b1; - int wide_pass_q[$], wide_strong_pass_q[$]; + int wide_pass_q[$]; // Wide range with multi-operand pure propp -- exercises the shared // $sampled(propp) hoist path; pre-fix would clone propp 33 times. assert property (@(posedge clk) always[1: 33] (a_high && b_high && c_high)) wide_pass_q.push_back(cyc); - // Wide strong s_always over the same expression (in-window matches weak). - assert property (@(posedge clk) s_always[1: 33] (a_high && b_high && c_high)) - wide_strong_pass_q.push_back(cyc); + // Strong wide s_always (and its end-of-simulation liveness) is covered by + // t_prop_s_always_liveness. always @(posedge clk) begin cyc <= cyc + 1; @@ -33,9 +32,6 @@ module t ( `checkd(wide_pass_q.size(), 17); `checkd(wide_pass_q[0], 33); `checkd(wide_pass_q[$], 49); - `checkd(wide_strong_pass_q.size(), 17); - `checkd(wide_strong_pass_q[0], 33); - `checkd(wide_strong_pass_q[$], 49); $write("*-* All Finished *-*\n"); $finish; end diff --git a/test_regress/t/t_prop_s_always_liveness.py b/test_regress/t/t_prop_s_always_liveness.py new file mode 100755 index 000000000..91b8bb235 --- /dev/null +++ b/test_regress/t/t_prop_s_always_liveness.py @@ -0,0 +1,23 @@ +#!/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.compile(verilator_flags2=['--assert']) + +# a is always 1 so there is no per-cycle safety failure: the ONLY failure source +# is the strong end-of-simulation liveness obligation of s_always[1:1] (its window +# is cut off by $finish), so the simulation must exit non-zero. If the in-window +# marking regresses (e.g. the offset-hi vertex stops being flagged), s_always[1:1] +# goes silent, the run succeeds, and this test fails -- catching the regression. +test.execute(fails=True) + +test.passes() diff --git a/test_regress/t/t_prop_s_always_liveness.v b/test_regress/t/t_prop_s_always_liveness.v new file mode 100644 index 000000000..f7958f33c --- /dev/null +++ b/test_regress/t/t_prop_s_always_liveness.v @@ -0,0 +1,42 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 PlanV GmbH +// SPDX-License-Identifier: CC0-1.0 + +module t ( + input clk +); + + int cyc = 0; + logic a = 1'b1; + logic rst = 1'b1; + + always @(posedge clk) begin + cyc <= cyc + 1; + if (cyc == 0) rst <= 1'b0; + end + + // a is always 1, so there is no per-cycle safety failure. The ONLY way these + // can fail is the strong end-of-simulation liveness obligation: attempts whose + // [m:n] window is cut off by $finish must fail (IEEE 1800-2023 16.12.11). + + // Single-tick window s_always[1:1]: its in-window state is ONE registered + // vertex, so a dropped end-of-trace obligation produces total silence (no + // shallower attempt can mask it). It is the most sensitive guard and shares + // the in-window marking with every s_always[m:n], so if it fires the deeper + // windows do too. $finish halts on the first liveness $error, so a single + // strong assertion keeps the failure attributable to this case. + as_mm: assert property (@(posedge clk) disable iff (rst) s_always [1:1] a); + + // Weak twin imposes no end-of-trace obligation: never fails on this trace. + as_weak: assert property (@(posedge clk) disable iff (rst) always [1:4] a); + + always @(posedge clk) begin + if (cyc == 10) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end + +endmodule