Support immediate cover statements & refactor coverage internals.

This commit is contained in:
Wilson Snyder 2019-12-16 21:43:52 -05:00
parent 8cdc0c4e00
commit 83a1bd0675
14 changed files with 152 additions and 154 deletions

View File

@ -8,6 +8,8 @@ The contributors that suggested a given feature are shown in []. Thanks!
*** Support string compare, ato*, etc methods, bug1606. [Yutetsu TAKATSUKASA]
**** Support immediate cover statements.
**** Ignore `uselib to end-of-line, bug1634. [Frederic Antonin]
**** Update FST trace API for better performance.

View File

@ -44,10 +44,10 @@ private:
AstNodeModule* m_modp; // Last module
AstBegin* m_beginp; // Last begin
unsigned m_modPastNum; // Module past numbering
VDouble0 m_statAsCover; // Statistic tracking
VDouble0 m_statAsPsl; // Statistic tracking
VDouble0 m_statCover; // Statistic tracking
VDouble0 m_statAsNotImm; // Statistic tracking
VDouble0 m_statAsImm; // Statistic tracking
VDouble0 m_statAsFull; // Statistic tracking
VDouble0 m_statAsSV; // Statistic tracking
// METHODS
string assertDisplayMessage(AstNode* nodep, const string& prefix, const string& message) {
@ -104,17 +104,28 @@ private:
return bodysp;
}
void newPslAssertion(AstNode* nodep, AstNode* propp, AstSenTree* sentreep,
AstNode* stmtsp, const string& message) {
propp->unlinkFrBack();
sentreep->unlinkFrBack();
if (stmtsp) stmtsp->unlinkFrBack();
void newPslAssertion(AstNodeCoverOrAssert* nodep, AstNode* failsp) {
if (m_beginp && nodep->name() == "") nodep->name(m_beginp->name());
AstNode* propp = nodep->propp()->unlinkFrBackWithNext();
AstSenTree* sentreep = nodep->sentreep();
const string& message = nodep->name();
AstNode* passsp = nodep->passsp();
if (passsp) passsp->unlinkFrBackWithNext();
if (failsp) failsp->unlinkFrBackWithNext();
if (nodep->immediate()) {
UASSERT_OBJ(!sentreep, nodep, "Immediate assertions don't have sensivity");
} else {
UASSERT_OBJ(sentreep, nodep, "Concurrent assertions must have sensivity");
sentreep->unlinkFrBack();
}
//
AstNode* bodysp = NULL;
bool selfDestruct = false;
AstIf* ifp = NULL;
if (AstPslCover* snodep = VN_CAST(nodep, PslCover)) {
++m_statAsCover;
if (AstCover* snodep = VN_CAST(nodep, Cover)) {
++m_statCover;
if (!v3Global.opt.coverageUser()) {
selfDestruct = true;
} else {
@ -126,35 +137,29 @@ private:
bodysp = covincp;
}
if (bodysp && stmtsp) bodysp = bodysp->addNext(stmtsp);
if (bodysp && passsp) bodysp = bodysp->addNext(passsp);
ifp = new AstIf(nodep->fileline(), propp, bodysp, NULL);
bodysp = ifp;
} else if (VN_IS(nodep, PslAssert)) {
++m_statAsPsl;
// Insert an automatic error message and $stop after
// any user-supplied statements.
AstNode* autoMsgp = newFireAssertUnchecked(nodep, "'assert property' failed.");
if (stmtsp) {
stmtsp->addNext(autoMsgp);
} else {
stmtsp = autoMsgp;
}
ifp = new AstIf(nodep->fileline(), propp, NULL, stmtsp);
} else if (VN_IS(nodep, Assert)) {
if (nodep->immediate()) ++m_statAsImm;
else ++m_statAsNotImm;
if (passsp) passsp = newIfAssertOn(passsp);
if (failsp) failsp = newIfAssertOn(failsp);
if (!failsp) failsp = newFireAssertUnchecked(nodep, "'assert' failed.");
ifp = new AstIf(nodep->fileline(), propp, passsp, failsp);
// It's more LIKELY that we'll take the NULL if clause
// than the sim-killing else clause:
ifp->branchPred(VBranchPred::BP_LIKELY);
bodysp = newIfAssertOn(ifp);
} else if (VN_IS(nodep, PslRestrict)) {
// IEEE says simulator ignores these
pushDeletep(nodep->unlinkFrBack()); VL_DANGLING(nodep);
return;
bodysp = ifp;
} else {
nodep->v3fatalSrc("Unknown node type");
}
AstNode* newp = new AstAlways(nodep->fileline(),
VAlwaysKwd::ALWAYS, sentreep, bodysp);
AstNode* newp;
if (sentreep) {
newp = new AstAlways(nodep->fileline(),
VAlwaysKwd::ALWAYS, sentreep, bodysp);
} else { newp = bodysp; }
// Install it
if (selfDestruct) {
// Delete it after making the tree. This way we can tell the user
@ -168,28 +173,6 @@ private:
pushDeletep(nodep); VL_DANGLING(nodep);
}
void newVAssertion(AstVAssert* nodep, AstNode* propp) {
propp->unlinkFrBackWithNext();
AstNode* passsp = nodep->passsp(); if (passsp) passsp->unlinkFrBackWithNext();
AstNode* failsp = nodep->failsp(); if (failsp) failsp->unlinkFrBackWithNext();
//
if (VN_IS(nodep, VAssert)) {
if (passsp) passsp = newIfAssertOn(passsp);
if (failsp) failsp = newIfAssertOn(failsp);
} else {
nodep->v3fatalSrc("Unknown node type");
}
AstIf* ifp = new AstIf(nodep->fileline(), propp, passsp, failsp);
AstNode* newp = ifp;
if (VN_IS(nodep, VAssert)) ifp->branchPred(VBranchPred::BP_UNLIKELY);
//
// Install it
nodep->replaceWith(newp);
// Bye
pushDeletep(nodep); VL_DANGLING(nodep);
}
// VISITORS
virtual void visit(AstIf* nodep) {
if (nodep->user1SetOnce()) return;
@ -358,16 +341,18 @@ private:
}
}
virtual void visit(AstNodePslCoverOrAssert* nodep) {
virtual void visit(AstAssert* nodep) {
iterateChildren(nodep);
if (m_beginp && nodep->name() == "") nodep->name(m_beginp->name());
newPslAssertion(nodep, nodep->propp(), nodep->sentreep(),
nodep->stmtsp(), nodep->name()); VL_DANGLING(nodep);
newPslAssertion(nodep, nodep->failsp());
}
virtual void visit(AstVAssert* nodep) {
virtual void visit(AstCover* nodep) {
iterateChildren(nodep);
newVAssertion(nodep, nodep->propp()); VL_DANGLING(nodep);
++m_statAsSV;
newPslAssertion(nodep, NULL);
}
virtual void visit(AstRestrict* nodep) {
iterateChildren(nodep);
// IEEE says simulator ignores these
pushDeletep(nodep->unlinkFrBack()); VL_DANGLING(nodep);
}
virtual void visit(AstNodeModule* nodep) {
@ -402,9 +387,9 @@ public:
iterate(nodep);
}
virtual ~AssertVisitor() {
V3Stats::addStat("Assertions, PSL asserts", m_statAsPsl);
V3Stats::addStat("Assertions, SystemVerilog asserts", m_statAsSV);
V3Stats::addStat("Assertions, cover statements", m_statAsCover);
V3Stats::addStat("Assertions, assert non-immediate statements", m_statAsNotImm);
V3Stats::addStat("Assertions, assert immediate statements", m_statAsImm);
V3Stats::addStat("Assertions, cover statements", m_statCover);
V3Stats::addStat("Assertions, full/parallel case", m_statAsFull);
}
};

View File

@ -92,12 +92,14 @@ private:
m_seniAlwaysp = NULL;
}
virtual void visit(AstNodePslCoverOrAssert* nodep) {
virtual void visit(AstNodeCoverOrAssert* nodep) {
if (nodep->sentreep()) return; // Already processed
clearAssertInfo();
// Find PslClocking's buried under nodep->exprsp
// Find Clocking's buried under nodep->exprsp
iterateChildren(nodep);
nodep->sentreep(newSenTree(nodep));
if (!nodep->immediate()) {
nodep->sentreep(newSenTree(nodep));
}
clearAssertInfo();
}
virtual void visit(AstPast* nodep) {
@ -105,7 +107,7 @@ private:
iterateChildren(nodep);
nodep->sentreep(newSenTree(nodep));
}
virtual void visit(AstPslClocked* nodep) {
virtual void visit(AstPropClocked* nodep) {
// No need to iterate the body, once replace will get iterated
iterateAndNextNull(nodep->sensesp());
if (m_senip) {

View File

@ -949,6 +949,10 @@ void AstCellInline::dump(std::ostream& str) const {
this->AstNode::dump(str);
str<<" -> "<<origModName();
}
void AstNodeCoverOrAssert::dump(std::ostream& str) const {
this->AstNode::dump(str);
if (immediate()) str<<" [IMMEDIATE]";
}
void AstDisplay::dump(std::ostream& str) const {
this->AstNode::dump(str);
//str<<" "<<displayType().ascii();

View File

@ -6167,28 +6167,6 @@ public:
void isDefault(bool flag) { m_default = flag; }
};
//======================================================================
// SysVerilog assertions
class AstVAssert : public AstNodeStmt {
// Verilog Assertion
// Parents: {statement list}
// Children: expression, if pass statements, if fail statements
public:
AstVAssert(FileLine* fl, AstNode* propp, AstNode* passsp, AstNode* failsp)
: AstNodeStmt(fl) {
addOp1p(propp);
addNOp2p(passsp);
addNOp3p(failsp);
}
ASTNODE_NODE_FUNCS(VAssert)
virtual V3Hash sameHash() const { return V3Hash(); }
virtual bool same(const AstNode* samep) const { return true; }
AstNode* propp() const { return op1p(); } // op1 = property
AstNode* passsp() const { return op2p(); } // op2 = if passes
AstNode* failsp() const { return op3p(); } // op3 = if fails
};
//======================================================================
// Assertions
@ -6210,69 +6188,80 @@ public:
//======================================================================
// PSL
class AstPslClocked : public AstNode {
class AstPropClocked : public AstNode {
// A clocked property
// Parents: ASSERT|COVER (property)
// Children: SENITEM, Properties
public:
AstPslClocked(FileLine* fl, AstNodeSenItem* sensesp, AstNode* disablep, AstNode* propp)
AstPropClocked(FileLine* fl, AstNodeSenItem* sensesp, AstNode* disablep, AstNode* propp)
: AstNode(fl) {
addNOp1p(sensesp);
addNOp2p(disablep);
addOp3p(propp);
}
ASTNODE_NODE_FUNCS(PslClocked)
virtual bool hasDType() const { return true; } // Used under PslCover, which expects a bool child
ASTNODE_NODE_FUNCS(PropClocked)
virtual bool hasDType() const { return true; } // Used under Cover, which expects a bool child
AstNodeSenItem* sensesp() const { return VN_CAST(op1p(), NodeSenItem); } // op1 = Sensitivity list
AstNode* disablep() const { return op2p(); } // op2 = disable
AstNode* propp() const { return op3p(); } // op3 = property
};
class AstNodePslCoverOrAssert : public AstNodeStmt {
// Psl Cover
class AstNodeCoverOrAssert : public AstNodeStmt {
// Cover or Assert
// Parents: {statement list}
// Children: expression, report string
private:
bool m_immediate; // Immediate assertion/cover
string m_name; // Name to report
public:
AstNodePslCoverOrAssert(FileLine* fl, AstNode* propp, AstNode* stmtsp, const string& name="")
AstNodeCoverOrAssert(FileLine* fl, AstNode* propp, AstNode* passsp,
bool immediate, const string& name="")
: AstNodeStmt(fl)
, m_immediate(immediate)
, m_name(name) {
addOp1p(propp);
addNOp4p(stmtsp);
addNOp4p(passsp);
}
ASTNODE_BASE_FUNCS(NodePslCoverOrAssert)
ASTNODE_BASE_FUNCS(NodeCoverOrAssert)
virtual string name() const { return m_name; } // * = Var name
virtual V3Hash sameHash() const { return V3Hash(name()); }
virtual bool same(const AstNode* samep) const { return samep->name() == name(); }
virtual void name(const string& name) { m_name = name; }
virtual void dump(std::ostream& str=std::cout) const;
AstNode* propp() const { return op1p(); } // op1 = property
AstSenTree* sentreep() const { return VN_CAST(op2p(), SenTree); } // op2 = clock domain
void sentreep(AstSenTree* sentreep) { addOp2p(sentreep); } // op2 = clock domain
AstNode* stmtsp() const { return op4p(); } // op4 = statements
AstNode* passsp() const { return op4p(); } // op4 = statements (assert/cover passes)
bool immediate() const { return m_immediate; }
};
class AstPslAssert : public AstNodePslCoverOrAssert {
class AstAssert : public AstNodeCoverOrAssert {
public:
ASTNODE_NODE_FUNCS(PslAssert)
AstPslAssert(FileLine* fl, AstNode* propp, AstNode* stmtsp, const string& name="")
: AstNodePslCoverOrAssert(fl, propp, stmtsp, name) {}
ASTNODE_NODE_FUNCS(Assert)
AstAssert(FileLine* fl, AstNode* propp, AstNode* passsp, AstNode* failsp,
bool immediate, const string& name = "")
: AstNodeCoverOrAssert(fl, propp, passsp, immediate, name) {
addNOp3p(failsp);
}
AstNode* failsp() const { return op3p(); } // op3 = if assertion fails
};
class AstPslCover : public AstNodePslCoverOrAssert {
class AstCover : public AstNodeCoverOrAssert {
public:
ASTNODE_NODE_FUNCS(PslCover)
AstPslCover(FileLine* fl, AstNode* propp, AstNode* stmtsp, const string& name="")
: AstNodePslCoverOrAssert(fl, propp, stmtsp, name) {}
ASTNODE_NODE_FUNCS(Cover)
AstCover(FileLine* fl, AstNode* propp, AstNode* stmtsp,
bool immediate, const string& name = "")
: AstNodeCoverOrAssert(fl, propp, stmtsp, immediate, name) {}
AstNode* coverincp() const { return op3p(); } // op3 = coverage node
void coverincp(AstCoverInc* nodep) { addOp3p(nodep); } // op3 = coverage node
virtual bool immediate() const { return false; }
};
class AstPslRestrict : public AstNodePslCoverOrAssert {
class AstRestrict : public AstNodeCoverOrAssert {
public:
ASTNODE_NODE_FUNCS(PslRestrict)
AstPslRestrict(FileLine* fl, AstNode* propp)
: AstNodePslCoverOrAssert(fl, propp, NULL, "") {}
ASTNODE_NODE_FUNCS(Restrict)
AstRestrict(FileLine* fl, AstNode* propp)
: AstNodeCoverOrAssert(fl, propp, NULL, false, "") {}
};
//======================================================================

View File

@ -353,8 +353,8 @@ private:
m_checkBlock = true; // Reset as a child may have cleared it
}
}
virtual void visit(AstPslCover* nodep) {
UINFO(4," PSLCOVER: "<<nodep<<endl);
virtual void visit(AstCover* nodep) {
UINFO(4," COVER: "<<nodep<<endl);
m_checkBlock = true; // Always do cover blocks, even if there's a $stop
iterateChildren(nodep);
if (!nodep->coverincp()) {

View File

@ -459,10 +459,10 @@ private:
visitIterateNoValueMod(nodep);
m_inAlways = false;
}
virtual void visit(AstPslCover* nodep) {
virtual void visit(AstCover* nodep) {
visitIterateNoValueMod(nodep);
}
virtual void visit(AstPslRestrict* nodep) {
virtual void visit(AstRestrict* nodep) {
visitIterateNoValueMod(nodep);
}

View File

@ -55,8 +55,8 @@ private:
// Below state needs to be preserved between each module call.
AstNodeModule* m_modp; // Current module
AstNodeFTask* m_ftaskp; // Function or task we're inside
AstVAssert* m_assertp; // Current assertion
int m_senitemCvtNum; // Temporary signal counter
AstNodeCoverOrAssert* m_assertp; // Current assertion
int m_senitemCvtNum; // Temporary signal counter
// METHODS
VL_DEBUG_FUNC; // Declare debug()
@ -82,7 +82,7 @@ private:
nodep->replaceWith(nodep->bodysp()->unlinkFrBackWithNext()); VL_DANGLING(nodep);
}
}
virtual void visit(AstVAssert* nodep) {
virtual void visit(AstNodeCoverOrAssert* nodep) {
if (m_assertp) nodep->v3error("Assert not allowed under another assert");
m_assertp = nodep;
iterateChildren(nodep);

View File

@ -2518,7 +2518,7 @@ private:
return times;
}
virtual void visit(AstPslClocked* nodep) {
virtual void visit(AstPropClocked* nodep) {
if (m_vup->prelim()) { // First stage evaluation
iterateCheckBool(nodep, "Property", nodep->propp(), BOTH);
userIterateAndNext(nodep->sensesp(), NULL);
@ -2891,17 +2891,21 @@ private:
assertAtStatement(nodep);
userIterateChildren(nodep, WidthVP(SELF, BOTH).p());
}
virtual void visit(AstNodePslCoverOrAssert* nodep) {
assertAtStatement(nodep);
iterateCheckBool(nodep, "Property", nodep->propp(), BOTH); // it's like an if() condition.
userIterateAndNext(nodep->stmtsp(), NULL);
}
virtual void visit(AstVAssert* nodep) {
virtual void visit(AstAssert* nodep) {
assertAtStatement(nodep);
iterateCheckBool(nodep, "Property", nodep->propp(), BOTH); // it's like an if() condition.
userIterateAndNext(nodep->passsp(), NULL);
userIterateAndNext(nodep->failsp(), NULL);
}
virtual void visit(AstCover* nodep) {
assertAtStatement(nodep);
iterateCheckBool(nodep, "Property", nodep->propp(), BOTH); // it's like an if() condition.
userIterateAndNext(nodep->passsp(), NULL);
}
virtual void visit(AstRestrict* nodep) {
assertAtStatement(nodep);
iterateCheckBool(nodep, "Property", nodep->propp(), BOTH); // it's like an if() condition.
}
virtual void visit(AstPin* nodep) {
//if (debug()) nodep->dumpTree(cout, "- PinPre: ");
// TOP LEVEL NODE

View File

@ -105,7 +105,7 @@ public:
return new AstText(fileline, newtext);
}
AstDisplay* createDisplayError(FileLine* fileline) {
AstDisplay* nodep = new AstDisplay(fileline,AstDisplayType::DT_ERROR, "", NULL,NULL);
AstDisplay* nodep = new AstDisplay(fileline, AstDisplayType::DT_ERROR, "", NULL, NULL);
nodep->addNext(new AstStop(fileline, true));
return nodep;
}
@ -3936,7 +3936,8 @@ clocking_declaration<nodep>: // IEEE: clocking_declaration (INCOMPLETE)
assertion_item<nodep>: // ==IEEE: assertion_item
concurrent_assertion_item { $$ = $1; }
| deferred_immediate_assertion_item { $$ = $1; }
| deferred_immediate_assertion_item
{ $$ = $1 ? new AstAlways($1->fileline(), VAlwaysKwd::ALWAYS_COMB, NULL, $1) : NULL; }
;
deferred_immediate_assertion_item<nodep>: // ==IEEE: deferred_immediate_assertion_item
@ -3959,16 +3960,16 @@ immediate_assertion_statement<nodep>: // ==IEEE: immediate_assertion_statement
;
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); }
// // action_block expanded here, for compatibility with AstAssert
yASSERT '(' expr ')' stmtBlock %prec prLOWER_THAN_ELSE { $$ = new AstAssert($1, $3, $5, NULL, true); }
| yASSERT '(' expr ')' yELSE stmtBlock { $$ = new AstAssert($1, $3, NULL, $6, true); }
| yASSERT '(' expr ')' stmtBlock yELSE stmtBlock { $$ = new AstAssert($1, $3, $5, $7, true); }
// // action_block expanded here, for compatibility with AstAssert
| yASSUME '(' expr ')' stmtBlock %prec prLOWER_THAN_ELSE { $$ = new AstAssert($1, $3, $5, NULL, true); }
| yASSUME '(' expr ')' yELSE stmtBlock { $$ = new AstAssert($1, $3, NULL, $6, true); }
| yASSUME '(' expr ')' stmtBlock yELSE stmtBlock { $$ = new AstAssert($1, $3, $5, $7, true); }
// // IEEE: simple_immediate_cover_statement
| yCOVER '(' expr ')' stmt { $$ = NULL; BBUNSUP($<fl>1, "Unsupported: immediate cover"); }
| yCOVER '(' expr ')' stmt { $$ = new AstCover($1, $3, $5, true); }
;
final_zero: // IEEE: part of deferred_immediate_assertion_statement
@ -3980,15 +3981,15 @@ final_zero: // IEEE: part of deferred_immediate_assertion_statement
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); }
yASSERT final_zero '(' expr ')' stmtBlock %prec prLOWER_THAN_ELSE { $$ = new AstAssert($1, $4, $6, NULL, true); }
| yASSERT final_zero '(' expr ')' yELSE stmtBlock { $$ = new AstAssert($1, $4, NULL, $7, true); }
| yASSERT final_zero '(' expr ')' stmtBlock yELSE stmtBlock { $$ = new AstAssert($1, $4, $6, $8, true); }
// // 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); }
| yASSUME final_zero '(' expr ')' stmtBlock %prec prLOWER_THAN_ELSE { $$ = new AstAssert($1, $4, $6, NULL, true); }
| yASSUME final_zero '(' expr ')' yELSE stmtBlock { $$ = new AstAssert($1, $4, NULL, $7, true); }
| yASSUME final_zero '(' expr ')' stmtBlock yELSE stmtBlock { $$ = new AstAssert($1, $4, $6, $8, true); }
// // IEEE: deferred_immediate_cover_statement
| yCOVER final_zero '(' expr ')' stmt { $$ = NULL; BBUNSUP($<fl>1, "Unsupported: immediate cover"); }
| yCOVER final_zero '(' expr ')' stmt { $$ = new AstCover($1, $4, $6, true); }
;
concurrent_assertion_item<nodep>: // IEEE: concurrent_assertion_item
@ -4000,11 +4001,11 @@ 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); }
yASSERT yPROPERTY '(' property_spec ')' elseStmtBlock { $$ = new AstAssert($1, $4, NULL, $6, false); }
// // IEEE: cover_property_statement
| yCOVER yPROPERTY '(' property_spec ')' stmtBlock { $$ = new AstPslCover($1,$4,$6); }
| yCOVER yPROPERTY '(' property_spec ')' stmtBlock { $$ = new AstCover($1, $4, $6, false); }
// // IEEE: restrict_property_statement
| yRESTRICT yPROPERTY '(' property_spec ')' ';' { $$ = new AstPslRestrict($1,$4); }
| yRESTRICT yPROPERTY '(' property_spec ')' ';' { $$ = new AstRestrict($1, $4); }
;
elseStmtBlock<nodep>: // Part of concurrent_assertion_statement
@ -4015,10 +4016,10 @@ elseStmtBlock<nodep>: // Part of concurrent_assertion_statement
property_spec<nodep>: // IEEE: property_spec
//UNSUP: This rule has been super-specialized to what is supported now
'@' '(' senitemEdge ')' yDISABLE yIFF '(' expr ')' expr
{ $$ = new AstPslClocked($1,$3,$8,$10); }
| '@' '(' senitemEdge ')' expr { $$ = new AstPslClocked($1,$3,NULL,$5); }
| yDISABLE yIFF '(' expr ')' expr { $$ = new AstPslClocked($4->fileline(),NULL,$4,$6); }
| expr { $$ = new AstPslClocked($1->fileline(),NULL,NULL,$1); }
{ $$ = new AstPropClocked($1, $3, $8, $10); }
| '@' '(' senitemEdge ')' expr { $$ = new AstPropClocked($1, $3, NULL, $5); }
| yDISABLE yIFF '(' expr ')' expr { $$ = new AstPropClocked($4->fileline(), NULL, $4, $6); }
| expr { $$ = new AstPropClocked($1->fileline(), NULL, NULL, $1); }
;
//************************************************

View File

@ -64,7 +64,15 @@ module Test
cover property (@(posedge clk) disable iff (!toggle) cyc==8)
$stop;
// Innediate assert
always_ff @ (posedge clk) begin
labeled_icov: cover (cyc==3 || cyc==4);
end
// Immediate cover
labeled_imm0: cover #0 (cyc == 0);
labeled_immf: cover final (cyc == 0);
// Immediate assert
labeled_imas: assert #0 (1);
assert final (1);

View File

@ -17,10 +17,8 @@ compile(
);
execute(
fails => 1,
);
file_grep($Self->{run_log_filename}, qr/'assert property' failed/);
# We expect to get a message when this assert fires:
file_grep($Self->{run_log_filename}, qr/cyc != 3/);

View File

@ -20,7 +20,7 @@ execute(
fails => 1
);
file_grep($Self->{run_log_filename}, qr/'assert property' failed/);
file_grep($Self->{run_log_filename}, qr/'assert' failed/);
ok(1);
1;

View File

@ -92,7 +92,12 @@ module Test2 (/*AUTOARG*/
reg [31:0] dly0;
reg [31:0] dly1;
always @(posedge clk) begin
dly0 <= in;
dly1 <= dly0;
end
default clocking @(posedge clk); endclocking
assert property (@(posedge clk) dly1 == $past(in, 2));
assert property (@(posedge clk) $time < 40 || dly1 == $past(in, 2));
endmodule