luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Support property abort operators (accept_on, reject_on) (#7578)

This commit is contained in:
Yilou Wang 2026-05-15 14:38:38 +02:00 committed by GitHub
parent 442dd91683
commit f9427c6d5f
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
12 changed files with 326 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

75
src/V3AssertNfa.cpp
View File

@ -32,6 +32,7 @@
#include "V3UniqueNames.h"
#include <set>
#include <unordered_set>
#include <vector>
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<AstNodeExpr*> 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<AstNodeExpr*> 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<const V3GraphVertex*> 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<SvaStateVertex*> abortSources;
abortSources.push_back(entryVtxp);
for (V3GraphVertex& vtxr : m_graph.m_graph.vertices()) {
if (preExisting.count(&vtxr)) continue;
auto* const sp = static_cast<SvaStateVertex*>(&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<SvaStateVertex*> 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,

23
src/V3AstAttr.h
View File

@ -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 {

26
src/V3AstNodeExpr.h
View File

@ -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

9
src/V3AstNodes.cpp
View File

@ -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 << " -> ";

7
src/V3EmitV.cpp
View File

@ -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)) {

13
src/V3Width.cpp
View File

@ -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)

8
src/verilog.y
View File

@ -6804,13 +6804,13 @@ pexpr<nodeExprp>: // 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

36
test_regress/t/t_debug_emitv.out
View File

@ -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

4
test_regress/t/t_debug_emitv.v
View File

@ -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;

18
test_regress/t/t_property_accept_reject_on.py Executable file
View File

@ -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()

111
test_regress/t/t_property_accept_reject_on.v Normal file
View File

@ -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

12
test_regress/t/t_property_pexpr_parse_unsup.out
View File

@ -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);
| ^~~~~~~~