Support assert property 'default disable iff` (#4848) (#7723)

src/V3Assert.cpp

@@ -23,6 +23,79 @@
 
 VL_DEFINE_DEBUG_FUNCTIONS;
 
+namespace {
+
+class DefaultDisableLocalVisitor final : public VNVisitor {
+    // STATE
+    AstNode* m_scopep = nullptr;
+
+    // VISITORS
+    void visit(AstNodeModule* nodep) override {
+        VL_RESTORER(m_scopep);
+        m_scopep = nodep;
+        nodep->defaultDisablep(nullptr);
+        iterateChildren(nodep);
+    }
+    void visit(AstGenBlock* nodep) override {
+        VL_RESTORER(m_scopep);
+        m_scopep = nodep;
+        nodep->defaultDisablep(nullptr);
+        iterateChildren(nodep);
+    }
+    void visit(AstDefaultDisable* nodep) override {
+        UASSERT_OBJ(nodep, m_scopep,
+                    "default disable iff must be inside a module or generate block");
+        AstDefaultDisable* defaultp = nullptr;
+        if (const AstNodeModule* const modp = VN_CAST(m_scopep, NodeModule)) {
+            defaultp = modp->defaultDisablep();
+        } else {
+            defaultp = VN_AS(m_scopep, GenBlock)->defaultDisablep();
+        }
+        if (VL_UNLIKELY(defaultp)) {
+            nodep->v3error("Only one 'default disable iff' allowed per "
+                           << (VN_IS(m_scopep, NodeModule) ? "module" : "generate block")
+                           << " (IEEE 1800-2023 16.15)");
+        } else if (AstNodeModule* const modp = VN_CAST(m_scopep, NodeModule)) {
+            modp->defaultDisablep(nodep);
+        } else {
+            VN_AS(m_scopep, GenBlock)->defaultDisablep(nodep);
+        }
+    }
+    void visit(AstNode* nodep) override { iterateChildren(nodep); }
+
+public:
+    explicit DefaultDisableLocalVisitor(AstNetlist* nodep) { iterate(nodep); }
+};
+
+class DefaultDisablePropagateVisitor final : public VNVisitor {
+    // STATE
+    AstDefaultDisable* m_defaultDisablep = nullptr;
+
+    // VISITORS
+    void visit(AstNodeModule* nodep) override {
+        VL_RESTORER(m_defaultDisablep);
+        m_defaultDisablep = nodep->defaultDisablep();
+        iterateChildren(nodep);
+    }
+    void visit(AstGenBlock* nodep) override {
+        VL_RESTORER(m_defaultDisablep);
+        if (!nodep->defaultDisablep()) nodep->defaultDisablep(m_defaultDisablep);
+        m_defaultDisablep = nodep->defaultDisablep();
+        iterateChildren(nodep);
+    }
+    void visit(AstNode* nodep) override { iterateChildren(nodep); }
+
+public:
+    explicit DefaultDisablePropagateVisitor(AstNetlist* nodep) { iterate(nodep); }
+};
+
+}  // namespace
+
+void V3AssertCommon::collectDefaultDisable(AstNetlist* nodep) {
+    { DefaultDisableLocalVisitor{nodep}; }
+    { DefaultDisablePropagateVisitor{nodep}; }
+}
+
 //######################################################################
 // AssertDeFutureVisitor
 // If any AstFuture, then move all non-future varrefs to be one cycle behind,

src/V3Assert.h

@@ -24,6 +24,11 @@
 
 //============================================================================
 
