From cd2475fbd4ee3ed9f167da1f2dfd02f9a33bffdc Mon Sep 17 00:00:00 2001
From: Artur Bieniek <abieniek@antmicro.com>
Date: Mon, 7 Sep 2026 19:50:13 +0200
Subject: [PATCH] Support non-overlapped property implications correctly
 (#8268)

Signed-off-by: Artur Bieniek <abieniek@antmicro.com>
---
 src/V3AstNodeExpr.h                        |  4 ++--
 test_regress/t/t_assert_ctl_pass_actions.v | 25 ++++++++++++++++++++++
 2 files changed, 27 insertions(+), 2 deletions(-)

diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h
index a1b2b8b6c..d0bc35961 100644
--- a/src/V3AstNodeExpr.h
+++ b/src/V3AstNodeExpr.h
@@ -1760,7 +1760,7 @@ public:
     bool sameNode(const AstNode* /*samep*/) const override { return true; }
 };
 class AstImplication final : public AstNodeExpr {
-    // Implication |-> |=> (IEEE 1800-2023 16.12.6) and followed-by #-# #=#
+    // Implication |-> |=> (IEEE 1800-2023 16.12.7) and followed-by #-# #=#
     // (IEEE 1800-2023 16.12.9). Antecedent-miss is vacuous-pass for implication
     // and non-vacuous-fail for followed-by, hence the separate flag.
     // @astgen op1 := lhsp : AstNodeExpr
@@ -1788,7 +1788,7 @@ public:
     string emitSimpleOperator() override { V3ERROR_NA_RETURN(""); }
     bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
     int instrCount() const override { return widthInstrs(); }
-    bool isMultiCycleSva() const override { return m_isFollowedBy; }
+    bool isMultiCycleSva() const override { return m_isFollowedBy || !m_isOverlapped; }
     bool isOverlapped() const { return m_isOverlapped; }
     bool isFollowedBy() const { return m_isFollowedBy; }
 };
diff --git a/test_regress/t/t_assert_ctl_pass_actions.v b/test_regress/t/t_assert_ctl_pass_actions.v
index 3a7065569..b53477c19 100644
--- a/test_regress/t/t_assert_ctl_pass_actions.v
+++ b/test_regress/t/t_assert_ctl_pass_actions.v
@@ -55,11 +55,16 @@ endinterface
 
 module t;
   bit clk = 0;
+  bit [6:0] stimulus = 7'b1;
   int imm_passes = 0;
   int imm_fails = 0;
   int vacuous_passes = 0;
   int nonvacuous_passes = 0;
   int concurrent_fails = 0;
+  int overlap_seq_passes = 0;
+  int overlap_seq_fails = 0;
+  int nonoverlap_seq_passes = 0;
+  int nonoverlap_seq_fails = 0;
   int class_fails = 0;
 
   class AssertCtlClass;
@@ -80,6 +85,7 @@ module t;
   virtual AssertCtlIface v_assert_ctl_iface = assert_ctl_iface;
 
   always #5 clk = !clk;
+  always @(negedge clk) stimulus = {stimulus[5:0], stimulus[6] ^ stimulus[5]};
 
   default clocking @(posedge clk);
   endclocking
@@ -98,6 +104,17 @@ module t;
   end
   else concurrent_fails++;
 
+  assert property (@(posedge clk) stimulus[0] |-> ##1 stimulus[3]) overlap_seq_passes++;
+  else overlap_seq_fails++;
+
+  assert property (@(posedge clk) stimulus[0] |=> stimulus[3]) nonoverlap_seq_passes++;
+  else nonoverlap_seq_fails++;
+
+  task automatic check_cycle_equivalence();
+    `checkd(nonoverlap_seq_passes, overlap_seq_passes);
+    `checkd(nonoverlap_seq_fails, overlap_seq_fails);
+  endtask
+
   task automatic tick_and_check(input int exp_vacuous, input int exp_nonvacuous,
                                 input int exp_concurrent_fails);
     @(posedge clk);
@@ -105,6 +122,7 @@ module t;
     `checkd(vacuous_passes, exp_vacuous);
     `checkd(nonvacuous_passes, exp_nonvacuous);
     `checkd(concurrent_fails, exp_concurrent_fails);
+    check_cycle_equivalence();
   endtask
 
   initial begin
@@ -221,6 +239,13 @@ module t;
     $assertcontrol(8, 1, 1);
     tick_and_check(4, 5, 1);
 
+    // Exercise all 127 states of the maximal-length LFSR, and wrap around
+    repeat (2 * 127) begin
+      @(posedge clk);
+      #2;
+      check_cycle_equivalence();
+    end
+
     $write("*-* All Finished *-*\n");
     $finish;
   end