From 72db0b575ed5f45a16644c45243cc92f54e168b1 Mon Sep 17 00:00:00 2001 From: Artur Bieniek Date: Wed, 3 Jun 2026 21:54:15 +0200 Subject: [PATCH] Support if/if-else in properties (#7692) --- src/verilog.y | 32 +++++---- test_regress/t/t_property_if_else.py | 18 +++++ test_regress/t/t_property_if_else.v | 72 +++++++++++++++++++ .../t/t_property_pexpr_parse_unsup.out | 6 -- 4 files changed, 107 insertions(+), 21 deletions(-) create mode 100755 test_regress/t/t_property_if_else.py create mode 100644 test_regress/t/t_property_if_else.v diff --git a/src/verilog.y b/src/verilog.y index f21b76bde..370693668 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -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: // IEEE: part of property_expr for if/case { $$ = new AstConst{$1, AstConst::BitFalse{}}; BBUNSUP($1, "Unsupported: property case expression"); DEL($3); } - | yIF '(' expr/*expression_or_dist*/ ')' pexpr %prec prLOWER_THAN_ELSE - { $$ = $5; BBUNSUP($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($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: // IEEE: {property_case_item} @@ -6773,22 +6775,22 @@ pexpr: // 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: // 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" diff --git a/test_regress/t/t_property_if_else.py b/test_regress/t/t_property_if_else.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/test_regress/t/t_property_if_else.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_if_else.v b/test_regress/t/t_property_if_else.v new file mode 100644 index 000000000..9368c24b1 --- /dev/null +++ b/test_regress/t/t_property_if_else.v @@ -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 diff --git a/test_regress/t/t_property_pexpr_parse_unsup.out b/test_regress/t/t_property_pexpr_parse_unsup.out index 0791bc120..8d3609b07 100644 --- a/test_regress/t/t_property_pexpr_parse_unsup.out +++ b/test_regress/t/t_property_pexpr_parse_unsup.out @@ -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