diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp
index a2fd9234c..bb388b846 100644
--- a/src/V3AssertNfa.cpp
+++ b/src/V3AssertNfa.cpp
@@ -528,6 +528,30 @@ class SvaNfaBuilder final {
         return {currentp, nullptr, {}};
     }
 
+    // always[lo:hi] / s_always[lo:hi] (IEEE 1800-2023 16.12.11).
+    BuildResult buildPropAlways(AstPropAlways* nodep, SvaStateVertex* entryVtxp,
+                                bool isTopLevelStep = false) {
+        FileLine* const flp = nodep->fileline();
+        AstNodeExpr* const propp = nodep->propp();
+        const int lo = getConstInt(nodep->loBoundp());
+        const int hi = getConstInt(nodep->hiBoundp());
+        UASSERT_OBJ(lo >= 0 && hi >= lo, nodep, "PropAlways bounds invariant (V3Width)");
+        SvaStateVertex* currentp = addDelayChain(entryVtxp, lo, flp);
+        for (int k = 0; k <= hi - lo; ++k) {
+            if (k > 0) {
+                SvaStateVertex* const nextp = scopedCreateVertex();
+                guardedEdge(currentp, nextp, flp);
+                currentp = nextp;
+            }
+            SvaStateVertex* const checkp = scopedCreateVertex();
+            SvaTransEdge* const linkp
+                = guardedLink(currentp, checkp, sampled(propp->cloneTreePure(false)), flp);
+            if (isTopLevelStep && !m_inUnboundedScope) linkp->m_rejectOnFail = true;
+            currentp = checkp;
+        }
+        return {currentp, nullptr, {}};
+    }
+
     BuildResult buildGotoRep(AstSGotoRep* repp, SvaStateVertex* entryVtxp) {
         FileLine* const flp = repp->fileline();
         AstNodeExpr* const exprp = repp->exprp();
@@ -734,6 +758,9 @@ public:
         if (AstSConsRep* const repp = VN_CAST(nodep, SConsRep)) {
             return buildConsRep(repp, entryVtxp, isTopLevelStep);
         }
+        if (AstPropAlways* const alwaysp = VN_CAST(nodep, PropAlways)) {
+            return buildPropAlways(alwaysp, entryVtxp, isTopLevelStep);
+        }
         if (AstSGotoRep* const repp = VN_CAST(nodep, SGotoRep)) {
             return buildGotoRep(repp, entryVtxp);
         }
diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h
index 2d156f3fb..56d302730 100644
--- a/src/V3AstNodeExpr.h
+++ b/src/V3AstNodeExpr.h
@@ -2027,6 +2027,32 @@ public:
     }
     string name() const override VL_MT_STABLE { return m_name; }
 };
