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

Optimize runtime assertOn() checks (#7707) 

Combine consecutive assertOn() checks into one, and hoist past enclosing
'if' statements if possible. This enables combining a lot of them, which
can be worth 10% performance on some assertion heavy designs depending
on how the assertions are written.
This commit is contained in:
Geza Lore 2026-06-03 18:09:49 +01:00 committed by GitHub
parent 1af9c39759
commit 41811d436f
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
3 changed files with 213 additions and 67 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

200
src/V3Assert.cpp
View File

@ -128,6 +128,7 @@ class AssertVisitor final : public VNVisitor {
// AstNode::user1() -> bool. True if processed
// AstAlways::user2p() -> std::vector<AstVar*>. Delayed variables via 'm_delayed'
// AstNodeVarRef::user2() -> bool. True if shouldn't be sampled
// AstIf::user2() -> bool. True for assertOn() checks inserted in this pass
const VNUser1InUse m_user1InUse;
const VNUser2InUse m_user2InUse;
AstUser2Allocator<AstAlways, std::vector<AstVar*>> m_delayed;
@ -146,6 +147,8 @@ class AssertVisitor final : public VNVisitor {
VDouble0 m_statAsImm; // Statistic tracking
VDouble0 m_statAsFull; // Statistic tracking
VDouble0 m_statPastVars; // Statistic tracking
VDouble0 m_statAssertOnCombined; // Statistic tracking
VDouble0 m_statAssertOnHoisted; // Statistic tracking
bool m_inSampled = false; // True inside a sampled expression
bool m_inRestrict = false; // True inside restrict assertion
AstNode* m_passsp = nullptr; // Current pass statement
@ -274,16 +277,16 @@ class AssertVisitor final : public VNVisitor {
varrefp->classOrPackagep(v3Global.rootp()->dollarUnitPkgAddp());
return varrefp;
}
static AstNodeStmt* newIfAssertOn(AstNode* bodyp, VAssertDirectiveType directiveType,
VAssertType type = VAssertType::INTERNAL) {
static AstIf* newIfAssertOn(AstNode* bodyp, VAssertDirectiveType directiveType,
VAssertType type = VAssertType::INTERNAL) {
// Add a internal if to check assertions are on.
// Don't make this a AND term, as it's unlikely to need to test this.
FileLine* const fl = bodyp->fileline();
AstNodeExpr* const condp = assertOnCond(fl, type, directiveType);
AstNodeIf* const newp = new AstIf{fl, condp, bodyp};
AstIf* const newp = new AstIf{fl, condp, bodyp};
newp->isBoundsCheck(true); // To avoid LATCH warning
newp->user1(true); // Don't assert/cover this if
newp->user2(true); // Mark as an assertOn() check
return newp;
}
@ -297,9 +300,8 @@ class AssertVisitor final : public VNVisitor {
return ifp;
}
AstNode* assertBody(const AstNodeCoverOrAssert* nodep, AstNode* propp, AstNode* passsp,
AstNode* failsp) {
AstNode* bodyp = nullptr;
AstNodeStmt* assertBody(const AstNodeCoverOrAssert* nodep, AstNode* propp, AstNode* passsp,
AstNode* failsp) {
if (AstPExpr* const pexprp = VN_CAST(propp, PExpr)) {
AstFork* const forkp = new AstFork{nodep->fileline(), VJoinType::JOIN_NONE};
forkp->addForksp(pexprp->bodyp()->unlinkFrBack());
@ -312,11 +314,10 @@ class AssertVisitor final : public VNVisitor {
}
}
VL_DO_DANGLING2(pushDeletep(pexprp), pexprp, propp);
bodyp = forkp;
} else {
bodyp = assertCond(nodep, VN_AS(propp, NodeExpr), passsp, failsp);
return forkp;
}
return newIfAssertOn(bodyp, nodep->directive(), nodep->userType());
return assertCond(nodep, VN_AS(propp, NodeExpr), passsp, failsp);
}
AstNodeStmt* newFireAssertUnchecked(const AstNodeStmt* nodep, const string& message,
@ -487,14 +488,12 @@ class AssertVisitor final : public VNVisitor {
} else {
propExprp = nodep->propp()->unlinkFrBack();
}
FileLine* const flp = nodep->fileline();
AstNode* bodysp = assertBody(nodep, propExprp, passsp, failsp);
if (disablep) {
bodysp
= new AstIf{nodep->fileline(), new AstLogNot{nodep->fileline(), disablep}, bodysp};
}
if (sentreep) {
bodysp = new AstAlways{nodep->fileline(), VAlwaysKwd::ALWAYS, sentreep, bodysp};
}
if (disablep) bodysp = new AstIf{flp, new AstLogNot{flp, disablep}, bodysp};
// Add assertOn check last, for better combining
bodysp = newIfAssertOn(bodysp, nodep->directive(), nodep->userType());
if (sentreep) bodysp = new AstAlways{flp, VAlwaysKwd::ALWAYS, sentreep, bodysp};
if (passsp && !passsp->backp()) VL_DO_DANGLING(pushDeletep(passsp), passsp);
if (failsp && !failsp->backp()) VL_DO_DANGLING(pushDeletep(failsp), failsp);
@ -512,67 +511,121 @@ class AssertVisitor final : public VNVisitor {
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
bool isEmptyStmt(AstNode* nodep) {
if (!nodep) return true;
if (AstBegin* const beginp = VN_CAST(nodep, Begin)) {
if (beginp->declsp()) return false;
for (AstNode* stmtp = beginp->stmtsp(); stmtp; stmtp = stmtp->nextp()) {
if (!isEmptyStmt(stmtp)) return false;
}
return true;
}
return false;
}
// VISITORS
void visit(AstIf* nodep) override {
if (nodep->user1SetOnce()) return;
if (nodep->uniquePragma() || nodep->unique0Pragma()) {
const AstNodeIf* ifp = nodep;
AstNodeExpr* propp = nullptr;
bool hasDefaultElse = false;
do {
// If this statement ends with 'else if', then nextIf will point to the
// nextIf statement. Otherwise it will be null.
const AstNodeIf* const nextifp = dynamic_cast<AstNodeIf*>(ifp->elsesp());
iterateAndNextNull(ifp->condp());
if (!nodep->user1SetOnce()) {
if (nodep->uniquePragma() || nodep->unique0Pragma()) {
const AstNodeIf* ifp = nodep;
AstNodeExpr* propp = nullptr;
bool hasDefaultElse = false;
do {
// If this statement ends with 'else if', then nextIf will point to the
// nextIf statement. Otherwise it will be null.
const AstNodeIf* const nextifp = dynamic_cast<AstNodeIf*>(ifp->elsesp());
iterateAndNextNull(ifp->condp());
// Recurse into the true case.
iterateAndNextNull(ifp->thensp());
// Recurse into the true case.
iterateAndNextNull(ifp->thensp());
// If the last else is not an else if, recurse into that too.
if (ifp->elsesp() && !nextifp) { //
iterateAndNextNull(ifp->elsesp());
}
// If the last else is not an else if, recurse into that too.
if (ifp->elsesp() && !nextifp) { //
iterateAndNextNull(ifp->elsesp());
}
// Build a bitmask of the true predicates
AstNodeExpr* const predp = ifp->condp()->cloneTreePure(false);
if (propp) {
propp = new AstConcat{nodep->fileline(), predp, propp};
} else {
propp = predp;
}
// Build a bitmask of the true predicates
AstNodeExpr* const predp = ifp->condp()->cloneTreePure(false);
if (propp) {
propp = new AstConcat{nodep->fileline(), predp, propp};
} else {
propp = predp;
}
// Record if this ends with an 'else' that does not have an if
if (ifp->elsesp() && !nextifp) hasDefaultElse = true;
// Record if this ends with an 'else' that does not have an if
if (ifp->elsesp() && !nextifp) hasDefaultElse = true;
ifp = nextifp;
} while (ifp);
ifp = nextifp;
} while (ifp);
AstIf* const newifp = nodep->cloneTree(false);
const bool allow_none = nodep->unique0Pragma();
AstIf* const newifp = nodep->cloneTree(false);
const bool allow_none = nodep->unique0Pragma();
// Empty case means no property
if (!propp) propp = new AstConst{nodep->fileline(), AstConst::BitFalse{}};
// Empty case means no property
if (!propp) propp = new AstConst{nodep->fileline(), AstConst::BitFalse{}};
// Note: if this ends with an 'else', then we don't need to validate that one of
// the predicates evaluates to true.
AstNodeExpr* const ohot
= ((allow_none || hasDefaultElse)
? static_cast<AstNodeExpr*>(new AstOneHot0{nodep->fileline(), propp})
: static_cast<AstNodeExpr*>(new AstOneHot{nodep->fileline(), propp}));
const VAssertType assertType
= nodep->uniquePragma() ? VAssertType::UNIQUE : VAssertType::UNIQUE0;
AstIf* const checkifp
= new AstIf{nodep->fileline(), new AstLogNot{nodep->fileline(), ohot},
newFireAssert(nodep, VAssertDirectiveType::VIOLATION_IF,
assertType, "'unique if' statement violated"),
newifp};
checkifp->isBoundsCheck(true); // To avoid LATCH warning
checkifp->branchPred(VBranchPred::BP_UNLIKELY);
nodep->replaceWith(checkifp);
VL_DO_DANGLING(pushDeletep(nodep), nodep);
return;
}
// Note: if this ends with an 'else', then we don't need to validate that one of the
// predicates evaluates to true.
AstNodeExpr* const ohot
= ((allow_none || hasDefaultElse)
? static_cast<AstNodeExpr*>(new AstOneHot0{nodep->fileline(), propp})
: static_cast<AstNodeExpr*>(new AstOneHot{nodep->fileline(), propp}));
const VAssertType assertType
= nodep->uniquePragma() ? VAssertType::UNIQUE : VAssertType::UNIQUE0;
AstIf* const checkifp
= new AstIf{nodep->fileline(), new AstLogNot{nodep->fileline(), ohot},
newFireAssert(nodep, VAssertDirectiveType::VIOLATION_IF, assertType,
"'unique if' statement violated"),
newifp};
checkifp->isBoundsCheck(true); // To avoid LATCH warning
checkifp->branchPred(VBranchPred::BP_UNLIKELY);
nodep->replaceWith(checkifp);
VL_DO_DANGLING(pushDeletep(nodep), nodep);
} else {
iterateChildren(nodep);
}
// Swap assertOn check with single statement 'if' statement to bubble up for combining
// Note we can't just swap the conditions as they two Ifs have different flags,
// so swapping the Ifs themeselves then swapping back the bodies.
if (nodep->condp()->isPure()) {
if (nodep->thensp() && !nodep->thensp()->nextp() && isEmptyStmt(nodep->elsesp())) {
AstIf* const checkp = VN_CAST(nodep->thensp(), If);
if (checkp && checkp->user2()) {
++m_statAssertOnHoisted;
nodep->replaceWith(checkp->unlinkFrBack());
nodep->addThensp(checkp->thensp()->unlinkFrBackWithNext());
checkp->addThensp(nodep);
return;
}
}
if (nodep->elsesp() && !nodep->elsesp()->nextp() && isEmptyStmt(nodep->thensp())) {
AstIf* const checkp = VN_CAST(nodep->elsesp(), If);
if (checkp && checkp->user2()) {
++m_statAssertOnHoisted;
nodep->replaceWith(checkp->unlinkFrBack());
nodep->addElsesp(checkp->thensp()->unlinkFrBackWithNext());
checkp->addThensp(nodep);
return;
}
}
}
// Combine consecutive assertOn checks if possible
if (nodep->user2()) {
if (AstIf* const backp = VN_CAST(nodep->backp(), If)) {
if (backp->nextp() == nodep //
&& backp->user2() //
&& backp->condp()->sameTree(nodep->condp())) {
++m_statAssertOnCombined;
backp->addThensp(nodep->thensp()->unlinkFrBackWithNext());
nodep->unlinkFrBack();
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
}
}
}
//========== Case assertions
@ -979,6 +1032,17 @@ class AssertVisitor final : public VNVisitor {
VL_RESTORER(m_beginp);
m_beginp = nodep;
iterateChildren(nodep);
// If the body is a single assertOn check, bubble it up for combining
if (!nodep->declsp()) {
if (AstIf* const ifp = VN_CAST(nodep->stmtsp(), If)) {
if (ifp->user2() && !ifp->nextp()) {
++m_statAssertOnHoisted;
nodep->replaceWith(ifp->unlinkFrBack());
nodep->addStmtsp(ifp->thensp()->unlinkFrBackWithNext());
ifp->addThensp(nodep);
}
}
}
}
void visit(AstNode* nodep) override { iterateChildren(nodep); }
@ -992,6 +1056,8 @@ public:
V3Stats::addStat("Assertions, cover statements", m_statCover);
V3Stats::addStat("Assertions, full/parallel case", m_statAsFull);
V3Stats::addStat("Assertions, $past variables", m_statPastVars);
V3Stats::addStat("Assertions, assertOn checks combined", m_statAssertOnCombined);
V3Stats::addStat("Assertions, assertOn checks hoisted", m_statAssertOnHoisted);
}
};

21
test_regress/t/t_assert_opt_check.py Executable file
View File

@ -0,0 +1,21 @@
#!/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(verilator_flags2=['--binary', '--stats'])
test.execute(check_finished=True)
test.file_grep(test.stats, r'Assertions, assertOn checks combined\s+(\d+)', 2)
test.file_grep(test.stats, r'Assertions, assertOn checks hoisted\s+(\d+)', 11)
test.passes()

59
test_regress/t/t_assert_opt_check.v Normal file
View File

@ -0,0 +1,59 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain.
// SPDX-FileCopyrightText: 2026 Wilson Snyder
// 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);
// verilog_format: on
module t;
logic clk = 1'b0;
always #5 clk = ~clk;
logic rst = 1'b1;
initial #22 rst = 1'b0;
logic assertEnable = 1'b0;
initial #44 assertEnable = 1'b1;
initial begin
#1000;
$write("*-* All Finished *-*\n");
$finish;
end
int cntA = 0;
int cntB = 100;
always @(posedge clk) begin
cntA <= cntA + 1;
cntB <= cntB + 1;
end
// Should combine the 2 assertOn checks after hoisting
always @(posedge clk) begin
if (rst) begin
// Blank
end else if (assertEnable) begin
assert (cntA == cntB - 100);
labelled_A: assert (cntB - cntA == 100);
end
end
// Should combine the 2 assertOn checks after hoisting
always @(posedge clk) begin
if (assertEnable) begin
labelled_B: assert (cntA + 100 == cntB);
end
if (!assertEnable) begin
// Blank
end else begin
assert (cntA - cntB == -100);
end
end
endmodule