From c3f0fcc1a3904af65c6f1bc2481d6ca1dcbe55ee Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Tue, 7 Jul 2026 16:15:01 +0200 Subject: [PATCH] Randomize disable iff tests with reference models, dedup Link OR propagation, extract shift-chain helpers --- src/V3AssertNfa.cpp | 170 +++++++++--------- test_regress/t/t_prop_always.v | 3 - .../t/t_property_disable_iff_counter.py | 2 + .../t/t_property_disable_iff_counter.v | 55 ++++-- test_regress/t/t_property_disable_iff_held.v | 72 +++++--- .../t/t_property_disable_iff_midpulse.v | 64 +++++-- test_regress/t/t_property_shift_chunk.py | 2 + test_regress/t/t_property_shift_chunk.v | 74 ++++++-- 8 files changed, 277 insertions(+), 165 deletions(-) diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index c8248d22f..04d7fb7fc 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -33,6 +33,7 @@ #include "V3UniqueNames.h" #include +#include #include #include @@ -1652,98 +1653,93 @@ class SvaNfaLowering final { AstNodeExpr* throughoutRejectp = nullptr; // Reject when a throughout guard drops }; - // Pack ##N delay and uniform b[*N] repetition sub-chains -- maximal simple - // paths of registered vertices, each holding the previous vertex's state - // delayed one cycle -- into single vectors shifted once per clock - // (verilator/verilator#7792). Sets shiftVecp/shiftBit/shiftStepCondp. + static const SvaTransEdge* singleClockedInEdge(SvaStateVertex* vtxp) { + const SvaTransEdge* inp = nullptr; + for (const V3GraphEdge& er : vtxp->inEdges()) { + const SvaTransEdge& te = static_cast(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; + } + static bool shiftable(const std::vector& vtx, int i, int startIdx) { + 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; + } + // Chain predecessor of a registered vertex and the per-step condition into it + // (null = unconditional ##N delay; else the b[*N] Link boolean). + static int chainPred(const std::vector& vtx, int ci, int startIdx, + AstNodeExpr*& condpr) { + condpr = nullptr; + const SvaTransEdge* const e = singleClockedInEdge(vtx[ci]); + if (!e || e->m_rejectOnFail || e->m_condVtxp) return -1; + const int mi = e->fromVtxp()->color(); + if (shiftable(vtx, mi, startIdx)) { // direct clocked step + condpr = e->m_condp; + return mi; + } + if (e->m_condp) return -1; // pass-through requires an unconditional ##1 edge + SvaStateVertex* const m = vtx[mi]; + const SvaTransEdge* linkp = nullptr; + for (const V3GraphEdge& er : m->inEdges()) { + if (linkp) return -1; // more than one input -> not a clean pass-through + linkp = static_cast(&er); + } + if (!linkp || linkp->m_consumesCycle || linkp->m_rejectOnFail || linkp->m_condVtxp) + return -1; + const int pi = linkp->fromVtxp()->color(); + if (!shiftable(vtx, pi, startIdx)) return -1; + condpr = linkp->m_condp; + return pi; + } + static bool sameCond(const AstNodeExpr* a, const AstNodeExpr* b) { + if (!a && !b) return true; + if (!a || !b) return false; + return a->sameTree(b); + } + + // Pack ##N delay and uniform b[*N] repetition chains of registered vertices + // into single vectors shifted once per clock. Sets shiftVecp/shiftBit/etc. void detectShiftChains(const std::vector& vtx, int N, int startIdx, const std::string& baseName, FileLine* flp) { - const auto singleClockedInEdge = [](SvaStateVertex* v) -> const SvaTransEdge* { - const SvaTransEdge* inp = nullptr; - for (const V3GraphEdge& er : v->inEdges()) { - const SvaTransEdge& te = static_cast(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; - }; - // Chain predecessor of a registered vertex, plus the per-step condition - // into it (null = unconditional). A shift step is a direct clocked edge - // (##N delay) or a clocked edge fed through one pass-through condition - // Link vertex (`b[*N]` repetition; the Link boolean is the condition). - const auto chainPred = [&](int ci, AstNodeExpr*& condpr) -> int { - condpr = nullptr; - const SvaTransEdge* const e = singleClockedInEdge(vtx[ci]); - if (!e || e->m_rejectOnFail || e->m_condVtxp) return -1; - const int mi = e->fromVtxp()->color(); - if (shiftable(mi)) { // direct clocked step - condpr = e->m_condp; - return mi; - } - if (e->m_condp) return -1; // pass-through requires an unconditional ##1 edge - SvaStateVertex* const m = vtx[mi]; - const SvaTransEdge* linkp = nullptr; - for (const V3GraphEdge& er : m->inEdges()) { - if (linkp) return -1; // more than one input -> not a clean pass-through - linkp = static_cast(&er); - } - if (!linkp || linkp->m_consumesCycle || linkp->m_rejectOnFail || linkp->m_condVtxp) - return -1; - const int pi = linkp->fromVtxp()->color(); - if (!shiftable(pi)) return -1; - condpr = linkp->m_condp; - return pi; - }; - const auto sameCond = [](const AstNodeExpr* a, const AstNodeExpr* b) -> bool { - if (!a && !b) return true; - if (!a || !b) return false; - return a->sameTree(b); - }; - // Bond each vertex to its chain predecessor; a predecessor feeding more - // than one chain vertex branches and cannot shift unambiguously. + // Link each shiftable vertex to its unique chain predecessor and successor. struct Bond final { int pred = -1; + int next = -1; + int childCount = 0; + bool hasPrev = false; AstNodeExpr* stepCondp = nullptr; // borrowed step condition into this vertex }; std::vector bond(N); - std::vector childCount(N, 0); for (int i = 0; i < N; ++i) { - if (!shiftable(i)) continue; + if (!shiftable(vtx, i, startIdx)) continue; AstNodeExpr* cp = nullptr; - const int p = chainPred(i, cp); + const int p = chainPred(vtx, i, startIdx, cp); if (p < 0) continue; - bond[i] = {p, cp}; - ++childCount[p]; + bond[i].pred = p; + bond[i].stepCondp = cp; + ++bond[p].childCount; } - std::vector nextInChain(N, -1); - std::vector hasPrevInChain(N, false); for (int i = 0; i < N; ++i) { const int p = bond[i].pred; - if (p < 0 || childCount[p] != 1) continue; - nextInChain[p] = i; - hasPrevInChain[i] = true; + if (p < 0 || bond[p].childCount != 1) continue; + bond[p].next = i; + bond[i].hasPrev = true; } - // Walk each chain head, splitting into maximal segments whose interior - // steps share one condition; each segment of >= 2 vertices packs into - // one vector. Segments cap at 64 bits: a wider (VlWide) shift emitted - // after V3Width is not word-split and breaks V3Subst. A capped chain - // carries into the next vector through the shared clocked predecessor. + // Split each chain into maximal segments sharing one step condition, + // each packed into one vector. Cap at 64 bits (wider VlWide breaks V3Subst). constexpr int kMaxShiftVec = 64; for (int h = 0; h < N; ++h) { - if (hasPrevInChain[h] || nextInChain[h] == -1) continue; + if (bond[h].hasPrev || bond[h].next == -1) continue; std::vector chain; - for (int j = h; j != -1; j = nextInChain[j]) chain.push_back(j); + for (int j = h; j != -1; j = bond[j].next) chain.push_back(j); int a = 0; while (a + 1 < static_cast(chain.size())) { AstNodeExpr* const segCondp = bond[chain[a + 1]].stepCondp; @@ -1787,8 +1783,7 @@ class SvaNfaLowering final { AstNodeExpr* srcSigp = c.vtx[fromIdx]->datap()->stateSigp->cloneTreePure(false); srcSigp = andCond(c.flp, srcSigp, te.m_condp); - // Zero in-flight state while the disable is active; the edge - // counter misses a held or mid-window disable (IEEE 1800-2023 16.12) + // Zero in-flight state while the disable is active. if (c.disableExprp) { AstNodeExpr* const notDisp = new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)}; @@ -1811,10 +1806,8 @@ class SvaNfaLowering final { } } - // Delay / uniform-repetition chains: one masked shift per vector. + // One masked shift per vector; bit 0 injects the head's feeder: // vec <= (((vec << 1) & {W{step}}) | inject) & {W{!disable & !kill}} - // bit 0 injects the head's feeder; `step` is the shared per-step - // condition (absent for a pure ##N delay), on the shifted bits only. 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; @@ -1919,8 +1912,7 @@ class SvaNfaLowering final { AstNodeExpr* donep = new AstLogOr{c.flp, killActive(c), new AstLogOr{c.flp, matchedNowp, counterAtEndp}}; - // A mid-window disable aborts the in-flight count (IEEE 1800-2023 - // 16.12); the expiry reject is separately disable-gated + // A mid-window disable aborts the in-flight count. if (c.disableExprp) donep = new AstLogOr{c.flp, donep, c.disableExprp->cloneTreePure(false)}; @@ -2004,8 +1996,7 @@ class SvaNfaLowering final { AstNodeExpr* clearCondp = new AstLogOr{ c.flp, killActive(c), c.vtx[ai]->datap()->stateSigp->cloneTreePure(false)}; - // A mid-window disable clears a half-latched side so a disabled - // attempt cannot pair with a later attempt (IEEE 1800-2023 16.12) + // A mid-window disable clears a half-latched side. if (c.disableExprp) clearCondp = new AstLogOr{c.flp, clearCondp, c.disableExprp->cloneTreePure(false)}; AstIf* const topp = new AstIf{c.flp, clearCondp, clearLp, setLIfp}; @@ -2215,6 +2206,7 @@ class SvaNfaLowering final { // Fixed-point propagation along zero-delay (Link) edges. // Worst case: longest chain is N hops; SAnd seeding adds one extra round; // factor-of-2 covers reverse-order dependencies. + std::unordered_map consumedSrcp; for (int pass = 0; pass < 2 * c.N + 2; ++pass) { bool changed = false; // Seed SAnd combiners (sub-NFA termVertices may only be available @@ -2246,14 +2238,18 @@ class SvaNfaLowering final { } // Propagate Link edges for (int fi = 0; fi < c.N; ++fi) { - if (!c.vtx[fi]->datap()->stateSigp) continue; + AstNodeExpr* const srcp = c.vtx[fi]->datap()->stateSigp; + if (!srcp) continue; for (const V3GraphEdge& er : c.vtx[fi]->outEdges()) { const SvaTransEdge& te = static_cast(er); if (te.m_consumesCycle) continue; const int ti = te.toVtxp()->color(); if (te.toVtxp()->m_isMatch || te.toVtxp()->m_isRejectSink) continue; - AstNodeExpr* const contributionp = andCond( - c.flp, c.vtx[fi]->datap()->stateSigp->cloneTreePure(false), te.m_condp); + // Consume each Link edge once per distinct source value + if (consumedSrcp[&te] == srcp) continue; + consumedSrcp[&te] = srcp; + AstNodeExpr* const contributionp + = andCond(c.flp, srcp->cloneTreePure(false), te.m_condp); if (!c.vtx[ti]->datap()->stateSigp) { c.vtx[ti]->datap()->stateSigp = contributionp; changed = true; diff --git a/test_regress/t/t_prop_always.v b/test_regress/t/t_prop_always.v index 9318287df..69ccda1c9 100644 --- a/test_regress/t/t_prop_always.v +++ b/test_regress/t/t_prop_always.v @@ -88,9 +88,6 @@ module t ( `checkd(rand_bounded_pass_q.size(), 0); `checkd(rand_bounded_fail_q.size(), 20); // Other sims: 19, 11 `checkd(disable_bounded_pass_q.size(), 0); - // A disable true anywhere in the [0:3] window suppresses the attempt; - // the residual vs other sims is a disable arriving only after an - // in-window failure already fired, which a streaming NFA cannot un-fire. `checkd(disable_bounded_fail_q.size(), 8); // Other sims: 5, 6 $write("*-* All Finished *-*\n"); $finish; diff --git a/test_regress/t/t_property_disable_iff_counter.py b/test_regress/t/t_property_disable_iff_counter.py index 35e44000c..36fbd6160 100755 --- a/test_regress/t/t_property_disable_iff_counter.py +++ b/test_regress/t/t_property_disable_iff_counter.py @@ -11,6 +11,8 @@ import vltest_bootstrap test.scenarios('simulator') +test.sim_time = 16000 + test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing']) test.execute() diff --git a/test_regress/t/t_property_disable_iff_counter.v b/test_regress/t/t_property_disable_iff_counter.v index 230f4b226..a25a67be5 100644 --- a/test_regress/t/t_property_disable_iff_counter.v +++ b/test_regress/t/t_property_disable_iff_counter.v @@ -9,38 +9,59 @@ `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 true at ANY point of a multi-cycle -// attempt window disables it. A range delay ##[1:N] with N over the 256 unroll -// limit lowers to a counter-FSM backend (not a state-register chain), which had -// the same mid-window-disable hole as the register path -// (verilator/verilator#7792 follow-up). value never matches, so a live attempt -// fails at window end; skip pulses once mid-window and must abort the in-flight -// counter so the disabled assert does not fire. +// disable iff mid-window on the counter-FSM path (##[1:N], N > 256 unroll limit). module t ( input clk ); + localparam int N = 257; // > 256 unroll limit -> counter FSM path + localparam int PERIOD = 260; // > N -> attempts never overlap + localparam int NATT = 30; + int cyc = 0; - wire trig = (cyc == 5); - wire value = 1'b0; // never matches -> attempt would fail at window end - wire skip = (cyc == 50); // single mid-window pulse + reg [63:0] crc = 64'h5aef0c8d_d70a4497; + + int phase = 0; + int idx = 0; + wire in_run = (idx < NATT); + wire trig = in_run && (phase == 0); + wire value = 1'b0; + + reg do_dis = 0; + int dis_at = 0; + wire dis = in_run && do_dis && (phase == dis_at); int n_dis_fire = 0; int n_ctrl_fire = 0; + int exp_dis_fire = 0; - // Range > 256 -> counter FSM. The cyc-5 attempt is hit by the skip pulse. - assert property (@(posedge clk) disable iff (skip) trig |-> ##[1:300] value) + assert property (@(posedge clk) disable iff (dis) trig |-> ##[1:N] value) else n_dis_fire <= n_dis_fire + 1; - // Control: same property never disabled -> the cyc-5 attempt fails once. - assert property (@(posedge clk) disable iff (1'b0) trig |-> ##[1:300] value) + assert property (@(posedge clk) disable iff (1'b0) trig |-> ##[1:N] value) else n_ctrl_fire <= n_ctrl_fire + 1; always @(posedge clk) begin cyc <= cyc + 1; - if (cyc == 320) begin - `checkd(n_dis_fire, 0); - `checkd(n_ctrl_fire, 1); + crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; + if (phase == PERIOD - 1) begin + phase <= 0; + idx <= idx + 1; + end else begin + phase <= phase + 1; + end + if (phase == 0) begin + do_dis <= crc[3]; + dis_at <= 1 + (int'(crc[20:12]) % (N - 1)); + end + if (in_run && phase == N && !do_dis) exp_dis_fire <= exp_dis_fire + 1; + if (idx == NATT && phase == 4) begin +`ifdef TEST_VERBOSE + $write("n_dis_fire=%0d exp=%0d n_ctrl_fire=%0d\n", n_dis_fire, exp_dis_fire, n_ctrl_fire); +`endif + `checkd(n_dis_fire, exp_dis_fire); + `checkd(n_ctrl_fire, NATT); + if (n_dis_fire == 0 || n_dis_fire == NATT) $stop; // guard a degenerate seed $write("*-* All Finished *-*\n"); $finish; end diff --git a/test_regress/t/t_property_disable_iff_held.v b/test_regress/t/t_property_disable_iff_held.v index 37fa06461..e1ef13a13 100644 --- a/test_regress/t/t_property_disable_iff_held.v +++ b/test_regress/t/t_property_disable_iff_held.v @@ -9,47 +9,65 @@ `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 held continuously true must -// disable every attempt of a multi-cycle property (verilator/verilator#7792). -// en_held is a plain non-$sampled, non-constant signal held 1, so it exercises -// the NFA disable-counter path. The held assert/cover must never fire; the -// `disable iff (1'b0)` controls prove the same assert/cover do fire when enabled. +// A disable iff held true for the whole attempt window disables it. module t ( input clk ); + localparam int N = 5; + localparam int PERIOD = 9; + localparam int NATT = 40; + int cyc = 0; reg [63:0] crc = 64'h5aef0c8d_d70a4497; - wire a = crc[0]; - wire b = crc[4]; - bit en_held = 1'b1; + int phase = 0; + int idx = 0; + wire in_run = (idx < NATT); + wire trig = in_run && (phase == 0); - int n_held_assert = 0; - int n_held_cover = 0; - int n_ctrl_assert = 0; - int n_ctrl_cover = 0; + reg hold = 0; + reg fail_now = 0; + wire value = !(in_run && (phase == N) && fail_now); + wire dis = in_run && hold && (phase >= 1); - // Held-true disable: assert + cover must be fully suppressed. - assert property (@(posedge clk) disable iff (en_held) (a ##1 b)) - else n_held_assert <= n_held_assert + 1; - cover property (@(posedge clk) disable iff (en_held) (a ##1 b)) - n_held_cover <= n_held_cover + 1; + int n_held_fire = 0; + int n_ctrl_fire = 0; + int exp_held_fire = 0; + int exp_ctrl_fire = 0; - // Enabled control (disable iff 1'b0): same assert + cover must fire. - assert property (@(posedge clk) disable iff (1'b0) (a ##1 b)) - else n_ctrl_assert <= n_ctrl_assert + 1; - cover property (@(posedge clk) disable iff (1'b0) (a ##1 b)) - n_ctrl_cover <= n_ctrl_cover + 1; + assert property (@(posedge clk) disable iff (dis) trig |-> ##N value) + else n_held_fire <= n_held_fire + 1; + + assert property (@(posedge clk) disable iff (1'b0) trig |-> ##N value) + else n_ctrl_fire <= n_ctrl_fire + 1; always @(posedge clk) begin cyc <= cyc + 1; crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; - if (cyc == 99) begin - `checkd(n_held_assert, 0); - `checkd(n_held_cover, 0); - `checkd(n_ctrl_assert, 58); - `checkd(n_ctrl_cover, 26); // Others: 26, One other: 0 + if (phase == PERIOD - 1) begin + phase <= 0; + idx <= idx + 1; + end + else begin + phase <= phase + 1; + end + if (phase == 0) begin + hold <= crc[3]; + fail_now <= crc[7]; + end + if (in_run && phase == N) begin + exp_ctrl_fire <= exp_ctrl_fire + (fail_now ? 1 : 0); + if (!hold) exp_held_fire <= exp_held_fire + (fail_now ? 1 : 0); + end + if (idx == NATT && phase == 4) begin +`ifdef TEST_VERBOSE + $write("n_held_fire=%0d exp=%0d n_ctrl_fire=%0d exp_ctrl=%0d\n", n_held_fire, exp_held_fire, + n_ctrl_fire, exp_ctrl_fire); +`endif + `checkd(n_held_fire, exp_held_fire); + `checkd(n_ctrl_fire, exp_ctrl_fire); + if (n_held_fire == 0 || n_held_fire == NATT) $stop; $write("*-* All Finished *-*\n"); $finish; end diff --git a/test_regress/t/t_property_disable_iff_midpulse.v b/test_regress/t/t_property_disable_iff_midpulse.v index 66f2bf73c..9106ab850 100644 --- a/test_regress/t/t_property_disable_iff_midpulse.v +++ b/test_regress/t/t_property_disable_iff_midpulse.v @@ -9,39 +9,67 @@ `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. +// Mid-window disable pulse on the packed ##N delay path (N < unroll limit). module t ( input clk ); + localparam int N = 8; + localparam int PERIOD = 12; + localparam int NATT = 40; + 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] + reg [63:0] crc = 64'h5aef0c8d_d70a4497; + + int phase = 0; + int idx = 0; + wire in_run = (idx < NATT); + wire trig = in_run && (phase == 0); + + reg do_dis = 0; + int dis_at = 0; + reg fail_now = 0; + wire value = !(in_run && (phase == N) && fail_now); + wire dis = in_run && do_dis && (phase == dis_at); int n_dis_fire = 0; int n_ctrl_fire = 0; + int exp_dis_fire = 0; + int exp_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)) + assert property (@(posedge clk) disable iff (dis) trig |-> ##N 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)) + assert property (@(posedge clk) disable iff (1'b0) trig |-> ##N 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); + crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; + if (phase == PERIOD - 1) begin + phase <= 0; + idx <= idx + 1; + end + else begin + phase <= phase + 1; + end + if (phase == 0) begin + do_dis <= crc[3]; + dis_at <= 1 + (int'(crc[20:12]) % (N - 1)); + fail_now <= crc[7]; + end + if (in_run && phase == N) begin + exp_ctrl_fire <= exp_ctrl_fire + (fail_now ? 1 : 0); + if (!do_dis) exp_dis_fire <= exp_dis_fire + (fail_now ? 1 : 0); + end + if (idx == NATT && phase == 4) begin +`ifdef TEST_VERBOSE + $write("n_dis_fire=%0d exp=%0d n_ctrl_fire=%0d exp_ctrl=%0d\n", n_dis_fire, exp_dis_fire, + n_ctrl_fire, exp_ctrl_fire); +`endif + `checkd(n_dis_fire, exp_dis_fire); + `checkd(n_ctrl_fire, exp_ctrl_fire); + if (n_dis_fire == 0 || n_dis_fire == NATT) $stop; $write("*-* All Finished *-*\n"); $finish; end diff --git a/test_regress/t/t_property_shift_chunk.py b/test_regress/t/t_property_shift_chunk.py index 35e44000c..31ef43ec1 100755 --- a/test_regress/t/t_property_shift_chunk.py +++ b/test_regress/t/t_property_shift_chunk.py @@ -11,6 +11,8 @@ import vltest_bootstrap test.scenarios('simulator') +test.sim_time = 4000 + test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing']) test.execute() diff --git a/test_regress/t/t_property_shift_chunk.v b/test_regress/t/t_property_shift_chunk.v index 6a90526c1..d2e7a591c 100644 --- a/test_regress/t/t_property_shift_chunk.v +++ b/test_regress/t/t_property_shift_chunk.v @@ -9,29 +9,77 @@ `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 -// A ##130 delay is a 129-vertex shift chain packed across three <=64-bit -// vectors (verilator/verilator#7792 optimization). This exercises the -// cross-chunk carry: each next vector's bit 0 injects the previous vector's top -// bit through the shared clocked predecessor. res is high only exactly 130 -// cycles after the single antecedent match, so an off-by-one or dropped carry -// makes the consequent miss and the assert fire. +// ##N delay and held[*N] repetition pack shift chains across 64-bit chunks; +// the completion must land on exactly cycle N (off-by-one brackets fail). module t ( input clk ); + localparam int LEN = 130; + localparam int PERIOD = 140; + localparam int NATT = 12; + int cyc = 0; - wire trig = (cyc == 5); - wire res = (cyc == 5 + 130); + reg [63:0] crc = 64'h5aef0c8d_d70a4497; - int n_fire = 0; + int phase = 0; + int idx = 0; + wire in_run = (idx < NATT); + wire trig = in_run && (phase == 0); - assert property (@(posedge clk) trig |-> ##130 res) - else n_fire <= n_fire + 1; + reg res_fail = 0; + reg rep_fail = 0; + wire res = in_run && (phase == LEN) && !res_fail; + wire rep_res = in_run && (phase == LEN) && !rep_fail; + wire held = in_run && (phase <= LEN - 1); + + int n_d129 = 0; + int n_d130 = 0; + int n_d131 = 0; + int n_rok = 0; + int n_rbad = 0; + int exp_d130 = 0; + int exp_rok = 0; + + assert property (@(posedge clk) trig |-> ##(LEN-1) res) + else n_d129 <= n_d129 + 1; + assert property (@(posedge clk) trig |-> ##LEN res) + else n_d130 <= n_d130 + 1; + assert property (@(posedge clk) trig |-> ##(LEN+1) res) + else n_d131 <= n_d131 + 1; + + assert property (@(posedge clk) trig |-> held[*LEN] ##1 rep_res) + else n_rok <= n_rok + 1; + assert property (@(posedge clk) trig |-> held[*(LEN + 1)] ##1 rep_res) + else n_rbad <= n_rbad + 1; always @(posedge clk) begin cyc <= cyc + 1; - if (cyc == 160) begin - `checkd(n_fire, 0); + crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; + if (phase == PERIOD - 1) begin + phase <= 0; + idx <= idx + 1; + end + else begin + phase <= phase + 1; + end + if (phase == 0) begin + res_fail <= crc[2]; + rep_fail <= crc[9]; + end + if (in_run && phase == LEN) exp_d130 <= exp_d130 + (res_fail ? 1 : 0); + if (in_run && phase == LEN) exp_rok <= exp_rok + (rep_fail ? 1 : 0); + if (idx == NATT && phase == 4) begin +`ifdef TEST_VERBOSE + $write("d129=%0d d130=%0d exp=%0d d131=%0d rok=%0d exp=%0d rbad=%0d\n", n_d129, n_d130, + exp_d130, n_d131, n_rok, exp_rok, n_rbad); +`endif + `checkd(n_d129, NATT); + `checkd(n_d130, exp_d130); + `checkd(n_d131, NATT); + `checkd(n_rok, exp_rok); + `checkd(n_rbad, NATT); + if (exp_d130 == 0 || exp_d130 == NATT) $stop; $write("*-* All Finished *-*\n"); $finish; end