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

Support if/if-else in properties (#7692)

This commit is contained in:
Artur Bieniek 2026-06-03 21:54:15 +02:00 committed by GitHub
parent bbd8d927ee
commit 72db0b575e
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
4 changed files with 107 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
src/verilog.y
View File

@ -901,7 +901,7 @@ BISONPRE_VERSION(3.7,%define api.header.include {"V3ParseBison.h"})
// Lowest precedence
// These are in IEEE 17.7.1
%nonassoc yALWAYS yS_ALWAYS yEVENTUALLY yS_EVENTUALLY yACCEPT_ON yREJECT_ON ySYNC_ACCEPT_ON ySYNC_REJECT_ON
%nonassoc prALWAYS prS_ALWAYS prEVENTUALLY prS_EVENTUALLY prIF prACCEPT_ON prREJECT_ON prSYNC_ACCEPT_ON prSYNC_REJECT_ON
%right yP_ORMINUSGT yP_OREQGT yP_POUNDMINUSPD yP_POUNDEQPD
%right yUNTIL yS_UNTIL yUNTIL_WITH yS_UNTIL_WITH yIMPLIES
@ -6685,10 +6685,12 @@ property_exprCaseIf<nodeExprp>: // IEEE: part of property_expr for if/case
{ $$ = new AstConst{$1, AstConst::BitFalse{}};
BBUNSUP($<fl>1, "Unsupported: property case expression");
DEL($3); }
| yIF '(' expr/*expression_or_dist*/ ')' pexpr %prec prLOWER_THAN_ELSE
{ $$ = $5; 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
{ $$ = $5; BBUNSUP($<fl>1, "Unsupported: property case expression"); DEL($3, $7); }
{ AstNodeExpr* const elseCondp = new AstLogNot{$1, $3->cloneTreePure(false)};
$$ = new AstSAnd{$1, new AstImplication{$1, $3, $5, true},
new AstImplication{$1, elseCondp, $7, true}}; }
;
property_case_itemList<caseItemp>: // IEEE: {property_case_item}
@ -6773,22 +6775,22 @@ pexpr<nodeExprp>: // IEEE: property_expr (The name pexpr is important as regex
{ $$ = $5; BBUNSUP($1, "Unsupported: nexttime[] (in property expression)"); DEL($3); }
| yS_NEXTTIME '[' constExpr ']' pexpr %prec yS_NEXTTIME
{ $$ = $5; BBUNSUP($1, "Unsupported: s_nexttime[] (in property expression)"); DEL($3); }
| yALWAYS pexpr
| yALWAYS pexpr %prec prALWAYS
{ $$ = $2; }
| yALWAYS '[' constExpr ':' constExpr ']' pexpr %prec yALWAYS
| yALWAYS '[' constExpr ':' constExpr ']' pexpr %prec prALWAYS
{ $$ = new AstPropAlways{$1, $7, $3, $5, false}; }
| yS_ALWAYS '[' constExpr ':' constExpr ']' pexpr %prec yS_ALWAYS
| yS_ALWAYS '[' constExpr ':' constExpr ']' pexpr %prec prS_ALWAYS
{ $$ = new AstPropAlways{$1, $7, $3, $5, true}; }
| yS_ALWAYS pexpr
| yS_ALWAYS pexpr %prec prS_ALWAYS
{ $$ = new AstPropAlways{$1, $2, new AstUnbounded{$1}, new AstUnbounded{$1}, true}; }
| yS_EVENTUALLY pexpr
| yS_EVENTUALLY pexpr %prec prS_EVENTUALLY
{
$$ = new AstSEventually{$1, $2};
PARSEP->importIfInStd($1, "process", true);
}
| yS_EVENTUALLY anyrange pexpr %prec yS_EVENTUALLY
| yS_EVENTUALLY anyrange pexpr %prec prS_EVENTUALLY
{ $$ = $3; BBUNSUP($1, "Unsupported: s_eventually[] (in property expression)"); DEL($2); }
| yEVENTUALLY anyrange pexpr %prec yS_EVENTUALLY
| yEVENTUALLY anyrange pexpr %prec prEVENTUALLY
{ $$ = $3; BBUNSUP($1, "Unsupported: eventually[] (in property expression)"); DEL($2); }
| ~o~pexpr yUNTIL pexpr
{ $$ = new AstUntil{$2, $1, $3, false, false}; }
@ -6803,13 +6805,13 @@ pexpr<nodeExprp>: // IEEE: property_expr (The name pexpr is important as regex
// // yIFF also used by event_expression
| ~o~pexpr yIFF pexpr
{ $$ = new AstLogEq{$2, $1, $3}; }
| yACCEPT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec yACCEPT_ON
| yACCEPT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec prACCEPT_ON
{ $$ = new AstAbortOn{$1, VAbortKind::ACCEPT_ON, $3, $5}; }
| yREJECT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec yREJECT_ON
| yREJECT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec prREJECT_ON
{ $$ = new AstAbortOn{$1, VAbortKind::REJECT_ON, $3, $5}; }
| ySYNC_ACCEPT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec ySYNC_ACCEPT_ON
| ySYNC_ACCEPT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec prSYNC_ACCEPT_ON
{ $$ = new AstAbortOn{$1, VAbortKind::SYNC_ACCEPT_ON, $3, $5}; }
| ySYNC_REJECT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec ySYNC_REJECT_ON
| ySYNC_REJECT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec prSYNC_REJECT_ON
{ $$ = new AstAbortOn{$1, VAbortKind::SYNC_REJECT_ON, $3, $5}; }
//
// // IEEE: "property_instance"

18
test_regress/t/t_property_if_else.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()

72
test_regress/t/t_property_if_else.v Normal file
View File

@ -0,0 +1,72 @@
// 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 (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0);
// verilog_format: on
module t (
input clk
);
int cyc = 0;
int vacuous_passes = 0;
wire sel = cyc inside {2, 6};
wire a = sel;
wire b = (cyc == 3) || (cyc == 7);
wire c = !sel;
wire nested_outer = cyc inside {2, 4, 6};
wire nested_inner = cyc inside {2, 6};
always @(posedge clk) begin
cyc <= cyc + 1;
if (cyc == 10) begin
`checkd(vacuous_passes, 10);
$write("*-* All Finished *-*\n");
$finish;
end
end
property p_named;
if (sel) a else c;
endproperty
// One-arm property if: false condition is a vacuous pass.
assert property (@(posedge clk) if (sel) a) begin
if (cyc != 0) ++vacuous_passes;
end else
$stop;
// Branch selection: untaken branch must not affect result.
assert property (@(posedge clk) if (sel) 1'b1 else c)
else $stop;
assert property (@(posedge clk) if (!sel) c else 1'b1)
else $stop;
// Named property body.
assert property (@(posedge clk) p_named)
else $stop;
// Temporal branch: if sel is true, require b on the following cycle; otherwise
// the else branch is checked on the current cycle.
assert property (@(posedge clk) if (sel) a |-> ##1 b else c)
else $stop;
// Dangling else binds to the inner property if. If it bound to the outer if,
// the false outer condition would select the failing 1'b0 branch.
assert property (@(posedge clk) if (nested_inner) if (nested_inner) 1'b1 else 1'b0)
else $stop;
// Fully nested if/else: checks the inner else at cyc == 4, the inner then at
// cyc == 2/6, and the outer else on all other cycles.
assert property (@(posedge clk)
if (nested_outer) if (nested_inner) 1'b1 else !nested_inner
else !nested_outer)
else $stop;
endmodule

6
test_regress/t/t_property_pexpr_parse_unsup.out
View File

@ -47,10 +47,4 @@
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:120:7: Unsupported: property case expression
120 | case (a) default: b; endcase
| ^~~~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:123:7: Unsupported: property case expression
123 | if (a) b
| ^~
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:126:7: Unsupported: property case expression
126 | if (a) b else c
| ^~
%Error: Exiting due to