From bb1bfabab38680bffa3e6845327257bfae186c3d Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Tue, 28 Apr 2026 12:50:16 +0200 Subject: [PATCH] Fix internal error on multi-cycle SVA under default clocking (#7472) (#7506) --- src/V3AssertNfa.cpp | 20 +++ src/V3AssertPre.cpp | 37 ++--- .../t/t_property_default_clocking_sexpr.py | 18 +++ .../t/t_property_default_clocking_sexpr.v | 138 ++++++++++++++++++ 4 files changed, 191 insertions(+), 22 deletions(-) create mode 100755 test_regress/t/t_property_default_clocking_sexpr.py create mode 100644 test_regress/t/t_property_default_clocking_sexpr.v diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index bb388b846..b4bb45263 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -1467,6 +1467,8 @@ public: class AssertNfaVisitor final : public VNVisitor { // STATE AstNodeModule* m_modp = nullptr; // Current module being processed + AstClocking* m_defaultClockingp = nullptr; // Default clocking + AstDefaultDisable* m_defaultDisablep = nullptr; // Default disable iff SvaNfaLowering* m_loweringp = nullptr; // NFA-to-hardware lowering engine V3UniqueNames m_propVarNames{"__Vpropvar"}; // Property-local variable names V3UniqueNames m_disableCntNames{"__VnfaDis"}; // Disable-iff counter names @@ -1815,6 +1817,13 @@ class AssertNfaVisitor final : public VNVisitor { bool senTreeOwned = false; // True if we created senTreep locally AstPropSpec* const propSpecp = VN_CAST(assertp->propp(), PropSpec); UASSERT_OBJ(propSpecp, assertp, "Concurrent assertion must have PropSpec"); + // Inherit module defaults (IEEE 14.12, 16.15) when assertion has none. + if (!propSpecp->sensesp() && m_defaultClockingp) { + propSpecp->sensesp(m_defaultClockingp->sensesp()->cloneTree(true)); + } + if (!propSpecp->disablep() && m_defaultDisablep) { + propSpecp->disablep(m_defaultDisablep->condp()->cloneTreePure(true)); + } if (!senTreep && propSpecp->sensesp()) { senTreep = new AstSenTree{propSpecp->fileline(), propSpecp->sensesp()->cloneTree(true)}; @@ -1886,11 +1895,22 @@ class AssertNfaVisitor final : public VNVisitor { void visit(AstNodeModule* nodep) override { VL_RESTORER(m_modp); VL_RESTORER(m_loweringp); + VL_RESTORER(m_defaultClockingp); + VL_RESTORER(m_defaultDisablep); m_modp = nodep; + m_defaultClockingp = nullptr; + m_defaultDisablep = nullptr; SvaNfaLowering lowering{nodep}; m_loweringp = &lowering; iterateChildren(nodep); } + void visit(AstClocking* nodep) override { + if (nodep->isDefault() && !m_defaultClockingp) m_defaultClockingp = nodep; + iterateChildren(nodep); + } + void visit(AstDefaultDisable* nodep) override { + if (!m_defaultDisablep) m_defaultDisablep = nodep; + } void visit(AstAssert* nodep) override { processAssertion(nodep); } void visit(AstCover* nodep) override { processAssertion(nodep); } void visit(AstRestrict* nodep) override { diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 160a6c63a..2577aace7 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -240,6 +240,15 @@ private: VL_RESTORER(m_clockingp); m_clockingp = nodep; UINFO(8, " CLOCKING" << nodep); + if (nodep->isDefault()) { + if (m_defaultClockingp) { + nodep->v3error("Only one default clocking block allowed per module" + " (IEEE 1800-2023 14.12)"); + } else { + m_defaultClockingp = nodep; + m_defaultClkEvtVarp = nodep->ensureEventp(); + } + } iterateChildren(nodep); if (nodep->eventp()) nodep->addNextHere(nodep->eventp()->unlinkFrBack()); VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep); @@ -1182,7 +1191,12 @@ private: } void visit(AstDefaultDisable* nodep) override { - // Done with these + if (m_defaultDisablep) { + nodep->v3error("Only one 'default disable iff' allowed per module" + " (IEEE 1800-2023 16.15)"); + } else { + m_defaultDisablep = nodep; + } VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep); } void visit(AstInferredDisable* nodep) override { @@ -1293,29 +1307,8 @@ private: VL_RESTORER(m_modp); m_defaultClockingp = nullptr; m_defaultClkEvtVarp = nullptr; - nodep->foreach([&](AstClocking* const clockingp) { - if (clockingp->isDefault()) { - if (m_defaultClockingp) { - clockingp->v3error("Only one default clocking block allowed per module" - " (IEEE 1800-2023 14.12)"); - } - m_defaultClockingp = clockingp; - } - }); m_defaultDisablep = nullptr; - nodep->foreach([&](AstDefaultDisable* const disablep) { - if (m_defaultDisablep) { - disablep->v3error("Only one 'default disable iff' allowed per module" - " (IEEE 1800-2023 16.15)"); - } - m_defaultDisablep = disablep; - }); m_modp = nodep; - // Pre-create and cache the clocking event var before iterating children. - // visit(AstClocking) will unlink the event from the clocking node and place it - // in the module tree, then delete the clocking. After that, ensureEventp() would - // create an orphaned var. Caching here avoids this. - m_defaultClkEvtVarp = m_defaultClockingp ? m_defaultClockingp->ensureEventp() : nullptr; iterateChildren(nodep); } void visit(AstProperty* nodep) override { diff --git a/test_regress/t/t_property_default_clocking_sexpr.py b/test_regress/t/t_property_default_clocking_sexpr.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/test_regress/t/t_property_default_clocking_sexpr.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(timing_loop=True, verilator_flags2=['--assert', '--timing']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_property_default_clocking_sexpr.v b/test_regress/t/t_property_default_clocking_sexpr.v new file mode 100644 index 000000000..b3d2d52e8 --- /dev/null +++ b/test_regress/t/t_property_default_clocking_sexpr.v @@ -0,0 +1,138 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 PlanV GmbH +// 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='h%x exp='h%x\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); +`define checkd(gotv, expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); +// verilog_format: on + +// Issue #7472 reproducer (default clocking + |=> + throughout). +module wsn ( + input clk, + input a, b, c, d +); + default clocking @(posedge clk); endclocking + int fail = 0; + assert property ( + a |=> b throughout (c ##1 d) + ) else fail <= fail + 1; +endmodule + +// Explicit @(edge) must override default clocking. +module clk_override ( + input clk_default, + input clk_explicit, + input a, b, c, d +); + default clocking @(posedge clk_default); endclocking + int default_fail = 0; + int explicit_fail = 0; + assert property (a |=> b throughout (c ##1 d)) + else default_fail <= default_fail + 1; + assert property (@(posedge clk_explicit) a |=> b throughout (c ##1 d)) + else explicit_fail <= explicit_fail + 1; +endmodule + +// Explicit `disable iff` must override default disable. +module dgate ( + input clk, + input rst, + input a, b, c, d +); + default clocking @(posedge clk); endclocking + default disable iff (rst); + int default_dis_fail = 0; + int explicit_dis_fail = 0; + assert property (a |=> b throughout (c ##1 d)) + else default_dis_fail <= default_dis_fail + 1; + assert property (disable iff (1'b0) a |=> b throughout (c ##1 d)) + else explicit_dis_fail <= explicit_dis_fail + 1; +endmodule + +// No defaults, explicit clock -- fix must not alter this path. +module nodef ( + input clk, + input a, b, c, d +); + int fail = 0; + assert property (@(posedge clk) a |=> b throughout (c ##1 d)) + else fail <= fail + 1; +endmodule + +module t ( + input clk +); + integer cyc = 0; + reg [63:0] crc = '0; + + wire a = crc[0]; + wire b = crc[4]; + wire c = crc[8]; + wire d = crc[12]; + + wire clk_alt = ~clk; + wire rst = (cyc < 10); + + default clocking @(posedge clk); endclocking + default disable iff (cyc < 10); + + int count_fail1 = 0; + int count_fail2 = 0; + int count_fail3 = 0; + int count_fail4 = 0; + + // Issue #7472 exact shape. + assert property (a |=> b throughout (c ##1 d)) + else count_fail1 <= count_fail1 + 1; + assert property (a |-> b throughout (c ##1 d)) + else count_fail2 <= count_fail2 + 1; + assert property (a |=> c ##1 d) + else count_fail3 <= count_fail3 + 1; + assert property (a |=> b throughout (c throughout (c ##1 d))) + else count_fail4 <= count_fail4 + 1; + + cover property (a throughout (c ##[1:2] d)); + cover property (a |=> b throughout (c ##1 d)); + + // Generate-scope: module foreach must reach inside generate blocks. + generate + if (1) begin : g + int gen_fail = 0; + assert property (a |=> b throughout (c ##1 d)) + else gen_fail <= gen_fail + 1; + end + endgenerate + + wsn u_wsn (.clk(clk), .a(a), .b(b), .c(c), .d(d)); + clk_override u_override (.clk_default(clk), .clk_explicit(clk_alt), + .a(a), .b(b), .c(c), .d(d)); + dgate u_dgate (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .d(d)); + nodef u_nodef (.clk(clk), .a(a), .b(b), .c(c), .d(d)); + + always_ff @(posedge clk) begin + cyc <= cyc + 1; + crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; + if (cyc == 0) begin + crc <= 64'h5aef0c8d_d70a4497; + end else if (cyc == 99) begin + `checkh(crc, 64'hc77bb9b3784ea091); + `checkd(count_fail1, 35); + `checkd(count_fail2, 36); + `checkd(count_fail3, 29); + `checkd(count_fail4, 35); + `checkd(u_wsn.fail, 39); + `checkd(u_override.default_fail, 39); + `checkd(u_override.explicit_fail, 39); + `checkd(u_dgate.default_dis_fail, 35); + `checkd(u_dgate.explicit_dis_fail, 39); + `checkd(u_nodef.fail, 39); + `checkd(g.gen_fail, 35); + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule