Support assert property statement-else-statement

This commit is contained in:
Wilson Snyder 2023-03-10 22:13:17 -05:00
parent 81e8388c3f
commit 60a6ed2a20
3 changed files with 40 additions and 13 deletions

View File

@ -182,7 +182,7 @@ private:
const bool force = VN_IS(nodep, AssertIntrinsic);
if (passsp) passsp = newIfAssertOn(passsp, force);
if (failsp) failsp = newIfAssertOn(failsp, force);
if (!failsp) failsp = newFireAssertUnchecked(nodep, "'assert' failed.");
if (!passsp && !failsp) failsp = newFireAssertUnchecked(nodep, "'assert' failed.");
ifp = new AstIf{nodep->fileline(), propp, passsp, failsp};
ifp->isBoundsCheck(true); // To avoid LATCH warning
// It's more LIKELY that we'll take the nullptr if clause

View File

@ -5772,14 +5772,13 @@ concurrent_assertion_item<nodep>: // IEEE: concurrent_assertion_item
concurrent_assertion_statement<nodep>: // ==IEEE: concurrent_assertion_statement
// // IEEE: assert_property_statement
// // IEEE: assume_property_statement
//UNSUP remove below:
assertOrAssume yPROPERTY '(' property_spec ')' elseStmtBlock
{ $$ = new AstAssert{$1, new AstSampled{$1, $4}, nullptr, $6, false}; }
//UNSUP remove above:
// // action_block expanded here
//UNSUP assertOrAssume yPROPERTY '(' property_spec ')' stmt %prec prLOWER_THAN_ELSE {}
//UNSUP assertOrAssume yPROPERTY '(' property_spec ')' stmt yELSE stmt {}
//UNSUP assertOrAssume yPROPERTY '(' property_spec ')' yELSE stmt {}
assertOrAssume yPROPERTY '(' property_spec ')' stmt %prec prLOWER_THAN_ELSE
{ $$ = new AstAssert{$1, new AstSampled{$1, $4}, $6, nullptr, false}; }
| assertOrAssume yPROPERTY '(' property_spec ')' stmt yELSE stmt
{ $$ = new AstAssert{$1, new AstSampled{$1, $4}, $6, $8, false}; }
| assertOrAssume yPROPERTY '(' property_spec ')' yELSE stmt
{ $$ = new AstAssert{$1, new AstSampled{$1, $4}, nullptr, $7, false}; }
// // IEEE: cover_property_statement
| yCOVER yPROPERTY '(' property_spec ')' stmtBlock
{ $$ = new AstCover{$1, $4, $6, false}; }
@ -5797,11 +5796,6 @@ concurrent_assertion_statement<nodep>: // ==IEEE: concurrent_assertion_statemen
{ $$ = new AstRestrict{$1, $4}; }
;
elseStmtBlock<nodep>: // Part of concurrent_assertion_statement
';' { $$ = nullptr; }
| yELSE stmtBlock { $$ = $2; }
;
property_declaration<nodeFTaskp>: // ==IEEE: property_declaration
property_declarationFront property_port_listE ';' property_declarationBody
yENDPROPERTY endLabelE

View File

@ -4,6 +4,8 @@
// any use, without warranty, 2022 by Antmicro Ltd.
// SPDX-License-Identifier: CC0-1.0
`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);
module t (/*AUTOARG*/
// Inputs
clk
@ -14,6 +16,7 @@ module t (/*AUTOARG*/
Test1 t1(clk, a, b);
Test2 t2(clk, a, b);
Test3 t3(clk, a, b);
initial begin
a = 0;
@ -54,3 +57,33 @@ module Test2(
assert property (@(posedge clk) a == b);
endmodule
module Test3(
clk, a, b
);
input clk;
input [3:0] a, b;
int hits[10];
assert property (@(posedge clk) a == b) hits[1]=1;
assert property (@(posedge clk) a == b) else hits[2]=1;
assert property (@(posedge clk) a == b) hits[3]=1; else hits[4]=1;
assert property (@(posedge clk) a != b) hits[5]=1;
assert property (@(posedge clk) a != b) else hits[6]=1;
assert property (@(posedge clk) a != b) hits[7]=1; else hits[8]=1;
final begin
`checkd(hits[1], 1);
`checkd(hits[2], 0);
`checkd(hits[3], 1);
`checkd(hits[4], 0);
`checkd(hits[5], 0);
`checkd(hits[6], 1);
`checkd(hits[7], 0);
`checkd(hits[8], 1);
end
endmodule