Support deferred assertions, bug1449.

This commit is contained in:
Wilson Snyder 2019-05-31 07:33:57 -04:00
parent 97fef7c60b
commit 97d9de3dad
3 changed files with 68 additions and 28 deletions

View File

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

View File

@ -1775,7 +1775,7 @@ module_common_item<nodep>: // ==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<nodep>:
;
stmt<nodep>: // 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<nodep>: // 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<nodep>: // IEEE: clocking_declaration (INCOMPLETE)
//************************************************
// Asserts
labeledStmt<nodep>:
immediate_assert_statement { $$ = $1; }
| immediate_assume_statement { $$ = $1; }
assertion_item<nodep>: // ==IEEE: assertion_item
concurrent_assertion_item { $$ = $1; }
| deferred_immediate_assertion_item { $$ = $1; }
;
deferred_immediate_assertion_item<nodep>: // ==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<nodep>: // ==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<nodep>: // ==IEEE: immediate_assertion_statement
simple_immediate_assertion_statement { $$ = $1; }
| deferred_immediate_assertion_statement { $$ = $1; }
;
simple_immediate_assertion_statement<nodep>: // ==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 { $<fl>1->v3error("Unsupported: immediate cover"); $$=NULL; }
;
final_zero: // IEEE: part of deferred_immediate_assertion_statement
'#' yaINTNUM
{ if ($2->isNeqZero()) { $<fl>2->v3error("Deferred assertions must use '#0' (IEEE 2017 16.4)"); } }
// // 1800-2012:
| yFINAL { }
;
deferred_immediate_assertion_statement<nodep>: // ==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 { $<fl>1->v3error("Unsupported: immediate cover"); $$=NULL; }
;
concurrent_assertion_item<nodep>: // IEEE: concurrent_assertion_item
@ -3828,8 +3875,9 @@ concurrent_assertion_item<nodep>: // IEEE: concurrent_assertion_item
;
concurrent_assertion_statement<nodep>: // ==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<nodep>: // IEEE: property_spec
| expr { $$ = new AstPslClocked($1->fileline(),NULL,NULL,$1); }
;
immediate_assert_statement<nodep>: // ==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<nodep>: // ==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

View File

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