From 67d2909c9817312b78af19b60eecb9acafe671db Mon Sep 17 00:00:00 2001 From: Patrick Creighton Date: Wed, 8 Jul 2026 08:12:56 -0700 Subject: [PATCH] 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> --- docs/CONTRIBUTORS | 1 + src/V3Coverage.cpp | 15 ++++++- test_regress/t/t_assert_inline_coverage.py | 18 ++++++++ test_regress/t/t_assert_inline_coverage.v | 49 ++++++++++++++++++++++ 4 files changed, 81 insertions(+), 2 deletions(-) create mode 100755 test_regress/t/t_assert_inline_coverage.py create mode 100644 test_regress/t/t_assert_inline_coverage.v diff --git a/docs/CONTRIBUTORS b/docs/CONTRIBUTORS index 24e3ced87..62f8d0bc3 100644 --- a/docs/CONTRIBUTORS +++ b/docs/CONTRIBUTORS @@ -220,6 +220,7 @@ Nikolai Kumar Nikolay Puzanov Nolan Poe Oleh Maksymenko +Patrick Creighton Patrick Stewart Paul Bowen-Huggett Paul Swirhun diff --git a/src/V3Coverage.cpp b/src/V3Coverage.cpp index 9db38cb6e..aa379aa35 100644 --- a/src/V3Coverage.cpp +++ b/src/V3Coverage.cpp @@ -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; diff --git a/test_regress/t/t_assert_inline_coverage.py b/test_regress/t/t_assert_inline_coverage.py new file mode 100755 index 000000000..fb117067b --- /dev/null +++ b/test_regress/t/t_assert_inline_coverage.py @@ -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() diff --git a/test_regress/t/t_assert_inline_coverage.v b/test_regress/t/t_assert_inline_coverage.v new file mode 100644 index 000000000..7d727510f --- /dev/null +++ b/test_regress/t/t_assert_inline_coverage.v @@ -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