Support assert under assert (#6146).

This commit is contained in:
Wilson Snyder 2025-12-16 20:45:31 -05:00
parent f1ee434dca
commit 41c4f948fe
6 changed files with 96 additions and 19 deletions

View File

@ -142,6 +142,7 @@ Verilator 5.042 2025-11-02
* Support modports referencing clocking blocks (#4555) (#6436). [Ryszard Rozak, Antmicro Ltd.]
* Support class package reference on pattern keys (#5653). [Todd Strader]
* Support digits in `$sscanf` field width formats (#6083). [Iztok Jeras]
* Support assert under assert (#6146). [Alex Solomatnikov]
* Support pure functions in sensitivity lists (#6393). [Krzysztof Bieganski, Antmicro Ltd.]
* Support simple alias statements (#6339) (#6501). [Ryszard Rozak, Antmicro Ltd.]
* Support simple cycle delay sequence expressions inside properties (#6508). [Bartłomiej Chmiel, Antmicro Ltd.]

View File

@ -80,10 +80,6 @@ private:
}
return newp;
}
void clearAssertInfo() {
m_senip = nullptr;
m_disablep = nullptr;
}
AstPropSpec* getPropertyExprp(const AstProperty* const propp) {
// The only statements possible in AstProperty are AstPropSpec (body)
// and AstVar (arguments).
@ -476,12 +472,14 @@ private:
void visit(AstNodeCoverOrAssert* nodep) override {
if (nodep->sentreep()) return; // Already processed
clearAssertInfo();
VL_RESTORER(m_senip);
VL_RESTORER(m_disablep);
m_senip = nullptr;
m_disablep = nullptr;
// Find Clocking's buried under nodep->exprsp
iterateChildren(nodep);
if (!nodep->immediate()) nodep->sentreep(newSenTree(nodep));
clearAssertInfo();
}
void visit(AstFalling* nodep) override {
if (nodep->user1SetOnce()) return;
@ -684,7 +682,6 @@ public:
// CONSTRUCTORS
explicit AssertPreVisitor(AstNetlist* nodep)
: m_netlistp{nodep} {
clearAssertInfo();
// Process
iterate(nodep);
// Fix up varref names

View File

@ -50,7 +50,6 @@ class LinkResolveVisitor final : public VNVisitor {
string m_randcIllegalWhy; // Why randc illegal
AstNode* m_randcIllegalp = nullptr; // Node causing randc illegal
AstNodeFTask* m_ftaskp = nullptr; // Function or task we're inside
AstNodeCoverOrAssert* m_assertp = nullptr; // Current assertion
int m_senitemCvtNum = 0; // Temporary signal counter
std::deque<AstGenFor*> m_underGenFors; // Stack of GenFor underneath
bool m_underGenerate = false; // Under GenFor/GenIf
@ -119,14 +118,6 @@ class LinkResolveVisitor final : public VNVisitor {
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
}
void visit(AstNodeCoverOrAssert* nodep) override {
if (m_assertp) {
nodep->v3warn(E_UNSUPPORTED, "Unsupported: Assert not allowed under another assert");
}
VL_RESTORER(m_assertp);
m_assertp = nodep;
iterateChildren(nodep);
}
void visit(AstVar* nodep) override {
iterateChildren(nodep);
if (m_classp && !nodep->isParam()) nodep->varType(VVarType::MEMBER);

View File

@ -0,0 +1,18 @@
#!/usr/bin/env python3
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# Copyright 2025 by Wilson Snyder. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0
import vltest_bootstrap
test.scenarios('simulator')
test.compile()
test.execute()
test.passes()

View File

@ -0,0 +1,58 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain, for
// any use, without warranty, 2025 by Wilson Snyder.
// 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 [2:0] value;
int cnt_tt;
int cnt_tf;
int cnt_ft;
int cnt_ff;
assert property (@(negedge clk) disable iff (value[1]) value[2]) begin
assert (value[0]) ++cnt_tt;
else ++cnt_tf;
end
else begin
assert (value[0]) ++cnt_ft;
else ++cnt_ff;
end
// Test loop
always @(posedge clk) begin
cyc <= cyc + 1;
if (cyc == 10) begin
assert(cyc == 10); // For debug to compare with other asserts
value <= 0;
cnt_tt = 0;
cnt_tf = 0;
cnt_ft = 0;
cnt_ff = 0;
end
else if (cyc > 10 && cyc < 90) begin
value <= cyc[2:0];
end
else if (cyc == 99) begin
`checkd(cnt_tt, 10);
`checkd(cnt_tf, 10);
`checkd(cnt_ft, 19);
`checkd(cnt_ff, 11);
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule

View File

@ -1,5 +1,17 @@
%Error-UNSUPPORTED: t/t_cover_assert.v:42:16: Unsupported: Assert not allowed under another assert
42 | A2: assert (b);
| ^~~~~~
%Warning-PROCASSINIT: t/t_cover_assert.v:13:18: Procedural assignment to declaration with initial value: 'cyc'
: ... note: In instance 't'
: ... Location of variable initialization
13 | integer cyc = 0;
| ^
t/t_cover_assert.v:19:7: ... Location of variable process write
: ... Perhaps should initialize instead using a reset in this process
19 | cyc <= cyc + 1;
| ^~~
... For warning description see https://verilator.org/warn/PROCASSINIT?v=latest
... Use "/* verilator lint_off PROCASSINIT */" and lint_on around source to disable this message.
%Error-UNSUPPORTED: t/t_cover_assert.v:39:11: Unsupported: Procedural concurrent assertion with clocking event inside always (IEEE 1800-2023 16.14.6)
: ... note: In instance 't'
39 | C1: cover property(a)
| ^~~~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error: Exiting due to