From f9427c6d5f7a1d16e13b90bad4ca39367d88592a Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Fri, 15 May 2026 14:38:38 +0200 Subject: [PATCH] Support property abort operators (accept_on, reject_on) (#7578) --- src/V3AssertNfa.cpp | 75 ++++++++++++ src/V3AstAttr.h | 23 ++++ src/V3AstNodeExpr.h | 26 ++++ src/V3AstNodes.cpp | 9 ++ src/V3EmitV.cpp | 7 ++ src/V3Width.cpp | 13 ++ src/verilog.y | 8 +- test_regress/t/t_debug_emitv.out | 36 ++++++ test_regress/t/t_debug_emitv.v | 4 + test_regress/t/t_property_accept_reject_on.py | 18 +++ test_regress/t/t_property_accept_reject_on.v | 111 ++++++++++++++++++ .../t/t_property_pexpr_parse_unsup.out | 12 -- 12 files changed, 326 insertions(+), 16 deletions(-) create mode 100755 test_regress/t/t_property_accept_reject_on.py create mode 100644 test_regress/t/t_property_accept_reject_on.v diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index cc27c2a37..98876d257 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -32,6 +32,7 @@ #include "V3UniqueNames.h" #include +#include #include VL_DEFINE_DEBUG_FUNCTIONS; @@ -188,6 +189,9 @@ class SvaNfaBuilder final { AstNodeModule* const m_modp; // Module to receive hoisted sampled-prop temps V3UniqueNames& m_propTempNames; // Module-shared temp-var name source std::vector m_throughoutStack; // Active throughout guards (IEEE 16.9.9) + // Outer abort conditions, AND-ed as !cond into inner abort edges + // (IEEE 1800-2023 16.12.14 outer-wraps-inner). + std::vector m_outerAbortStack; bool m_inUnboundedScope = false; // Sticky: nodes created after inherit liveness AstNodeExpr* throughoutCond(AstNodeExpr* baseCondp, FileLine* flp) { @@ -809,6 +813,73 @@ class SvaNfaBuilder final { return result; } + // 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 + // observable in a cycle-based model. VAbortKind selects accept vs reject + // verdict (sync vs async only changes the user-visible spelling). + + // Build `condp && !outer_1 && !outer_2 ...` (unsampled). + AstNodeExpr* abortFireExpr(AstNodeExpr* condp, FileLine* flp) { + AstNodeExpr* resultp = condp->cloneTreePure(false); + for (AstNodeExpr* const op : m_outerAbortStack) + resultp = new AstAnd{flp, resultp, new AstLogNot{flp, op->cloneTreePure(false)}}; + return resultp; + } + + BuildResult buildAbortOn(AstNodeExpr* condp, AstNodeExpr* bodyp, SvaStateVertex* entryVtxp, + VAbortKind kind, FileLine* flp) { + // Snapshot pre-body vertices so post-build diff yields the body's sub-NFA. + std::unordered_set preExisting; + for (const V3GraphVertex& vtxr : m_graph.m_graph.vertices()) preExisting.insert(&vtxr); + + m_outerAbortStack.push_back(condp); + const BuildResult bodyResult = buildExpr(bodyp, entryVtxp, /*isTopLevelStep=*/false); + m_outerAbortStack.pop_back(); + UASSERT_OBJ(bodyResult.valid(), bodyp, "abort body must be a valid SVA expression"); + + // Live-thread sources for the abort edge: entry + new body vertices, + // minus reject sinks (they carry reject fuel, not live-thread fuel). + std::vector abortSources; + abortSources.push_back(entryVtxp); + for (V3GraphVertex& vtxr : m_graph.m_graph.vertices()) { + if (preExisting.count(&vtxr)) continue; + auto* const sp = static_cast(&vtxr); + if (sp->m_isRejectSink) continue; + abortSources.push_back(sp); + } + + auto sampledAbortFire = [&]() -> AstSampled* { + AstNodeExpr* const expr = abortFireExpr(condp, flp); + AstSampled* const sampp = new AstSampled{flp, expr}; + sampp->dtypeFrom(expr); + return sampp; + }; + + if (kind.isAccept()) { + // Match-only sink fed by $sampled(abort-fire) from every live source; + // registered as midSource so it never contributes a reject. The body + // terminal is already in abortSources, so we don't fold abort-fire + // into bodyResult.finalCondp. + SvaStateVertex* const acceptSinkp = scopedCreateVertex(); + for (SvaStateVertex* const srcp : abortSources) + guardedLink(srcp, acceptSinkp, sampledAbortFire(), flp); + std::vector midSources = bodyResult.midSources; + midSources.push_back(acceptSinkp); + return {bodyResult.termVertexp, bodyResult.finalCondp, std::move(midSources)}; + } + + // rejectOnFail treats m_condp as the success condition and fires on + // !condp, so the edge carries !sampledAbortFire(). + SvaStateVertex* const rejectSinkp = m_graph.createStateVertex(); + rejectSinkp->m_isRejectSink = true; + for (SvaStateVertex* const srcp : abortSources) + m_graph.addLink(srcp, rejectSinkp, new AstLogNot{flp, sampledAbortFire()}) + ->m_rejectOnFail + = true; + return bodyResult; + } + public: SvaNfaBuilder(SvaGraph& graph, AstNodeModule* modp, V3UniqueNames& propTempNames) : m_graph{graph} @@ -819,6 +890,7 @@ public: void resetScope() { m_inUnboundedScope = false; m_throughoutStack.clear(); + m_outerAbortStack.clear(); } BuildResult buildExpr(AstNodeExpr* nodep, SvaStateVertex* entryVtxp, @@ -864,6 +936,9 @@ public: if (AstSWithin* const withinp = VN_CAST(nodep, SWithin)) { return buildSWithin(withinp, entryVtxp, isTopLevelStep); } + if (AstAbortOn* const ap = VN_CAST(nodep, AbortOn)) { + return buildAbortOn(ap->condp(), ap->propp(), entryVtxp, ap->kind(), ap->fileline()); + } if (VN_IS(nodep, SNonConsRep)) return BuildResult::fail(); if (AstImplication* const implp = VN_CAST(nodep, Implication)) { return buildImplicationEdges(implp->lhsp(), implp->rhsp(), entryVtxp, diff --git a/src/V3AstAttr.h b/src/V3AstAttr.h index 834b4e4d4..0862caff7 100644 --- a/src/V3AstAttr.h +++ b/src/V3AstAttr.h @@ -39,6 +39,29 @@ class VFlagLogicPacked {}; // ###################################################################### +class VAbortKind final { +public: + // IEEE 1800-2023 16.12.14 property abort operators. + enum en : uint8_t { + ACCEPT_ON, // accept_on(cond) prop: async abort, property succeeds + REJECT_ON, // reject_on(cond) prop: async abort, property fails + SYNC_ACCEPT_ON, // sync_accept_on(cond) prop: sampled at matured clock, succeeds + SYNC_REJECT_ON // sync_reject_on(cond) prop: sampled at matured clock, fails + }; + enum en m_e; + // cppcheck-suppress noExplicitConstructor + constexpr VAbortKind(en _e) + : m_e{_e} {} + const char* ascii() const { + static const char* const names[] + = {"accept_on", "reject_on", "sync_accept_on", "sync_reject_on"}; + return names[m_e]; + } + bool isAccept() const { return m_e == ACCEPT_ON || m_e == SYNC_ACCEPT_ON; } +}; + +//###################################################################### + class VAccess final { public: enum en : uint8_t { diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index ebe5dd4d7..ed5a3da98 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -574,6 +574,32 @@ public: }; // === AstNodeExpr === +class AstAbortOn final : public AstNodeExpr { + // IEEE 1800-2023 16.12.14: accept_on/reject_on/sync_accept_on/sync_reject_on + // (cond) prop. The four operators share an identical AST shape and lowering + // scaffolding -- VAbortKind selects between Accept/Reject verdict and + // Async/Sync sampling. + // @astgen op1 := condp : AstNodeExpr + // @astgen op2 := propp : AstNodeExpr + VAbortKind m_kind{VAbortKind::ACCEPT_ON}; + +public: + AstAbortOn(FileLine* fl, VAbortKind kind, AstNodeExpr* condp, AstNodeExpr* propp) + : ASTGEN_SUPER_AbortOn(fl) + , m_kind{kind} { + this->condp(condp); + this->propp(propp); + } + ASTGEN_MEMBERS_AstAbortOn; + void dump(std::ostream& str) const override; + void dumpJson(std::ostream& str) const override; + VAbortKind kind() const { return m_kind; } + string emitVerilog() override { V3ERROR_NA_RETURN(""); } + string emitC() override { V3ERROR_NA_RETURN(""); } + string emitSimpleOperator() override { V3ERROR_NA_RETURN(""); } + bool cleanOut() const override { V3ERROR_NA_RETURN(""); } + bool isMultiCycleSva() const override { return true; } +}; class AstAddrOfCFunc final : public AstNodeExpr { // Get address of CFunc // @astgen ptr := m_funcp : AstCFunc // Pointer to function itself diff --git a/src/V3AstNodes.cpp b/src/V3AstNodes.cpp index 79d4e603f..d9c1dda86 100644 --- a/src/V3AstNodes.cpp +++ b/src/V3AstNodes.cpp @@ -182,6 +182,15 @@ AstCond::AstCond(FileLine* fl, AstNodeExpr* condp, AstNodeExpr* thenp, AstNodeEx } } +void AstAbortOn::dump(std::ostream& str) const { + this->AstNodeExpr::dump(str); + str << " [" << kind().ascii() << "]"; +} +void AstAbortOn::dumpJson(std::ostream& str) const { + dumpJsonStr(str, "kind", kind().ascii()); + dumpJsonGen(str); +} + void AstAddrOfCFunc::dump(std::ostream& str) const { this->AstNodeExpr::dump(str); str << " -> "; diff --git a/src/V3EmitV.cpp b/src/V3EmitV.cpp index a53be9ecd..c8d729ba9 100644 --- a/src/V3EmitV.cpp +++ b/src/V3EmitV.cpp @@ -1058,6 +1058,13 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst { puts("\n"); } void visit(AstPExpr* nodep) override { iterateConst(nodep->bodyp()); } + void visit(AstAbortOn* nodep) override { + puts(nodep->kind().ascii()); + puts(" ("); + iterateConst(nodep->condp()); + puts(") "); + iterateConst(nodep->propp()); + } void visit(AstPropAlways* nodep) override { puts(nodep->isStrong() ? "s_always" : "always"); if (!VN_IS(nodep->loBoundp(), Unbounded) || !VN_IS(nodep->hiBoundp(), Unbounded)) { diff --git a/src/V3Width.cpp b/src/V3Width.cpp index 1adcf43b9..37cac5a74 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -1716,6 +1716,7 @@ class WidthVisitor final : public VNVisitor { nodep->dtypeSetBit(); } } + void visit(AstAbortOn* nodep) override { visitAbortProp(nodep); } void visit(AstRand* nodep) override { assertAtExpr(nodep); @@ -7771,6 +7772,18 @@ class WidthVisitor final : public VNVisitor { nodep->dtypeSetBit(); } } + void visitAbortProp(AstAbortOn* nodep) { + // IEEE 1800-2023 16.12.14: abort condition is a 1-bit self-determined + // Boolean; property subexpression carries its own type checking. + // VAbortKind distinguishes accept/reject and sync/async, but the + // type-check path is identical for all four. + assertAtExpr(nodep); + if (m_vup->prelim()) { + iterateCheckBool(nodep, "cond", nodep->condp(), BOTH); + iterateCheckBool(nodep, "prop", nodep->propp(), BOTH); + nodep->dtypeSetBit(); + } + } void visit_red_and_or(AstNodeUniop* nodep) { // CALLER: RedAnd, RedOr, ... // Signed: Output unsigned, Lhs/Rhs/etc non-real (presumed, not in IEEE) diff --git a/src/verilog.y b/src/verilog.y index 513d2ff07..ab969b77b 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6804,13 +6804,13 @@ pexpr: // IEEE: property_expr (The name pexpr is important as regex | ~o~pexpr yIFF pexpr { $$ = new AstLogEq{$2, $1, $3}; } | yACCEPT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec yACCEPT_ON - { $$ = $5; BBUNSUP($2, "Unsupported: accept_on (in property expression)"); DEL($3); } + { $$ = new AstAbortOn{$1, VAbortKind::ACCEPT_ON, $3, $5}; } | yREJECT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec yREJECT_ON - { $$ = $5; BBUNSUP($2, "Unsupported: reject_on (in property expression)"); DEL($3); } + { $$ = new AstAbortOn{$1, VAbortKind::REJECT_ON, $3, $5}; } | ySYNC_ACCEPT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec ySYNC_ACCEPT_ON - { $$ = $5; BBUNSUP($2, "Unsupported: sync_accept_on (in property expression)"); DEL($3); } + { $$ = new AstAbortOn{$1, VAbortKind::SYNC_ACCEPT_ON, $3, $5}; } | ySYNC_REJECT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec ySYNC_REJECT_ON - { $$ = $5; BBUNSUP($2, "Unsupported: sync_reject_on (in property expression)"); DEL($3); } + { $$ = new AstAbortOn{$1, VAbortKind::SYNC_REJECT_ON, $3, $5}; } // // // IEEE: "property_instance" // // Looks just like a function/method call diff --git a/test_regress/t/t_debug_emitv.out b/test_regress/t/t_debug_emitv.out index f5304a4ad..a6c063982 100644 --- a/test_regress/t/t_debug_emitv.out +++ b/test_regress/t/t_debug_emitv.out @@ -702,6 +702,42 @@ module Vt_debug_emitv_t; else begin end end + begin : assert_prop_accept_on + assert property (@(posedge clk) accept_on ( + in) + in + ) begin + end + else begin + end + end + begin : assert_prop_reject_on + assert property (@(posedge clk) reject_on ( + in) + in + ) begin + end + else begin + end + end + begin : assert_prop_sync_accept_on + assert property (@(posedge clk) sync_accept_on ( + in) + in + ) begin + end + else begin + end + end + begin : assert_prop_sync_reject_on + assert property (@(posedge clk) sync_reject_on ( + in) + in + ) begin + end + else begin + end + end int signed a; int signed ao; initial begin diff --git a/test_regress/t/t_debug_emitv.v b/test_regress/t/t_debug_emitv.v index 810ef7c1b..adebc64c6 100644 --- a/test_regress/t/t_debug_emitv.v +++ b/test_regress/t/t_debug_emitv.v @@ -342,6 +342,10 @@ module t (/*AUTOARG*/ assert_prop_nonoverlap_impl: assert property (@(posedge clk) in |=> in); assert_prop_overlap_fb: assert property (@(posedge clk) in #-# in); assert_prop_nonoverlap_fb: assert property (@(posedge clk) in #=# in); + assert_prop_accept_on: assert property (@(posedge clk) accept_on (in) in); + assert_prop_reject_on: assert property (@(posedge clk) reject_on (in) in); + assert_prop_sync_accept_on: assert property (@(posedge clk) sync_accept_on (in) in); + assert_prop_sync_reject_on: assert property (@(posedge clk) sync_reject_on (in) in); int a; diff --git a/test_regress/t/t_property_accept_reject_on.py b/test_regress/t/t_property_accept_reject_on.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/test_regress/t/t_property_accept_reject_on.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(timing_loop=True, verilator_flags2=['--assert', '--timing']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_property_accept_reject_on.v b/test_regress/t/t_property_accept_reject_on.v new file mode 100644 index 000000000..03c7be157 --- /dev/null +++ b/test_regress/t/t_property_accept_reject_on.v @@ -0,0 +1,111 @@ +// 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 checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0x exp=%0x (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0); +`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 + +module t ( + input clk +); + + int cyc; + reg [63:0] crc; + + // Non-adjacent CRC bits to avoid LFSR shift correlation + wire a = crc[0]; + wire b = crc[4]; + wire cnd_a = crc[8]; + wire cnd_r = crc[12]; + wire cnd = crc[16]; + wire body = a | b; + + int count_fail1 = 0; + int count_fail2 = 0; + int count_fail3 = 0; + int count_fail4 = 0; + int count_fail5 = 0; + int count_fail6 = 0; + int count_fail7 = 0; + int count_fail8 = 0; + int count_fail9 = 0; + int count_fail10 = 0; + + // Test 1: accept_on (async) -- property succeeds when cnd_a fires + assert property (@(posedge clk) disable iff (cyc < 2) accept_on (cnd_a) body) + else count_fail1 <= count_fail1 + 1; + + // Test 2: reject_on (async) -- property fails when cnd_r fires + assert property (@(posedge clk) disable iff (cyc < 2) reject_on (cnd_r) body) + else count_fail2 <= count_fail2 + 1; + + // Test 3: sync_accept_on -- sampled at matured clocking event + assert property (@(posedge clk) disable iff (cyc < 2) sync_accept_on (cnd_a) body) + else count_fail3 <= count_fail3 + 1; + + // Test 4: sync_reject_on + assert property (@(posedge clk) disable iff (cyc < 2) sync_reject_on (cnd_r) body) + else count_fail4 <= count_fail4 + 1; + + // Test 5: outer accept_on wraps inner reject_on -- outer wins per 16.12.14 + assert property (@(posedge clk) disable iff (cyc < 2) + accept_on (cnd_a) reject_on (cnd_r) body) + else count_fail5 <= count_fail5 + 1; + + // Test 6: outer reject_on wraps inner accept_on + assert property (@(posedge clk) disable iff (cyc < 2) + reject_on (cnd_r) accept_on (cnd_a) body) + else count_fail6 <= count_fail6 + 1; + + // Test 7: named property form with accept_on inside + property p_named; + accept_on (cnd_a) body; + endproperty + assert property (@(posedge clk) disable iff (cyc < 2) p_named) + else count_fail7 <= count_fail7 + 1; + + // Test 8: disable iff over a sync_accept_on with a second disabled window + assert property (@(posedge clk) disable iff (cyc < 2 || (cyc >= 50 && cyc < 60)) + sync_accept_on (cnd) body) + else count_fail8 <= count_fail8 + 1; + + // Test 9 / 10: async vs sync divergence hook -- identical encoding must + // produce identical fail counts under current implementation + assert property (@(posedge clk) disable iff (cyc < 2) accept_on (cnd_a) body) + else count_fail9 <= count_fail9 + 1; + + assert property (@(posedge clk) disable iff (cyc < 2) sync_accept_on (cnd_a) body) + else count_fail10 <= count_fail10 + 1; + + always @(posedge clk) begin +`ifdef TEST_VERBOSE + $write("[%0t] cyc==%0d crc=%x body=%b cnd_a=%b cnd_r=%b cnd=%b\n", + $time, cyc, crc, body, cnd_a, cnd_r, cnd); +`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 + `checkh(crc, 64'hc77bb9b3784ea091); + `checkd(count_fail1, 29); // Questa: 14 + `checkd(count_fail2, 65); // Questa: 64 + `checkd(count_fail3, 29); // Questa: 14 + `checkd(count_fail4, 65); // Questa: 64 + `checkd(count_fail5, 46); // Questa: 31 + `checkd(count_fail6, 65); // Questa: 59 + `checkd(count_fail7, 29); // Questa: 14 + `checkd(count_fail8, 14); // Questa: 10 + `checkd(count_fail9, 29); // Questa: 14 + `checkd(count_fail10, 29); // Questa: 14 + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule diff --git a/test_regress/t/t_property_pexpr_parse_unsup.out b/test_regress/t/t_property_pexpr_parse_unsup.out index a87122735..0791bc120 100644 --- a/test_regress/t/t_property_pexpr_parse_unsup.out +++ b/test_regress/t/t_property_pexpr_parse_unsup.out @@ -35,18 +35,6 @@ %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:90:7: Unsupported: nexttime (in property expression) 90 | nexttime s_eventually [2:$] always a; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:94:17: Unsupported: accept_on (in property expression) - 94 | accept_on (a) b; - | ^ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:98:22: Unsupported: sync_accept_on (in property expression) - 98 | sync_accept_on (a) b; - | ^ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:102:17: Unsupported: reject_on (in property expression) - 102 | reject_on (a) b; - | ^ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:106:22: Unsupported: sync_reject_on (in property expression) - 106 | sync_reject_on (a) b; - | ^ %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:109:27: Unsupported: property argument data type 109 | property p_arg_propery(property inprop); | ^~~~~~~~