Support unbounded always [m:$] and strong s_always liveness (#7798)
This commit is contained in:
Yilou Wang
GitHub
parent
22b45f0fd7
commit
a5a16cfbfd
|
|
@ -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<AstNodeExpr*> 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;
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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()
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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()
|
||||
|
|
@ -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
|
||||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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));
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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...
|
||||
|
|
@ -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()
|
||||
|
|
@ -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
|
||||
Loading…
Reference in New Issue