diff --git a/src/V3ParseImp.cpp b/src/V3ParseImp.cpp index 7cf4e76e6..549166f6d 100644 --- a/src/V3ParseImp.cpp +++ b/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(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(); diff --git a/src/V3ParseImp.h b/src/V3ParseImp.h index 33dd99957..882b0e817 100644 --- a/src/V3ParseImp.h +++ b/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); diff --git a/src/verilog.y b/src/verilog.y index 441d6f3de..663e8a206 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6678,13 +6678,9 @@ property_spec: // IEEE: property_spec property_exprCaseIf: // IEEE: part of property_expr for if/case yCASE '(' expr/*expression_or_dist*/ ')' property_case_itemList yENDCASE - { $$ = new AstConst{$1, AstConst::BitFalse{}}; - BBUNSUP($1, "Unsupported: property case expression"); - DEL($3, $5); } + { $$ = PARSEP->makePropertyCase($1, $3, $5); } | yCASE '(' expr/*expression_or_dist*/ ')' yENDCASE - { $$ = new AstConst{$1, AstConst::BitFalse{}}; - BBUNSUP($1, "Unsupported: property case expression"); - DEL($3); } + { $$ = PARSEP->makePropertyCase($1, $3, nullptr); } | 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: // IEEE: part of property_expr for if/case property_case_itemList: // 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: // ==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}; } - | yDEFAULT pexpr { $$ = new AstCaseItem{$1, nullptr, $2}; } + caseCondList ':' pexpr ';' { $$ = new AstCaseItem{$2, $1, $3}; } + | yDEFAULT pexpr ';' { $$ = new AstCaseItem{$1, nullptr, $2}; } | yDEFAULT ':' pexpr ';' { $$ = new AstCaseItem{$1, nullptr, $3}; } ; diff --git a/test_regress/t/t_property_case.py b/test_regress/t/t_property_case.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/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() diff --git a/test_regress/t/t_property_case.v b/test_regress/t/t_property_case.v new file mode 100644 index 000000000..62f875570 --- /dev/null +++ b/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 diff --git a/test_regress/t/t_property_case_bad.out b/test_regress/t/t_property_case_bad.out new file mode 100644 index 000000000..c2c064b26 --- /dev/null +++ b/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 diff --git a/test_regress/t/t_property_case_bad.py b/test_regress/t/t_property_case_bad.py new file mode 100755 index 000000000..38cf36b43 --- /dev/null +++ b/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() diff --git a/test_regress/t/t_property_case_bad.v b/test_regress/t/t_property_case_bad.v new file mode 100644 index 000000000..a66bf805b --- /dev/null +++ b/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 diff --git a/test_regress/t/t_property_pexpr_parse_unsup.out b/test_regress/t/t_property_pexpr_parse_unsup.out index 976b9669f..6a23bc18e 100644 --- a/test_regress/t/t_property_pexpr_parse_unsup.out +++ b/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 diff --git a/test_regress/t/t_property_pexpr_unsup.out b/test_regress/t/t_property_pexpr_unsup.out index c7d9bb601..bae43d802 100644 --- a/test_regress/t/t_property_pexpr_unsup.out +++ b/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 diff --git a/test_regress/t/t_property_pexpr_unsup.v b/test_regress/t/t_property_pexpr_unsup.v index a582241b7..10798685e 100644 --- a/test_regress/t/t_property_pexpr_unsup.v +++ b/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));