luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Fix mid-window disable iff and pack pure delay chains into a shift vector

This commit is contained in:
Yilou Wang 2026-07-01 15:54:51 +02:00
parent 0019a967b4
commit 4ccf6847a5
5 changed files with 190 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

118
src/V3AssertNfa.cpp
View File

@ -54,6 +54,10 @@ struct SvaVertexData final {
AstVar* doneRVarp = nullptr; // SAnd RHS done-latch
AstNodeExpr* stateSigp = nullptr; // Combinational state signal (owned during lowering)
bool needsReg = false; // True if vertex has incoming clocked edge
// Pure ##N delay chains collapse to one packed vector shifted once per clock
// instead of one 1-bit register per position (verilator/verilator#7792).
AstVar* shiftVecp = nullptr; // Shared packed shift vector, or null for a standalone reg
int shiftBit = -1; // Bit index within shiftVecp (0 = chain entry)
};
// NFA state vertex -- one per NFA position in the sequence evaluation
@ -1669,7 +1673,10 @@ class SvaNfaLowering final {
AstNodeExpr* srcSigp = c.vtx[fromIdx]->datap()->stateSigp->cloneTreePure(false);
srcSigp = andCond(c.flp, srcSigp, te.m_condp);
if (c.disableExprp && !c.snapshotVarp) {
// Zero in-flight state on an active disable in both modes; the
// edge counter misses a held or mid-window disable (IEEE
// 1800-2023 16.12, level-based).
if (c.disableExprp) {
AstNodeExpr* const notDisp
= new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)};
srcSigp = new AstLogAnd{c.flp, srcSigp, notDisp};
@ -1691,6 +1698,47 @@ class SvaNfaLowering final {
}
}
// Pure ##N delay chains: one masked shift per vector.
// vec <= ((vec << 1) | inject) & {W{!disable & !kill}}
// bit 0 injects the head's feeder contribution; interior bits shift up.
// The per-bit mask reproduces the same disable/kill gating the standalone
// registers get, so mid-window disable zeroing is preserved.
for (int i = 0; i < c.N; ++i) {
if (!c.vtx[i]->datap()->shiftVecp || c.vtx[i]->datap()->shiftBit != 0) continue;
AstVar* const vecp = c.vtx[i]->datap()->shiftVecp;
const int width = vecp->width();
AstNodeExpr* injectp = nullptr;
for (const V3GraphEdge& er : c.vtx[i]->inEdges()) {
const SvaTransEdge& te = static_cast<const SvaTransEdge&>(er);
if (!te.m_consumesCycle) continue;
const int fromIdx = te.fromVtxp()->color();
UASSERT_OBJ(c.vtx[fromIdx]->datap()->stateSigp, te.fromVtxp(),
"Shift-chain head feeder missing stateSig");
injectp = andCond(c.flp, c.vtx[fromIdx]->datap()->stateSigp->cloneTreePure(false),
te.m_condp);
}
UASSERT_OBJ(injectp, c.vtx[i], "Shift-chain head has no clocked feeder");
AstNodeExpr* const shiftedp
= new AstShiftL{c.flp, new AstVarRef{c.flp, vecp, VAccess::READ},
new AstConst{c.flp, AstConst::WidthedValue{}, 32, 1u}, width};
AstNodeExpr* const nextp
= new AstOr{c.flp, shiftedp, new AstExtend{c.flp, injectp, width}};
AstNodeExpr* gatep = notKillActive(c);
if (c.disableExprp) {
gatep = new AstLogAnd{
c.flp, new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)}, gatep};
}
AstNodeExpr* const maskedp = new AstAnd{
c.flp, nextp, new AstReplicate{c.flp, gatep, static_cast<uint32_t>(width)}};
AstAssignDly* const assignp
= new AstAssignDly{c.flp, new AstVarRef{c.flp, vecp, VAccess::WRITE}, maskedp};
if (!bodyp) {
bodyp = assignp;
} else {
bodyp->addNext(assignp);
}
}
if (!bodyp) return;
// Capture disableCnt in Phase-2 NBA before any reactive re-evaluation.
// snapshotVarp and disableCntVarp are allocated together.
@ -2024,7 +2072,11 @@ class SvaNfaLowering final {
// datap() was freshly allocated in lower() -- all stateSigp start null.
c.vtx[c.startIdx]->datap()->stateSigp = triggerExprp->cloneTreePure(false);
for (int i = 0; i < c.N; ++i) {
if (c.vtx[i]->datap()->stateVarp) {
if (c.vtx[i]->datap()->shiftVecp) {
c.vtx[i]->datap()->stateSigp = new AstSel{
c.flp, new AstVarRef{c.flp, c.vtx[i]->datap()->shiftVecp, VAccess::READ},
c.vtx[i]->datap()->shiftBit, 1};
} else if (c.vtx[i]->datap()->stateVarp) {
c.vtx[i]->datap()->stateSigp
= new AstVarRef{c.flp, c.vtx[i]->datap()->stateVarp, VAccess::READ};
} else if (c.vtx[i]->datap()->counterActiveVarp) {
@ -2227,6 +2279,67 @@ public:
}
}
// Pure ##N delay sub-chains: a maximal simple path of registered vertices
// whose state is a plain 1-cycle copy of a single predecessor. Each such
// chain lowers to one packed vector shifted once per clock instead of L
// separate 1-bit registers with L shift assignments (igorosky,
// verilator/verilator#7792). Uniform disable/kill gating is preserved by
// masking the whole vector, so the mid-window disable fix is unaffected.
const auto singleClockedInEdge = [](SvaStateVertex* v) -> const SvaTransEdge* {
const SvaTransEdge* inp = nullptr;
for (const V3GraphEdge& er : v->inEdges()) {
const SvaTransEdge& te = static_cast<const SvaTransEdge&>(er);
if (!te.m_consumesCycle) return nullptr; // an incoming Link disqualifies
if (inp) return nullptr; // more than one clocked source -> OR-merge
inp = &te;
}
return inp;
};
const auto shiftable = [&](int i) -> bool {
SvaStateVertex* const v = vtx[i];
if (!v->datap()->needsReg) return false;
if (i == startIdx || v->m_isMatch) return false;
if (v->m_isCounter || v->m_isAndCombiner || v->m_isRejectSink) return false;
if (v->m_isUnbounded) return false; // self-loop accumulator, not a pure shift
if (v->m_strongPending) return false; // final-block liveness reads its own reg
if (!v->m_throughoutConds.empty()) return false;
return singleClockedInEdge(v) != nullptr;
};
const auto outClockedCount = [](SvaStateVertex* v) -> int {
int n = 0;
for (const V3GraphEdge& er : v->outEdges())
if (static_cast<const SvaTransEdge&>(er).m_consumesCycle) ++n;
return n;
};
std::vector<int> nextInChain(N, -1);
std::vector<bool> hasPrevInChain(N, false);
for (int i = 0; i < N; ++i) {
if (!shiftable(i)) continue;
const SvaTransEdge* const inp = singleClockedInEdge(vtx[i]);
// A conditional/reject in-edge keeps its own inject; such a vertex can
// still be a chain head, never a shifted interior bit.
if (inp->m_condp || inp->m_rejectOnFail || inp->m_condVtxp) continue;
const int p = inp->fromVtxp()->color();
if (!shiftable(p) || outClockedCount(vtx[p]) != 1) continue; // p branches
nextInChain[p] = i;
hasPrevInChain[i] = true;
}
for (int i = 0; i < N; ++i) {
if (hasPrevInChain[i] || nextInChain[i] == -1) continue; // head of a >=2 chain only
int len = 0;
for (int j = i; j != -1; j = nextInChain[j]) ++len;
AstVar* const vecp
= new AstVar{flp, VVarType::MODULETEMP, baseName + "__v" + std::to_string(i),
m_modp->findBitDType(len, len, VSigning::UNSIGNED)};
vecp->lifetime(VLifetime::STATIC_EXPLICIT);
m_modp->addStmtsp(vecp);
int bit = 0;
for (int j = i; j != -1; j = nextInChain[j], ++bit) {
vtx[j]->datap()->shiftVecp = vecp;
vtx[j]->datap()->shiftBit = bit;
}
}
AstNodeDType* const u32DTypep = m_modp->findBasicDType(VBasicDTypeKwd::UINT32);
AstVar* const killVarp
= new AstVar{flp, VVarType::MODULETEMP, baseName + "__kill", u32DTypep};
@ -2263,6 +2376,7 @@ public:
}
if (!vtx[i]->datap()->needsReg) continue;
if (i == startIdx || vtx[i]->m_isMatch) continue;
if (vtx[i]->datap()->shiftVecp) continue; // lives in a packed shift vector
const std::string varName = baseName + "__s" + std::to_string(i);
AstVar* const varp
= new AstVar{flp, VVarType::MODULETEMP, varName, m_modp->findBitDType()};

6
test_regress/t/t_prop_always.v
View File

@ -90,7 +90,11 @@ module t (
`checkd(rand_bounded_pass_q.size(), 0);
`checkd(rand_bounded_fail_q.size(), 20);
`checkd(disable_bounded_pass_q.size(), 0);
`checkd(disable_bounded_fail_q.size(), 13);
// Level-based disable now suppresses attempts whose [0:3] window touches
// rst_rand (not only the start cyc), dropping 13 -> 8 toward Questa. The
// residual 8 vs 6 is a disable that goes true AFTER an in-window failure
// already fired: a streaming NFA cannot retroactively un-fire it.
`checkd(disable_bounded_fail_q.size(), 8); // Questa: 6
$write("*-* All Finished *-*\n");
$finish;
end

18
test_regress/t/t_property_disable_iff_midpulse.py Executable file
View File

@ -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('simulator')
test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing'])
test.execute()
test.passes()

49
test_regress/t/t_property_disable_iff_midpulse.v Normal file
View File

@ -0,0 +1,49 @@
// 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
// IEEE 1800-2023 16.12: a disable iff condition true at ANY point of a
// multi-cycle attempt window disables that attempt, not only when held
// continuously (verilator/verilator#7792 follow-up to #7841). skip is a plain
// non-$sampled, non-constant signal pulsed true for a single cycle in the
// MIDDLE of the ##10 window. value is low only at the attempt's match cycle, so
// exactly one attempt would fail; the mid-window skip pulse must disable it.
// Pre-fix the in-flight NFA states were not zeroed on a mid-window pulse, so the
// disabled assert fired; the control proves the same attempt fails when enabled.
module t (
input clk
);
int cyc = 0;
wire value = (cyc != 10); // low only at the cyc-0 attempt's match cycle
wire skip = (cyc == 5); // single-cycle pulse, mid-window of [0..10]
int n_dis_fire = 0;
int n_ctrl_fire = 0;
// Mid-window-pulse disable: the cyc-0 attempt (matches at cyc 10, where value
// is low -> would fail) must be disabled by the skip pulse at cyc 5.
assert property (@(posedge clk) disable iff (skip) (##10 value))
else n_dis_fire <= n_dis_fire + 1;
// Control: same property always enabled -> the cyc-0 attempt fails once.
assert property (@(posedge clk) disable iff (1'b0) (##10 value))
else n_ctrl_fire <= n_ctrl_fire + 1;
always @(posedge clk) begin
cyc <= cyc + 1;
if (cyc == 20) begin
`checkd(n_dis_fire, 0);
`checkd(n_ctrl_fire, 1);
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule

4
test_regress/t/t_sequence_within.v
View File

@ -107,14 +107,14 @@ module t (
// engine-wide behavior, not within-specific.
`checkd(count_p1, 23); // Questa: 23
`checkd(count_p2, 44); // Questa: 44
`checkd(count_p3, 25); // Questa: 20
`checkd(count_p3, 24); // Questa: 20
`checkd(count_p4, 23); // Questa: 22
`checkd(count_p5, 26); // Questa: 26
`checkd(count_p6, 21); // Questa: 16
`checkd(count_p7, 15); // Questa: 9
`checkd(count_p8, 15); // Questa: 4
`checkd(count_p9, 15); // Questa: 10
`checkd(count_p10, 23); // Questa: 15
`checkd(count_p10, 21); // Questa: 15
$write("*-* All Finished *-*\n");
$finish;
end