Support `s_until` and `s_until_with` (IEEE1800-2023 16.12.12)

Signed-off-by: Artur Bieniek <abieniek@antmicro.com>

src/V3Assert.cpp

@@ -253,8 +253,7 @@ class AssertVisitor final : public VNVisitor {
         }
     }
     AstSampled* newSampledExpr(AstNodeExpr* nodep) {
-        AstSampled* const sampledp = new AstSampled{nodep->fileline(), nodep};
+        AstSampled* const sampledp = new AstSampled{nodep->fileline(), nodep, nodep->dtypep()};
-        sampledp->dtypeFrom(nodep);
         return sampledp;
     }
     AstVarRef* newMonitorNumVarRefp(const AstNode* nodep, VAccess access) {

src/V3AssertNfa.cpp

@@ -182,8 +182,7 @@ struct BuildResult final {
 };
 
 static AstNodeExpr* sampled(AstNodeExpr* exprp) {
-    AstSampled* const sp = new AstSampled{exprp->fileline(), exprp};
+    AstSampled* const sp = new AstSampled{exprp->fileline(), exprp, exprp->dtypep()};
-    sp->dtypeFrom(exprp);
     return sp;
 }
 
@@ -838,13 +837,14 @@ class SvaNfaBuilder final {
     BuildResult buildUntil(AstUntil* nodep, SvaStateVertex* entryVtxp, bool isTopLevelStep) {
         FileLine* const flp = nodep->fileline();
         if (!isTopLevelStep) {
-            nodep->v3warn(E_UNSUPPORTED, "Unsupported: 'until' in complex property expression");
+            nodep->v3warn(E_UNSUPPORTED, "Unsupported: '" << nodep->verilogKwd()
+                                                          << "' in complex property expression");
             return BuildResult::failWithError();
         }
         if (nodep->isStrong()) {
             nodep->v3warn(E_UNSUPPORTED, "Unsupported: s_until"
                                              << (nodep->isOverlapping() ? "_with" : "")
-                                             << " (in property expresion)");
+                                             << " (in property expression)");
             return BuildResult::failWithError();
         }
         AstNodeExpr* const lhsp = nodep->lhsp();
@@ -853,7 +853,8 @@ class SvaNfaBuilder final {
             return ep->exists([](const AstNodeExpr* np) { return np->isMultiCycleSva(); });
         };
         if (hasSeq(lhsp) || hasSeq(rhsp)) {
-            nodep->v3warn(E_UNSUPPORTED, "Unsupported: 'until' in complex property expression");
+            nodep->v3warn(E_UNSUPPORTED, "Unsupported: '" << nodep->verilogKwd()
+                                                          << "' in complex property expression");
             return BuildResult::failWithError();
         }
 
@@ -1926,16 +1927,16 @@ class AssertNfaVisitor final : public VNVisitor {
 
     // Bare `assert property (p until q)` with boolean operands stays on
     // V3AssertPre's AstLoop lowering, which preserves per-attempt action-block
-    // firings that this NFA's single-bit aggregated state cannot. NFA still
+    // firings that this NFA's single-bit aggregated state cannot. Strong bare
-    // owns strong forms, sequence operands, and any embedding inside a
+    // forms are also lowered there. NFA still owns sequence operands and any
-    // multi-cycle context (implication consequent, or/and operands, etc.).
+    // embedding inside a multi-cycle context (implication consequent, or/and
+    // operands, etc.).
     static bool isBareTopLevelUntil(AstNode* propp) {
         AstNode* p = propp;
         if (AstPropSpec* const specp = VN_CAST(p, PropSpec)) p = specp->propp();
         while (AstLogNot* const notp = VN_CAST(p, LogNot)) p = notp->lhsp();
         AstUntil* const untilp = VN_CAST(p, Until);
         if (!untilp) return false;
-        if (untilp->isStrong()) return false;
         const auto hasSeq = [](const AstNodeExpr* ep) {
             return ep->exists([](const AstNodeExpr* np) { return np->isMultiCycleSva(); });
         };

src/V3AssertPre.cpp

@@ -366,8 +366,8 @@ private:
             if (skewp->num().is1Step()) {
                 // #1step means the value that is sampled is always the signal's last value
                 // before the clock edge (IEEE 1800-2023 14.4)
-                AstSampled* const sampledp = new AstSampled{flp, exprp->cloneTreePure(false)};
+                AstSampled* const sampledp
-                sampledp->dtypeFrom(exprp);
+                    = new AstSampled{flp, exprp->cloneTreePure(false), exprp->dtypep()};
                 AstAssign* const assignp = new AstAssign{flp, refp, sampledp};
                 m_clockingp->addNextHere(new AstAlways{
                     flp, VAlwaysKwd::ALWAYS,
@@ -413,7 +413,7 @@ private:
         }
     }
     void visit(AstDelay* nodep) override {
-        m_hasCycleDelay = true;
+        m_hasCycleDelay |= nodep->isCycleDelay();
         // Only cycle delays are relevant in this stage; also only process once
         if (!nodep->isCycleDelay()) {
             if (m_inSynchDrive) {
@@ -846,7 +846,7 @@ private:
 
         // Assertion condition check
         AstLoop* const loopp = new AstLoop{flp};
-        AstNodeExpr* const condp = new AstSampled{flp, nodep->exprp()->unlinkFrBack()};
+        AstNodeExpr* const condp = new AstSampled{flp, nodep->exprp()->unlinkFrBack(), nullptr};
         loopp->addStmtsp(new AstLoopTest{flp, loopp, new AstLogNot{flp, condp}});
         loopp->addStmtsp(new AstEventControl{flp, sentreep, nullptr});
 
@@ -1300,17 +1300,121 @@ private:
     }
     void visit(AstUntil* nodep) override {
         FileLine* const flp = nodep->fileline();
-        if (m_pexprp) {
+        UASSERT_OBJ(
-            nodep->v3warn(E_UNSUPPORTED, "Unsupported: 'until' in complex property expression");
+            !m_pexprp, nodep,
-            nodep->replaceWith(new AstConst{flp, AstConst::BitFalse{}});
+            "'" << nodep->verilogKwd()
-            VL_DO_DANGLING(pushDeletep(nodep), nodep);
+                << "' in complex property expression should have been rejected by V3AssertNfa");
-            return;
-        }
         if (nodep->isStrong()) {
-            nodep->v3warn(E_UNSUPPORTED, "Unsupported: s_until"
+            // p s_until q / p s_until_with q: q must eventually be true. Until then, p must
-                                             << (nodep->isOverlapping() ? "_with" : "")
+            // be true on every sampled tick. For s_until, check q first: when q is true on
-                                             << " (in property expresion)");
+            // this tick, p is not required. For s_until_with, p must be true on the q tick too.
-            nodep->replaceWith(new AstConst{flp, AstConst::BitFalse{}});
+            AstNodeExpr* const rawLhsp = nodep->lhsp()->unlinkFrBack();
+            AstNodeExpr* const rawRhsp = nodep->rhsp()->unlinkFrBack();
+            AstSampled* const lhsp = new AstSampled{flp, rawLhsp, rawLhsp->dtypep()};
+            AstSampled* const rhsp = new AstSampled{flp, rawRhsp, rawRhsp->dtypep()};
+            AstNodeExpr* finalCondp = rhsp->cloneTreePure(false);
+            if (nodep->isOverlapping()) {
+                finalCondp = new AstLogAnd{flp, lhsp->cloneTreePure(false), finalCondp};
+            }
+
+            // Track active assertion attempts. Only the count is needed to emit final failures.
+            AstVar* const activep = new AstVar{flp, VVarType::MODULETEMP, m_activeNames.get(""),
+                                               nodep->findBasicDType(VBasicDTypeKwd::UINT32)};
+            activep->lifetime(VLifetime::STATIC_EXPLICIT);
+            m_modp->addStmtsp(activep);
+
+            AstVar* const donep
+                = new AstVar{flp, VVarType::BLOCKTEMP, "__VassertDone", nodep->findBitDType()};
+            donep->lifetime(VLifetime::AUTOMATIC_EXPLICIT);
+            auto setDone = [&]() {
+                return new AstAssign{flp, new AstVarRef{flp, donep, VAccess::WRITE},
+                                     new AstConst{flp, AstConst::BitTrue{}}};
+            };
+
+            AstLoop* const loopp = new AstLoop{flp};
+            AstAssign* const decrementVar = new AstAssign{
+                flp, new AstVarRef{flp, activep, VAccess::WRITE},
+                new AstSub{flp, new AstVarRef{flp, activep, VAccess::READ}, new AstConst{flp, 1}}};
+            loopp->addStmtsp(new AstLoopTest{
+                flp, loopp, new AstLogNot{flp, new AstVarRef{flp, donep, VAccess::READ}}});
+            {
+                AstBegin* const passp = new AstBegin{flp, "", nullptr, true};
+                passp->addStmtsp(new AstPExprClause{flp});
+                passp->addStmtsp(decrementVar);
+                passp->addStmtsp(setDone());
+                AstNodeExpr* passCondp = rhsp;
+                if (nodep->isOverlapping()) {
+                    passCondp = new AstLogAnd{flp, lhsp->cloneTreePure(false), passCondp};
+                }
+                loopp->addStmtsp(new AstIf{flp, passCondp, passp});
+            }
+            {
+                AstBegin* const failp = new AstBegin{flp, "", nullptr, true};
+                failp->addStmtsp(new AstPExprClause{flp, false});
+                failp->addStmtsp(decrementVar->cloneTree(false));
+                failp->addStmtsp(setDone());
+                loopp->addStmtsp(new AstIf{
+                    flp,
+                    new AstLogAnd{flp,
+                                  new AstLogNot{flp, new AstVarRef{flp, donep, VAccess::READ}},
+                                  new AstLogNot{flp, lhsp}},
+                    failp});
+            }
+            AstDelay* const delayp = new AstDelay{flp, new AstConst{flp, 1}, false};
+            delayp->timeunit(m_modp->timeunit());
+            loopp->addStmtsp(new AstIf{
+                flp, new AstLogNot{flp, new AstVarRef{flp, donep, VAccess::READ}}, delayp});
+
+            // Main assertion block
+            AstBegin* const bodyp = new AstBegin{flp, "", nullptr, true};
+            bodyp->addStmtsp(donep);
+            bodyp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, donep, VAccess::WRITE},
+                                           new AstConst{flp, AstConst::BitFalse{}}});
+            FileLine* const flp = activep->fileline();
+            bodyp->addStmtsp(
+                new AstAssign{flp, new AstVarRef{flp, activep, VAccess::WRITE},
+                              new AstAdd{flp, new AstVarRef{flp, activep, VAccess::READ},
+                                         new AstConst{flp, 1}}});
+            bodyp->addStmtsp(loopp);
+
+            // Validate assertion condition for each active assert
+            AstVar* const activeCountp = new AstVar{flp, VVarType::BLOCKTEMP, "__VassertCount",
+                                                    nodep->findBasicDType(VBasicDTypeKwd::UINT32)};
+            activeCountp->lifetime(VLifetime::AUTOMATIC_EXPLICIT);
+
+            AstAssign* const initActiveCountp
+                = new AstAssign{flp, new AstVarRef{flp, activeCountp, VAccess::WRITE},
+                                new AstVarRef{flp, activep, VAccess::READ}};
+            AstLoop* const finalLoopp = new AstLoop{flp};
+            finalLoopp->addStmtsp(
+                new AstLoopTest{flp, finalLoopp,
+                                new AstNeq{flp, new AstVarRef{flp, activeCountp, VAccess::READ},
+                                           new AstConst{flp, 0}}});
+            finalLoopp->addStmtsp(new AstIf{flp, finalCondp, new AstPExprClause{flp},
+                                            new AstPExprClause{flp, false}});
+            finalLoopp->addStmtsp(
+                new AstAssign{flp, new AstVarRef{flp, activeCountp, VAccess::WRITE},
+                              new AstSub{flp, new AstVarRef{flp, activeCountp, VAccess::READ},
+                                         new AstConst{flp, 1}}});
+
+            // Final assertion block
+            AstBegin* const finalp = new AstBegin{flp, "", nullptr, true};
+            finalp->addStmtsp(activeCountp);
+            finalp->addStmtsp(initActiveCountp);
+            finalp->addStmtsp(finalLoopp);
+
+            AstPExpr* const pexprp = new AstPExpr{flp, bodyp, finalp, nodep->dtypep()};
+            VL_RESTORER(m_pexprp);
+            VL_RESTORER(m_hasCycleDelay);
+            m_pexprp = pexprp;
+            m_hasCycleDelay = false;
+            iterate(bodyp);
+            iterate(finalp);
+
+            UASSERT_OBJ(!m_hasCycleDelay, nodep,
+                        "s_until cycle delay should have been handled by V3AssertNfa");
+
+            nodep->replaceWith(pexprp);
             VL_DO_DANGLING(pushDeletep(nodep), nodep);
             return;
         }
@@ -1369,8 +1473,8 @@ private:
         iterateNull(nodep->disablep());
         if (!VN_AS(nodep->backp(), NodeCoverOrAssert)->immediate()) {
             const AstNodeDType* const propDtp = nodep->propp()->dtypep();
-            nodep->propp(new AstSampled{nodep->fileline(), nodep->propp()->unlinkFrBack()});
+            nodep->propp(new AstSampled{nodep->fileline(), nodep->propp()->unlinkFrBack(),
-            nodep->propp()->dtypeFrom(propDtp);
+                                        propDtp->dtypep()});
         }
         iterate(nodep->propp());
     }

src/V3AstNodeExpr.h

@@ -2519,9 +2519,10 @@ class AstSampled final : public AstNodeExpr {
     // Verilog $sampled
     // @astgen op1 := exprp : AstNode<AstNodeExpr|AstPropSpec>
 public:
-    AstSampled(FileLine* fl, AstNode* exprp)
+    AstSampled(FileLine* fl, AstNode* exprp, AstNodeDType* dtypep)
         : ASTGEN_SUPER_Sampled(fl) {
         this->exprp(exprp);
+        this->dtypep(dtypep);
     }
     ASTGEN_MEMBERS_AstSampled;
     string emitVerilog() override { return "$sampled(%l)"; }
@@ -2906,6 +2907,9 @@ public:
     string emitVerilog() override { V3ERROR_NA_RETURN(""); }
     string emitC() override { V3ERROR_NA_RETURN(""); }
     string emitSimpleOperator() override { V3ERROR_NA_RETURN(""); }
+    string verilogKwd() const override {
+        return (isStrong() ? "s_" : string()) + "until" + (isOverlapping() ? "_with" : "");
+    }
     bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
     int instrCount() const override { return widthInstrs(); }
     bool sameNode(const AstNode* /*samep*/) const override { return true; }

src/V3Slice.cpp

@@ -210,7 +210,7 @@ class SliceVisitor final : public VNVisitor {
             UINFO(9, "  cloneSliceSel(" << elements << "," << elemIdx << ") " << nodep);
             AstNodeExpr* const exprp = VN_AS(snodep->exprp(), NodeExpr);
             AstNodeExpr* const selp = cloneAndSel(exprp, elements, elemIdx, needPure);
-            return new AstSampled{nodep->fileline(), selp};
+            return new AstSampled{nodep->fileline(), selp, nullptr};
         } else if (AstExprStmt* const snodep = VN_CAST(nodep, ExprStmt)) {
             UINFO(9, "  cloneExprStmt(" << elements << "," << elemIdx << ") " << nodep);
             AstNodeExpr* const resultSelp

src/V3Width.cpp

@@ -1714,6 +1714,13 @@ class WidthVisitor final : public VNVisitor {
     }
 
     void visit(AstUntil* nodep) override {
+        if (nodep->isStrong()
+            && (v3Global.opt.timing().isSetFalse() || !v3Global.opt.timing().isSetTrue())) {
+            nodep->v3warn(E_NOTIMING, nodep->verilogKwd() << " requires --timing");
+            nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}});
+            VL_DO_DANGLING(nodep->deleteTree(), nodep);
+            return;
+        }
         assertAtExpr(nodep);
         if (m_vup->prelim()) {
             iterateCheckBool(nodep, "LHS", nodep->lhsp(), BOTH);

src/verilog.y

@@ -4531,7 +4531,7 @@ system_f_or_t_expr_call<nodeExprp>:  // IEEE: part of system_tf_call (can be tas
         |       yD_ROSE '(' expr ',' expr ')'           { $$ = new AstRose{$1, $3, GRAMMARP->createSenTreeChanged($1, $5)}; }
         |       yD_ROSE_GCLK '(' expr ')'               { $$ = new AstRose{$1, $3, GRAMMARP->createGlobalClockSenTree($1)}; }
         |       yD_RTOI '(' expr ')'                    { $$ = new AstRToIS{$1, $3}; }
-        |       yD_SAMPLED '(' expr ')'                 { $$ = new AstSampled{$1, $3}; }
+        |       yD_SAMPLED '(' expr ')'                 { $$ = new AstSampled{$1, $3, $3->dtypep()}; }
         |       yD_SFORMATF '(' exprDispList ')'        { $$ = new AstSFormatF{$1, AstSFormatF::ExprFormat{}, $3, 'd', false}; }
         |       yD_SHORTREALTOBITS '(' expr ')'         { $$ = new AstRealToBits{$1, $3}; UNSUPREAL($1); }
         |       yD_SIGNED '(' expr ')'                  { $$ = new AstSigned{$1, $3}; }

test_regress/t/t_notiming.out

@@ -51,4 +51,12 @@
                                      : ... note: In instance 't'
    38 |    assert property (@(e) s_eventually 1'h1);
       |                          ^~~~~~~~~~~~
+%Error-NOTIMING: t/t_notiming.v:39:31: s_until requires --timing
+                                     : ... note: In instance 't'
+   39 |    assert property (@(e) 1'h1 s_until 1'h1);
+      |                               ^~~~~~~
+%Error-NOTIMING: t/t_notiming.v:40:31: s_until_with requires --timing
+                                     : ... note: In instance 't'
+   40 |    assert property (@(e) 1'h1 s_until_with 1'h1);
+      |                               ^~~~~~~~~~~~
 %Error: Exiting due to

test_regress/t/t_notiming.v

@@ -36,6 +36,8 @@ module t;
        s.get();
    end
    assert property (@(e) s_eventually 1'h1);
+   assert property (@(e) 1'h1 s_until 1'h1);
+   assert property (@(e) 1'h1 s_until_with 1'h1);
 endmodule
 
 `ifdef VERILATOR_TIMING

test_regress/t/t_property_sexpr_parse_unsup.out

@@ -1,16 +1,16 @@
-%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:72:14: Logical operator IMPLICATION expects 1 bit on the RHS, but RHS's CMETHODHARD 'at' generates 8 bits.
+%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:80:14: Logical operator IMPLICATION expects 1 bit on the RHS, but RHS's CMETHODHARD 'at' generates 8 bits.
                                                      : ... note: In instance 't.ieee'
-   72 |     $rose(a) |-> q[0];
+   80 |     $rose(a) |-> q[0];
       |              ^~~
                      ... For warning description see https://verilator.org/warn/WIDTHTRUNC?v=latest
                      ... Use "/* verilator lint_off WIDTHTRUNC */" and lint_on around source to disable this message.
-%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:77:29: Logical operator SEXPR expects 1 bit on the exprp, but exprp's CMETHODHARD 'at' generates 8 bits.
+%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:85:29: Logical operator SEXPR expects 1 bit on the exprp, but exprp's CMETHODHARD 'at' generates 8 bits.
                                                      : ... note: In instance 't.ieee'
-   77 |     ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
+   85 |     ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
       |                             ^~
-%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:98:31: Logical operator SEXPR expects 1 bit on the exprp, but exprp's VARREF 'b' generates 32 bits.
+%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:106:31: Logical operator SEXPR expects 1 bit on the exprp, but exprp's VARREF 'b' generates 32 bits.
-                                                     : ... note: In instance 't.ieee'
+                                                      : ... note: In instance 't.ieee'
-   98 |   assert property (@clk not a ##1 b);
+  106 |   assert property (@clk not a ##1 b);
       |                               ^~
 %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:47:39: Unsupported: 'until' in complex property expression
                                                     : ... note: In instance 't'
@@ -21,16 +21,32 @@
                                                     : ... note: In instance 't'
    49 |   assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, 49);
       |                                       ^~~~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:51:39: Unsupported: s_until (in property expresion)
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:51:44: Unsupported: s_until (in property expression)
                                                     : ... note: In instance 't'
-   51 |   assert property (@(posedge clk) val s_until !val) $display("[%0t] s_until, fileline:%d", $time, 51);
+   51 |   assert property (@(posedge clk) ##1 (val s_until val)) $display("[%0t] s_until in sequence, fileline:%d", $time, 51);
+      |                                            ^~~~~~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:53:39: Unsupported: s_until (in property expression)
+                                                    : ... note: In instance 't'
+   53 |   assert property (@(posedge clk) val s_until val s_until val) $display("[%0t] nested s_until, fileline:%d", $time, 53);
       |                                       ^~~~~~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:53:39: Unsupported: s_until_with (in property expresion)
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:39: Unsupported: s_until (in property expression)
                                                     : ... note: In instance 't'
-   53 |   assert property (@(posedge clk) val s_until_with val) $display("[%0t] s_until_with, fileline:%d", $time, 53);
+   55 |   assert property (@(posedge clk) val s_until (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, 55);
+      |                                       ^~~~~~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:57:44: Unsupported: s_until_with (in property expression)
+                                                    : ... note: In instance 't'
+   57 |   assert property (@(posedge clk) ##1 (val s_until_with val)) $display("[%0t] s_until_with in sequence, fileline:%d", $time, 57);
+      |                                            ^~~~~~~~~~~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:59:39: Unsupported: s_until_with (in property expression)
+                                                    : ... note: In instance 't'
+   59 |   assert property (@(posedge clk) val s_until_with val s_until_with val) $display("[%0t] nested s_until_with, fileline:%d", $time, 59);
       |                                       ^~~~~~~~~~~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:40: Unsupported: 'until' in complex property expression
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:61:39: Unsupported: s_until_with (in property expression)
                                                     : ... note: In instance 't'
-   55 |   assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, 55);
+   61 |   assert property (@(posedge clk) val s_until_with (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, 61);
+      |                                       ^~~~~~~~~~~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:63:40: Unsupported: 'until' in complex property expression
+                                                    : ... note: In instance 't'
+   63 |   assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, 63);
       |                                        ^~~~~
 %Error: Exiting due to

test_regress/t/t_property_sexpr_unsup.out

@@ -7,16 +7,32 @@
                                                     : ... note: In instance 't'
    49 |   assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, 49);
       |                                       ^~~~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:51:39: Unsupported: s_until (in property expresion)
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:51:44: Unsupported: s_until (in property expression)
                                                     : ... note: In instance 't'
-   51 |   assert property (@(posedge clk) val s_until !val) $display("[%0t] s_until, fileline:%d", $time, 51);
+   51 |   assert property (@(posedge clk) ##1 (val s_until val)) $display("[%0t] s_until in sequence, fileline:%d", $time, 51);
+      |                                            ^~~~~~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:53:39: Unsupported: s_until (in property expression)
+                                                    : ... note: In instance 't'
+   53 |   assert property (@(posedge clk) val s_until val s_until val) $display("[%0t] nested s_until, fileline:%d", $time, 53);
       |                                       ^~~~~~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:53:39: Unsupported: s_until_with (in property expresion)
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:39: Unsupported: s_until (in property expression)
                                                     : ... note: In instance 't'
-   53 |   assert property (@(posedge clk) val s_until_with val) $display("[%0t] s_until_with, fileline:%d", $time, 53);
+   55 |   assert property (@(posedge clk) val s_until (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, 55);
+      |                                       ^~~~~~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:57:44: Unsupported: s_until_with (in property expression)
+                                                    : ... note: In instance 't'
+   57 |   assert property (@(posedge clk) ##1 (val s_until_with val)) $display("[%0t] s_until_with in sequence, fileline:%d", $time, 57);
+      |                                            ^~~~~~~~~~~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:59:39: Unsupported: s_until_with (in property expression)
+                                                    : ... note: In instance 't'
+   59 |   assert property (@(posedge clk) val s_until_with val s_until_with val) $display("[%0t] nested s_until_with, fileline:%d", $time, 59);
       |                                       ^~~~~~~~~~~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:40: Unsupported: 'until' in complex property expression
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:61:39: Unsupported: s_until_with (in property expression)
                                                     : ... note: In instance 't'
-   55 |   assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, 55);
+   61 |   assert property (@(posedge clk) val s_until_with (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, 61);
+      |                                       ^~~~~~~~~~~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:63:40: Unsupported: 'until' in complex property expression
+                                                    : ... note: In instance 't'
+   63 |   assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, 63);
       |                                        ^~~~~
 %Error: Exiting due to

test_regress/t/t_property_sexpr_unsup.v

@@ -48,9 +48,17 @@ module t (  /*AUTOARG*/
 
   assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, `__LINE__);
 
-  assert property (@(posedge clk) val s_until !val) $display("[%0t] s_until, fileline:%d", $time, `__LINE__);
+  assert property (@(posedge clk) ##1 (val s_until val)) $display("[%0t] s_until in sequence, fileline:%d", $time, `__LINE__);
 
-  assert property (@(posedge clk) val s_until_with val) $display("[%0t] s_until_with, fileline:%d", $time, `__LINE__);
+  assert property (@(posedge clk) val s_until val s_until val) $display("[%0t] nested s_until, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) val s_until (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) ##1 (val s_until_with val)) $display("[%0t] s_until_with in sequence, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) val s_until_with val s_until_with val) $display("[%0t] nested s_until_with, fileline:%d", $time, `__LINE__);
+
+  assert property (@(posedge clk) val s_until_with (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, `__LINE__);
 
   assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, `__LINE__);
 

test_regress/t/t_property_until.v

@@ -46,6 +46,40 @@ module t (  /*AUTOARG*/
     results[5].passs++;
   else results[5].fails++;
 
+  assert property (@(posedge clk) 0 s_until 1)
+    results[6].passs++;
+  else results[6].fails++;
+
+  assert property (@(posedge clk) cyc < 5 s_until cyc >= 5)
+    results[7].passs++;
+  else results[7].fails++;
+
+  assert property (@(posedge clk) cyc % 3 == 0 s_until cyc % 5 == 0)
+    results[8].passs++;
+  else results[8].fails++;
+
+  // Check that s_until accepts immediately when RHS is true, even if LHS is false.
+  assert property (@(posedge clk) cyc % 2 == 0 s_until 1)
+    results[9].passs++;
+  else results[9].fails++;
+
+  // Check that s_until_with requires LHS when RHS is true on the same tick.
+  assert property (@(posedge clk) 0 s_until_with 1)
+    results[10].passs++;
+  else results[10].fails++;
+
+  assert property (@(posedge clk) 1 s_until_with cyc >= 5)
+    results[11].passs++;
+  else results[11].fails++;
+
+  assert property (@(posedge clk) cyc <= 5 s_until_with cyc >= 5)
+    results[12].passs++;
+  else results[12].fails++;
+
+  assert property (@(posedge clk) cyc < 5 s_until_with cyc >= 5)
+    results[13].passs++;
+  else results[13].fails++;
+
   always @(edge clk) begin
     ++cyc;
     if (cyc == MAX) begin
@@ -54,6 +88,14 @@ module t (  /*AUTOARG*/
       expected[3] = '{0, 7};
       expected[4] = '{5, 2};
       expected[5] = '{2, 5};
+      expected[6] = '{0, 7};
+      expected[7] = '{0, 7};
+      expected[8] = '{5, 2};
+      expected[9] = '{0, 7};
+      expected[10] = '{7, 0};
+      expected[11] = '{0, 7};
+      expected[12] = '{4, 3};
+      expected[13] = '{7, 0};
       `checkh(results, expected);
       $write("*-* All Finished *-*\n");
       $finish;

test_regress/t/t_timing_unset1.out

@@ -52,4 +52,12 @@
    38 |    assert property (@(e) s_eventually 1'h1);
       |                          ^~~~~~~~~~~~
                  ... For error description see https://verilator.org/warn/NOTIMING?v=latest
+%Error-NOTIMING: t/t_notiming.v:39:31: s_until requires --timing
+                                     : ... note: In instance 't'
+   39 |    assert property (@(e) 1'h1 s_until 1'h1);
+      |                               ^~~~~~~
+%Error-NOTIMING: t/t_notiming.v:40:31: s_until_with requires --timing
+                                     : ... note: In instance 't'
+   40 |    assert property (@(e) 1'h1 s_until_with 1'h1);
+      |                               ^~~~~~~~~~~~
 %Error: Exiting due to