Fix pre/post increments in assertions (#6434)

This commit is contained in:
Bartłomiej Chmiel 2025-09-15 16:50:31 +02:00 committed by GitHub
parent b11ec23891
commit dca555b6d7
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
3 changed files with 99 additions and 2 deletions

View File

@ -47,8 +47,6 @@
#include "V3LinkInc.h"
#include <algorithm>
VL_DEFINE_DEBUG_FUNCTIONS;
//######################################################################
@ -102,6 +100,19 @@ class LinkIncVisitor final : public VNVisitor {
m_ftaskp = nodep;
iterateChildren(nodep);
}
void visit(AstNodeCoverOrAssert* nodep) override {
VL_RESTORER(m_insStmtp);
m_insStmtp = nodep;
iterateAndNextNull(nodep->propp());
m_insStmtp = nullptr;
// Note: no iterating over sentreep here as they will be ignored anyway
if (AstAssert* const assertp = VN_CAST(nodep, Assert)) {
iterateAndNextNull(assertp->failsp());
} else if (AstAssertIntrinsic* const intrinsicp = VN_CAST(nodep, AssertIntrinsic)) {
iterateAndNextNull(intrinsicp->failsp());
}
iterateAndNextNull(nodep->passsp());
}
void visit(AstWhile* nodep) override {
// Special, as statements need to be put in different places
m_insStmtp = nodep;

18
test_regress/t/t_assert_pre.py Executable file
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,68 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain, for
// any use, without warranty, 2025 by Antmicro.
// SPDX-License-Identifier: CC0-1.0
`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);
module t ( /*AUTOARG*/
// Inputs
clk
);
input clk;
bit toggle = 0;
int inc = 0;
int dec = 0;
assert property (@(negedge clk) not toggle)
else ++inc;
assert property (@(negedge clk) not toggle)
else --dec;
int passsInc = 0;
int passsDec = 0;
assert property (@(negedge clk) not toggle) ++passsInc;
else --passsDec;
assert property (@(negedge clk) not toggle) ++passsInc;
cover property (@(negedge clk) not toggle) ++passsInc;
int inc2 = 0;
assert property (@(e) not toggle) begin
`checkh(inc2, 0);
inc2++;
`checkh(inc2,1);
end
event e;
int cyc = 0;
always @(posedge clk) begin
`ifdef TEST_VERBOSE
$write("[%0t] cyc==%0d toggle==%d\n", $time, cyc, toggle);
`endif
if (cyc % 3 == 0) begin
toggle <= 1;
end else begin
toggle <= 0;
end
cyc <= cyc + 1;
if (cyc == 5) begin
->e;
`checkh(inc, 2);
`checkh(dec, -2);
`checkh(passsInc, 6);
`checkh(passsDec, -2);
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule