Support property case

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

src/V3ParseImp.cpp

@@ -94,6 +94,69 @@ void V3ParseImp::importIfInStd(FileLine* fileline, const string& id, bool doImpo
     }
 }
 
+AstNodeExpr* V3ParseImp::makePropertyCase(FileLine* flp, AstNodeExpr* exprp, AstCaseItem* itemsp) {
+    AstNodeExpr* resultp = nullptr;
+    AstNodeExpr* matchedp = nullptr;
+    AstNodeExpr* defaultPropp = nullptr;
+    FileLine* defaultFlp = flp;
+
+    if (!itemsp) {
+        flp->v3error("Property case statement with no items");
+        exprp->deleteTree();
+        return new AstConst{flp, AstConst::BitTrue{}};
+    }
+
+    for (AstCaseItem *nextp, *itemp = itemsp; itemp; itemp = nextp) {
+        nextp = VN_AS(itemp->nextp(), CaseItem);
+        AstNodeExpr* const propp = VN_AS(itemp->stmtsp()->unlinkFrBack(), NodeExpr);
+
+        if (itemp->isDefault()) {
+            if (defaultPropp) {
+                itemp->v3error("Multiple default statements in property case statement");
+                defaultPropp->deleteTree();
+                exprp->deleteTree();
+                return new AstConst{flp, AstConst::BitTrue{}};
+            }
+            defaultFlp = itemp->fileline();
+            defaultPropp = propp;
+            continue;
+        }
+
+        AstNodeExpr* itemMatchp = nullptr;
+        for (AstNodeExpr *condNextp, *condp = itemp->condsp(); condp; condp = condNextp) {
+            condNextp = VN_AS(condp->nextp(), NodeExpr);
+            condp->unlinkFrBack();
+            AstNodeExpr* const eqp
+                = new AstEqCase{condp->fileline(), exprp->cloneTreePure(false), condp};
+            itemMatchp = itemMatchp ? new AstLogOr{itemp->fileline(), itemMatchp, eqp} : eqp;
+        }
+        UASSERT_OBJ(itemMatchp, itemp, "Property case item without condition");
+        AstNodeExpr* const guardp
+            = matchedp
+                  ? new AstLogAnd{itemp->fileline(), itemMatchp->cloneTreePure(false),
+                                  new AstLogNot{itemp->fileline(), matchedp->cloneTreePure(false)}}
+                  : itemMatchp->cloneTreePure(false);
+        AstNodeExpr* const branchp = new AstImplication{itemp->fileline(), guardp, propp, true};
+        resultp = resultp ? new AstSAnd{flp, resultp, branchp} : branchp;
+        matchedp = matchedp ? new AstLogOr{itemp->fileline(), matchedp, itemMatchp} : itemMatchp;
+    }
+    itemsp->deleteTree();
+
+    if (defaultPropp) {
+        if (!matchedp) {
+            exprp->deleteTree();
+            return defaultPropp;
+        }
+        AstNodeExpr* const noMatchp
+            = static_cast<AstNodeExpr*>(new AstLogNot{defaultFlp, matchedp->cloneTreePure(false)});
+        AstNodeExpr* const branchp = new AstImplication{defaultFlp, noMatchp, defaultPropp, true};
+        resultp = new AstSAnd{flp, resultp, branchp};
+    }
+    matchedp->deleteTree();
+    exprp->deleteTree();
+    return resultp;
+}
+
 void V3ParseImp::lexPpline(const char* textp) {
     // Handle lexer `line directive
     // FileLine* const prevFl = lexFileline();

src/V3ParseImp.h

@@ -309,6 +309,7 @@ public:
     void dumpTokensAhead(int line) VL_MT_DISABLED;
     static void candidatePli(VSpellCheck* spellerp) VL_MT_DISABLED;
     void importIfInStd(FileLine* fileline, const string& id, bool doImport);
+    AstNodeExpr* makePropertyCase(FileLine* flp, AstNodeExpr* exprp, AstCaseItem* itemsp);
 
 private:
     void preprocDumps(std::ostream& os);

src/verilog.y

@@ -6678,13 +6678,9 @@ property_spec<propSpecp>:               // IEEE: property_spec
 
 property_exprCaseIf<nodeExprp>:  // IEEE: part of property_expr for if/case
                 yCASE '(' expr/*expression_or_dist*/ ')' property_case_itemList yENDCASE
-                        { $$ = new AstConst{$1, AstConst::BitFalse{}};
+                        { $$ = PARSEP->makePropertyCase($1, $3, $5); }
-                          BBUNSUP($<fl>1, "Unsupported: property case expression");
-                          DEL($3, $5); }
         |       yCASE '(' expr/*expression_or_dist*/ ')' yENDCASE
-                        { $$ = new AstConst{$1, AstConst::BitFalse{}};
+                        { $$ = PARSEP->makePropertyCase($1, $3, nullptr); }
-                          BBUNSUP($<fl>1, "Unsupported: property case expression");
-                          DEL($3); }
         |       yIF '(' expr/*expression_or_dist*/ ')' pexpr  %prec prIF
                         { $$ = new AstImplication{$1, $3, $5, true}; }
         |       yIF '(' expr/*expression_or_dist*/ ')' pexpr yELSE pexpr
@@ -6695,16 +6691,15 @@ property_exprCaseIf<nodeExprp>:  // IEEE: part of property_expr for if/case
 
 property_case_itemList<caseItemp>:  // IEEE: {property_case_item}
                 property_case_item                      { $$ = $1; }
-        |       property_case_itemList ',' property_case_item   { $$ = addNextNull($1, $3); }
+        |       property_case_itemList property_case_item   { $$ = addNextNull($1, $2); }
         ;
 
 property_case_item<caseItemp>:  // ==IEEE: property_case_item
-        //                      // IEEE: expression_or_dist { ',' expression_or_dist } ':' property_statement
+        //                      // IEEE: expression_or_dist { ',' expression_or_dist } ':' property_expr
         //                      // IEEE 1800-2012 changed from property_statement to property_expr
         //                      // IEEE 1800-2017 changed to require the semicolon
-                caseCondList ':' pexpr                  { $$ = new AstCaseItem{$2, $1, $3}; }
+                caseCondList ':' pexpr ';'              { $$ = new AstCaseItem{$2, $1, $3}; }
-        |       caseCondList ':' pexpr ';'              { $$ = new AstCaseItem{$2, $1, $3}; }
+        |       yDEFAULT pexpr ';'                      { $$ = new AstCaseItem{$1, nullptr, $2}; }
-        |       yDEFAULT pexpr                          { $$ = new AstCaseItem{$1, nullptr, $2}; }
         |       yDEFAULT ':' pexpr ';'                  { $$ = new AstCaseItem{$1, nullptr, $3}; }
         ;
 

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

test_regress/t/t_property_case.v

@@ -0,0 +1,90 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 Antmicro
+// 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
+);
+
+  int cyc = 0;
+  logic [1:0] sel;
+  logic a;
+  logic b;
+
+  int linear_f = 0;
+  int default_f = 0;
+  int vacuous_f = 0;
+  int delay_f = 0;
+
+  always_comb begin
+    sel = cyc[1:0];
+    a = 1'b1;
+    b = 1'b1;
+  end
+
+  property p_delay(logic [1:0] delay);
+    case (delay)
+      2'd0 : a && b;
+      2'd1 : a ##2 b;
+      2'd2 : a ##4 b;
+      2'd3 : a ##8 b;
+      default: 0;
+    endcase
+  endproperty
+
+  property p_linear_search;
+    case (sel)
+      2'd0 : 1'b0;
+      2'd0, 2'd1 : 1'b1;
+      default 1'b1;
+    endcase
+  endproperty
+
+  property p_default_ignored_during_search;
+    case (sel)
+      default: 1'b0;
+      2'd2 : 1'b1;
+    endcase
+  endproperty
+
+  property p_no_default_vacuous_success;
+    case (sel)
+      2'd0 : 1'b0;
+    endcase
+  endproperty
+
+  property p_only_default;
+    case (sel)
+      default: 1'b1;
+    endcase
+  endproperty
+
+  assert property (@(posedge clk) p_delay(sel)) else delay_f++;
+  assert property (@(posedge clk) p_linear_search) else linear_f++;
+  assert property (@(posedge clk) p_default_ignored_during_search) else default_f++;
+  assert property (@(posedge clk) p_no_default_vacuous_success) else vacuous_f++;
+  assert property (@(posedge clk) p_only_default) else `stop;
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+  end
+
+  always @(negedge clk) begin
+    if (cyc == 16) begin
+      `checkd(delay_f, 0);
+      `checkd(linear_f, 4);
+      `checkd(default_f, 12);
+      `checkd(vacuous_f, 4);
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+
+endmodule

test_regress/t/t_property_case_bad.out

@@ -0,0 +1,8 @@
+%Error: t/t_property_case_bad.v:13:7: Multiple default statements in property case statement
+   13 |       default: 1'b0;
+      |       ^~~~~~~
+        ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
+%Error: t/t_property_case_bad.v:18:5: Property case statement with no items
+   18 |     case (sel)
+      |     ^~~~
+%Error: Exiting due to

test_regress/t/t_property_case_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('linter')
+
+test.lint(fails=True, expect_filename=test.golden_filename)
+
+test.passes()

test_regress/t/t_property_case_bad.v

@@ -0,0 +1,21 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 Antmicro
+// SPDX-License-Identifier: CC0-1.0
+
+module t;
+  logic [1:0] sel;
+
+  property p1;
+    case (sel)
+      default: 1'b1;
+      default: 1'b0;
+    endcase
+  endproperty
+
+  property p2;
+    case (sel)
+    endcase
+  endproperty
+endmodule

test_regress/t/t_property_pexpr_parse_unsup.out

@@ -41,10 +41,4 @@
 %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:110:26: Unsupported: sequence argument data type
   110 |   property p_arg_seqence(sequence inseq);
       |                          ^~~~~~~~
-%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:115:5: Unsupported: property case expression
-  115 |     case (a) endcase
-      |     ^~~~
-%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:118:5: Unsupported: property case expression
-  118 |     case (a) default: b; endcase
-      |     ^~~~
 %Error: Exiting due to

test_regress/t/t_property_pexpr_unsup.out

@@ -1,26 +1,26 @@
-%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:128:21: Unsupported: Unclocked assertion
+%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:115:21: Unsupported: Unclocked assertion
                                                      : ... note: In instance 't'
-  128 |   assert property ((s_eventually a) implies (s_eventually a));
+  115 |   assert property ((s_eventually a) implies (s_eventually a));
       |                     ^~~~~~~~~~~~
                     ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
-%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:128:46: Unsupported: Unclocked assertion
+%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:115:46: Unsupported: Unclocked assertion
                                                      : ... note: In instance 't'
-  128 |   assert property ((s_eventually a) implies (s_eventually a));
+  115 |   assert property ((s_eventually a) implies (s_eventually a));
       |                                              ^~~~~~~~~~~~
-%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:128:3: Unsupported: Unclocked assertion
+%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:115:3: Unsupported: Unclocked assertion
                                                     : ... note: In instance 't'
-  128 |   assert property ((s_eventually a) implies (s_eventually a));
+  115 |   assert property ((s_eventually a) implies (s_eventually a));
       |   ^~~~~~
-%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:130:21: Unsupported: Unclocked assertion
+%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:117:21: Unsupported: Unclocked assertion
                                                      : ... note: In instance 't'
-  130 |   assert property ((s_eventually a) iff (s_eventually a));
+  117 |   assert property ((s_eventually a) iff (s_eventually a));
       |                     ^~~~~~~~~~~~
-%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:130:42: Unsupported: Unclocked assertion
+%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:117:42: Unsupported: Unclocked assertion
                                                      : ... note: In instance 't'
-  130 |   assert property ((s_eventually a) iff (s_eventually a));
+  117 |   assert property ((s_eventually a) iff (s_eventually a));
       |                                          ^~~~~~~~~~~~
-%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:130:3: Unsupported: Unclocked assertion
+%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:117:3: Unsupported: Unclocked assertion
                                                     : ... note: In instance 't'
-  130 |   assert property ((s_eventually a) iff (s_eventually a));
+  117 |   assert property ((s_eventually a) iff (s_eventually a));
       |   ^~~~~~
 %Error: Exiting due to

test_regress/t/t_property_pexpr_unsup.v

@@ -110,19 +110,6 @@ module t (
   property p_arg_seqence(sequence inseq);
     inseq;
   endproperty
-
-  property p_case_1;
-    case (a) endcase
-  endproperty
-  property p_case_2;
-    case (a) default: b; endcase
-  endproperty
-  property p_if;
-    if (a) b
-  endproperty
-  property p_ifelse;
-    if (a) b else c
-  endproperty
 `endif
 
   assert property ((s_eventually a) implies (s_eventually a));