From 39b99010322b43cbca999a809af58b8368fd8842 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Tue, 2 Jun 2026 02:50:13 +0800 Subject: [PATCH] Support weak `until` / `until_with` property operators (#7290) (#7548) (#7685) Fixes #7290. Fixes #7685. --- src/V3AssertNfa.cpp | 108 ++++++++++++++++++ src/V3AstNodeExpr.h | 1 + src/V3Width.cpp | 6 + .../t/t_property_sexpr_parse_unsup.out | 38 +++--- test_regress/t/t_property_sexpr_unsup.out | 26 ++--- test_regress/t/t_property_sexpr_unsup.v | 2 + .../t/t_property_until_implication.py | 18 +++ test_regress/t/t_property_until_implication.v | 64 +++++++++++ 8 files changed, 227 insertions(+), 36 deletions(-) create mode 100755 test_regress/t/t_property_until_implication.py create mode 100644 test_regress/t/t_property_until_implication.v diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 6450e1a9b..3bfe7dfda 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -818,6 +818,91 @@ class SvaNfaBuilder final { return result; } + // until / until_with (weak forms only) per IEEE 1800-2023 16.12.12. + // Topology: combinational wait vertex with self-feeding state register. + // entry --link[T]--> waitC + // waitR --link[T]--> waitC (back-loop) + // waitC --edge[##1, sampled(p) && !sampled(q)]--> waitR (continue) + // waitC --link[REQUIRE, rejectOnFail]--> sink (per-cycle fail) + // waitC --link[T]--> match (added by wireMatchAndMidSources; + // accept condition rides via finalCondp) + // waitC is m_isUnbounded so the terminal-match link contributes only to + // terminalActive, not to rejectBase (which would otherwise spuriously fire + // every cycle q is false). Per-cycle reject comes from the explicit + // rejectOnFail link to the sink vertex. + // + // Weak non-overlapping (p until q): + // REQUIRE = sampled(p) || sampled(q) accept = sampled(q) + // Weak overlapping (p until_with q): + // REQUIRE = sampled(p) accept = sampled(p) && sampled(q) + BuildResult buildUntil(AstUntil* nodep, SvaStateVertex* entryVtxp, bool isTopLevelStep) { + FileLine* const flp = nodep->fileline(); + if (!isTopLevelStep) { + nodep->v3warn(E_UNSUPPORTED, "Unsupported: 'until' in complex property expression"); + return BuildResult::failWithError(); + } + if (nodep->isStrong()) { + nodep->v3warn(E_UNSUPPORTED, "Unsupported: s_until" + << (nodep->isOverlapping() ? "_with" : "") + << " (in property expresion)"); + return BuildResult::failWithError(); + } + AstNodeExpr* const lhsp = nodep->lhsp(); + AstNodeExpr* const rhsp = nodep->rhsp(); + const auto hasSeq = [](const AstNodeExpr* ep) { + return ep->exists([](const AstNodeExpr* np) { return np->isMultiCycleSva(); }); + }; + if (hasSeq(lhsp) || hasSeq(rhsp)) { + nodep->v3warn(E_UNSUPPORTED, "Unsupported: 'until' in complex property expression"); + return BuildResult::failWithError(); + } + + const bool ov = nodep->isOverlapping(); + AstNodeExpr* const lhsBitp = nodep->lhsp(); + AstNodeExpr* const rhsBitp = nodep->rhsp(); + // p hoist count: continue, require (ov: 1 use; nov: 1 use). At least 2 uses. + AstVar* const pHoistp = tryHoistSampled(lhsBitp, flp, 2); + // q hoist count: continue (1) + require nov (1) = 2; ov: continue only (1). + AstVar* const qHoistp = ov ? nullptr : tryHoistSampled(rhsBitp, flp, 2); + + SvaStateVertex* const waitCp = scopedCreateVertex(); + SvaStateVertex* const waitRp = scopedCreateVertex(); + waitCp->m_isUnbounded = true; + + // Entry and back-loop Links carry no condition; throughout-folding still applies. + guardedLink(entryVtxp, waitCp, flp); + guardedLink(waitRp, waitCp, flp); + + // Continue clocked edge: p && !q advances to next-cycle wait. + AstNodeExpr* const contCondp + = new AstLogAnd{flp, sampledRefOrClone(pHoistp, lhsBitp, flp), + new AstLogNot{flp, sampledRefOrClone(qHoistp, rhsBitp, flp)}}; + guardedEdge(waitCp, waitRp, contCondp, flp); + + // Reject sink: fires when require-condition is false. + SvaStateVertex* const sinkVtxp = m_graph.createStateVertex(); + sinkVtxp->m_isRejectSink = true; + AstNodeExpr* requireCondp; + if (ov) { + requireCondp = sampledRefOrClone(pHoistp, lhsBitp, flp); + } else { + requireCondp = new AstLogOr{flp, sampledRefOrClone(pHoistp, lhsBitp, flp), + sampledRefOrClone(qHoistp, rhsBitp, flp)}; + } + SvaTransEdge* const rejEdgep = m_graph.addLink(waitCp, sinkVtxp, requireCondp); + rejEdgep->m_rejectOnFail = true; + + // Accept condition rides via finalCondp; assembleResult $sampled-wraps it. + AstNodeExpr* acceptCondp; + if (ov) { + acceptCondp + = new AstLogAnd{flp, lhsBitp->cloneTreePure(false), rhsBitp->cloneTreePure(false)}; + } else { + acceptCondp = rhsBitp->cloneTreePure(false); + } + return {waitCp, acceptCondp, {}}; + } + // IEEE 1800-2023 16.12.14 property abort operators. Sync and async share // the same NFA encoding: AstSampled already gives matured values at every // maturing clocking event, and async firing "between clocks" is not @@ -948,6 +1033,9 @@ public: implp->isOverlapped(), implp->isFollowedBy(), implp->lhsp(), implp->fileline()); } + if (AstUntil* const untilp = VN_CAST(nodep, Until)) { + return buildUntil(untilp, entryVtxp, isTopLevelStep); + } // Boolean leaf (including LogAnd): return as finalCond return {entryVtxp, nodep, {}}; } @@ -1836,6 +1924,25 @@ class AssertNfaVisitor final : public VNVisitor { }); } + // Bare `assert property (p until q)` with boolean operands stays on + // V3AssertPre's AstLoop lowering, which preserves per-attempt action-block + // firings that this NFA's single-bit aggregated state cannot. NFA still + // owns strong forms, sequence operands, and any embedding inside a + // multi-cycle context (implication consequent, or/and operands, etc.). + static bool isBareTopLevelUntil(AstNode* propp) { + AstNode* p = propp; + if (AstPropSpec* const specp = VN_CAST(p, PropSpec)) p = specp->propp(); + while (AstLogNot* const notp = VN_CAST(p, LogNot)) p = notp->lhsp(); + AstUntil* const untilp = VN_CAST(p, Until); + if (!untilp) return false; + if (untilp->isStrong()) return false; + const auto hasSeq = [](const AstNodeExpr* ep) { + return ep->exists([](const AstNodeExpr* np) { return np->isMultiCycleSva(); }); + }; + if (hasSeq(untilp->lhsp()) || hasSeq(untilp->rhsp())) return false; + return true; + } + struct PropertyParts final { AstNodeExpr* triggerExprp = nullptr; AstNodeExpr* seqExprp = nullptr; @@ -2083,6 +2190,7 @@ class AssertNfaVisitor final : public VNVisitor { AstNode* const propp = assertp->propp(); if (!hasMultiCycleExpr(propp)) return; + if (isBareTopLevelUntil(propp)) return; PropertyParts parts = decomposeProperty(propp); UASSERT_OBJ(parts.seqExprp, propp, "Property body must be an expression"); diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index d1840a1c0..4d33a0aa0 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -2908,6 +2908,7 @@ public: bool cleanOut() const override { V3ERROR_NA_RETURN(""); } int instrCount() const override { return widthInstrs(); } bool sameNode(const AstNode* /*samep*/) const override { return true; } + bool isMultiCycleSva() const override { return true; } bool isStrong() const { return m_strong; } bool isOverlapping() const { return m_overlapping; } }; diff --git a/src/V3Width.cpp b/src/V3Width.cpp index 7005b72dd..ffb300d68 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -1715,6 +1715,12 @@ class WidthVisitor final : public VNVisitor { if (m_vup->prelim()) { iterateCheckBool(nodep, "LHS", nodep->lhsp(), BOTH); iterateCheckBool(nodep, "RHS", nodep->rhsp(), BOTH); + // Coerce unsized constant operands (e.g. literal 0/1) to actual + // 1-bit width; iterateCheckBool keeps widthMin-fitting unsized + // constants at their nominal 32-bit width, which trips the + // downstream NFA lowering's Log* chains in V3AssertNfa. + if (nodep->lhsp()->width() != 1) fixWidthReduce(nodep->lhsp()); + if (nodep->rhsp()->width() != 1) fixWidthReduce(nodep->rhsp()); nodep->dtypeSetBit(); } } diff --git a/test_regress/t/t_property_sexpr_parse_unsup.out b/test_regress/t/t_property_sexpr_parse_unsup.out index 000137bfe..f84b96594 100644 --- a/test_regress/t/t_property_sexpr_parse_unsup.out +++ b/test_regress/t/t_property_sexpr_parse_unsup.out @@ -1,22 +1,26 @@ -%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:70:14: Logical operator IMPLICATION expects 1 bit on the RHS, but RHS's CMETHODHARD 'at' generates 8 bits. +%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:72:14: Logical operator IMPLICATION expects 1 bit on the RHS, but RHS's CMETHODHARD 'at' generates 8 bits. : ... note: In instance 't.ieee' - 70 | $rose(a) |-> q[0]; + 72 | $rose(a) |-> q[0]; | ^~~ ... For warning description see https://verilator.org/warn/WIDTHTRUNC?v=latest ... Use "/* verilator lint_off WIDTHTRUNC */" and lint_on around source to disable this message. -%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:75:29: Logical operator SEXPR expects 1 bit on the exprp, but exprp's CMETHODHARD 'at' generates 8 bits. +%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:77:29: Logical operator SEXPR expects 1 bit on the exprp, but exprp's CMETHODHARD 'at' generates 8 bits. : ... note: In instance 't.ieee' - 75 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; + 77 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; | ^~ -%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:96:31: Logical operator SEXPR expects 1 bit on the exprp, but exprp's VARREF 'b' generates 32 bits. +%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:98:31: Logical operator SEXPR expects 1 bit on the exprp, but exprp's VARREF 'b' generates 32 bits. : ... note: In instance 't.ieee' - 96 | assert property (@clk not a ##1 b); + 98 | assert property (@clk not a ##1 b); | ^~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:47:49: Unsupported: 'until' in complex property expression +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:47:39: Unsupported: 'until' in complex property expression : ... note: In instance 't' 47 | assert property (@(posedge clk) val until val until val) $display("[%0t] nested until, fileline:%d", $time, 47); - | ^~~~~ + | ^~~~~ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:49:39: Unsupported: 'until' in complex property expression + : ... note: In instance 't' + 49 | assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, 49); + | ^~~~~ %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:51:39: Unsupported: s_until (in property expresion) : ... note: In instance 't' 51 | assert property (@(posedge clk) val s_until !val) $display("[%0t] s_until, fileline:%d", $time, 51); @@ -25,16 +29,8 @@ : ... note: In instance 't' 53 | assert property (@(posedge clk) val s_until_with val) $display("[%0t] s_until_with, fileline:%d", $time, 53); | ^~~~~~~~~~~~ -%Error: t/t_property_sexpr_unsup.v:49:50: Duplicate declaration of block: '__VcycleDly_h########__2__block' - : ... note: In instance 't' - 49 | assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, 49); - | ^~ - t/t_property_sexpr_unsup.v:49:50: ... Location of original declaration - 49 | assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, 49); - | ^~ - ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. -%Error: Internal Error: t/t_property_sexpr_unsup.v:45:44: ../V3Ast.cpp:#: AstPExpr::bodyp() cannot have a non-nullptr nextp() - : ... note: In instance 't' - 45 | assert property (@(posedge clk) ##1 (val until val)) $display("[%0t] until in sequence, fileline:%d", $time, 45); - | ^~~~~ - ... This fatal error may be caused by the earlier error(s); resolve those first. +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:40: Unsupported: 'until' in complex property expression + : ... note: In instance 't' + 55 | assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, 55); + | ^~~~~ +%Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr_unsup.out b/test_regress/t/t_property_sexpr_unsup.out index 541d3194a..a13d0fd31 100644 --- a/test_regress/t/t_property_sexpr_unsup.out +++ b/test_regress/t/t_property_sexpr_unsup.out @@ -1,8 +1,12 @@ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:47:49: Unsupported: 'until' in complex property expression +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:47:39: Unsupported: 'until' in complex property expression : ... note: In instance 't' 47 | assert property (@(posedge clk) val until val until val) $display("[%0t] nested until, fileline:%d", $time, 47); - | ^~~~~ + | ^~~~~ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:49:39: Unsupported: 'until' in complex property expression + : ... note: In instance 't' + 49 | assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, 49); + | ^~~~~ %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:51:39: Unsupported: s_until (in property expresion) : ... note: In instance 't' 51 | assert property (@(posedge clk) val s_until !val) $display("[%0t] s_until, fileline:%d", $time, 51); @@ -11,16 +15,8 @@ : ... note: In instance 't' 53 | assert property (@(posedge clk) val s_until_with val) $display("[%0t] s_until_with, fileline:%d", $time, 53); | ^~~~~~~~~~~~ -%Error: t/t_property_sexpr_unsup.v:49:50: Duplicate declaration of block: '__VcycleDly_h########__2__block' - : ... note: In instance 't' - 49 | assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, 49); - | ^~ - t/t_property_sexpr_unsup.v:49:50: ... Location of original declaration - 49 | assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, 49); - | ^~ - ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. -%Error: Internal Error: t/t_property_sexpr_unsup.v:45:44: ../V3Ast.cpp:#: AstPExpr::bodyp() cannot have a non-nullptr nextp() - : ... note: In instance 't' - 45 | assert property (@(posedge clk) ##1 (val until val)) $display("[%0t] until in sequence, fileline:%d", $time, 45); - | ^~~~~ - ... This fatal error may be caused by the earlier error(s); resolve those first. +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:40: Unsupported: 'until' in complex property expression + : ... note: In instance 't' + 55 | assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, 55); + | ^~~~~ +%Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr_unsup.v b/test_regress/t/t_property_sexpr_unsup.v index c59b2b738..d6a5b4aca 100644 --- a/test_regress/t/t_property_sexpr_unsup.v +++ b/test_regress/t/t_property_sexpr_unsup.v @@ -52,6 +52,8 @@ module t ( /*AUTOARG*/ assert property (@(posedge clk) val s_until_with val) $display("[%0t] s_until_with, fileline:%d", $time, `__LINE__); + assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, `__LINE__); + property prop_implication; ##1 cyc == 4 |-> 1; endproperty diff --git a/test_regress/t/t_property_until_implication.py b/test_regress/t/t_property_until_implication.py new file mode 100755 index 000000000..d93b04ea1 --- /dev/null +++ b/test_regress/t/t_property_until_implication.py @@ -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(verilator_flags2=['--assert']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_property_until_implication.v b/test_regress/t/t_property_until_implication.v new file mode 100644 index 000000000..6023ac501 --- /dev/null +++ b/test_regress/t/t_property_until_implication.v @@ -0,0 +1,64 @@ +// 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 (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0); +// verilog_format: on + +module t ( + input clk +); + + int cyc; + reg [63:0] crc; + + // CRC bits chosen far apart to keep antecedent/consequent uncorrelated. + wire trig = crc[0]; + wire c = crc[10]; + wire d = crc[20] | crc[40]; + + int fail_nonoverlap = 0; + int fail_overlap = 0; + + // Weak non-overlapping until as implication consequent. + // IEEE 1800-2023 16.12.12: c true at every tick until at least one tick + // before d holds. Cycle-aggregated reject fires when c=0 and d=0 in a cycle + // where the consequent attempt is still live. + assert property (@(posedge clk) trig |=> c until d) + else fail_nonoverlap = fail_nonoverlap + 1; + + // Weak overlapping (until_with) as implication consequent. + assert property (@(posedge clk) trig |=> c until_with d) + else fail_overlap = fail_overlap + 1; + + // Exercises buildUntil's bit-coerce branch: V3Width leaves unsized constants + // at their nominal 32-bit dtype, so hoist-temp assignments need an explicit + // 1-bit reduction. The assertion itself is trivially true (q == 1). + assert property (@(posedge clk) trig |=> 0 until 1); + + always @(posedge clk) begin +`ifdef TEST_VERBOSE + $write("[%0t] cyc==%0d crc=%x trig=%b c=%b d=%b\n", $time, cyc, crc, trig, c, d); +`endif + cyc <= cyc + 1; + crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; + if (cyc == 0) begin + crc <= 64'h5aef0c8d_d70a4497; + end + else if (cyc == 99) begin + // Counts reflect NFA per-cycle reject aggregation, not Questa's + // per-attempt action_block firing; the two differ by a small constant + // (see PR description for the model gap). Test is a regression for + // "no internal error on `until` as |=> consequent" (issue #7548). + `checkd(fail_nonoverlap, 7); + `checkd(fail_overlap, 22); + $write("*-* All Finished *-*\n"); + $finish; + end + end + +endmodule