luke/verilator
1
0
Fork 0
mirror of https://github.com/verilator/verilator.git synced 2026-09-03 06:03:03 +02:00
Code Issues Packages Projects Releases Wiki Activity

Support SVA goto repetition with range [->M:N] (#7569)

Browse Source
This commit is contained in:
Yilou Wang
2026-05-11 07:07:51 -04:00
committed by GitHub
parent 485c0e746c
commit b0d58bbcef
17 changed files with 397 additions and 68 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/V3AssertNfa.cpp
+33 -7
View File
@@ -593,15 +593,20 @@ class SvaNfaBuilder final {
BuildResult buildGotoRep(AstSGotoRep* repp, SvaStateVertex* entryVtxp) {
FileLine* const flp = repp->fileline();
AstNodeExpr* const exprp = repp->exprp();
const int n = getConstInt(repp->countp());
if (n <= 0) return BuildResult::fail();
const int minN = getConstInt(repp->countp());
if (minN <= 0) return BuildResult::fail();
const bool hasMax = repp->maxCountp() != nullptr;
const int maxN = hasMax ? getConstInt(repp->maxCountp()) : minN;
UASSERT_OBJ(maxN >= minN, repp, "GotoRep range max < min (V3Width invariant)");
// Wait + match per iter -> 2n sites. NOT($sampled(x)) matches
// Wait + match per iter -> 2 sites per iteration; range form needs
// sites for every iteration in [0..maxN). NOT($sampled(x)) matches
// $sampled(NOT(x)) at the value level (IEEE 1800-2023 16.9.9);
// purity is enforced uniformly via cloneTreePure inside sampledRefOrClone.
AstVar* const hoistVarp = tryHoistSampled(exprp, flp, 2 * n);
AstVar* const hoistVarp = tryHoistSampled(exprp, flp, 2 * maxN);
SvaStateVertex* currentp = entryVtxp;
for (int i = 0; i < n; ++i) {
// Build minN match-wait chains to reach the first accept point.
for (int i = 0; i < minN; ++i) {
SvaStateVertex* const waitVtxp = scopedCreateVertex();
// Edge (not Link) for all iterations: IEEE expansion ##1 before each
// match. A Link at i==0 was wrong -- it allowed same-cycle matching
@@ -614,9 +619,30 @@ class SvaNfaBuilder final {
guardedLink(waitVtxp, matchVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp);
currentp = matchVtxp;
}
currentp->m_isUnbounded = true; // [->N] waits unboundedly
if (!hasMax) {
currentp->m_isUnbounded = true; // [->N] waits unboundedly
m_inUnboundedScope = true;
return {currentp, nullptr, {}};
}
// [->M:N]: every match in [M..N] feeds a shared merge vertex so the
// property can accept at any count in that range. Mirrors
// buildConsRep's range fan-out.
SvaStateVertex* const mergeVtxp = scopedCreateVertex();
guardedLink(currentp, mergeVtxp, flp); // accept at match_M
for (int i = minN; i < maxN; ++i) {
SvaStateVertex* const waitVtxp = scopedCreateVertex();
guardedEdge(currentp, waitVtxp, flp);
AstNodeExpr* const waitCondp
= new AstNot{flp, sampledRefOrClone(hoistVarp, exprp, flp)};
guardedEdge(waitVtxp, waitVtxp, waitCondp, flp);
SvaStateVertex* const matchVtxp = scopedCreateVertex();
guardedLink(waitVtxp, matchVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp);
guardedLink(matchVtxp, mergeVtxp, flp); // accept at match_(i+1)
currentp = matchVtxp;
}
mergeVtxp->m_isUnbounded = true; // [->M:N] still has unbounded waits between matches
m_inUnboundedScope = true;
return {currentp, nullptr, {}};
return {mergeVtxp, nullptr, {}};
}
// Build merge vertex for SOr / LogOr: both branches feed into one vertex.