From ff3028aca3a3cc2755d1af38894540cd2cdd91dd Mon Sep 17 00:00:00 2001 From: Ryszard Rozak Date: Thu, 19 Feb 2026 11:33:30 +0100 Subject: [PATCH] Support `disable iff` with sequences (#7090) --- src/V3AssertPre.cpp | 65 +++++++++++++++++-- src/V3Width.cpp | 4 -- test_regress/t/t_property_sexpr_disable.py | 18 +++++ test_regress/t/t_property_sexpr_disable.v | 52 +++++++++++++++ ...t_property_sexpr_disable_sampled_unsup.out | 6 ++ .../t_property_sexpr_disable_sampled_unsup.py | 18 +++++ .../t_property_sexpr_disable_sampled_unsup.v | 35 ++++++++++ .../t/t_property_sexpr_parse_unsup.out | 28 ++++---- test_regress/t/t_property_sexpr_unsup.out | 20 +----- test_regress/t/t_property_sexpr_unsup.v | 10 --- 10 files changed, 205 insertions(+), 51 deletions(-) create mode 100755 test_regress/t/t_property_sexpr_disable.py create mode 100644 test_regress/t/t_property_sexpr_disable.v create mode 100644 test_regress/t/t_property_sexpr_disable_sampled_unsup.out create mode 100755 test_regress/t/t_property_sexpr_disable_sampled_unsup.py create mode 100644 test_regress/t/t_property_sexpr_disable_sampled_unsup.v diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 81ebc2afc..f740de1c9 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -54,8 +54,10 @@ private: AstSenItem* m_seniAlwaysp = nullptr; // Last sensitivity in always // Reset each assertion: AstNodeExpr* m_disablep = nullptr; // Last disable + AstIf* m_disableSeqIfp = nullptr; // Used for handling disable iff in sequences // Other: V3UniqueNames m_cycleDlyNames{"__VcycleDly"}; // Cycle delay counter name generator + V3UniqueNames m_disableCntNames{"__VdisableCnt"}; // Disable condition counter name generator bool m_inAssign = false; // True if in an AssignNode bool m_inAssignDlyLhs = false; // True if in AssignDly's LHS bool m_inSynchDrive = false; // True if in synchronous drive @@ -374,6 +376,11 @@ private: new AstConst{flp, 1}}}); beginp->addStmtsp(loopp); } + if (m_disableSeqIfp) { + AstIf* const disableSeqIfp = m_disableSeqIfp->cloneTree(false); + disableSeqIfp->addThensp(nodep->nextp()->unlinkFrBackWithNext()); + nodep->addNextHere(disableSeqIfp); + } nodep->replaceWith(beginp); VL_DO_DANGLING(nodep->deleteTree(), nodep); } @@ -648,16 +655,64 @@ private: iterate(nodep->propp()); } void visit(AstPExpr* nodep) override { - VL_RESTORER(m_inPExpr); - m_inPExpr = true; - if (AstLogNot* const notp = VN_CAST(nodep->backp(), LogNot)) { notp->replaceWith(nodep->unlinkFrBack()); VL_DO_DANGLING(pushDeletep(notp), notp); iterate(nodep); - } else { - iterateChildren(nodep); + return; } + VL_RESTORER(m_inPExpr); + VL_RESTORER(m_disableSeqIfp); + m_inPExpr = true; + + if (m_disablep) { + const AstSampled* sampledp; + if (m_disablep->exists([&sampledp](const AstSampled* const sp) { + sampledp = sp; + return true; + })) { + sampledp->v3warn(E_UNSUPPORTED, + "Unsupported: $sampled inside disabled condition of a sequence"); + m_disablep = new AstConst{m_disablep->fileline(), AstConst::BitFalse{}}; + // always a copy is used, so remove it now + pushDeletep(m_disablep); + } + FileLine* const flp = nodep->fileline(); + // Add counter which counts times the condition turned true + AstVar* const disableCntp + = new AstVar{flp, VVarType::MODULETEMP, m_disableCntNames.get(""), + nodep->findBasicDType(VBasicDTypeKwd::UINT32)}; + disableCntp->lifetime(VLifetime::STATIC_EXPLICIT); + m_modp->addStmtsp(disableCntp); + AstVarRef* const readCntRefp = new AstVarRef{flp, disableCntp, VAccess::READ}; + AstVarRef* const writeCntRefp = new AstVarRef{flp, disableCntp, VAccess::WRITE}; + AstAssign* const incrStmtp = new AstAssign{ + flp, writeCntRefp, new AstAdd{flp, readCntRefp, new AstConst{flp, 1}}}; + AstAlways* const alwaysp + = new AstAlways{flp, VAlwaysKwd::ALWAYS, + new AstSenTree{flp, new AstSenItem{flp, VEdgeType::ET_POSEDGE, + m_disablep->cloneTree(false)}}, + incrStmtp}; + disableCntp->addNextHere(alwaysp); + + // Store value of that counter at the beginning of sequence evaluation + AstBegin* const bodyp = nodep->bodyp(); + AstVar* const initialCntp = new AstVar{flp, VVarType::BLOCKTEMP, "__VinitialCnt", + nodep->findBasicDType(VBasicDTypeKwd::UINT32)}; + initialCntp->lifetime(VLifetime::AUTOMATIC_EXPLICIT); + bodyp->stmtsp()->addHereThisAsNext(initialCntp); + AstAssign* const assignp + = new AstAssign{flp, new AstVarRef{flp, initialCntp, VAccess::WRITE}, + readCntRefp->cloneTree(false)}; + initialCntp->addNextHere(assignp); + + m_disableSeqIfp + = new AstIf{flp, new AstEq{flp, new AstVarRef{flp, initialCntp, VAccess::READ}, + readCntRefp->cloneTree(false)}}; + // Delete it, because it is always copied before insetion to the AST + pushDeletep(m_disableSeqIfp); + } + iterateChildren(nodep); } void visit(AstNodeModule* nodep) override { VL_RESTORER(m_defaultClockingp); diff --git a/src/V3Width.cpp b/src/V3Width.cpp index 50f0cb2dd..a61a0904e 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -5489,10 +5489,6 @@ class WidthVisitor final : public VNVisitor { newp->dtypeFrom(nodep); nodep->replaceWith(newp); VL_DO_DANGLING(pushDeletep(nodep), nodep); - } else if (nodep->disablep()) { - nodep->disablep()->v3warn(E_UNSUPPORTED, - "Unsupported: Disable iff with sequence expression"); - VL_DO_DANGLING(pushDeletep(nodep->disablep()->unlinkFrBack()), nodep); } } } diff --git a/test_regress/t/t_property_sexpr_disable.py b/test_regress/t/t_property_sexpr_disable.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/test_regress/t/t_property_sexpr_disable.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_sexpr_disable.v b/test_regress/t/t_property_sexpr_disable.v new file mode 100644 index 000000000..bbefecde3 --- /dev/null +++ b/test_regress/t/t_property_sexpr_disable.v @@ -0,0 +1,52 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 Antmicro +// SPDX-License-Identifier: CC0-1.0 + +`define stop $stop +`define checkh(gotv, + expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got='h%p exp='h%p\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0) + +module t ( /*AUTOARG*/ + // Inputs + clk +); + + input clk; + + typedef struct { + int fails; + int passs; + } result_t; + + result_t results [int]; + result_t expected[int]; + + localparam MAX = 15; + integer cyc = 0; + + assert property (@(posedge clk) disable iff (cyc == 5 || cyc > MAX) 1 ##1 cyc < 10) + results[1].passs++; + else results[1].fails++; + + assert property (@(posedge clk) disable iff (1) 1 ##1 0) + results[2].passs++; + else results[2].fails++; + + assert property (@(posedge clk) disable iff (0) 1 ##1 0) + results[3].passs++; + else results[3].fails++; + + always @(clk) begin + ++cyc; + if (cyc == MAX) begin + expected[1] = '{2, 3}; + // expected[2] shouldn't be initialized + expected[3] = '{6, 0}; + `checkh(results, expected); + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule diff --git a/test_regress/t/t_property_sexpr_disable_sampled_unsup.out b/test_regress/t/t_property_sexpr_disable_sampled_unsup.out new file mode 100644 index 000000000..9c988bb01 --- /dev/null +++ b/test_regress/t/t_property_sexpr_disable_sampled_unsup.out @@ -0,0 +1,6 @@ +%Error-UNSUPPORTED: t/t_property_sexpr_disable_sampled_unsup.v:23:48: Unsupported: $sampled inside disabled condition of a sequence + : ... note: In instance 't' + 23 | assert property (@(posedge clk) disable iff ($sampled(cyc) == 4) 1 ##1 cyc % 3 == 0) passes++; + | ^~~~~~~~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr_disable_sampled_unsup.py b/test_regress/t/t_property_sexpr_disable_sampled_unsup.py new file mode 100755 index 000000000..504773395 --- /dev/null +++ b/test_regress/t/t_property_sexpr_disable_sampled_unsup.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('vlt') + +test.lint(expect_filename=test.golden_filename, + verilator_flags2=['--assert', '--timing', '--error-limit 1000'], + fails=True) + +test.passes() diff --git a/test_regress/t/t_property_sexpr_disable_sampled_unsup.v b/test_regress/t/t_property_sexpr_disable_sampled_unsup.v new file mode 100644 index 000000000..1172b73c1 --- /dev/null +++ b/test_regress/t/t_property_sexpr_disable_sampled_unsup.v @@ -0,0 +1,35 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 Antmicro +// SPDX-License-Identifier: CC0-1.0 + +`define stop $stop +`define checkh(gotv, + expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got='h%p exp='h%p\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0) + +module t ( /*AUTOARG*/ + // Inputs + clk +); + + input clk; + + localparam MAX = 10; + int cyc = 0; + int passes = 0; + int fails = 0; + + assert property (@(posedge clk) disable iff ($sampled(cyc) == 4) 1 ##1 cyc % 3 == 0) passes++; + else fails++; + + always @(posedge clk) begin + cyc <= cyc + 1; + if (cyc == MAX) begin + `checkh(passes, 3); + `checkh(fails, 4); + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule diff --git a/test_regress/t/t_property_sexpr_parse_unsup.out b/test_regress/t/t_property_sexpr_parse_unsup.out index 4c017ae88..0449d4338 100644 --- a/test_regress/t/t_property_sexpr_parse_unsup.out +++ b/test_regress/t/t_property_sexpr_parse_unsup.out @@ -1,23 +1,23 @@ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:75:14: Unsupported: sequence match items - 75 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:65:14: Unsupported: sequence match items + 65 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; | ^ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:75:29: Unsupported: ## range cycle delay range expression - 75 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:65:29: Unsupported: ## range cycle delay range expression + 65 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; | ^~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:74:13: Unsupported: property variable declaration - 74 | integer l_b; +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:64:13: Unsupported: property variable declaration + 64 | integer l_b; | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:16: Unsupported: sequence match items - 92 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:16: Unsupported: sequence match items + 82 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; | ^ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:51: Unsupported: [-> boolean abbrev expression - 92 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:51: Unsupported: [-> boolean abbrev expression + 82 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:54: Unsupported: boolean abbrev (in sequence expression) - 92 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:54: Unsupported: boolean abbrev (in sequence expression) + 82 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; | ^ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:90:14: Unsupported: property variable declaration - 90 | realtime l_t; +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:80:14: Unsupported: property variable declaration + 80 | realtime l_t; | ^~~ %Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr_unsup.out b/test_regress/t/t_property_sexpr_unsup.out index 67f822d29..137ce4bfb 100644 --- a/test_regress/t/t_property_sexpr_unsup.out +++ b/test_regress/t/t_property_sexpr_unsup.out @@ -27,24 +27,8 @@ : ... note: In instance 't' 43 | assert property (@(posedge clk) (##1 val) |-> (##1 val)) $display("[%0t] two delays implication stmt, fileline:%d", $time, 43); | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:45:52: Unsupported: Disable iff with sequence expression +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:46:18: Unsupported: Implication with sequence expression : ... note: In instance 't' - 45 | assert property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 45); - | ^~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:47:52: Unsupported: Disable iff with sequence expression - : ... note: In instance 't' - 47 | assume property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 47); - | ^~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:49:51: Unsupported: Disable iff with sequence expression - : ... note: In instance 't' - 49 | cover property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 49); - | ^~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:52:37: Unsupported: Disable iff with sequence expression - : ... note: In instance 't' - 52 | @(posedge clk) disable iff (cyc != 5) ##1 0; - | ^~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:56:18: Unsupported: Implication with sequence expression - : ... note: In instance 't' - 56 | ##1 cyc == 4 |-> 1; + 46 | ##1 cyc == 4 |-> 1; | ^~~ %Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr_unsup.v b/test_regress/t/t_property_sexpr_unsup.v index 21e7127f0..a424d576d 100644 --- a/test_regress/t/t_property_sexpr_unsup.v +++ b/test_regress/t/t_property_sexpr_unsup.v @@ -42,16 +42,6 @@ module t ( /*AUTOARG*/ assert property (@(posedge clk) (##1 val) |-> (##1 val)) $display("[%0t] two delays implication stmt, fileline:%d", $time, `__LINE__); - assert property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, `__LINE__); - - assume property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, `__LINE__); - - cover property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, `__LINE__); - - property prop_disableiff; - @(posedge clk) disable iff (cyc != 5) ##1 0; - endproperty - property prop_implication; ##1 cyc == 4 |-> 1; endproperty