+class V3AssertCommon final {
+public:
+    static void collectDefaultDisable(AstNetlist* nodep) VL_MT_DISABLED;
+};
+
 class V3Assert final {
 public:
     static void assertAll(AstNetlist* nodep) VL_MT_DISABLED;

src/V3AssertNfa.cpp

@@ -26,6 +26,7 @@
 
 #include "V3AssertNfa.h"
 
+#include "V3Assert.h"
 #include "V3Const.h"
 #include "V3Graph.h"
 #include "V3Task.h"
@@ -2301,7 +2302,7 @@ class AssertNfaVisitor final : public VNVisitor {
         VL_RESTORER(m_defaultDisablep);
         m_modp = nodep;
         m_defaultClockingp = nullptr;
-        m_defaultDisablep = nullptr;
+        m_defaultDisablep = nodep->defaultDisablep();
         SvaNfaLowering lowering{nodep};
         m_loweringp = &lowering;
         iterateChildren(nodep);
@@ -2310,9 +2311,12 @@ class AssertNfaVisitor final : public VNVisitor {
         if (nodep->isDefault() && !m_defaultClockingp) m_defaultClockingp = nodep;
         iterateChildren(nodep);
     }
-    void visit(AstDefaultDisable* nodep) override {
-        if (!m_defaultDisablep) m_defaultDisablep = nodep;
+    void visit(AstGenBlock* nodep) override {
+        VL_RESTORER(m_defaultDisablep);
+        m_defaultDisablep = nodep->defaultDisablep();
+        iterateChildren(nodep);
     }
+    void visit(AstDefaultDisable* nodep) override {}
     void visit(AstAssert* nodep) override { processAssertion(nodep); }
     void visit(AstCover* nodep) override { processAssertion(nodep); }
     void visit(AstRestrict* nodep) override {

src/V3AssertPre.cpp

@@ -23,6 +23,7 @@
 
 #include "V3AssertPre.h"
 
+#include "V3Assert.h"
 #include "V3Const.h"
 #include "V3Task.h"
 #include "V3UniqueNames.h"
@@ -1438,12 +1439,6 @@ private:
     }
 
     void visit(AstDefaultDisable* nodep) override {
-        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 {
@@ -1565,10 +1560,15 @@ private:
         VL_RESTORER(m_modp);
         m_defaultClockingp = nullptr;
         m_defaultClkEvtVarp = nullptr;
-        m_defaultDisablep = nullptr;
+        m_defaultDisablep = nodep->defaultDisablep();
         m_modp = nodep;
         iterateChildren(nodep);
     }
+    void visit(AstGenBlock* nodep) override {
+        VL_RESTORER(m_defaultDisablep);
+        m_defaultDisablep = nodep->defaultDisablep();
+        iterateChildren(nodep);
+    }
     void visit(AstProperty* nodep) override {
         // The body will be visited when will be substituted in place of property reference
         // (AstFuncRef)

src/V3AstNodeOther.h

@@ -301,6 +301,7 @@ class AstNodeModule VL_NOT_FINAL : public AstNode {
     VLifetime m_lifetime;  // Lifetime
     VTimescale m_timeunit;  // Global time unit
     VOptionBool m_unconnectedDrive;  // State of `unconnected_drive
+    AstDefaultDisable* m_defaultDisablep = nullptr;  // Default disable iff in this scope
 
     bool m_modPublic : 1;  // Module has public references
     bool m_modTrace : 1;  // Tracing this module
@@ -351,6 +352,8 @@ public:
     string origName() const override { return m_origName; }
     string someInstanceName() const VL_MT_SAFE { return m_someInstanceName; }
     void someInstanceName(const string& name) { m_someInstanceName = name; }
+    AstDefaultDisable* defaultDisablep() const { return m_defaultDisablep; }
+    void defaultDisablep(AstDefaultDisable* nodep) { m_defaultDisablep = nodep; }
     bool inLibrary() const { return m_inLibrary; }
     void inLibrary(bool flag) { m_inLibrary = flag; }
     void depth(int value) { m_depth = value; }
@@ -2810,6 +2813,7 @@ class AstGenBlock final : public AstNodeGen {
     std::string m_name;  // Name of block
     const bool m_unnamed;  // Originally unnamed (name change does not affect this)
     const bool m_implied;  // Not inserted by user
+    AstDefaultDisable* m_defaultDisablep = nullptr;  // Default disable iff in this scope
 
 public:
     AstGenBlock(FileLine* fl, const string& name, AstNode* itemsp, bool implied)
@@ -2826,6 +2830,8 @@ public:
     void name(const std::string& name) override { m_name = name; }
     bool unnamed() const { return m_unnamed; }
     bool implied() const { return m_implied; }
+    AstDefaultDisable* defaultDisablep() const { return m_defaultDisablep; }
+    void defaultDisablep(AstDefaultDisable* nodep) { m_defaultDisablep = nodep; }
 };
 class AstGenCase final : public AstNodeGen {
     // Generate 'case'

src/Verilator.cpp

@@ -260,6 +260,7 @@ static void process() {
 
         // Assertion insertion
         //    After we've added block coverage, but before other nasty transforms
+        V3AssertCommon::collectDefaultDisable(v3Global.rootp());
         V3AssertNfa::assertNfaAll(v3Global.rootp());
         // V3AssertProp removed: NFA subsumes multi-cycle property lowering.
         // Unsupported constructs fall through to V3AssertPre.

src/verilog.y

@@ -6664,14 +6664,8 @@ property_spec<propSpecp>:               // IEEE: property_spec
                         { $$ = new AstPropSpec{$1, $3, nullptr, $5}; }
         |       '@' senitemVar pexpr
                         { $$ = new AstPropSpec{$1, $2, nullptr, $3}; }
-        //                      // Disable applied after the event occurs,
-        //                      // so no existing AST can represent this
-        |       yDISABLE yIFF '(' expr ')' '@' '(' senitemEdge ')' pexpr
-                        { $$ = new AstPropSpec{$1, $8, nullptr, new AstLogOr{$1, $4, $10}};
-                          BBUNSUP($<fl>1, "Unsupported: property '(disable iff (...) @ (...)'\n"
-                                  + $<fl>1->warnMore()
-                                  + "... Suggest use property '(@(...) disable iff (...))'"); }
-        //UNSUP remove above
+        |       yDISABLE yIFF '(' expr ')' '@' '(' senitem ')' pexpr
+                        { $$ = new AstPropSpec{$1, $8, $4, $10}; }
         |       yDISABLE yIFF '(' expr ')' pexpr        { $$ = new AstPropSpec{$4->fileline(), nullptr, $4, $6}; }
         |       pexpr                                   { $$ = new AstPropSpec{$1->fileline(), nullptr, nullptr, $1}; }
         ;

test_regress/t/t_assert_iff_clk.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()

test_regress/t/t_assert_iff_clk.v

@@ -0,0 +1,48 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 Antmicro Ltd
+// SPDX-License-Identifier: CC0-1.0
+
+module t (
+    input clk
+);
+
+  int cyc;
+  logic rst = 1'b1;
+  logic x = 1'b1;
+  int issue_fail;
+  int pre_fail;
+  int post_fail;
+  int pre_temporal_fail;
+  int post_temporal_fail;
+
+  a_issue: assert property (disable iff(rst !== 1'b0) @(posedge clk) !x)
+    else issue_fail++;
+
+  assert property (disable iff (cyc < 5) @(posedge clk) 0)
+    else pre_fail++;
+
+  assert property (@(posedge clk) disable iff (cyc < 5) 0)
+    else post_fail++;
+
+  assert property (disable iff (cyc < 5) @(posedge clk) 1 ##1 0)
+    else pre_temporal_fail++;
+
+  assert property (@(posedge clk) disable iff (cyc < 5) 1 ##1 0)
+    else post_temporal_fail++;
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    rst <= cyc < 4;
+    x <= cyc < 4;
+    if (cyc == 12) begin
+      if (issue_fail != 0) $stop;
+      if (pre_fail != post_fail) $stop;
+      if (pre_temporal_fail != post_temporal_fail) $stop;
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+
+endmodule

test_regress/t/t_assert_iff_clk_unsup.out

@@ -1,6 +0,0 @@
-%Error-UNSUPPORTED: t/t_assert_iff_clk_unsup.v:20:20: Unsupported: property '(disable iff (...) @ (...)'
-                                                    : ... Suggest use property '(@(...) disable iff (...))'
-   20 |   assert property (disable iff (cyc < 5) @(posedge clk) cyc >= 5);
-      |                    ^~~~~~~
-                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
-%Error: Exiting due to

test_regress/t/t_assert_iff_clk_unsup.v

@@ -1,22 +0,0 @@
-// DESCRIPTION: Verilator: Verilog Test module
-//
-// This file ONLY is placed under the Creative Commons Public Domain.
-// SPDX-FileCopyrightText: 2022 Antmicro Ltd
-// SPDX-License-Identifier: CC0-1.0
-
-module t (
-    input clk
-);
-
-  input clk;
-  int cyc = 0;
-  logic val = 0;
-
-  always @(posedge clk) begin
-    cyc <= cyc + 1;
-    val = ~val;
-  end
-
-  assert property (disable iff (cyc < 5) @(posedge clk) cyc >= 5);
-
-endmodule

test_regress/t/t_default_disable_iff_gen_multi_bad.out

@@ -0,0 +1,6 @@
+%Error: t/t_default_disable_iff_gen_multi_bad.v:15:7: Only one 'default disable iff' allowed per generate block (IEEE 1800-2023 16.15)
+                                                    : ... note: In instance 't'
+   15 |       default disable iff (cyc < 7);
+      |       ^~~~~~~
+        ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
+%Error: Exiting due to

test_regress/t/t_default_disable_iff_gen_multi_bad.py

@@ -4,13 +4,13 @@
 # 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: 2024 Wilson Snyder
+# SPDX-FileCopyrightText: 2026 Wilson Snyder
 # SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
 
 import vltest_bootstrap
 
-test.scenarios('vlt')
+test.scenarios('linter')
 
-test.lint(expect_filename=test.golden_filename, verilator_flags2=['--assert'], fails=True)
+test.lint(fails=True, expect_filename=test.golden_filename)
 
 test.passes()

test_regress/t/t_default_disable_iff_gen_multi_bad.v

@@ -0,0 +1,20 @@
+// 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
+
+module t(input clk);
+  int cyc;
+
+  default disable iff (cyc < 3);
+
+  generate
+    begin : g
+      default disable iff (cyc < 5);
+      default disable iff (cyc < 7);
+
+      assert property (@(posedge clk) 0);
+    end
+  endgenerate
+endmodule

test_regress/t/t_default_disable_iff_scope.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()

test_regress/t/t_default_disable_iff_scope.v

@@ -0,0 +1,230 @@
+// 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
+
+// verilog_format: off
+`define stop $stop
+`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0);
+// verilog_format: on
+
+module t;
+  bit clk;
+  int cyc;
+
+  always #1 clk = !clk;
+
+  bit rst_mod;
+  int before_mod_false;
+  int before_mod_gen_false;
+  int before_gen_default_false;
+  int before_gen_child_default_false;
+  int prog_false_count;
+
+  always_comb rst_mod = (cyc < 3);
+
+  // The default declaration appears later in the module, but still applies here.
+  assert property (@(posedge clk) 0)
+    else before_mod_false++;
+
+  generate
+    begin : g_before_mod_default
+      // Inherits the module default declaration that appears later in this module.
+      assert property (@(posedge clk) 0)
+        else before_mod_gen_false++;
+    end
+
+    begin : g_before_local_default
+      // The generate-local default declaration appears later in the block.
+      assert property (@(posedge clk) 0)
+        else before_gen_default_false++;
+
+      begin : g_child_inherit
+        // Inherits the generate-local default declaration that appears later.
+        assert property (@(posedge clk) 0)
+          else before_gen_child_default_false++;
+      end
+      default disable iff (cyc < 7);
+    end
+  endgenerate
+
+  default disable iff (rst_mod);
+
+  generate
+    begin : g_override
+      bit rst_gen;
+      int override_false;
+
+      always_comb rst_gen = (cyc < 5);
+
+      default disable iff (rst_gen);
+
+      assert property (@(posedge clk) 0)
+        else override_false++;
+    end
+
+    begin : g_inherit
+      bit rst_mod;
+      int inherit_false;
+
+      always_comb rst_mod = (cyc < 8);
+
+      // Inherits the module default, whose rst_mod was resolved in module scope.
+      assert property (@(posedge clk) 0)
+        else inherit_false++;
+    end
+  endgenerate
+
+  if_scope u_if (.clk(clk), .cyc(cyc));
+  p_scope u_prog (.clk(clk), .cyc(cyc), .false_count(prog_false_count));
+  examples_with_default_count u_with (.clk(clk), .cyc(cyc));
+  examples_without_default_count u_without (.clk(clk), .cyc(cyc));
+  examples_with_default u_ieee_with (.a(1'b0), .b(1'b0), .clk(clk), .rst(1'b0), .rst1(1'b0));
+  examples_without_default u_ieee_without (.a(1'b0), .b(1'b0), .clk(clk), .rst(1'b0));
+  m_override u_m_override (.clk(clk), .cyc(cyc));
+
+  // The disable iff expression is unsampled, so same-edge updates race in MT simulation.
+  // Change clk on negedge while the properties are sampled on posedge to avoid races.
+  always @(negedge clk) begin
+    cyc++;
+    if (cyc == 12) begin
+      `checkd(before_mod_false, 9);
+      `checkd(before_mod_gen_false, 9);
+      `checkd(before_gen_default_false, 5);
+      `checkd(before_gen_child_default_false, 5);
+      `checkd(g_inherit.inherit_false, 9);
+      `checkd(g_override.override_false, 7);
+      `checkd(u_if.false_count, 6);
+      `checkd(u_if.g_inherit.false_count, 6);
+      `checkd(prog_false_count, 4);
+      `checkd(u_with.explicit_assert_false, 5);
+      `checkd(u_with.explicit_property_false, 5);
+      `checkd(u_with.inferred_default_false, 9);
+      `checkd(u_without.explicit_assert_false, 9);
+      `checkd(u_without.explicit_property_false, 9);
+      `checkd(u_m_override.false_count, 7);
+      `checkd(u_m_override.g_inherit_from_module.false_count, 7);
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+endmodule
+
+module examples_with_default (input logic a, b, clk, rst, rst1);
+default disable iff rst;
+property p1;
+disable iff (rst1) a |=> b;
+endproperty
+// Disable condition is rst1 - explicitly specified within a1
+a1 : assert property (@(posedge clk) disable iff (rst1) a |=> b);
+// Disable condition is rst1 - explicitly specified within p1
+a2 : assert property (@(posedge clk) p1);
+// Disable condition is rst - no explicit specification, inferred from
+// default disable iff declaration
+a3 : assert property (@(posedge clk) a |=> b);
+// Disable condition is 1'b0. This is the only way to
+// cancel the effect of default disable.
+a4 : assert property (@(posedge clk) disable iff (1'b0) a |=> b);
+endmodule
+
+module examples_without_default (input logic a, b, clk, rst);
+property p2;
+disable iff (rst) a |=> b;
+endproperty
+// Disable condition is rst - explicitly specified within a5
+a5 : assert property (@(posedge clk) disable iff (rst) a |=> b);
+// Disable condition is rst - explicitly specified within p2
+a6 : assert property (@ (posedge clk) p2);
+// No disable condition
+a7 : assert property (@ (posedge clk) a |=> b);
+endmodule
+
+module examples_with_default_count(input bit clk, input int cyc);
+  int explicit_assert_false;
+  int explicit_property_false;
+  int inferred_default_false;
+
+  default disable iff (cyc < 3);
+
+  property p1;
+    disable iff (cyc < 7) 0;
+  endproperty
+
+  // Disable condition is explicit in the assertion.
+  assert property (@(posedge clk) disable iff (cyc < 7) 0)
+    else explicit_assert_false++;
+
+  // Disable condition is explicit in the property.
+  assert property (@(posedge clk) p1)
+    else explicit_property_false++;
+
+  // Disable condition is inferred from the default.
+  assert property (@(posedge clk) 0)
+    else inferred_default_false++;
+
+endmodule
+
+module examples_without_default_count(input bit clk, input int cyc);
+  int explicit_assert_false;
+  int explicit_property_false;
+
+  property p2;
+    disable iff (cyc < 3) 0;
+  endproperty
+
+  // Disable condition is explicit in the assertion.
+  assert property (@(posedge clk) disable iff (cyc < 3) 0)
+    else explicit_assert_false++;
+
+  // Disable condition is explicit in the property.
+  assert property (@(posedge clk) p2)
+    else explicit_property_false++;
+
+endmodule
+
+module m_override(input bit clk, input int cyc);
+  bit rst2;
+  int false_count;
+
+  always_comb rst2 = (cyc < 5);
+  default disable iff (rst2);
+
+  assert property (@(posedge clk) 0)
+    else false_count++;
+
+  generate
+    begin : g_inherit_from_module
+      int false_count;
+      assert property (@(posedge clk) 0)
+        else false_count++;
+    end
+  endgenerate
+endmodule
+
+interface if_scope(input bit clk, input int cyc);
+  bit rst_if;
+  int false_count;
+
+  always_comb rst_if = (cyc < 6);
+  default disable iff (rst_if);
+
+  assert property (@(posedge clk) 0)
+    else false_count++;
+
+  generate
+    begin : g_inherit
+      int false_count;
+      assert property (@(posedge clk) 0)
+        else false_count++;
+    end
+  endgenerate
+endinterface
+
+program p_scope(input bit clk, input int cyc,
+                output int false_count);
+  default disable iff (cyc < 8);
+
+  assert property (@(posedge clk) 0)
+    else false_count++;
+endprogram