Fix --coverage on labelled inline assert/cover property (#7898)
With --coverage, expression coverage was injected into concurrent
assertion property expressions. A statement label (e.g.
`a : assert property (...)`) wraps the assertion in an implied begin, so
the injected coverage statements (cloned VarRefs, extracted sampled-value
functions) were placed as siblings of the concurrent assert, outside any
procedural context. This tripped V3Localize ("AstVarRef not under
function") and perturbed the property so its clock could no longer be
resolved ("Concurrent assertion has no clock").
The previous fix (#6830) only skipped named AstProperty nodes, so inline
assert/cover property expressions were still instrumented. Suppress
expression coverage uniformly at the AstPropSpec boundary, which covers
both named property bodies and inline assert/cover property expressions,
and drop the now-redundant Property blocklist.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
parent
646dcd3838
commit
67d2909c98
|
|
@ -220,6 +220,7 @@ Nikolai Kumar
|
|||
Nikolay Puzanov
|
||||
Nolan Poe
|
||||
Oleh Maksymenko
|
||||
Patrick Creighton
|
||||
Patrick Stewart
|
||||
Paul Bowen-Huggett
|
||||
Paul Swirhun
|
||||
|
|
|
|||
|
|
@ -385,8 +385,7 @@ class CoverageVisitor final : public VNVisitor {
|
|||
VL_RESTORER(m_state);
|
||||
VL_RESTORER(m_exprStmtsp);
|
||||
VL_RESTORER(m_inToggleOff);
|
||||
// skip properties for expresison coverage
|
||||
if (!VN_IS(nodep, Property)) m_exprStmtsp = nodep;
|
||||
m_exprStmtsp = nodep;
|
||||
m_inToggleOff = true;
|
||||
createHandle(nodep);
|
||||
iterateChildren(nodep);
|
||||
|
|
@ -745,6 +744,18 @@ class CoverageVisitor final : public VNVisitor {
|
|||
newCoverInc(nodep->fileline(), declp, m_beginHier + "_vlCoverageUserTrace"));
|
||||
}
|
||||
}
|
||||
void visit(AstPropSpec* nodep) override {
|
||||
// A property specification holds a concurrent (temporal) property
|
||||
// expression, which is not a procedural statement context. Expression
|
||||
// coverage must not inject statements into it, else the injected
|
||||
// references end up outside any procedural context (tripping V3Localize)
|
||||
// or perturb the property so its clock can no longer be resolved. This
|
||||
// uniformly covers both named 'property' bodies and inline assert/cover
|
||||
// property expressions, regardless of any enclosing labelled begin.
|
||||
VL_RESTORER(m_exprStmtsp);
|
||||
m_exprStmtsp = nullptr;
|
||||
iterateChildren(nodep);
|
||||
}
|
||||
void visit(AstStop* nodep) override {
|
||||
UINFO(4, " STOP: " << nodep);
|
||||
m_state.m_on = false;
|
||||
|
|
|
|||
|
|
@ -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(verilator_flags2=['--assert --cc --coverage'])
|
||||
|
||||
test.execute()
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,49 @@
|
|||
// 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
|
||||
|
||||
module t (
|
||||
input clk
|
||||
);
|
||||
|
||||
integer cyc = 0;
|
||||
logic rst_n = 0;
|
||||
logic en = 0;
|
||||
logic q = 0;
|
||||
logic [7:0] cnt = 0;
|
||||
|
||||
// Synchronous active-low reset driving runtime-varying signals, so the
|
||||
// asserted and covered properties are not constant-folded away.
|
||||
always_ff @(posedge clk) begin
|
||||
rst_n <= (cyc >= 2);
|
||||
en <= cyc[0];
|
||||
if (!rst_n) begin
|
||||
q <= 1'b0;
|
||||
cnt <= '0;
|
||||
end else if (en) begin
|
||||
q <= ~q;
|
||||
cnt <= cnt + 8'd1;
|
||||
end
|
||||
end
|
||||
|
||||
// Labelled INLINE concurrent assertion (not wrapped in a named
|
||||
// property ... endproperty). With --coverage this previously hit an
|
||||
// internal error (V3Localize.cpp: 'AstVarRef not under function').
|
||||
a : assert property (@(posedge clk) !rst_n |=> q == 1'b0);
|
||||
|
||||
// Labelled INLINE concurrent cover with disable-iff and a sampled-value
|
||||
// function. With --coverage this previously emitted a false
|
||||
// 'Concurrent assertion has no clock' error.
|
||||
c : cover property (@(posedge clk) disable iff (!rst_n) en && cnt == $past(cnt));
|
||||
|
||||
always @(posedge clk) begin
|
||||
cyc <= cyc + 1;
|
||||
if (cyc == 10) begin
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
end
|
||||
|
||||
endmodule
|
||||
Loading…
Reference in New Issue