Fix `cover property` of an implication counting vacuous matches (#7789)

src/V3AssertPre.cpp

@@ -61,6 +61,7 @@ private:
     AstNodeExpr* m_disablep = nullptr;  // Last disable
     AstIf* m_disableSeqIfp = nullptr;  // Used for handling disable iff in sequences
     AstPExpr* m_pexprp = nullptr;  // Last AstPExpr
+    bool m_underCover = false;  // True if the enclosing assertion is a cover
     // Other:
     V3UniqueNames m_cycleDlyNames{"__VcycleDly"};  // Cycle delay counter name generator
     V3UniqueNames m_consRepNames{"__VconsRep"};  // Consecutive repetition counter name generator
@@ -1282,7 +1283,10 @@ private:
             // Don't iterate pexprp here -- it was already iterated when created
             // (in visit(AstSExpr*)), so delays and disable iff are already processed.
         } else if (nodep->isOverlapped()) {
-            nodep->replaceWith(new AstLogOr{flp, new AstLogNot{flp, lhsp}, rhsp});
+            AstNodeExpr* const exprp
+                = m_underCover ? static_cast<AstNodeExpr*>(new AstLogAnd{flp, lhsp, rhsp})
+                               : new AstLogOr{flp, new AstLogNot{flp, lhsp}, rhsp};
+            nodep->replaceWith(exprp);
         } else {
             if (m_disablep) {
                 lhsp = new AstAnd{flp, new AstNot{flp, m_disablep->cloneTreePure(false)}, lhsp};
@@ -1291,7 +1295,9 @@ private:
             AstPast* const pastp = new AstPast{flp, lhsp};
             pastp->dtypeFrom(lhsp);
             pastp->sentreep(newSenTree(nodep));
-            AstNodeExpr* const exprp = new AstOr{flp, new AstNot{flp, pastp}, rhsp};
+            AstNodeExpr* const exprp
+                = m_underCover ? static_cast<AstNodeExpr*>(new AstAnd{flp, pastp, rhsp})
+                               : new AstOr{flp, new AstNot{flp, pastp}, rhsp};
             exprp->dtypeSetBit();
             nodep->replaceWith(exprp);
         }
@@ -1469,6 +1475,10 @@ private:
             nodep->propp(new AstSampled{nodep->fileline(), nodep->propp()->unlinkFrBack(),
                                         propDtp->dtypep()});
         }
+        // cover counts non-vacuous matches only (IEEE 1800-2023 16.15.2), so an
+        // implication antecedent must hold; assert passes vacuously instead.
+        VL_RESTORER(m_underCover);
+        m_underCover = VN_IS(nodep->backp(), Cover);
         iterate(nodep->propp());
     }
     void visit(AstPExpr* nodep) override {

test_regress/t/t_cover_property.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.compile(verilator_flags2=['--coverage', '--assert', '--timing'])
+
+test.execute()
+
+test.passes()

test_regress/t/t_cover_property.v

@@ -0,0 +1,77 @@
+// 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 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
+
+module t (
+    input clk
+);
+
+  logic [63:0] crc = 64'h5aef0c8dd70a4497;
+  logic a, b;
+  int cyc = 0;
+
+  int n_imp_no = 0;  // cover property (a |=> b)  -- non-overlapped implication
+  int n_imp_ov = 0;  // cover property (a |-> b)  -- overlapped implication
+  int n_seq = 0;  // cover property (a ##1 b)  -- identity with |=>
+  int n_seq0 = 0;  // cover property (a ##0 b)  -- identity with |->
+  int n_bool = 0;  // cover property (a)        -- bare boolean baseline
+  int n_named = 0;  // cover property (named pr) -- identity with |=>
+
+  default clocking cb @(posedge clk);
+  endclocking
+
+  assign a = crc[0];
+  assign b = crc[5];
+
+  property pr;
+    a |=> b;
+  endproperty
+
+  cp_imp_no :
+  cover property (a |=> b) n_imp_no++;
+  cp_imp_ov :
+  cover property (a |-> b) n_imp_ov++;
+  cp_seq :
+  cover property (a ##1 b) n_seq++;
+  cp_seq0 :
+  cover property (a ##0 b) n_seq0++;
+  cp_bool :
+  cover property (a) n_bool++;
+  cp_named :
+  cover property (pr) n_named++;
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[1] ^ crc[0]};
+    if (cyc == 99) begin
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+
+  final begin
+    // A cover of an implication counts only non-vacuous matches (IEEE
+    // 1800-2023 16.15.2): the antecedent must match. So it is identical to the
+    // corresponding sequence cover, not the vacuous implication value.
+    `checkd(n_imp_no, n_seq)
+    `checkd(n_imp_ov, n_seq0)
+    // A named-property cover lowers the same implication, so it also counts
+    // non-vacuously (regression guard for the property-inlining path).
+    `checkd(n_named, n_imp_no)
+    // Pinned Verilator counts; Questa golden cross-checked.
+    `checkd(n_imp_no, 28)  // Questa: 28
+    `checkd(n_imp_ov, 27)  // Questa: 27
+    `checkd(n_seq, 28)  // Questa: 28
+    `checkd(n_seq0, 27)  // Questa: 27
+    `checkd(n_bool, 55)  // Questa: 54
+    `checkd(n_named, 28)  // Questa: 28
+  end
+
+endmodule