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

Support followed-by operators `#-#` and `#=#` in properties (#7523)

This commit is contained in:
Yilou Wang 2026-05-04 14:10:37 +02:00 committed by GitHub
parent ddcb04b921
commit bc1acc8aa3
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
14 changed files with 295 additions and 50 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

93
src/V3AssertNfa.cpp
View File

@ -839,10 +839,75 @@ public:
return buildSWithin(withinp, entryVtxp, isTopLevelStep);
}
if (VN_IS(nodep, SNonConsRep)) return BuildResult::fail();
if (AstImplication* const implp = VN_CAST(nodep, Implication)) {
return buildImplicationEdges(implp->lhsp(), implp->rhsp(), entryVtxp,
implp->isOverlapped(), implp->isFollowedBy(),
implp->lhsp(), implp->fileline());
}
// Boolean leaf (including LogAnd): return as finalCond
return {entryVtxp, nodep, {}};
}
// Wire an implication / followed-by from `entryVtxp`: builds the antecedent,
// emits the match-link (and for followed-by the reject-sink edge), inserts a
// delay vertex for non-overlapped forms, and builds the body. Used both for
// nested AstImplication in pexpr position and for the top-level assertion
// antecedent -- `errorNodep` anchors the "unsupported sequence antecedent"
// error, which differs between the two call sites.
BuildResult buildImplicationEdges(AstNodeExpr* antExprp, AstNodeExpr* bodyExprp,
SvaStateVertex* entryVtxp, bool isOverlapped,
bool isFollowedBy, AstNode* errorNodep, FileLine* flp) {
const BuildResult antResult = buildExpr(antExprp, entryVtxp);
if (!antResult.valid()) return antResult;
// Followed-by requires pure-boolean antecedent for non-vacuous-fail at
// the attempt-start cycle. IEEE 1800-2023 16.12.9 permits a multi-cycle
// sequence LHS, so this is an implementation gap rather than illegal SV.
if (isFollowedBy && antResult.termVertexp != entryVtxp) {
errorNodep->v3warn(E_UNSUPPORTED,
"Unsupported: sequence expression as antecedent of followed-by"
" (#-# / #=#) (IEEE 1800-2023 16.12.9)");
return BuildResult::failWithError();
}
UASSERT_OBJ(!isFollowedBy || antResult.finalCondp, errorNodep,
"followed-by antecedent terminal at entry must carry finalCondp");
// Use raw createStateVertex() so trigVtxp starts without liveness --
// reaching the antecedent terminal is a definitive event.
SvaStateVertex* const trigVtxp = m_graph.createStateVertex();
if (antResult.finalCondp) {
m_graph.addLink(antResult.termVertexp, trigVtxp,
sampled(antResult.finalCondp->cloneTreePure(false)));
// Followed-by non-vacuous fail: rejectOnFail fires when the attempt
// is live (termVtx reachable) and sampled(antecedent) is false.
if (isFollowedBy) {
SvaStateVertex* const sinkVtxp = m_graph.createStateVertex();
sinkVtxp->m_isRejectSink = true;
SvaTransEdge* const ep
= m_graph.addLink(antResult.termVertexp, sinkVtxp,
sampled(antResult.finalCondp->cloneTreePure(false)));
ep->m_rejectOnFail = true;
}
// finalCondp is cloned into the Sampled nodes; if the original is
// not parented anywhere in the AST anymore it must be freed here
// or ASan flags it as a leak (e.g. t_sequence_bool_ops).
if (!antResult.finalCondp->backp()) {
VL_DO_DANGLING(antResult.finalCondp->deleteTree(), antResult.finalCondp);
}
} else {
m_graph.addLink(antResult.termVertexp, trigVtxp);
}
resetScope();
SvaStateVertex* bodyEntryp = trigVtxp;
if (!isOverlapped) {
SvaStateVertex* const delayVtxp = m_graph.createStateVertex();
m_graph.addClockedEdge(trigVtxp, delayVtxp);
bodyEntryp = delayVtxp;
}
return buildExpr(bodyExprp, bodyEntryp, /*isTopLevelStep=*/true);
}
BuildResult build(AstNodeExpr* exprp) {
m_graph.m_startVertexp = scopedCreateVertex();
return buildExpr(exprp, m_graph.m_startVertexp, /*isTopLevelStep=*/true);
@ -1688,6 +1753,7 @@ class AssertNfaVisitor final : public VNVisitor {
AstNodeExpr* seqExprp = nullptr;
bool isOverlapped = true;
bool hasImplication = false;
bool isFollowedBy = false; // True for #-# / #=# (non-vacuous-fail on antecedent miss)
};
static PropertyParts decomposeProperty(AstNode* propp) {
@ -1696,6 +1762,7 @@ class AssertNfaVisitor final : public VNVisitor {
if (AstImplication* const implp = VN_CAST(propp, Implication)) {
parts.hasImplication = true;
parts.isOverlapped = implp->isOverlapped();
parts.isFollowedBy = implp->isFollowedBy();
parts.triggerExprp = implp->lhsp();
parts.seqExprp = implp->rhsp();
} else if (AstNodeExpr* const exprp = VN_CAST(propp, NodeExpr)) {
@ -1759,29 +1826,9 @@ class AssertNfaVisitor final : public VNVisitor {
if (!parts.hasImplication) return builder.build(seqBodyp);
graph.m_startVertexp = graph.createStateVertex();
const BuildResult antResult = builder.buildExpr(parts.triggerExprp, graph.m_startVertexp);
if (!antResult.valid()) return antResult;
// Use raw createStateVertex() (not scopedCreateVertex) so trigVtxp starts
// without liveness. Reaching the antecedent terminal is a definitive event.
SvaStateVertex* const trigVtxp = graph.createStateVertex();
if (antResult.finalCondp) {
AstSampled* const sampp
= new AstSampled{flp, antResult.finalCondp->cloneTreePure(false)};
sampp->dtypeFrom(antResult.finalCondp);
graph.addLink(antResult.termVertexp, trigVtxp, sampp);
if (!antResult.finalCondp->backp()) pushDeletep(antResult.finalCondp);
} else {
graph.addLink(antResult.termVertexp, trigVtxp);
}
builder.resetScope();
if (parts.isOverlapped) {
return builder.buildExpr(seqBodyp, trigVtxp, /*isTopLevelStep=*/true);
}
SvaStateVertex* const delayVtxp = graph.createStateVertex();
graph.addClockedEdge(trigVtxp, delayVtxp);
return builder.buildExpr(seqBodyp, delayVtxp, /*isTopLevelStep=*/true);
return builder.buildImplicationEdges(parts.triggerExprp, seqBodyp, graph.m_startVertexp,
parts.isOverlapped, parts.isFollowedBy,
parts.triggerExprp, flp);
}
// Install the pass-action handler and per-thread fail-handlers generated by

12
src/V3AssertPre.cpp
View File

@ -1002,6 +1002,18 @@ private:
void visit(AstImplication* nodep) override {
if (nodep->sentreep()) return; // Already processed
// Top-level followed-by is claimed by V3AssertNfa; anything reaching here
// is nested inside iff/implies/or. IEEE 1800-2023 16.12.9 permits the
// composition, but silent lowering would drop non-vacuous-fail semantics.
if (nodep->isFollowedBy()) {
nodep->v3warn(E_UNSUPPORTED,
"Unsupported: followed-by (#-# / #=#) nested inside property operator"
" (iff/implies/or) (IEEE 1800-2023 16.12.9)");
nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}});
VL_DO_DANGLING(pushDeletep(nodep), nodep);
return;
}
// Handle goto repetition as antecedent before iterateChildren,
// so the standalone AstSGotoRep visitor doesn't process it
if (AstSGotoRep* const gotop = VN_CAST(nodep->lhsp(), SGotoRep)) {

20
src/V3AstNodeExpr.h
View File

@ -1685,31 +1685,37 @@ public:
bool sameNode(const AstNode* /*samep*/) const override { return true; }
};
class AstImplication final : public AstNodeExpr {
// Verilog Implication Operator
// Nonoverlapped "|=>"
// Overlapped "|->"
// Implication |-> |=> (IEEE 1800-2023 16.12.6) and followed-by #-# #=#
// (IEEE 1800-2023 16.12.9). Antecedent-miss is vacuous-pass for implication
// and non-vacuous-fail for followed-by, hence the separate flag.
// @astgen op1 := lhsp : AstNodeExpr
// @astgen op2 := rhsp : AstNodeExpr
// @astgen op3 := sentreep : Optional[AstSenTree]
private:
const bool m_isOverlapped; // True if overlapped
const bool m_isOverlapped; // True if overlapped form (|-> / #-#)
const bool m_isFollowedBy; // True if followed-by (#-# / #=#) rather than implication
public:
AstImplication(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp, bool isOverlapped)
AstImplication(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp, bool isOverlapped,
bool isFollowedBy = false)
: ASTGEN_SUPER_Implication(fl)
, m_isOverlapped{isOverlapped} {
, m_isOverlapped{isOverlapped}
, m_isFollowedBy{isFollowedBy} {
this->lhsp(lhsp);
this->rhsp(rhsp);
}
ASTGEN_MEMBERS_AstImplication;
void dump(std::ostream& str) const override;
void dumpJson(std::ostream& str) const override;
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(""); }
int instrCount() const override { return widthInstrs(); }
bool sameNode(const AstNode* /*samep*/) const override { return true; }
bool isMultiCycleSva() const override { return m_isFollowedBy; }
bool isOverlapped() const { return m_isOverlapped; }
bool isFollowedBy() const { return m_isFollowedBy; }
};
class AstInitArray final : public AstNodeExpr {
// This is also used as an array value in V3Simulate/const prop.

10
src/V3AstNodes.cpp
View File

@ -2161,6 +2161,16 @@ void AstIfaceRefDType::dumpSmall(std::ostream& str) const {
this->AstNodeDType::dumpSmall(str);
str << "iface";
}
void AstImplication::dump(std::ostream& str) const {
this->AstNodeExpr::dump(str);
if (isOverlapped()) str << " [overlapped]";
if (isFollowedBy()) str << " [followed-by]";
}
void AstImplication::dumpJson(std::ostream& str) const {
this->AstNodeExpr::dumpJson(str);
dumpJsonBoolFuncIf(str, isOverlapped);
dumpJsonBoolFuncIf(str, isFollowedBy);
}
void AstInitArray::dumpInitList(std::ostream& str) const {
int n = 0;
const auto& mapr = map();

6
src/verilog.y
View File

@ -6755,10 +6755,12 @@ pexpr<nodeExprp>: // IEEE: property_expr (The name pexpr is important as regex
// // IEEE-2012: yIF and yCASE
| property_exprCaseIf { $$ = $1; }
//
// // IEEE: "sequence_expr yP_POUNDMINUSPD pexpr" (followed-by #-#/#=#)
// // Reuses AstImplication with m_isFollowedBy to carry non-vacuous-fail polarity
| ~o~pexpr/*sexpr*/ yP_POUNDMINUSPD pexpr
{ $$ = $1; BBUNSUP($2, "Unsupported: #-# (in property expression)"); DEL($3); }
{ $$ = new AstImplication{$2, $1, $3, true, true}; }
| ~o~pexpr/*sexpr*/ yP_POUNDEQPD pexpr
{ $$ = $1; BBUNSUP($2, "Unsupported: #=# (in property expression)"); DEL($3); }
{ $$ = new AstImplication{$2, $1, $3, false, true}; }
| yNEXTTIME pexpr
{ $$ = $2; BBUNSUP($1, "Unsupported: nexttime (in property expression)"); }
| yS_NEXTTIME pexpr

36
test_regress/t/t_debug_emitv.out
View File

@ -666,6 +666,42 @@ module Vt_debug_emitv_t;
else begin
end
end
begin : assert_prop_overlap_impl
assert property (@(posedge clk)
???? // IMPLICATION
inin
) begin
end
else begin
end
end
begin : assert_prop_nonoverlap_impl
assert property (@(posedge clk)
???? // IMPLICATION
inin
) begin
end
else begin
end
end
begin : assert_prop_overlap_fb
assert property (@(posedge clk)
???? // IMPLICATION
inin
) begin
end
else begin
end
end
begin : assert_prop_nonoverlap_fb
assert property (@(posedge clk)
???? // IMPLICATION
inin
) begin
end
else begin
end
end
int signed a;
int signed ao;
initial begin

4
test_regress/t/t_debug_emitv.v
View File

@ -338,6 +338,10 @@ module t (/*AUTOARG*/
assert_prop_always: assert property (@(posedge clk) always [0:3] in);
assert_prop_s_always: assert property (@(posedge clk) s_always [1:2] in);
assert_prop_overlap_impl: assert property (@(posedge clk) in |-> in);
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);
int a;

18
test_regress/t/t_prop_followed_by.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()
test.execute()
test.passes()

69
test_regress/t/t_prop_followed_by.v Normal file
View File

@ -0,0 +1,69 @@
// 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
`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);
module t (
input clk
);
integer cyc = 0;
reg [63:0] crc = 64'h5aef0c8d_d70a4497;
wire a = crc[0];
wire b = crc[1];
wire wide = crc[2] | crc[3] | crc[4] | crc[5] | crc[6];
integer ovl_f = 0;
integer novl_f = 0;
integer impl_f = 0;
integer nimp_f = 0;
integer wide_f = 0;
// Smoke: trivially-true forms must compile and never fail.
assert property (@(posedge clk) 1'b1 #-# 1'b1);
assert property (@(posedge clk) 0 |-> (0 #-# 0));
assert property (@(posedge clk) 0 |-> (0 #=# 0));
// Duality: #-# / #=# non-vacuously fail on antecedent miss; |-> / |=> vacuously
// pass. Counters expose the asymmetry: ovl / novl include both antecedent-miss
// and consequent-miss; impl / nimp count consequent-miss only.
assert property (@(posedge clk) a #-# b)
else ovl_f = ovl_f + 1;
assert property (@(posedge clk) a #=# b)
else novl_f = novl_f + 1;
assert property (@(posedge clk) a |-> b)
else impl_f = impl_f + 1;
assert property (@(posedge clk) a |=> b)
else nimp_f = nimp_f + 1;
// Antecedent-implies-self consequent: never fails on any cycle.
assert property (@(posedge clk) wide |-> (wide #-# wide))
else wide_f = wide_f + 1;
always @(posedge clk) begin
cyc <= cyc + 1;
crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
if (cyc == 32) begin
// Counts are deterministic for this CRC seed. Questa reference run
// (IEEE 1800-2023 16.12.9) reports ovl=28, novl=19, impl=9, nimp=0; the
// ovl/novl deltas vs Verilator are 1-cycle preponed-sampling differences.
$display("ovl=%0d novl=%0d impl=%0d nimp=%0d wide=%0d", ovl_f, novl_f, impl_f, nimp_f,
wide_f);
`checkd(ovl_f, 29);
`checkd(novl_f, 20);
`checkd(impl_f, 9);
`checkd(nimp_f, 0);
`checkd(wide_f, 0);
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule

10
test_regress/t/t_prop_followed_by_bad.out Normal file
View File

@ -0,0 +1,10 @@
%Error-UNSUPPORTED: t/t_prop_followed_by_bad.v:23:38: Unsupported: sequence expression as antecedent of followed-by (#-# / #=#) (IEEE 1800-2023 16.12.9)
: ... note: In instance 't'
23 | assert property (@(posedge clk) (a ##1 b) #-# c);
| ^~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_prop_followed_by_bad.v:29:38: Unsupported: followed-by (#-# / #=#) nested inside property operator (iff/implies/or) (IEEE 1800-2023 16.12.9)
: ... note: In instance 't'
29 | assert property (@(posedge clk) (a #-# b) iff c);
| ^~~
%Error: Exiting due to

18
test_regress/t/t_prop_followed_by_bad.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('vlt')
test.compile(expect_filename=test.golden_filename,
verilator_flags2=['--timing'],
fails=test.vlt_all)
test.passes()

31
test_regress/t/t_prop_followed_by_bad.v Normal file
View File

@ -0,0 +1,31 @@
// 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
module t ( /*AUTOARG*/
// Inputs
clk
);
input clk;
reg a = 0;
reg b = 0;
reg c = 0;
// True multi-cycle sequence LHS of followed-by is not yet supported.
// IEEE 1800-2023 16.12.9 allows sequence_expr #-# property_expr, but the
// NFA needs a different fail detector for sequence-failure than for
// boolean-failure (see V3AssertNfa::buildImplication). Rejected with an
// explicit UNSUPPORTED message.
assert property (@(posedge clk) (a ##1 b) #-# c);
// Followed-by embedded inside boolean property connectives (`implies`, `iff`)
// is currently unsupported: NFA claims the assertion but only routes
// top-level / directly-reachable AstImplication through the followed-by
// NFA builder. A loud UNSUPPORTED beats a silent lowering-as-plain-implication.
assert property (@(posedge clk) (a #-# b) iff c);
endmodule

6
test_regress/t/t_property_pexpr_unsup.out
View File

@ -5,12 +5,6 @@
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:27:9: Unsupported: weak (in property expression)
27 | weak(a);
| ^
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:43:7: Unsupported: #-# (in property expression)
43 | a #-# b;
| ^~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:47:7: Unsupported: #=# (in property expression)
47 | a #=# b;
| ^~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:51:5: Unsupported: nexttime (in property expression)
51 | nexttime a;
| ^~~~~~~~

12
test_regress/t/t_property_unsup.out
View File

@ -17,12 +17,6 @@
%Error-UNSUPPORTED: t/t_property_unsup.v:92:46: Unsupported: s_eventually (in property expression)
92 | assert property ((s_eventually a) implies (s_eventually a));
| ^~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_unsup.v:102:23: Unsupported: #-# (in property expression)
102 | assert property ((a #-# b) implies (a #-# b));
| ^~~
%Error-UNSUPPORTED: t/t_property_unsup.v:102:41: Unsupported: #-# (in property expression)
102 | assert property ((a #-# b) implies (a #-# b));
| ^~~
%Error-UNSUPPORTED: t/t_property_unsup.v:112:21: Unsupported: eventually[] (in property expression)
112 | assert property ((eventually[0: 1] a) iff (eventually[0: 1] a));
| ^~~~~~~~~~
@ -35,10 +29,4 @@
%Error-UNSUPPORTED: t/t_property_unsup.v:114:42: Unsupported: s_eventually (in property expression)
114 | assert property ((s_eventually a) iff (s_eventually a));
| ^~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_property_unsup.v:124:23: Unsupported: #-# (in property expression)
124 | assert property ((a #-# b) iff (a #-# b));
| ^~~
%Error-UNSUPPORTED: t/t_property_unsup.v:124:37: Unsupported: #-# (in property expression)
124 | assert property ((a #-# b) iff (a #-# b));
| ^~~
%Error: Exiting due to