From 97d9de3dad2a6e470607a74afeafeeea4473256b Mon Sep 17 00:00:00 2001 From: Wilson Snyder Date: Fri, 31 May 2019 07:33:57 -0400 Subject: [PATCH] Support deferred assertions, bug1449. --- Changes | 2 + src/verilog.y | 90 +++++++++++++++++++++++---------- test_regress/t/t_assert_cover.v | 4 ++ 3 files changed, 68 insertions(+), 28 deletions(-) diff --git a/Changes b/Changes index 42050b778..65177c2b3 100644 --- a/Changes +++ b/Changes @@ -10,6 +10,8 @@ The contributors that suggested a given feature are shown in []. Thanks! **** Support VerilatedFstC set_time_unit, bug1433. [Pieter Kapsenberg] +**** Support deferred assertions, bug1449. [Charles Eddleston] + **** Mark infrequently called functions with GCC cold attribute. **** Fix sign-compare warning in verilated.cpp, bug1437. [Sergey Kvachonok] diff --git a/src/verilog.y b/src/verilog.y index de90a4d42..ada6ede06 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -1775,7 +1775,7 @@ module_common_item: // ==IEEE: module_common_item // // + IEEE: program_instantiation // // + module_instantiation from module_or_generate_item | etcInst { $$ = $1; } - | concurrent_assertion_item { $$ = $1; } + | assertion_item { $$ = $1; } | bind_directive { $$ = $1; } | continuous_assign { $$ = $1; } // // IEEE: net_alias @@ -2336,10 +2336,9 @@ stmtList: ; stmt: // IEEE: statement_or_null == function_statement_or_null - statement_item { } - //UNSUP: Labeling any statement - | labeledStmt { $$ = $1; } - | id ':' labeledStmt { $$ = new AstBegin($2, *$1, $3); } /*S05 block creation rule*/ + statement_item { $$ = $1; } + // // S05 block creation rule + | id/*block_identifier*/ ':' statement_item { $$ = new AstBegin($2, *$1, $3); } // // from _or_null | ';' { $$ = NULL; } ; @@ -2467,11 +2466,7 @@ statement_item: // IEEE: statement_item //UNSUP yWAIT_ORDER '(' hierarchical_identifierList ')' action_block { UNSUP } // // // IEEE: procedural_assertion_statement - // // Verilator: Label included instead - | concurrent_assertion_item { $$ = $1; } - // // concurrent_assertion_statement { $$ = $1; } - // // Verilator: Part of labeledStmt instead - // // immediate_assert_statement { UNSUP } + | procedural_assertion_statement { $$ = $1; } // // // IEEE: clocking_drive ';' // // Pattern w/o cycle_delay handled by nonblocking_assign above @@ -3815,9 +3810,61 @@ clocking_declaration: // IEEE: clocking_declaration (INCOMPLETE) //************************************************ // Asserts -labeledStmt: - immediate_assert_statement { $$ = $1; } - | immediate_assume_statement { $$ = $1; } +assertion_item: // ==IEEE: assertion_item + concurrent_assertion_item { $$ = $1; } + | deferred_immediate_assertion_item { $$ = $1; } + ; + +deferred_immediate_assertion_item: // ==IEEE: deferred_immediate_assertion_item + deferred_immediate_assertion_statement { $$ = $1; } + | id/*block_identifier*/ ':' deferred_immediate_assertion_statement + { $$ = new AstBegin($2, *$1, $3); } + ; + +procedural_assertion_statement: // ==IEEE: procedural_assertion_statement + concurrent_assertion_statement { $$ = $1; } + | immediate_assertion_statement { $$ = $1; } + // // IEEE: checker_instantiation + // // Unlike modules, checkers are the only "id id (...)" form in statements. + //UNSUP checker_instantiation { } + ; + +immediate_assertion_statement: // ==IEEE: immediate_assertion_statement + simple_immediate_assertion_statement { $$ = $1; } + | deferred_immediate_assertion_statement { $$ = $1; } + ; + +simple_immediate_assertion_statement: // ==IEEE: simple_immediate_assertion_statement + // // action_block expanded here, for compatibility with AstVAssert + yASSERT '(' expr ')' stmtBlock %prec prLOWER_THAN_ELSE { $$ = new AstVAssert($1,$3,$5, GRAMMARP->createDisplayError($1)); } + | yASSERT '(' expr ')' yELSE stmtBlock { $$ = new AstVAssert($1,$3,NULL,$6); } + | yASSERT '(' expr ')' stmtBlock yELSE stmtBlock { $$ = new AstVAssert($1,$3,$5,$7); } + // // action_block expanded here, for compatibility with AstVAssert + | yASSUME '(' expr ')' stmtBlock %prec prLOWER_THAN_ELSE { $$ = new AstVAssert($1,$3,$5, GRAMMARP->createDisplayError($1)); } + | yASSUME '(' expr ')' yELSE stmtBlock { $$ = new AstVAssert($1,$3,NULL,$6); } + | yASSUME '(' expr ')' stmtBlock yELSE stmtBlock { $$ = new AstVAssert($1,$3,$5,$7); } + // // IEEE: simple_immediate_cover_statement + | yCOVER '(' expr ')' stmt { $1->v3error("Unsupported: immediate cover"); $$=NULL; } + ; + +final_zero: // IEEE: part of deferred_immediate_assertion_statement + '#' yaINTNUM + { if ($2->isNeqZero()) { $2->v3error("Deferred assertions must use '#0' (IEEE 2017 16.4)"); } } + // // 1800-2012: + | yFINAL { } + ; + +deferred_immediate_assertion_statement: // ==IEEE: deferred_immediate_assertion_statement + // // IEEE: deferred_immediate_assert_statement + yASSERT final_zero '(' expr ')' stmtBlock %prec prLOWER_THAN_ELSE { $$ = new AstVAssert($1,$4,$6, GRAMMARP->createDisplayError($1)); } + | yASSERT final_zero '(' expr ')' yELSE stmtBlock { $$ = new AstVAssert($1,$4,NULL,$7); } + | yASSERT final_zero '(' expr ')' stmtBlock yELSE stmtBlock { $$ = new AstVAssert($1,$4,$6,$8); } + // // IEEE: deferred_immediate_assume_statement + | yASSUME final_zero '(' expr ')' stmtBlock %prec prLOWER_THAN_ELSE { $$ = new AstVAssert($1,$4,$6, GRAMMARP->createDisplayError($1)); } + | yASSUME final_zero '(' expr ')' yELSE stmtBlock { $$ = new AstVAssert($1,$4,NULL,$7); } + | yASSUME final_zero '(' expr ')' stmtBlock yELSE stmtBlock { $$ = new AstVAssert($1,$4,$6,$8); } + // // IEEE: deferred_immediate_cover_statement + | yCOVER final_zero '(' expr ')' stmt { $1->v3error("Unsupported: immediate cover"); $$=NULL; } ; concurrent_assertion_item: // IEEE: concurrent_assertion_item @@ -3828,8 +3875,9 @@ concurrent_assertion_item: // IEEE: concurrent_assertion_item ; concurrent_assertion_statement: // ==IEEE: concurrent_assertion_statement + // // IEEE: assert_property_statement yASSERT yPROPERTY '(' property_spec ')' elseStmtBlock { $$ = new AstPslAssert($1,$4,$6); } - // // IEEE: cover_property_statement + // // IEEE: cover_property_statement | yCOVER yPROPERTY '(' property_spec ')' stmtBlock { $$ = new AstPslCover($1,$4,$6); } // // IEEE: restrict_property_statement | yRESTRICT yPROPERTY '(' property_spec ')' ';' { $$ = new AstPslRestrict($1,$4); } @@ -3849,20 +3897,6 @@ property_spec: // IEEE: property_spec | expr { $$ = new AstPslClocked($1->fileline(),NULL,NULL,$1); } ; -immediate_assert_statement: // ==IEEE: immediate_assert_statement - // // action_block expanded here, for compatibility with AstVAssert - yASSERT '(' expr ')' stmtBlock %prec prLOWER_THAN_ELSE { $$ = new AstVAssert($1,$3,$5, GRAMMARP->createDisplayError($1)); } - | yASSERT '(' expr ')' yELSE stmtBlock { $$ = new AstVAssert($1,$3,NULL,$6); } - | yASSERT '(' expr ')' stmtBlock yELSE stmtBlock { $$ = new AstVAssert($1,$3,$5,$7); } - ; - -immediate_assume_statement: // ==IEEE: immediate_assume_statement - // // action_block expanded here, for compatibility with AstVAssert - yASSUME '(' expr ')' stmtBlock %prec prLOWER_THAN_ELSE { $$ = new AstVAssert($1,$3,$5, GRAMMARP->createDisplayError($1)); } - | yASSUME '(' expr ')' yELSE stmtBlock { $$ = new AstVAssert($1,$3,NULL,$6); } - | yASSUME '(' expr ')' stmtBlock yELSE stmtBlock { $$ = new AstVAssert($1,$3,$5,$7); } - ; - //************************************************ // Covergroup diff --git a/test_regress/t/t_assert_cover.v b/test_regress/t/t_assert_cover.v index 8d5e10391..587dc0b2a 100644 --- a/test_regress/t/t_assert_cover.v +++ b/test_regress/t/t_assert_cover.v @@ -64,6 +64,10 @@ module Test cover property (@(posedge clk) disable iff (!toggle) cyc==8) $stop; + // Innediate assert + labeled_imas: assert #0 (1); + assert final (1); + //============================================================ // Using a macro and generate wire reset = (cyc < 2);