From a5a16cfbfd0f169929c0a5aafb716860aec197fb Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Thu, 18 Jun 2026 17:17:09 +0200 Subject: [PATCH] Support unbounded always [m:$] and strong s_always liveness (#7798) --- src/V3AssertNfa.cpp | 60 +++++++++++++++++++ src/V3Width.cpp | 40 +++++++------ test_regress/t/t_assert_always_unbounded.py | 18 ++++++ test_regress/t/t_assert_always_unbounded.v | 57 ++++++++++++++++++ .../t/t_assert_always_unbounded_bad.out | 14 +++++ .../t/t_assert_always_unbounded_bad.py | 16 +++++ .../t/t_assert_always_unbounded_bad.v | 20 +++++++ test_regress/t/t_prop_always.v | 8 --- test_regress/t/t_prop_always_bad.out | 20 +++---- test_regress/t/t_prop_always_unsup.out | 16 ++--- test_regress/t/t_prop_always_unsup.v | 3 - test_regress/t/t_prop_always_wide.v | 9 +-- test_regress/t/t_prop_s_always_liveness.out | 4 ++ test_regress/t/t_prop_s_always_liveness.py | 17 ++++++ test_regress/t/t_prop_s_always_liveness.v | 43 +++++++++++++ 15 files changed, 289 insertions(+), 56 deletions(-) create mode 100755 test_regress/t/t_assert_always_unbounded.py create mode 100644 test_regress/t/t_assert_always_unbounded.v create mode 100644 test_regress/t/t_assert_always_unbounded_bad.out create mode 100755 test_regress/t/t_assert_always_unbounded_bad.py create mode 100644 test_regress/t/t_assert_always_unbounded_bad.v create mode 100644 test_regress/t/t_prop_s_always_liveness.out create mode 100755 test_regress/t/t_prop_s_always_liveness.py create mode 100644 test_regress/t/t_prop_s_always_liveness.v diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index e302be9eb..222d88128 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -78,6 +78,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) @@ -206,6 +210,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 // IEEE 1800-2023 16.14.3 cover sequence: each end-of-match fires the action, // not just the first. Builder builds parallel-branch (no first-match-wins) // topology when true. Default false preserves cover_property semantics. @@ -348,6 +353,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; } @@ -673,10 +679,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) { @@ -1885,6 +1918,33 @@ 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}; + } + } + if (pendingp) { + AstCExpr* const assertOnp + = new AstCExpr{flp, AstCExpr::Pure{}, "vlSymsp->_vm_contextp__->assertOn()", 1}; + AstNodeExpr* const condp = new AstLogAnd{flp, assertOnp, pendingp}; + AstDisplay* const dispp + = new AstDisplay{flp, VDisplayType::DT_ERROR, "", nullptr, nullptr}; + dispp->fmtp()->timeunit(m_modp->timeunit()); + AstNodeStmt* const 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 b323c0b92..dbbea7022 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -1563,33 +1563,39 @@ 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)) { + AstNode* const boundp = loUnbounded ? nodep->loBoundp() : nodep->hiBoundp(); + boundp->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->loBoundp()->v3error("always range low bound must be a constant expression" + " (IEEE 1800-2023 16.12.11)"); nodep->dtypeSetBit(); return; } const AstConst* const loConstp = VN_CAST(nodep->loBoundp(), Const); const AstConst* const hiConstp = VN_CAST(nodep->hiBoundp(), Const); if (!loConstp) { - nodep->v3error("always range low bound must be a constant expression" - " (IEEE 1800-2023 16.12.11)"); + nodep->loBoundp()->v3error("always range low bound must be a constant expression" + " (IEEE 1800-2023 16.12.11)"); } - if (!hiConstp) { - nodep->v3error("always range high bound must be a constant expression" - " (IEEE 1800-2023 16.12.11)"); + if (!hiUnbounded && !hiConstp) { + nodep->hiBoundp()->v3error("always range high bound must be a constant expression" + " (IEEE 1800-2023 16.12.11)"); } if (loConstp && loConstp->toSInt() < 0) { - nodep->v3error("always range low bound must be non-negative" - " (IEEE 1800-2023 16.12.11)"); + nodep->loBoundp()->v3error("always range low bound must be non-negative" + " (IEEE 1800-2023 16.12.11)"); } - if (loConstp && hiConstp && hiConstp->toSInt() < loConstp->toSInt()) { - nodep->v3error("always range high bound must be >= low bound" - " (IEEE 1800-2023 16.12.11)"); + if (!hiUnbounded && loConstp && hiConstp && hiConstp->toSInt() < loConstp->toSInt()) { + nodep->hiBoundp()->v3error("always range high bound must be >= low bound" + " (IEEE 1800-2023 16.12.11)"); } bool hasPropertyOp = propp->isMultiCycleSva(); if (!hasPropertyOp) { 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..155120065 --- /dev/null +++ b/test_regress/t/t_assert_always_unbounded_bad.out @@ -0,0 +1,14 @@ +%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:47: 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: t/t_assert_always_unbounded_bad.v:18:43: always range low bound must be a constant expression (IEEE 1800-2023 16.12.11) + : ... note: In instance 't' + 18 | assert property (@(posedge clk) always [$:5] 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..9103865ef --- /dev/null +++ b/test_regress/t/t_assert_always_unbounded_bad.v @@ -0,0 +1,20 @@ +// 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); + + // A weak always range may only place $ on the high bound; an unbounded low + // bound is not a legal cycle_delay_const_range_expression. + assert property (@(posedge clk) always [$:5] a); + +endmodule diff --git a/test_regress/t/t_prop_always.v b/test_regress/t/t_prop_always.v index 3f54b1023..52cfea02c 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,9 +38,6 @@ 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); - // 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 +79,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_bad.out b/test_regress/t/t_prop_always_bad.out index 4e06a8feb..62d3d66a8 100644 --- a/test_regress/t/t_prop_always_bad.out +++ b/test_regress/t/t_prop_always_bad.out @@ -1,34 +1,34 @@ -%Error: t/t_prop_always_bad.v:13:20: always range low bound must be non-negative (IEEE 1800-2023 16.12.11) +%Error: t/t_prop_always_bad.v:13:28: always range low bound must be non-negative (IEEE 1800-2023 16.12.11) : ... note: In instance 't' 13 | assert property (always [-1:3] a); - | ^~~~~~ + | ^ ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. -%Error: t/t_prop_always_bad.v:14:20: always range high bound must be >= low bound (IEEE 1800-2023 16.12.11) +%Error: t/t_prop_always_bad.v:14:30: always range high bound must be >= low bound (IEEE 1800-2023 16.12.11) : ... note: In instance 't' 14 | assert property (always [5:2] a); - | ^~~~~~ + | ^ %Error: t/t_prop_always_bad.v:15:28: Expecting expression to be constant, but variable isn't const: 'x' : ... note: In instance 't' 15 | assert property (always [x:3] a); | ^ -%Error: t/t_prop_always_bad.v:15:20: always range low bound must be a constant expression (IEEE 1800-2023 16.12.11) +%Error: t/t_prop_always_bad.v:15:28: always range low bound must be a constant expression (IEEE 1800-2023 16.12.11) : ... note: In instance 't' 15 | assert property (always [x:3] a); - | ^~~~~~ + | ^ %Error: t/t_prop_always_bad.v:16:30: Expecting expression to be constant, but variable isn't const: 'x' : ... note: In instance 't' 16 | assert property (always [1:x] a); | ^ -%Error: t/t_prop_always_bad.v:16:20: always range high bound must be a constant expression (IEEE 1800-2023 16.12.11) +%Error: t/t_prop_always_bad.v:16:30: always range high bound must be a constant expression (IEEE 1800-2023 16.12.11) : ... note: In instance 't' 16 | assert property (always [1:x] a); - | ^~~~~~ + | ^ %Error: t/t_prop_always_bad.v:17:20: s_always range must be bounded (IEEE 1800-2023 16.12.11) : ... note: In instance 't' 17 | assert property (s_always a); | ^~~~~~~~ -%Error: t/t_prop_always_bad.v:18:20: s_always range must be bounded (IEEE 1800-2023 16.12.11) +%Error: t/t_prop_always_bad.v:18:32: s_always range must be bounded (IEEE 1800-2023 16.12.11) : ... note: In instance 't' 18 | assert property (s_always [1:$] a); - | ^~~~~~~~ + | ^ %Error: Exiting due to 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..742e37d9a 100644 --- a/test_regress/t/t_prop_always_wide.v +++ b/test_regress/t/t_prop_always_wide.v @@ -15,17 +15,13 @@ 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); - always @(posedge clk) begin cyc <= cyc + 1; if (cyc == 49) begin @@ -33,9 +29,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.out b/test_regress/t/t_prop_s_always_liveness.out new file mode 100644 index 000000000..8a1f69c16 --- /dev/null +++ b/test_regress/t/t_prop_s_always_liveness.out @@ -0,0 +1,4 @@ +*-* All Finished *-* +[115] %Error: t_prop_s_always_liveness.v:25: Assertion failed in top.t +%Error: t/t_prop_s_always_liveness.v:25: Verilog $stop +Aborting... 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..e6fa1c51f --- /dev/null +++ b/test_regress/t/t_prop_s_always_liveness.py @@ -0,0 +1,17 @@ +#!/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']) +test.execute(fails=True, expect_filename=test.golden_filename) + +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..3251b7754 --- /dev/null +++ b/test_regress/t/t_prop_s_always_liveness.v @@ -0,0 +1,43 @@ +// 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; + + int low_s_fail_q[$]; + int low_w_fail_q[$]; + + // The youngest [2:5] windows are still open at $finish, so strong s_always + // reports a liveness failure even with a_high always 1; weak always does not. + assert property (@(posedge clk) s_always [2:5] a_high); + assert property (@(posedge clk) always [2:5] a_high); + + assert property (@(posedge clk) s_always [2:5] a_low) + else low_s_fail_q.push_back(cyc); + assert property (@(posedge clk) always [2:5] a_low) + else low_w_fail_q.push_back(cyc); + + always @(posedge clk) begin + cyc <= cyc + 1; + if (cyc == 10) begin + `checkd(low_s_fail_q.size(), low_w_fail_q.size()); + `checkd(low_w_fail_q.size(), 9); + $write("*-* All Finished *-*\n"); + $finish; + end + end + +endmodule