From 988376614c792580904323216e4fd403ebaa98fc Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Mon, 6 Jul 2026 16:49:44 +0200 Subject: [PATCH] Reject unsupported sequence event topology and drop matching-value comments --- src/V3AssertNfa.cpp | 27 ++++++++++++++------- test_regress/t/t_assert_seq_event_ctl.v | 4 +-- test_regress/t/t_assert_seq_event_unsup.out | 3 +++ test_regress/t/t_assert_seq_event_unsup.v | 7 ++++++ 4 files changed, 30 insertions(+), 11 deletions(-) diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 4c99c19f2..f01e0da62 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -287,6 +287,8 @@ class SvaNfaBuilder final { // not just the first. Builder builds parallel-branch (no first-match-wins) // topology when true. Default false preserves cover_property semantics. bool m_isCoverSeq = false; + // Unsupported endpoint topology must reject, not ignore, or the wait hangs + bool m_isSeqEvent = false; struct RangeDelayRejectInfo final { SvaStateVertex* startp = nullptr; @@ -294,6 +296,15 @@ class SvaNfaBuilder final { int rhsLen = 0; }; + void warnEndpointUnsupported(FileLine* flp, const string& what) const { + if (m_isSeqEvent) { + flp->v3warn(E_UNSUPPORTED, + "Unsupported: sequence used as an event control with " << what); + } else { + flp->v3warn(COVERIGN, "Ignoring unsupported: cover sequence with " << what); + } + } + AstNodeExpr* throughoutCond(AstNodeExpr* baseCondp, FileLine* flp) { if (m_throughoutStack.empty()) return baseCondp; // AND all throughout conditions (supports nesting) @@ -574,8 +585,7 @@ class SvaNfaBuilder final { // overlapping ends and the nested-sequence merge collapses them, so // reject those for a cover sequence rather than under-count. if (m_isCoverSeq && (range > kChainLimit || VN_IS(rhsExprp, SExpr))) { - flp->v3warn(COVERIGN, - "Ignoring unsupported: cover sequence with this ranged cycle delay"); + warnEndpointUnsupported(flp, "this ranged cycle delay"); outErrorEmitted = true; return false; } @@ -881,8 +891,7 @@ class SvaNfaBuilder final { // terminal, so a cover sequence would under-count. Reject the ranged form // (the single-count b[->N] has one end and is enumerated correctly). if (m_isCoverSeq && hasMax && maxN > minN) { - flp->v3warn(COVERIGN, - "Ignoring unsupported: cover sequence with a ranged goto repetition"); + warnEndpointUnsupported(flp, "a ranged goto repetition"); return BuildResult::failWithError(); } @@ -946,8 +955,7 @@ class SvaNfaBuilder final { // than under-count. Plain boolean disjunction has one end per cycle and // is handled by the OR-fold. if (m_isCoverSeq && (lhs.termVertexp != entryVtxp || rhs.termVertexp != entryVtxp)) { - flp->v3warn(COVERIGN, - "Ignoring unsupported: cover sequence with a sequence operand of 'or'"); + warnEndpointUnsupported(flp, "a sequence operand of 'or'"); return BuildResult::failWithError(); } SvaStateVertex* const mergeVtxp = scopedCreateVertex(); @@ -1442,11 +1450,12 @@ class SvaNfaBuilder final { public: SvaNfaBuilder(SvaGraph& graph, AstNodeModule* modp, V3UniqueNames& propTempNames, - bool isCoverSeq = false) + bool isCoverSeq = false, bool isSeqEvent = false) : m_graph{graph} , m_modp{modp} , m_propTempNames{propTempNames} - , m_isCoverSeq{isCoverSeq} {} + , m_isCoverSeq{isCoverSeq} + , m_isSeqEvent{isSeqEvent} {} // Reset scope between antecedent and consequent: liveness must not leak. void resetScope() { @@ -2900,7 +2909,7 @@ class AssertNfaVisitor final : public VNVisitor { FileLine* const flp = assertp->fileline(); SvaGraph graph; - SvaNfaBuilder builder{graph, m_modp, m_propTempNames, isCoverSeq}; + SvaNfaBuilder builder{graph, m_modp, m_propTempNames, isCoverSeq, isSeqEvent}; const BuildResult result = buildAssertionGraph(builder, graph, seqBodyp, parts, flp); if (result.valid()) wireMatchAndMidSources(graph, result, flp); diff --git a/test_regress/t/t_assert_seq_event_ctl.v b/test_regress/t/t_assert_seq_event_ctl.v index d36f916ec..ce9931e4b 100644 --- a/test_regress/t/t_assert_seq_event_ctl.v +++ b/test_regress/t/t_assert_seq_event_ctl.v @@ -66,8 +66,8 @@ module t ( final begin `checkd(hits, ref_hits); `checkd(one_hits, one_ref); - `checkd(hits, 19); // Other simulator: 19 - `checkd(one_hits, 60); // Other simulator: 60 + `checkd(hits, 19); + `checkd(one_hits, 60); $write("*-* All Finished *-*\n"); end endmodule diff --git a/test_regress/t/t_assert_seq_event_unsup.out b/test_regress/t/t_assert_seq_event_unsup.out index 4d77a1c85..61d38b9f7 100644 --- a/test_regress/t/t_assert_seq_event_unsup.out +++ b/test_regress/t/t_assert_seq_event_unsup.out @@ -3,6 +3,9 @@ 18 | @(g) a ##1 b; | ^ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:28:30: Unsupported: sequence used as an event control with a sequence operand of 'or' + 28 | @(posedge clk) (a ##1 b) or (a ##2 b); + | ^~ %Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:21:12: Unsupported: sequence referenced outside assertion property : ... note: In instance 't' 21 | sequence s_ref; diff --git a/test_regress/t/t_assert_seq_event_unsup.v b/test_regress/t/t_assert_seq_event_unsup.v index 0a39d3734..eda3b0772 100644 --- a/test_regress/t/t_assert_seq_event_unsup.v +++ b/test_regress/t/t_assert_seq_event_unsup.v @@ -21,6 +21,12 @@ module t ( sequence s_ref; @(posedge clk) a; endsequence + + // Legal but its endpoint topology is not buildable, so the wait could never + // resume; rejected rather than silently ignored. + sequence s_or; + @(posedge clk) (a ##1 b) or (a ##2 b); + endsequence // verilog_format: on // Legal: p is never asserted, so s_ref stays referenced outside any @@ -31,5 +37,6 @@ module t ( initial begin @s_nonedge; + @s_or; end endmodule