From f7c087468dd2e76b1b1b72096a4cbcb2e1f578e7 Mon Sep 17 00:00:00 2001
From: Artur Bieniek <abieniek@antmicro.com>
Date: Thu, 20 Aug 2026 21:20:54 +0200
Subject: [PATCH] Support overlong `within` sequences as never-matching (#8177)

Signed-off-by: Artur Bieniek <abieniek@antmicro.com>
---
 src/V3AssertNfa.cpp                            |  7 +------
 .../t/t_sequence_intersect_nevermatch.v        |  7 +++++++
 test_regress/t/t_sequence_within_bad.out       |  6 ------
 test_regress/t/t_sequence_within_bad.py        | 18 ------------------
 test_regress/t/t_sequence_within_bad.v         | 16 ----------------
 5 files changed, 8 insertions(+), 46 deletions(-)
 delete mode 100644 test_regress/t/t_sequence_within_bad.out
 delete mode 100755 test_regress/t/t_sequence_within_bad.py
 delete mode 100644 test_regress/t/t_sequence_within_bad.v

diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp
index 05375f41e..e10b43108 100644
--- a/src/V3AssertNfa.cpp
+++ b/src/V3AssertNfa.cpp
@@ -1087,12 +1087,7 @@ class SvaNfaBuilder final {
             nodep->v3warn(E_UNSUPPORTED, "Unsupported: within with ranged cycle-delay operand");
             return BuildResult::failWithError();
         }
-        if (innerLen > outerLen) {
-            nodep->v3error("'within' inner sequence " + std::to_string(innerLen)
-                           + " cycles exceeds outer sequence " + std::to_string(outerLen)
-                           + " cycles (IEEE 1800-2023 16.9.10)");
-            return BuildResult::failWithError();
-        }
+        if (innerLen > outerLen) return buildNeverMatchIntersect(nodep, entryVtxp, isTopLevelStep);
         FileLine* const flp = nodep->fileline();
         const int slack = outerLen - innerLen;
         AstNodeExpr* innerOrp = nullptr;
diff --git a/test_regress/t/t_sequence_intersect_nevermatch.v b/test_regress/t/t_sequence_intersect_nevermatch.v
index 38abde53a..ea968d70c 100644
--- a/test_regress/t/t_sequence_intersect_nevermatch.v
+++ b/test_regress/t/t_sequence_intersect_nevermatch.v
@@ -22,6 +22,7 @@ module t (
 
   int f_fix = 0;
   int f_dis = 0;
+  int f_within = 0;
 
   always_ff @(posedge clk) begin
     cyc <= cyc + 1;
@@ -51,9 +52,15 @@ module t (
   assert property (disable iff (cyc < 2) ((a ##[1:2] b) intersect (c ##[4:5] d)) |-> 1'b0)
   else f_dis <= f_dis + 1;
 
+  // Inner length 3 cannot fit within outer length 1.
+  ap_within :
+  assert property (disable iff (cyc < 2) ((a ##3 b) within (c ##1 d)) |-> 1'b0)
+  else f_within <= f_within + 1;
+
   final begin
     // TODO need better non-zero test
     `checkd(f_fix, 0);
     `checkd(f_dis, 0);
+    `checkd(f_within, 0);
   end
 endmodule
diff --git a/test_regress/t/t_sequence_within_bad.out b/test_regress/t/t_sequence_within_bad.out
deleted file mode 100644
index 58a0e5525..000000000
--- a/test_regress/t/t_sequence_within_bad.out
+++ /dev/null
@@ -1,6 +0,0 @@
-%Error: t/t_sequence_within_bad.v:14:17: 'within' inner sequence 3 cycles exceeds outer sequence 1 cycles (IEEE 1800-2023 16.9.10)
-                                       : ... note: In instance 't'
-   14 |       (a ##3 b) within (c ##1 d));
-      |                 ^~~~~~
-        ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
-%Error: Exiting due to
diff --git a/test_regress/t/t_sequence_within_bad.py b/test_regress/t/t_sequence_within_bad.py
deleted file mode 100755
index 58fc7aeba..000000000
--- a/test_regress/t/t_sequence_within_bad.py
+++ /dev/null
@@ -1,18 +0,0 @@
-#!/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_all')
-
-test.compile(verilator_flags2=['--assert', '--timing', '--lint-only'],
-             fails=True,
-             expect_filename=test.golden_filename)
-
-test.passes()
diff --git a/test_regress/t/t_sequence_within_bad.v b/test_regress/t/t_sequence_within_bad.v
deleted file mode 100644
index 18b83c37b..000000000
--- a/test_regress/t/t_sequence_within_bad.v
+++ /dev/null
@@ -1,16 +0,0 @@
-// 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
-
-module t (input clk);
-  logic a, b, c, d;
-
-  // Inner length (3) exceeds outer length (1). IEEE 1800-2023 16.9.10
-  // requires the inner sequence to fit entirely within the outer match
-  // window, so this is a hard error.
-  assert property (@(posedge clk)
-      (a ##3 b) within (c ##1 d));
-
-endmodule