luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Support property case (#7721)

This commit is contained in:
Artur Bieniek 2026-06-09 00:16:30 +02:00 committed by GitHub
parent 85348e3979
commit 1d29f65eae
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
11 changed files with 235 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

63
src/V3ParseImp.cpp
View File

@ -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();

1
src/V3ParseImp.h
View File

@ -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);

17
src/verilog.y
View File

@ -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{}};
BBUNSUP($<fl>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($<fl>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<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}; }
| 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}; }
;

18
test_regress/t/t_property_case.py Executable file
View File

@ -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()

90
test_regress/t/t_property_case.v Normal file
View File

@ -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

8
test_regress/t/t_property_case_bad.out Normal file
View File

@ -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

16
test_regress/t/t_property_case_bad.py Executable file
View File

@ -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()

21
test_regress/t/t_property_case_bad.v Normal file
View File

@ -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

6
test_regress/t/t_property_pexpr_parse_unsup.out
View File

@ -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

24
test_regress/t/t_property_pexpr_unsup.out
View File

@ -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

13
test_regress/t/t_property_pexpr_unsup.v
View File

@ -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));