+class AstPropAlways final : public AstNodeExpr {
+    // always[m:n] / s_always[m:n] (IEEE 1800-2023 16.12.11)
+    // @astgen op1 := propp : AstNodeExpr
+    // @astgen op2 := loBoundp : AstNodeExpr
+    // @astgen op3 := hiBoundp : AstNodeExpr
+    const bool m_isStrong = false;  // s_always
+public:
+    AstPropAlways(FileLine* fl, AstNodeExpr* propp, AstNodeExpr* loBoundp, AstNodeExpr* hiBoundp,
+                  bool isStrong)
+        : ASTGEN_SUPER_PropAlways(fl)
+        , m_isStrong{isStrong} {
+        this->propp(propp);
+        this->loBoundp(loBoundp);
+        this->hiBoundp(hiBoundp);
+    }
+    ASTGEN_MEMBERS_AstPropAlways;
+    void dump(std::ostream& str) const override;
+    void dumpJson(std::ostream& str) const override;
+    string emitVerilog() override { V3ERROR_NA_RETURN(""); }
+    string emitC() override { V3ERROR_NA_RETURN(""); }
+    string emitSimpleOperator() override { V3ERROR_NA_RETURN(""); }
+    bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
+    int instrCount() const override { V3ERROR_NA_RETURN(0); }
+    bool isStrong() const { return m_isStrong; }
+    bool isMultiCycleSva() const override { return true; }
+};
 class AstRand final : public AstNodeExpr {
     // $random/$random(seed) or $urandom/$urandom(seed)
     // Return a random number, based upon width()
diff --git a/src/V3AstNodes.cpp b/src/V3AstNodes.cpp
index 510703e4f..9745f65b8 100644
--- a/src/V3AstNodes.cpp
+++ b/src/V3AstNodes.cpp
@@ -456,6 +456,14 @@ void AstSConsRep::dumpJson(std::ostream& str) const {
     dumpJsonBoolFuncIf(str, unbounded);
     dumpJsonGen(str);
 }  // LCOV_EXCL_STOP
+void AstPropAlways::dump(std::ostream& str) const {
+    this->AstNodeExpr::dump(str);
+    if (isStrong()) str << " [strong]";
+}
+void AstPropAlways::dumpJson(std::ostream& str) const {
+    dumpJsonBoolFuncIf(str, isStrong);
+    dumpJsonGen(str);
+}
 void AstConsQueue::dump(std::ostream& str) const {
     this->AstNodeExpr::dump(str);
     if (lhsIsValue()) str << " [LVAL]";
diff --git a/src/V3EmitV.cpp b/src/V3EmitV.cpp
index ea82d070c..a53be9ecd 100644
--- a/src/V3EmitV.cpp
+++ b/src/V3EmitV.cpp
@@ -1058,6 +1058,18 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
         puts("\n");
     }
     void visit(AstPExpr* nodep) override { iterateConst(nodep->bodyp()); }
+    void visit(AstPropAlways* nodep) override {
+        puts(nodep->isStrong() ? "s_always" : "always");
+        if (!VN_IS(nodep->loBoundp(), Unbounded) || !VN_IS(nodep->hiBoundp(), Unbounded)) {
+            puts(" [");
+            iterateConst(nodep->loBoundp());
+            puts(":");
+            iterateConst(nodep->hiBoundp());
+            puts("]");
+        }
+        puts(" ");
+        iterateConst(nodep->propp());
+    }
     void visit(AstSExpr* nodep) override {
         iterateConstNull(nodep->preExprp());
         {
diff --git a/src/V3Width.cpp b/src/V3Width.cpp
index 34d60cf06..c0ce22de3 100644
--- a/src/V3Width.cpp
+++ b/src/V3Width.cpp
@@ -1545,6 +1545,65 @@ class WidthVisitor final : public VNVisitor {
             nodep->dtypeSetBit();
         }
     }
+    void visit(AstPropAlways* nodep) override {
+        // IEEE 1800-2023 16.12.11
+        assertAtExpr(nodep);
+        if (m_vup->prelim()) {
+            userIterateAndNext(nodep->propp(), WidthVP{SELF, BOTH}.p());
+            if (!VN_IS(nodep->loBoundp(), Unbounded)) {
+                userIterateAndNext(nodep->loBoundp(), WidthVP{SELF, BOTH}.p());
+                V3Const::constifyParamsEdit(nodep->loBoundp());
+            }
+            if (!VN_IS(nodep->hiBoundp(), Unbounded)) {
+                userIterateAndNext(nodep->hiBoundp(), WidthVP{SELF, BOTH}.p());
+                V3Const::constifyParamsEdit(nodep->hiBoundp());
+            }
+            const bool loUnbounded = VN_IS(nodep->loBoundp(), Unbounded);
+            const bool hiUnbounded = VN_IS(nodep->hiBoundp(), Unbounded);
+            if (loUnbounded || hiUnbounded) {
+                if (nodep->isStrong()) {
+                    nodep->v3error("s_always range must be bounded (IEEE 1800-2023 16.12.11)");
+                } else {
+                    nodep->v3warn(E_UNSUPPORTED,
+                                  "Unsupported: unbounded always range (always [m:$])");
+                }
+                nodep->dtypeSetBit();
+                return;
+            }
+            const AstConst* const loConstp = VN_CAST(nodep->loBoundp(), Const);
+            const AstConst* const hiConstp = VN_CAST(nodep->hiBoundp(), Const);
+            if (!loConstp) {
+                nodep->v3error("always range low bound must be a constant expression"
+                               " (IEEE 1800-2023 16.12.11)");
+            }
+            if (!hiConstp) {
+                nodep->v3error("always range high bound must be a constant expression"
+                               " (IEEE 1800-2023 16.12.11)");
+            }
+            if (loConstp && loConstp->toSInt() < 0) {
+                nodep->v3error("always range low bound must be non-negative"
+                               " (IEEE 1800-2023 16.12.11)");
+            }
+            if (loConstp && hiConstp && hiConstp->toSInt() < loConstp->toSInt()) {
+                nodep->v3error("always range high bound must be >= low bound"
+                               " (IEEE 1800-2023 16.12.11)");
+            }
+            bool hasPropertyOp = nodep->propp()->isMultiCycleSva();
+            if (!hasPropertyOp) {
+                nodep->propp()->foreach([&](const AstNode* np) {
+                    if (VN_IS(np, Implication) || VN_IS(np, Until) || VN_IS(np, PropSpec)) {
+                        hasPropertyOp = true;
+                    }
+                });
+            }
+            if (hasPropertyOp) {
+                nodep->v3warn(E_UNSUPPORTED,
+                              "Unsupported: property/sequence operator inside bounded"
+                              " always (IEEE 1800-2023 16.12.11)");
+            }
+            nodep->dtypeSetBit();
+        }
+    }
     void visit(AstRising* nodep) override {
         assertAtExpr(nodep);
         if (m_vup->prelim()) {
diff --git a/src/verilog.y b/src/verilog.y
index 93ccefa49..d1923d820 100644
--- a/src/verilog.y
+++ b/src/verilog.y
@@ -6753,11 +6753,13 @@ pexpr<nodeExprp>:  // IEEE: property_expr  (The name pexpr is important as regex
         |       yS_NEXTTIME '[' constExpr ']' pexpr %prec yS_NEXTTIME
                         { $$ = $5; BBUNSUP($1, "Unsupported: s_nexttime[] (in property expression)"); DEL($3); }
         |       yALWAYS pexpr
-                        { $$ = $2; BBUNSUP($1, "Unsupported: always (in property expression)"); }
-        |       yALWAYS anyrange pexpr  %prec yALWAYS
-                        { $$ = $3; BBUNSUP($1, "Unsupported: always[] (in property expression)"); DEL($2); }
-        |       yS_ALWAYS anyrange pexpr  %prec yS_ALWAYS
-                        { $$ = $3; BBUNSUP($1, "Unsupported: s_always (in property expression)"); DEL($2); }
+                        { $$ = $2; }
+        |       yALWAYS '[' constExpr ':' constExpr ']' pexpr  %prec yALWAYS
+                        { $$ = new AstPropAlways{$1, $7, $3, $5, false}; }
+        |       yS_ALWAYS '[' constExpr ':' constExpr ']' pexpr  %prec yS_ALWAYS
+                        { $$ = new AstPropAlways{$1, $7, $3, $5, true}; }
+        |       yS_ALWAYS pexpr
+                        { $$ = new AstPropAlways{$1, $2, new AstUnbounded{$1}, new AstUnbounded{$1}, true}; }
         |       yS_EVENTUALLY pexpr
                         { $$ = $2; BBUNSUP($1, "Unsupported: s_eventually (in property expression)"); }
         |       yS_EVENTUALLY anyrange pexpr  %prec yS_EVENTUALLY
diff --git a/test_regress/t/t_assert_always_unsup.out b/test_regress/t/t_assert_always_unsup.out
index 7bbe0404c..a339cc1fd 100644
--- a/test_regress/t/t_assert_always_unsup.out
+++ b/test_regress/t/t_assert_always_unsup.out
@@ -1,15 +1,9 @@
-%Error-UNSUPPORTED: t/t_assert_always_unsup.v:20:5: Unsupported: always[] (in property expression)
-   20 |     always [2:5] a;
-      |     ^~~~~~
-                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
-%Error-UNSUPPORTED: t/t_assert_always_unsup.v:24:5: Unsupported: s_always (in property expression)
-   24 |     s_always [2:5] a;
-      |     ^~~~~~~~
-%Error-UNSUPPORTED: t/t_assert_always_unsup.v:28:5: Unsupported: eventually[] (in property expression)
-   28 |     eventually [2:5] a;
+%Error-UNSUPPORTED: t/t_assert_always_unsup.v:20:5: Unsupported: eventually[] (in property expression)
+   20 |     eventually [2:5] a;
       |     ^~~~~~~~~~
-%Error: t/t_assert_always_unsup.v:32:18: syntax error, unexpected ']', expecting ':'
-   32 |     eventually [2] a;
+                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
+%Error: t/t_assert_always_unsup.v:24:18: syntax error, unexpected ']', expecting ':'
+   24 |     eventually [2] a;
       |                  ^
         ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
 %Error: Cannot continue
diff --git a/test_regress/t/t_assert_always_unsup.v b/test_regress/t/t_assert_always_unsup.v
index 332064fee..cc1382e24 100644
--- a/test_regress/t/t_assert_always_unsup.v
+++ b/test_regress/t/t_assert_always_unsup.v
@@ -16,14 +16,6 @@ module t (
     val = ~val;
   end
 
-  property p_alw;
-    always [2:5] a;
-  endproperty
-
-  property p_s_alw;
-    s_always [2:5] a;
-  endproperty
-
   property p_ev;
     eventually [2:5] a;
   endproperty
diff --git a/test_regress/t/t_debug_emitv.out b/test_regress/t/t_debug_emitv.out
index b7bea1967..005b185bc 100644
--- a/test_regress/t/t_debug_emitv.out
+++ b/test_regress/t/t_debug_emitv.out
@@ -650,6 +650,22 @@ module Vt_debug_emitv_t;
             $display("pass");
         end
     end
+    begin : assert_prop_always
+        assert property (@(posedge clk) always ['sh0:
+                         'sh3] in
+        ) begin
+        end
+        else begin
+        end
+    end
+    begin : assert_prop_s_always
+        assert property (@(posedge clk) s_always ['sh1:
+                         'sh2] in
+        ) begin
+        end
+        else begin
+        end
+    end
     int signed a;
     int signed ao;
     initial begin
diff --git a/test_regress/t/t_debug_emitv.v b/test_regress/t/t_debug_emitv.v
index 9594487f1..4f94bd864 100644
--- a/test_regress/t/t_debug_emitv.v
+++ b/test_regress/t/t_debug_emitv.v
@@ -330,6 +330,9 @@ module t (/*AUTOARG*/
   cover_concurrent: cover property(prop);
   cover_concurrent_stmt: cover property(prop) $display("pass");
 
+  assert_prop_always: assert property (@(posedge clk) always [0:3] in);
+  assert_prop_s_always: assert property (@(posedge clk) s_always [1:2] in);
+
 
   int a;
   int ao;
diff --git a/test_regress/t/t_prop_always.py b/test_regress/t/t_prop_always.py
new file mode 100755
index 000000000..2351d6963
--- /dev/null
+++ b/test_regress/t/t_prop_always.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()
+
+test.execute()
+
+test.passes()
diff --git a/test_regress/t/t_prop_always.v b/test_regress/t/t_prop_always.v
new file mode 100644
index 000000000..3f54b1023
--- /dev/null
+++ b/test_regress/t/t_prop_always.v
@@ -0,0 +1,107 @@
+// 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
+);
+
+  bit [63:0] crc = 64'h5aef0c8d_d70a4497;
+  int cyc = 0;
+  logic a_high = 1'b1;
+  logic a_low = 1'b0;
+  wire a_rand = crc[0];
+  wire rst_rand = crc[5];
+
+  // Per-assertion queues record the simulation cyc on each pass / else fire.
+  // For "always [m:n] P" the action runs at cyc=K+n on success and at the
+  // detected-violation cyc on failure -- both deterministic given the inputs.
+  int high_bounded_pass_q[$];
+  int high_sbounded_pass_q[$];
+  int high_degenerate_pass_q[$];
+  int low_bounded_fail_q[$];
+  int low_degenerate_fail_q[$];
+  int rand_bounded_pass_q[$];
+  int rand_bounded_fail_q[$];
+  int disable_bounded_pass_q[$];
+  int disable_bounded_fail_q[$];
+
+  // Bare always (collapses to immediate P).
+  assert property (@(posedge clk) always 1'b1);
+
+  // Bounded weak always over constant-true input.
+  assert property (@(posedge clk) always [0:3] a_high) high_bounded_pass_q.push_back(cyc);
+
+  // Bounded strong s_always over constant-true input.
+  assert property (@(posedge clk) s_always [1:2] a_high) high_sbounded_pass_q.push_back(cyc);
+
+  // Degenerate [0:0]: equivalent to immediate sample.
+  assert property (@(posedge clk) always [0:0] a_high) high_degenerate_pass_q.push_back(cyc);
+
+  // Constant-false: every attempt fails.
+  assert property (@(posedge clk) always [0:3] a_low)
+    ;
+  else low_bounded_fail_q.push_back(cyc);
+
+  assert property (@(posedge clk) always [0:0] a_low)
+    ;
+  else low_degenerate_fail_q.push_back(cyc);
+
+  // CRC-driven random input: window [cyc..cyc+3] of a_rand.
+  assert property (@(posedge clk) always [0:3] a_rand) rand_bounded_pass_q.push_back(cyc);
+  else rand_bounded_fail_q.push_back(cyc);
+
+  // disable iff suppresses attempts whose start cyc has rst_rand=1.
+  assert property (@(posedge clk) disable iff (rst_rand) always [0:3] a_rand)
+    disable_bounded_pass_q.push_back(cyc);
+  else disable_bounded_fail_q.push_back(cyc);
+
+  // Bare always inside named property.
+  property p_always_true;
+    @(posedge clk) always (1'b1);
+  endproperty
+  assert property (p_always_true);
+
+  // disable iff inside named property.
+  property p_disable_named;
+    @(posedge clk) disable iff (rst_rand) always [1:2] a_high;
+  endproperty
+  assert property (p_disable_named);
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
+    if (cyc == 19) begin
+      // Constant-true window [0:3]: K=0..16 succeed at cyc K+3 = 3..19.
+      `checkd(high_bounded_pass_q.size(), 17);
+      `checkd(high_bounded_pass_q[0], 3);
+      `checkd(high_bounded_pass_q[$], 19);
+      // Strong [1:2]: K=0..17 succeed at cyc K+2 = 2..19.
+      `checkd(high_sbounded_pass_q.size(), 18);
+      `checkd(high_sbounded_pass_q[0], 2);
+      `checkd(high_sbounded_pass_q[$], 19);
+      // Degenerate [0:0]: K=0..19 succeed at cyc K = 0..19.
+      `checkd(high_degenerate_pass_q.size(), 20);
+      `checkd(high_degenerate_pass_q[0], 0);
+      `checkd(high_degenerate_pass_q[$], 19);
+      // Constant-false: every attempt fails immediately.
+      `checkd(low_bounded_fail_q.size(), 20);
+      `checkd(low_degenerate_fail_q.size(), 20);
+      // CRC + disable streams: counts pinned (cross-checked against Questa).
+      `checkd(rand_bounded_pass_q.size(), 0);
+      `checkd(rand_bounded_fail_q.size(), 20);
+      `checkd(disable_bounded_pass_q.size(), 0);
+      `checkd(disable_bounded_fail_q.size(), 13);
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+
+endmodule
diff --git a/test_regress/t/t_prop_always_bad.out b/test_regress/t/t_prop_always_bad.out
new file mode 100644
index 000000000..4e06a8feb
--- /dev/null
+++ b/test_regress/t/t_prop_always_bad.out
@@ -0,0 +1,34 @@
+%Error: t/t_prop_always_bad.v:13:20: always range low bound must be non-negative (IEEE 1800-2023 16.12.11)
+                                   : ... note: In instance 't'
+   13 |   assert property (always [-1:3] a);
+      |                    ^~~~~~
+        ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
+%Error: t/t_prop_always_bad.v:14:20: always range high bound must be >= low bound (IEEE 1800-2023 16.12.11)
+                                   : ... note: In instance 't'
+   14 |   assert property (always [5:2] a);
+      |                    ^~~~~~
+%Error: t/t_prop_always_bad.v:15:28: Expecting expression to be constant, but variable isn't const: 'x'
+                                   : ... note: In instance 't'
+   15 |   assert property (always [x:3] a);
+      |                            ^
+%Error: t/t_prop_always_bad.v:15:20: always range low bound must be a constant expression (IEEE 1800-2023 16.12.11)
+                                   : ... note: In instance 't'
+   15 |   assert property (always [x:3] a);
+      |                    ^~~~~~
+%Error: t/t_prop_always_bad.v:16:30: Expecting expression to be constant, but variable isn't const: 'x'
+                                   : ... note: In instance 't'
+   16 |   assert property (always [1:x] a);
+      |                              ^
+%Error: t/t_prop_always_bad.v:16:20: always range high bound must be a constant expression (IEEE 1800-2023 16.12.11)
+                                   : ... note: In instance 't'
+   16 |   assert property (always [1:x] a);
+      |                    ^~~~~~
+%Error: t/t_prop_always_bad.v:17:20: s_always range must be bounded (IEEE 1800-2023 16.12.11)
+                                   : ... note: In instance 't'
+   17 |   assert property (s_always a);
+      |                    ^~~~~~~~
+%Error: t/t_prop_always_bad.v:18:20: s_always range must be bounded (IEEE 1800-2023 16.12.11)
+                                   : ... note: In instance 't'
+   18 |   assert property (s_always [1:$] a);
+      |                    ^~~~~~~~
+%Error: Exiting due to
diff --git a/test_regress/t/t_prop_always_bad.py b/test_regress/t/t_prop_always_bad.py
new file mode 100755
index 000000000..77a0ac64b
--- /dev/null
+++ b/test_regress/t/t_prop_always_bad.py
@@ -0,0 +1,16 @@
+#!/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, fails=True)
+
+test.passes()
diff --git a/test_regress/t/t_prop_always_bad.v b/test_regress/t/t_prop_always_bad.v
new file mode 100644
index 000000000..8fa30b3eb
--- /dev/null
+++ b/test_regress/t/t_prop_always_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 PlanV GmbH
+// SPDX-License-Identifier: CC0-1.0
+
+module t (input clk);
+  int x;
+  logic a;
+
+  default clocking cb @(posedge clk); endclocking
+
+  assert property (always [-1:3] a);
+  assert property (always [5:2] a);
+  assert property (always [x:3] a);
+  assert property (always [1:x] a);
+  assert property (s_always a);
+  assert property (s_always [1:$] a);
+
+endmodule
diff --git a/test_regress/t/t_prop_always_unsup.out b/test_regress/t/t_prop_always_unsup.out
new file mode 100644
index 000000000..52bd14918
--- /dev/null
+++ b/test_regress/t/t_prop_always_unsup.out
@@ -0,0 +1,18 @@
+%Error-UNSUPPORTED: t/t_prop_always_unsup.v:12:35: Unsupported: unbounded always range (always [m:$])
+                                                 : ... note: In instance 't'
+   12 |   assert property (@(posedge clk) always [2:$] a);
+      |                                   ^~~~~~
+                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
+%Error-UNSUPPORTED: t/t_prop_always_unsup.v:15:35: Unsupported: property/sequence operator inside bounded always (IEEE 1800-2023 16.12.11)
+                                                 : ... note: In instance 't'
+   15 |   assert property (@(posedge clk) always [0:3] (a |-> b));
+      |                                   ^~~~~~
+%Error-UNSUPPORTED: t/t_prop_always_unsup.v:16:35: Unsupported: property/sequence operator inside bounded always (IEEE 1800-2023 16.12.11)
+                                                 : ... note: In instance 't'
+   16 |   assert property (@(posedge clk) always [0:3] (a |=> b));
+      |                                   ^~~~~~
+%Error-UNSUPPORTED: t/t_prop_always_unsup.v:17:35: Unsupported: property/sequence operator inside bounded always (IEEE 1800-2023 16.12.11)
+                                                 : ... note: In instance 't'
+   17 |   assert property (@(posedge clk) always [0:3] (a ##1 b));
+      |                                   ^~~~~~
+%Error: Exiting due to
diff --git a/test_regress/t/t_prop_always_unsup.py b/test_regress/t/t_prop_always_unsup.py
new file mode 100755
index 000000000..77a0ac64b
--- /dev/null
+++ b/test_regress/t/t_prop_always_unsup.py
@@ -0,0 +1,16 @@
+#!/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, fails=True)
+
+test.passes()
diff --git a/test_regress/t/t_prop_always_unsup.v b/test_regress/t/t_prop_always_unsup.v
new file mode 100644
index 000000000..7013c9fff
--- /dev/null
+++ b/test_regress/t/t_prop_always_unsup.v
@@ -0,0 +1,19 @@
+// 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;
+  logic b;
+
+  // IEEE-legal but engine has no sim-end liveness.
+  assert property (@(posedge clk) always [2:$] a);
+
+  // Nested sequence/property operators inside bounded always.
+  assert property (@(posedge clk) always [0:3] (a |-> b));
+  assert property (@(posedge clk) always [0:3] (a |=> b));
+  assert property (@(posedge clk) always [0:3] (a ##1 b));
+
+endmodule
diff --git a/test_regress/t/t_property_pexpr_unsup.out b/test_regress/t/t_property_pexpr_unsup.out
index 0a93880ae..a021411dc 100644
--- a/test_regress/t/t_property_pexpr_unsup.out
+++ b/test_regress/t/t_property_pexpr_unsup.out
@@ -23,21 +23,12 @@
 %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:63:5: Unsupported: s_nexttime[] (in property expression)
    63 |     s_nexttime [2] a;
       |     ^~~~~~~~~~
-%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:67:14: Unsupported: always (in property expression)
-   67 |     nexttime always a;
-      |              ^~~~~~
 %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:67:5: Unsupported: nexttime (in property expression)
    67 |     nexttime always a;
       |     ^~~~~~~~
-%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:71:18: Unsupported: always (in property expression)
-   71 |     nexttime [2] always a;
-      |                  ^~~~~~
 %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:71:5: Unsupported: nexttime[] (in property expression)
    71 |     nexttime [2] always a;
       |     ^~~~~~~~
-%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:75:18: Unsupported: always (in property expression)
-   75 |     nexttime [2] always a;
-      |                  ^~~~~~
 %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:75:5: Unsupported: nexttime[] (in property expression)
    75 |     nexttime [2] always a;
       |     ^~~~~~~~
@@ -47,9 +38,6 @@
 %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:79:5: Unsupported: nexttime (in property expression)
    79 |     nexttime s_eventually a;
       |     ^~~~~~~~
-%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:83:33: Unsupported: always (in property expression)
-   83 |     nexttime s_eventually [2:$] always a;
-      |                                 ^~~~~~
 %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:83:14: Unsupported: s_eventually[] (in property expression)
    83 |     nexttime s_eventually [2:$] always a;
       |              ^~~~~~~~~~~~
diff --git a/test_regress/t/t_property_unsup.out b/test_regress/t/t_property_unsup.out
index ec5a79c63..d6dda24c3 100644
--- a/test_regress/t/t_property_unsup.out
+++ b/test_regress/t/t_property_unsup.out
@@ -5,58 +5,40 @@
 %Error-UNSUPPORTED: t/t_property_unsup.v:80:20: Unsupported: eventually[] (in property expression)
    80 |   assert property (eventually[0: 2] counter == 3);
       |                    ^~~~~~~~~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:90:21: Unsupported: always (in property expression)
-   90 |   assert property ((always a) implies (always a));
-      |                     ^~~~~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:90:40: Unsupported: always (in property expression)
-   90 |   assert property ((always a) implies (always a));
-      |                                        ^~~~~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:92:26: Unsupported: always (in property expression)
-   92 |   assert property ((a or(always b)) implies (a or(always b)));
-      |                          ^~~~~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:92:51: Unsupported: always (in property expression)
-   92 |   assert property ((a or(always b)) implies (a or(always b)));
-      |                                                   ^~~~~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:94:21: Unsupported: eventually[] (in property expression)
-   94 |   assert property ((eventually[0: 1] a) implies (eventually[0: 1] a));
+%Error-UNSUPPORTED: t/t_property_unsup.v:90:21: Unsupported: eventually[] (in property expression)
+   90 |   assert property ((eventually[0: 1] a) implies (eventually[0: 1] a));
       |                     ^~~~~~~~~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:94:50: Unsupported: eventually[] (in property expression)
-   94 |   assert property ((eventually[0: 1] a) implies (eventually[0: 1] a));
+%Error-UNSUPPORTED: t/t_property_unsup.v:90:50: Unsupported: eventually[] (in property expression)
+   90 |   assert property ((eventually[0: 1] a) implies (eventually[0: 1] a));
       |                                                  ^~~~~~~~~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:96:21: Unsupported: s_eventually (in property expression)
-   96 |   assert property ((s_eventually a) implies (s_eventually a));
+%Error-UNSUPPORTED: t/t_property_unsup.v:92:21: Unsupported: s_eventually (in property expression)
+   92 |   assert property ((s_eventually a) implies (s_eventually a));
       |                     ^~~~~~~~~~~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:96:46: Unsupported: s_eventually (in property expression)
-   96 |   assert property ((s_eventually a) implies (s_eventually a));
+%Error-UNSUPPORTED: t/t_property_unsup.v:92:46: Unsupported: s_eventually (in property expression)
+   92 |   assert property ((s_eventually a) implies (s_eventually a));
       |                                              ^~~~~~~~~~~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:106:23: Unsupported: #-# (in property expression)
-  106 |   assert property ((a #-# b) implies (a #-# b));
+%Error-UNSUPPORTED: t/t_property_unsup.v:102:23: Unsupported: #-# (in property expression)
+  102 |   assert property ((a #-# b) implies (a #-# b));
       |                       ^~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:106:41: Unsupported: #-# (in property expression)
-  106 |   assert property ((a #-# b) implies (a #-# b));
+%Error-UNSUPPORTED: t/t_property_unsup.v:102:41: Unsupported: #-# (in property expression)
+  102 |   assert property ((a #-# b) implies (a #-# b));
       |                                         ^~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:116:21: Unsupported: always (in property expression)
-  116 |   assert property ((always a) iff (always a));
-      |                     ^~~~~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:116:36: Unsupported: always (in property expression)
-  116 |   assert property ((always a) iff (always a));
-      |                                    ^~~~~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:118:21: Unsupported: eventually[] (in property expression)
-  118 |   assert property ((eventually[0: 1] a) iff (eventually[0: 1] a));
+%Error-UNSUPPORTED: t/t_property_unsup.v:112:21: Unsupported: eventually[] (in property expression)
+  112 |   assert property ((eventually[0: 1] a) iff (eventually[0: 1] a));
       |                     ^~~~~~~~~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:118:46: Unsupported: eventually[] (in property expression)
-  118 |   assert property ((eventually[0: 1] a) iff (eventually[0: 1] a));
+%Error-UNSUPPORTED: t/t_property_unsup.v:112:46: Unsupported: eventually[] (in property expression)
+  112 |   assert property ((eventually[0: 1] a) iff (eventually[0: 1] a));
       |                                              ^~~~~~~~~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:120:21: Unsupported: s_eventually (in property expression)
-  120 |   assert property ((s_eventually a) iff (s_eventually a));
+%Error-UNSUPPORTED: t/t_property_unsup.v:114:21: Unsupported: s_eventually (in property expression)
+  114 |   assert property ((s_eventually a) iff (s_eventually a));
       |                     ^~~~~~~~~~~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:120:42: Unsupported: s_eventually (in property expression)
-  120 |   assert property ((s_eventually a) iff (s_eventually a));
+%Error-UNSUPPORTED: t/t_property_unsup.v:114:42: Unsupported: s_eventually (in property expression)
+  114 |   assert property ((s_eventually a) iff (s_eventually a));
       |                                          ^~~~~~~~~~~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:130:23: Unsupported: #-# (in property expression)
-  130 |   assert property ((a #-# b) iff (a #-# b));
+%Error-UNSUPPORTED: t/t_property_unsup.v:124:23: Unsupported: #-# (in property expression)
+  124 |   assert property ((a #-# b) iff (a #-# b));
       |                       ^~~
-%Error-UNSUPPORTED: t/t_property_unsup.v:130:37: Unsupported: #-# (in property expression)
-  130 |   assert property ((a #-# b) iff (a #-# b));
+%Error-UNSUPPORTED: t/t_property_unsup.v:124:37: Unsupported: #-# (in property expression)
+  124 |   assert property ((a #-# b) iff (a #-# b));
       |                                     ^~~
 %Error: Exiting due to
diff --git a/test_regress/t/t_property_unsup.v b/test_regress/t/t_property_unsup.v
index e496b28c9..e57ee2485 100644
--- a/test_regress/t/t_property_unsup.v
+++ b/test_regress/t/t_property_unsup.v
@@ -86,10 +86,6 @@ module sva_implies2 (
     b
 );
 
-  p0 :
-  assert property ((always a) implies (always a));
-  p1 :
-  assert property ((a or(always b)) implies (a or(always b)));
   p2 :
   assert property ((eventually[0: 1] a) implies (eventually[0: 1] a));
   p3 :
@@ -112,8 +108,6 @@ module sva_iff2 (
     b
 );
 
-  p0 :
-  assert property ((always a) iff (always a));
   p1 :
   assert property ((eventually[0: 1] a) iff (eventually[0: 1] a));
   p2 :