From 79ab50d84f15ab871fc67c8a4f99c01da6739c75 Mon Sep 17 00:00:00 2001 From: Wilson Snyder Date: Tue, 6 Mar 2007 21:43:38 +0000 Subject: [PATCH] Support trivial SV assertions git-svn-id: file://localhost/svn/verilator/trunk/verilator@898 77ca24e4-aefa-0310-84f0-b9a241c72d87 --- bin/verilator | 37 ++++++--- src/V3Assert.cpp | 105 +++++++++++++++++++++---- src/V3Ast.cpp | 2 +- src/V3Ast.h | 29 +++++++ src/V3AstNodes.h | 43 ++++++++-- src/V3Clock.cpp | 3 +- src/V3Descope.cpp | 4 +- src/V3EmitC.cpp | 3 +- src/V3LinkResolve.cpp | 16 ++++ src/V3Width.cpp | 7 ++ src/Verilator.cpp | 12 ++- src/verilog.l | 11 ++- src/verilog.y | 60 +++++++++++--- test_regress/driver.pl | 2 +- test_regress/t/t_assert_basic.pl | 19 +++++ test_regress/t/t_assert_basic.v | 48 +++++++++++ test_regress/t/t_assert_basic_cover.pl | 27 +++++++ test_regress/t/t_assert_basic_fail.pl | 23 ++++++ test_regress/t/t_assert_basic_off.pl | 21 +++++ 19 files changed, 406 insertions(+), 66 deletions(-) create mode 100755 test_regress/t/t_assert_basic.pl create mode 100644 test_regress/t/t_assert_basic.v create mode 100755 test_regress/t/t_assert_basic_cover.pl create mode 100755 test_regress/t/t_assert_basic_fail.pl create mode 100755 test_regress/t/t_assert_basic_off.pl diff --git a/bin/verilator b/bin/verilator index 2ded9a60d..3c1c3fbcd 100755 --- a/bin/verilator +++ b/bin/verilator @@ -903,17 +903,21 @@ declarations inside port lists. Verilator supports the `begin_keywords and `end_keywords compiler directives. -Verilator supports the uwire, $countones, $isunknown, $onehot and $onehot0 -keywords. Verilator partially supports the uwire keyword. +Verilator partially supports the uwire keyword. =head1 SYSTEMVERILOG (IEEE 1800-2005) SUPPORT -Verilator currently has very minimal support for SystemVerilog. +Verilator currently has very minimal support for SystemVerilog as they +become more common, contact the author if a feature you need is missing. Verilator implements the full SystemVerilog 1800-2005 preprocessor subset, -including function call-like preprocessor defines. Verilator also -implements $bits, $countones, $isunknown, $onehot, and $onehot0, -always_comb, always_ff, always_latch, and final. +including function call-like preprocessor defines. + +Verilator supports $bits, $countones, $error, $fatal, $info, $isunknown, +$onehot, $onehot0, $warning, always_comb, always_ff, always_latch, and +final. + +Verilator partially supports assert. =head1 SUGAR/PSL SUPPORT @@ -934,18 +938,16 @@ report, true. Verilator implements these operators: -> (logical if). Verilator does not support SEREs yet. All assertion and coverage -statements must be simple expressions that complete in one cycle. -(Arguably SEREs are the whole point of PSL, but one must start somewhere.) - -PSL vmode/vprop/vunits are not supported. PSL statements must be in the -module they reference, at the module level where you would put an +statements must be simple expressions that complete in one cycle. PSL +vmode/vprop/vunits are not supported. PSL statements must be in the module +they reference, at the module level where you would put an initial... statement. Verilator only supports (posedge CLK) or (negedge CLK), where CLK is the name of a one bit signal. You may not use arbitrary expressions as assertion clocks. -=head1 SYNTHESIS DIRECTIVE ASSERTIONS +=head1 SYNTHESIS DIRECTIVE ASSERTION SUPPORT With the --assert switch, Verilator reads any "//synopsys full_case" or "// synopsys parallel_case" directives. The same applies to any "//cadence" or @@ -1354,6 +1356,17 @@ will give a width warning and wrap around the power-of-2 size. For non-power-of-2 sizes, it will return a unspecified constant of the appropriate width. +=head2 Assertions + +Verilator is beginning to add support for assertions. Verilator currently +only converts assertions to simple "if (...) error" statements, and +coverage statements to increment the line counters described in the +coverage section. + +Verilator does not support SEREs yet. All assertion and coverage +statements must be simple expressions that complete in one cycle. +(Arguably SEREs are much of the point, but one must start somewhere.) + =head1 LANGUAGE KEYWORD LIMITATIONS This section describes specific limitations for each language keyword. diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp index a2803ef66..18f23a84e 100644 --- a/src/V3Assert.cpp +++ b/src/V3Assert.cpp @@ -47,28 +47,58 @@ private: V3Double0 m_statAsCover; // Statistic tracking V3Double0 m_statAsPsl; // Statistic tracking V3Double0 m_statAsFull; // Statistic tracking + V3Double0 m_statAsSV; // Statistic tracking // METHODS - AstNode* newFireAssert(AstNode* nodep, const string& message) { - AstNode* bodysp = new AstDisplay - (nodep->fileline(), '\0', - (string("[%0t] %%Error: ")+nodep->fileline()->filebasename() - +":"+cvtToStr(nodep->fileline()->lineno()) - +": Assertion failed in %m" - +((message != "")?": ":"")+message - +"\\n"), - NULL, - new AstTime(nodep->fileline())); - bodysp->addNext(new AstStop (nodep->fileline())); + string assertDisplayMessage(AstNode* nodep, const string& prefix, const string& message) { + return (string("[%0t] "+prefix+": ")+nodep->fileline()->filebasename() + +":"+cvtToStr(nodep->fileline()->lineno()) + +": Assertion failed in %m" + +((message != "")?": ":"")+message + +"\\n"); + } + void replaceDisplay(AstDisplay* nodep, const string& prefix) { + nodep->displayType(AstDisplayType::WRITE); + nodep->text(assertDisplayMessage(nodep, prefix, nodep->text())); + AstNode* timesp = nodep->exprsp(); if (timesp) timesp->unlinkFrBack(); + timesp = timesp->addNext(new AstTime(nodep->fileline())); + nodep->exprsp(timesp); + } + + AstNode* newIfAssertOn(AstNode* nodep) { // Add a internal if to check assertions are on. // Don't make this a AND term, as it's unlikely to need to test this. - bodysp = new AstIf (nodep->fileline(), - new AstCMath(nodep->fileline(), "Verilated::assertOn()", 1), - bodysp, NULL); + return new AstIf (nodep->fileline(), + // If assertions are off, have constant propagation rip them out later + // This allows syntax errors and such to be detected normally. + (v3Global.opt.assertOn() + ? (AstNode*)(new AstCMath(nodep->fileline(), "Verilated::assertOn()", 1)) + : (AstNode*)(new AstConst(nodep->fileline(), V3Number(nodep->fileline(), 1, 0)))), + nodep, NULL); + } + + AstNode* newIfCoverageOn(AstNode* nodep) { + // Add a internal if to check coverage is on + // Don't make this a AND term, as it's unlikely to need to test this. + return new AstIf (nodep->fileline(), + // If assertions are off, have constant propagation rip them out later + // This allows syntax errors and such to be detected normally. + (v3Global.opt.coverage() + ? (AstNode*)(new AstConst(nodep->fileline(), V3Number(nodep->fileline(), 1, 1))) + : (AstNode*)(new AstConst(nodep->fileline(), V3Number(nodep->fileline(), 1, 0)))), + nodep, NULL); + } + + AstNode* newFireAssert(AstNode* nodep, const string& message) { + AstDisplay* dispp = new AstDisplay (nodep->fileline(), AstDisplayType::ERROR, message, NULL, NULL); + AstNode* bodysp = dispp; + replaceDisplay(dispp, "%%Error"); // Convert to standard DISPLAY format + bodysp->addNext(new AstStop (nodep->fileline())); + bodysp = newIfAssertOn(bodysp); return bodysp; } - void newAssertion(AstNode* nodep, AstNode* propp, AstSenTree* sentreep, const string& message) { + void newPslAssertion(AstNode* nodep, AstNode* propp, AstSenTree* sentreep, const string& message) { propp->unlinkFrBack(); sentreep->unlinkFrBack(); // @@ -114,6 +144,28 @@ private: pushDeletep(nodep); nodep=NULL; } + 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 (nodep->castVAssert()) { + 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 (nodep->castVAssert()) ifp->branchPred(AstBranchPred::UNLIKELY); + // + // Install it + nodep->replaceWith(newp); + // Bye + pushDeletep(nodep); nodep=NULL; + } + // VISITORS //========== Case assertions virtual void visit(AstCase* nodep, AstNUser*) { nodep->iterateChildren(*this); @@ -163,16 +215,34 @@ private: } // VISITORS //========== Statements + virtual void visit(AstDisplay* nodep, AstNUser*) { + nodep->iterateChildren(*this); + // Replace the special types with standard text + if (nodep->displayType()==AstDisplayType::INFO) { + replaceDisplay(nodep, "-Info"); + } else if (nodep->displayType()==AstDisplayType::WARNING) { + replaceDisplay(nodep, "%%Warning"); + } else if (nodep->displayType()==AstDisplayType::ERROR + || nodep->displayType()==AstDisplayType::FATAL) { + replaceDisplay(nodep, "%%Error"); + } + } + virtual void visit(AstPslCover* nodep, AstNUser*) { nodep->iterateChildren(*this); - newAssertion(nodep, nodep->propp(), nodep->sentreep(), nodep->name()); nodep=NULL; + newPslAssertion(nodep, nodep->propp(), nodep->sentreep(), nodep->name()); nodep=NULL; m_statAsCover++; } virtual void visit(AstPslAssert* nodep, AstNUser*) { nodep->iterateChildren(*this); - newAssertion(nodep, nodep->propp(), nodep->sentreep(), nodep->name()); nodep=NULL; + newPslAssertion(nodep, nodep->propp(), nodep->sentreep(), nodep->name()); nodep=NULL; m_statAsPsl++; } + virtual void visit(AstVAssert* nodep, AstNUser*) { + nodep->iterateChildren(*this); + newVAssertion(nodep, nodep->propp()); nodep=NULL; + m_statAsSV++; + } virtual void visit(AstModule* nodep, AstNUser*) { m_modp = nodep; @@ -203,6 +273,7 @@ public: } 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, full/parallel case", m_statAsFull); } diff --git a/src/V3Ast.cpp b/src/V3Ast.cpp index 4223af047..8e61e6a8b 100644 --- a/src/V3Ast.cpp +++ b/src/V3Ast.cpp @@ -789,7 +789,7 @@ void AstNode::dumpTreeFile(const string& filename, bool append) { if (logsp->fail()) v3fatalSrc("Can't write "<"; *logsp<<" to "<(_e)) {}; + operator en () const { return m_e; }; + bool addNewline() const { return m_e!=WRITE; } + bool needScopeTracking() const { return m_e!=DISPLAY && m_e!=WRITE; } + const char* ascii() const { + static const char* names[] = { + "display","write","info","error","warning","fatal"}; + return names[m_e];}; + }; + inline bool operator== (AstDisplayType lhs, AstDisplayType rhs) { return (lhs.m_e == rhs.m_e); } + inline bool operator== (AstDisplayType lhs, AstDisplayType::en rhs) { return (lhs.m_e == rhs); } + inline bool operator== (AstDisplayType::en lhs, AstDisplayType rhs) { return (lhs == rhs.m_e); } + +//###################################################################### + class AstParseRefExp { public: enum en { @@ -906,6 +934,7 @@ public: virtual ~AstNodePli() {} virtual string name() const { return m_text; } virtual int instrCount() const { return instrCountPli(); } + void exprsp(AstNode* nodep) { addOp1p(nodep); } // op1 = Expressions to output AstNode* exprsp() const { return op1p()->castNode(); } // op1 = Expressions to output string text() const { return m_text; } // * = Text to display void text(const string& text) { m_text=text; } diff --git a/src/V3AstNodes.h b/src/V3AstNodes.h index b773cc458..0dff4bd49 100644 --- a/src/V3AstNodes.h +++ b/src/V3AstNodes.h @@ -1236,19 +1236,19 @@ struct AstDisplay : public AstNodePli { // Parents: stmtlist // Children: file which must be a varref, MATH to print private: - char m_newline; + AstDisplayType m_displayType; public: - AstDisplay(FileLine* fileline, char newln, const string& text, AstNode* filep, AstNode* exprsp) + AstDisplay(FileLine* fileline, AstDisplayType dispType, const string& text, AstNode* filep, AstNode* exprsp) : AstNodePli (fileline, text, exprsp) { setNOp2p(filep); - m_newline = newln; + m_displayType = dispType; } virtual ~AstDisplay() {} virtual AstType type() const { return AstType::DISPLAY;} virtual AstNode* clone() { return new AstDisplay(*this); } virtual void accept(AstNVisitor& v, AstNUser* vup=NULL) { v.visit(this,vup); } - virtual string verilogKwd() const { return (filep() ? ((newline() == '\n')?"$fdisplay":"$fwrite") - : ((newline() == '\n')?"$display":"$write")); }; + virtual string verilogKwd() const { return (filep() ? (string)"$f"+(string)displayType().ascii() + : (string)"$"+(string)displayType().ascii()); } virtual bool isGateOptimizable() const { return false; } virtual bool isPredictOptimizable() const { return false; } virtual bool isSplittable() const { return false; } // SPECIAL: $display has 'visual' ordering @@ -1256,16 +1256,19 @@ public: virtual bool isUnlikely() const { return true; } virtual V3Hash sameHash() const { return V3Hash(text()); } virtual bool same(AstNode* samep) const { - return newline()==samep->castDisplay()->newline() + return displayType()==samep->castDisplay()->displayType() && text()==samep->castDisplay()->text(); } // op1 used by AstNodePli - char newline() const { return m_newline; } // * = Add a newline for $display + AstDisplayType displayType() const { return m_displayType; } + void displayType(AstDisplayType type) { m_displayType = type; } + bool addNewline() const { return displayType().addNewline(); } // * = Add a newline for $display AstNode* filep() const { return op2p(); } void filep(AstNodeVarRef* nodep) { setNOp2p(nodep); } AstNode* scopeAttrp() const { return op3p(); } AstText* scopeTextp() const { return op3p()->castText(); } void scopeAttrp(AstNode* nodep) { addOp3p(nodep); } - bool needScopeTracking() { return name().find("%m") != string::npos; } + bool needScopeTracking() { return (displayType().needScopeTracking() + || name().find("%m") != string::npos); } }; struct AstFClose : public AstNodeStmt { @@ -2617,6 +2620,30 @@ struct AstReplicate : public AstNodeBiop { virtual int instrCount() const { return widthInstrs()*2; } }; +//====================================================================== +// SysVerilog assertions + +struct AstVAssert : public AstNodeStmt { + // Verilog Assertion + // Parents: {statement list} + // Children: expression, if pass statements, if fail statements + AstVAssert(FileLine* fl, AstNode* propp, AstNode* passsp, AstNode* failsp) + : AstNodeStmt(fl) { + addOp1p(propp); + addNOp2p(passsp); + addNOp3p(failsp); + } + virtual ~AstVAssert() {} + virtual AstType type() const { return AstType::VASSERT;} + virtual AstNode* clone() { return new AstVAssert(*this); } + virtual void accept(AstNVisitor& v, AstNUser* vup=NULL) { v.visit(this,vup); } + virtual V3Hash sameHash() const { return V3Hash(); } + virtual bool same(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 +}; + //====================================================================== // PSL diff --git a/src/V3Clock.cpp b/src/V3Clock.cpp index 3e10ca83c..02569efe7 100644 --- a/src/V3Clock.cpp +++ b/src/V3Clock.cpp @@ -472,7 +472,8 @@ private: ifstmtp->addNext(new AstIf(fl, new AstLt (fl, new AstConst(fl, 100), new AstVarRef(fl, countVarp, false)), - (new AstDisplay (fl, '\n', "%%Error: Verilated model didn't converge", NULL, NULL)) + (new AstDisplay (fl, AstDisplayType::DISPLAY, + "%%Error: Verilated model didn't converge", NULL, NULL)) ->addNext(new AstStop (fl)), NULL)); untilp->addBodysp(new AstIf(fl, new AstNeq(fl, new AstConst(fl, 0), diff --git a/src/V3Descope.cpp b/src/V3Descope.cpp index dc1e19613..e40002226 100644 --- a/src/V3Descope.cpp +++ b/src/V3Descope.cpp @@ -160,8 +160,8 @@ private: } } // Not really any way the user could do this, and we'd need to come up with some return value - //newfuncp->addStmtsp(new AstDisplay (newfuncp->fileline(), - // '\n', string("%%Error: ")+name+"() called with bad scope", NULL)); + //newfuncp->addStmtsp(new AstDisplay (newfuncp->fileline(), AstDisplayType::DISPLAY, + // string("%%Error: ")+name+"() called with bad scope", NULL)); //newfuncp->addStmtsp(new AstStop (newfuncp->fileline())); if (debug()>=9) newfuncp->dumpTree(cout," newfunc: "); } else { diff --git a/src/V3EmitC.cpp b/src/V3EmitC.cpp index b65ce1bdb..603713b27 100644 --- a/src/V3EmitC.cpp +++ b/src/V3EmitC.cpp @@ -1013,7 +1013,6 @@ void EmitCStmts::displayArg(AstDisplay* dispp, AstNode** elistp, string fmt, cha void EmitCStmts::visit(AstDisplay* nodep, AstNUser*) { string vformat = nodep->text(); - bool addNewline = (nodep->newline() == '\n'); AstNode* elistp = nodep->exprsp(); // Convert Verilog display to C printf formats @@ -1076,7 +1075,7 @@ void EmitCStmts::visit(AstDisplay* nodep, AstNUser*) { if (elistp != NULL) { nodep->v3error("Extra arguments for $display format\n"); } - if (addNewline) emitDispState.pushFormat("\\n"); + if (nodep->addNewline()) emitDispState.pushFormat("\\n"); displayEmit(nodep); } diff --git a/src/V3LinkResolve.cpp b/src/V3LinkResolve.cpp index 0da121b93..e992b2876 100644 --- a/src/V3LinkResolve.cpp +++ b/src/V3LinkResolve.cpp @@ -54,6 +54,7 @@ private: // Below state needs to be preserved between each module call. AstModule* m_modp; // Current module AstNodeFTask* m_ftaskp; // Function or task we're inside + AstVAssert* m_assertp; // Current assertion //int debug() { return 9; } @@ -72,6 +73,13 @@ private: nodep->iterateChildren(*this); m_modp = NULL; } + virtual void visit(AstVAssert* nodep, AstNUser*) { + if (m_assertp) nodep->v3error("Assert not allowed under another assert"); + m_assertp = nodep; + nodep->iterateChildren(*this); + m_assertp = NULL; + } + virtual void visit(AstVar* nodep, AstNUser*) { nodep->iterateChildren(*this); if (nodep->arraysp() && nodep->isIO()) { @@ -320,6 +328,13 @@ private: virtual void visit(AstDisplay* nodep, AstNUser*) { nodep->iterateChildren(*this); if (nodep->filep()) expectDescriptor(nodep, nodep->filep()->castNodeVarRef()); + if (!m_assertp + && (nodep->displayType() == AstDisplayType::INFO + || nodep->displayType() == AstDisplayType::WARNING + || nodep->displayType() == AstDisplayType::ERROR + || nodep->displayType() == AstDisplayType::FATAL)) { + nodep->v3error(nodep->verilogKwd()+" only allowed under a assertion."); + } } virtual void visit(AstScCtor* nodep, AstNUser*) { @@ -348,6 +363,7 @@ public: LinkResolveVisitor(AstNetlist* rootp) { m_ftaskp = NULL; m_modp = NULL; + m_assertp = NULL; // rootp->accept(*this); } diff --git a/src/V3Width.cpp b/src/V3Width.cpp index 0bfc90a1f..6deb94f8a 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -575,6 +575,13 @@ private: nodep->propp()->iterateAndNext(*this,WidthVP(1,1,BOTH).p()); widthCheckReduce(nodep,"Property",nodep->propp(),1,1); // it's like a if() condition. } + virtual void visit(AstVAssert* nodep, AstNUser*) { + // TOP LEVEL NODE + nodep->propp()->iterateAndNext(*this,WidthVP(1,1,BOTH).p()); + nodep->passsp()->iterateAndNext(*this); + nodep->failsp()->iterateAndNext(*this); + widthCheckReduce(nodep,"Property",nodep->propp(),1,1); // it's like a if() condition. + } virtual void visit(AstPin* nodep, AstNUser*) { //if (debug()) nodep->dumpTree(cout,"- PinPre: "); // TOP LEVEL NODE diff --git a/src/Verilator.cpp b/src/Verilator.cpp index f16d16475..351c64066 100644 --- a/src/Verilator.cpp +++ b/src/Verilator.cpp @@ -159,13 +159,11 @@ void process () { // Assertion insertion // After we've added block coverage, but before other nasty transforms - if (v3Global.opt.assertOn() || v3Global.opt.psl()) { - V3AssertPre::assertPreAll(v3Global.rootp()); - v3Global.rootp()->dumpTreeFile(v3Global.debugFilename("assertpre.tree")); - // - V3Assert::assertAll(v3Global.rootp()); - v3Global.rootp()->dumpTreeFile(v3Global.debugFilename("assert.tree")); - } + V3AssertPre::assertPreAll(v3Global.rootp()); + v3Global.rootp()->dumpTreeFile(v3Global.debugFilename("assertpre.tree")); + // + V3Assert::assertAll(v3Global.rootp()); + v3Global.rootp()->dumpTreeFile(v3Global.debugFilename("assert.tree")); // Add top level wrapper with instance pointing to old top // Must do this after we know the width of any parameters diff --git a/src/verilog.l b/src/verilog.l index e8bb124c0..1608dadc8 100644 --- a/src/verilog.l +++ b/src/verilog.l @@ -297,9 +297,13 @@ escid \\[^ \t\f\r\n]+ /* System Tasks */ "$bits" {yylval.fileline = CRELINE(); return yD_BITS;} "$countones" {yylval.fileline = CRELINE(); return yD_COUNTONES;} + "$error" {yylval.fileline = CRELINE(); return yD_ERROR;} + "$fatal" {yylval.fileline = CRELINE(); return yD_FATAL;} + "$info" {yylval.fileline = CRELINE(); return yD_INFO;} "$isunknown" {yylval.fileline = CRELINE(); return yD_ISUNKNOWN;} "$onehot" {yylval.fileline = CRELINE(); return yD_ONEHOT;} "$onehot0" {yylval.fileline = CRELINE(); return yD_ONEHOT0;} + "$warning" {yylval.fileline = CRELINE(); return yD_WARNING;} /* Keywords */ "always_comb" {yylval.fileline = CRELINE(); return yALWAYS;} "always_ff" {yylval.fileline = CRELINE(); return yALWAYS;} @@ -395,8 +399,9 @@ escid \\[^ \t\f\r\n]+ /* SystemVerilog ONLY not PSL; different rules for PSL as specified below */ { + /* Keywords */ + "assert" {yylval.fileline = CRELINE(); return yASSERT;} /* Generic unsupported warnings */ - "assert" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented in non-PSL context: %s",yytext);} "assume" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented in non-PSL context: %s",yytext);} "before" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented in non-PSL context: %s",yytext);} "const" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented in non-PSL context: %s",yytext);} @@ -424,8 +429,8 @@ escid \\[^ \t\f\r\n]+ /* Special things */ "psl" { ; } // 'psl' may occur in middle of statement, so easier just to suppress /* Keywords */ - "assert" {yylval.fileline = CRELINE(); return yASSERT;} - "assume" {yylval.fileline = CRELINE(); return yASSERT;} //==assert + "assert" {yylval.fileline = CRELINE(); return yPSL_ASSERT;} + "assume" {yylval.fileline = CRELINE(); return yPSL_ASSERT;} //==assert "before_!" {yyerrorf("Illegal syntax, use before!_ instead of %s",yytext);} "clock" {yylval.fileline = CRELINE(); return yCLOCK;} "countones" {yylval.fileline = CRELINE(); return yD_COUNTONES;} diff --git a/src/verilog.y b/src/verilog.y index aaa15184d..b50cf9056 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -60,6 +60,11 @@ public: static AstVar* createVariable(FileLine* fileline, string name, AstRange* arrayp); static AstNode* createSupplyExpr(FileLine* fileline, string name, int value); static AstText* createTextQuoted(FileLine* fileline, string text); + static AstDisplay* createDisplayError(FileLine* fileline) { + AstDisplay* nodep = new AstDisplay(fileline,AstDisplayType::ERROR, "", NULL,NULL); + nodep->addNext(new AstStop(fileline)); + return nodep; + } static string deQuote(FileLine* fileline, string text); }; @@ -140,15 +145,20 @@ class AstSenTree; %token yREPORT "report" %token yTRUE "true" +%token yPSL_ASSERT "PSL assert" + %token yD_BITS "$bits" %token yD_C "$c" %token yD_COUNTONES "$countones" %token yD_DISPLAY "$display" +%token yD_ERROR "$error" +%token yD_FATAL "$fatal" %token yD_FCLOSE "$fclose" %token yD_FDISPLAY "$fdisplay" %token yD_FINISH "$finish" %token yD_FOPEN "$fopen" %token yD_FWRITE "$fwrite" +%token yD_INFO "$info" %token yD_ISUNKNOWN "$isunknown" %token yD_ONEHOT "$onehot" %token yD_ONEHOT0 "$onehot0" @@ -158,6 +168,7 @@ class AstSenTree; %token yD_STOP "$stop" %token yD_TIME "$time" %token yD_UNSIGNED "$unsigned" +%token yD_WARNING "$warning" %token yD_WRITE "$write" %token yVL_CLOCK "/*verilator sc_clock*/" @@ -232,7 +243,8 @@ class AstSenTree; %type defpList defpOne %type sensitivityE %type senList senitem senitemEdge -%type stmtBlock stmtList stmt stateCaseForIf +%type stmtBlock stmtList stmt labeledStmt stateCaseForIf +%type assertStmt %type beginNamed %type caseStmt %type caseList @@ -257,6 +269,7 @@ class AstSenTree; %type gateOrList gateNorList gateXorList gateXnorList %type gateBuf gateNot gateAnd gateNand gateOr gateNor gateXor gateXnor %type gateAndPinList gateOrPinList gateXorPinList +%type commaEListE %type pslStmt pslDir pslDirOne pslProp %type pslDecl @@ -652,6 +665,9 @@ stmtList: stmtBlock { $$ = $1; } ; stmt: ';' { $$ = NULL; } + | labeledStmt { $$ = $1; } + | yID ':' labeledStmt { $$ = new AstBegin($2, *$1, $3); } /*S05 block creation rule*/ + | varRefDotBit yLTE delayE expr ';' { $$ = new AstAssignDly($2,$1,$4); } | varRefDotBit '=' delayE expr ';' { $$ = new AstAssign($2,$1,$4); } | varRefDotBit '=' yD_FOPEN '(' expr ',' expr ')' ';' { $$ = new AstFOpen($3,$1,$5,$7); } @@ -666,21 +682,31 @@ stmt: ';' { $$ = NULL; } | stateCaseForIf { $$ = $1; } | taskRef ';' { $$ = $1; } - | yD_DISPLAY ';' { $$ = new AstDisplay($1,'\n',"",NULL,NULL); } - | yD_DISPLAY '(' ySTRING ')' ';' { $$ = new AstDisplay($1,'\n',*$3,NULL,NULL); } - | yD_DISPLAY '(' ySTRING ',' eList ')' ';' { $$ = new AstDisplay($1,'\n',*$3,NULL,$5); } - | yD_WRITE '(' ySTRING ')' ';' { $$ = new AstDisplay($1,'\0',*$3,NULL,NULL); } - | yD_WRITE '(' ySTRING ',' eList ')' ';' { $$ = new AstDisplay($1,'\0',*$3,NULL,$5); } - | yD_FDISPLAY '(' varRefDotBit ',' ySTRING ')' ';' { $$ = new AstDisplay($1,'\n',*$5,$3,NULL); } - | yD_FDISPLAY '(' varRefDotBit ',' ySTRING ',' eList ')' ';' { $$ = new AstDisplay($1,'\n',*$5,$3,$7); } - | yD_FWRITE '(' varRefDotBit ',' ySTRING ')' ';' { $$ = new AstDisplay($1,'\0',*$5,$3,NULL); } - | yD_FWRITE '(' varRefDotBit ',' ySTRING ',' eList ')' ';' { $$ = new AstDisplay($1,'\0',*$5,$3,$7); } + | yD_DISPLAY ';' { $$ = new AstDisplay($1,AstDisplayType::DISPLAY,"", NULL,NULL); } + | yD_DISPLAY '(' ySTRING commaEListE ')' ';' { $$ = new AstDisplay($1,AstDisplayType::DISPLAY,*$3,NULL,$4); } + | yD_WRITE '(' ySTRING commaEListE ')' ';' { $$ = new AstDisplay($1,AstDisplayType::WRITE, *$3,NULL,$4); } + | yD_FDISPLAY '(' varRefDotBit ',' ySTRING commaEListE ')' ';' { $$ = new AstDisplay($1,AstDisplayType::DISPLAY,*$5,$3,$6); } + | yD_FWRITE '(' varRefDotBit ',' ySTRING commaEListE ')' ';' { $$ = new AstDisplay($1,AstDisplayType::WRITE, *$5,$3,$6); } + | yD_INFO ';' { $$ = new AstDisplay($1,AstDisplayType::INFO, "", NULL,NULL); } + | yD_INFO '(' ySTRING commaEListE ')' ';' { $$ = new AstDisplay($1,AstDisplayType::INFO, *$3,NULL,$4); } + | yD_WARNING ';' { $$ = new AstDisplay($1,AstDisplayType::WARNING,"", NULL,NULL); } + | yD_WARNING '(' ySTRING commaEListE ')' ';' { $$ = new AstDisplay($1,AstDisplayType::WARNING,*$3,NULL,$4); } + | yD_ERROR ';' { $$ = V3Parse::createDisplayError($1); } + | yD_ERROR '(' ySTRING commaEListE ')' ';' { $$ = new AstDisplay($1,AstDisplayType::ERROR, *$3,NULL,$4); $$->addNext(new AstStop($1)); } + | yD_FATAL ';' { $$ = new AstDisplay($1,AstDisplayType::FATAL, "", NULL,NULL); $$->addNext(new AstStop($1)); } + | yD_FATAL '(' expr ')' ';' { $$ = new AstDisplay($1,AstDisplayType::FATAL, "", NULL,NULL); $$->addNext(new AstStop($1)); } + | yD_FATAL '(' expr ',' ySTRING commaEListE ')' ';' { $$ = new AstDisplay($1,AstDisplayType::FATAL, *$5,NULL,$6); $$->addNext(new AstStop($1)); } + | yD_READMEMB '(' expr ',' varRefMem ')' ';' { $$ = new AstReadMem($1,false,$3,$5,NULL,NULL); } | yD_READMEMB '(' expr ',' varRefMem ',' expr ')' ';' { $$ = new AstReadMem($1,false,$3,$5,$7,NULL); } | yD_READMEMB '(' expr ',' varRefMem ',' expr ',' expr ')' ';' { $$ = new AstReadMem($1,false,$3,$5,$7,$9); } | yD_READMEMH '(' expr ',' varRefMem ')' ';' { $$ = new AstReadMem($1,true, $3,$5,NULL,NULL); } | yD_READMEMH '(' expr ',' varRefMem ',' expr ')' ';' { $$ = new AstReadMem($1,true, $3,$5,$7,NULL); } | yD_READMEMH '(' expr ',' varRefMem ',' expr ',' expr ')' ';' { $$ = new AstReadMem($1,true, $3,$5,$7,$9); } + + ; + +labeledStmt: assertStmt { $$ = $1; } ; stateCaseForIf: caseStmt caseAttrE caseList yENDCASE { $$ = $1; $1->addItemsp($3); } @@ -692,6 +718,11 @@ stateCaseForIf: caseStmt caseAttrE caseList yENDCASE { $$ = $1; $1->addItemsp($3 ,$13);} ; +assertStmt: yASSERT '(' expr ')' stmtBlock %prec yLOWER_THAN_ELSE { $$ = new AstVAssert($1,$3,$5, V3Parse::createDisplayError($1)); } + | yASSERT '(' expr ')' yELSE stmtBlock { $$ = new AstVAssert($1,$3,NULL,$6); } + | yASSERT '(' expr ')' stmtBlock yELSE stmtBlock { $$ = new AstVAssert($1,$3,$5,$7); } + ; + caseStmt: yCASE '(' expr ')' { $$ = V3Parse::s_caseAttrp = new AstCase($1,false,$3,NULL); } | yCASEX '(' expr ')' { $$ = V3Parse::s_caseAttrp = new AstCase($1,true,$3,NULL); $1->v3warn(CASEX,"Suggest casez (with ?'s) in place of casex (with X's)\n"); } | yCASEZ '(' expr ')' { $$ = V3Parse::s_caseAttrp = new AstCase($1,true,$3,NULL); } @@ -834,6 +865,11 @@ eList: expr { $$ = $1; } | eList ',' expr { $$ = $1;$1->addNext($3); } ; +commaEListE: /* empty */ { $$ = NULL; } + | ',' eList { $$ = $2; } + ; + + // Gate declarations gateDecl: yBUF gateBufList ';' { $$ = $2; } | yNOT gateNotList ';' { $$ = $2; } @@ -1013,8 +1049,8 @@ pslDir: yID ':' pslDirOne { $$ = $3; } // ADD: Create label on $1 ; //ADD: | yRESTRICT pslSequence ';' { $$ = PSLUNSUP(new AstPslRestrict($1,$2)); } -pslDirOne: yASSERT pslProp ';' { $$ = new AstPslAssert($1,$2); } - | yASSERT pslProp yREPORT ySTRING ';' { $$ = new AstPslAssert($1,$2,*$4); } +pslDirOne: yPSL_ASSERT pslProp ';' { $$ = new AstPslAssert($1,$2); } + | yPSL_ASSERT pslProp yREPORT ySTRING ';' { $$ = new AstPslAssert($1,$2,*$4); } | yCOVER pslProp ';' { $$ = new AstPslCover($1,$2); } | yCOVER pslProp yREPORT ySTRING ';' { $$ = new AstPslCover($1,$2,*$4); } ; diff --git a/test_regress/driver.pl b/test_regress/driver.pl index 6049a96d4..ebe59cf9c 100755 --- a/test_regress/driver.pl +++ b/test_regress/driver.pl @@ -200,7 +200,7 @@ sub new { vcs_flags2 => [], # Overridden in some sim files # NC nc => 0, - nc_flags => [split(/\s+/,"+licqueue +nowarn+LIBNOU +define+nc=1 -q +assert +sv31a")], + nc_flags => [split(/\s+/,"+licqueue +nowarn+LIBNOU +define+nc=1 -q +assert +sv")], nc_flags2 => [], # Overridden in some sim files # Verilator 'v3' => 0, diff --git a/test_regress/t/t_assert_basic.pl b/test_regress/t/t_assert_basic.pl new file mode 100755 index 000000000..f4de78c1d --- /dev/null +++ b/test_regress/t/t_assert_basic.pl @@ -0,0 +1,19 @@ +#!/usr/bin/perl +if (!$::Driver) { use FindBin; exec("./driver.pl", @ARGV, $0); die; } +# $Id$ +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2003-2007 by Wilson Snyder. This program is free software; you can +# redistribute it and/or modify it under the terms of either the GNU +# General Public License or the Perl Artistic License. + +compile ( + v_flags2 => [$Last_Self->{v3}?'--assert':($Last_Self->{nc}?'+assert':'')], + ); + +execute ( + check_finished=>1, + ); + +ok(1); +1; diff --git a/test_regress/t/t_assert_basic.v b/test_regress/t/t_assert_basic.v new file mode 100644 index 000000000..c9e1ed180 --- /dev/null +++ b/test_regress/t/t_assert_basic.v @@ -0,0 +1,48 @@ +// $Id$ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed into the Public Domain, for any use, +// without warranty, 2007 by Wilson Snyder. + +module t (/*AUTOARG*/ + // Inputs + clk + ); + + input clk; + + reg toggle; + + integer cyc; initial cyc=1; + wire [7:0] cyc_copy = cyc[7:0]; + + always @ (negedge clk) begin + AssertionFalse1: assert (cyc<100); + assert (!(cyc==5) || toggle); + // FIX cover {cyc==3 || cyc==4}; + // FIX cover {cyc==9} report "DefaultClock,expect=1"; + // FIX cover {(cyc==5)->toggle} report "ToggleLogIf,expect=1"; + end + + always @ (posedge clk) begin + if (cyc!=0) begin + cyc <= cyc + 1; + toggle <= !cyc[0]; + if (cyc==9) begin +`ifdef FAILING_ASSERTIONS + assert (0) else $info; + assert (0) else $info("Info message"); + assert (0) else $info("Info message, cyc=%d", cyc); + InWarningBlock: assert (0) else $warning("Warning...."); + InErrorBlock: assert (0) else $error("Error...."); + assert (0) else $fatal(1,"Fatal...."); +`endif + end + if (cyc==10) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end + end + +endmodule diff --git a/test_regress/t/t_assert_basic_cover.pl b/test_regress/t/t_assert_basic_cover.pl new file mode 100755 index 000000000..93405bf45 --- /dev/null +++ b/test_regress/t/t_assert_basic_cover.pl @@ -0,0 +1,27 @@ +#!/usr/bin/perl +if (!$::Driver) { use FindBin; exec("./driver.pl", @ARGV, $0); die; } +# $Id$ +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2003-2007 by Wilson Snyder. This program is free software; you can +# redistribute it and/or modify it under the terms of either the GNU +# General Public License or the Perl Artistic License. + +top_filename("t/t_assert_basic.v"); + +compile ( + v_flags2 => [$Last_Self->{v3}?'--assert --sp --coverage-user':''], + ); + +execute ( + check_finished=>1, + ); + +#Needs work +print "-Info: NOT checking for coverage\n"; +#file_grep ($Last_Self->{coverage_filename}, qr/t=>'psl_cover',o=>'cover',c=>2\);/); +#file_grep ($Last_Self->{coverage_filename}, qr/DefaultClock.*,c=>1\);/); +#file_grep ($Last_Self->{coverage_filename}, qr/ToggleLogIf.*,c=>9\);/); + +ok(1); +1; diff --git a/test_regress/t/t_assert_basic_fail.pl b/test_regress/t/t_assert_basic_fail.pl new file mode 100755 index 000000000..a0333a62d --- /dev/null +++ b/test_regress/t/t_assert_basic_fail.pl @@ -0,0 +1,23 @@ +#!/usr/bin/perl +if (!$::Driver) { use FindBin; exec("./driver.pl", @ARGV, $0); die; } +# $Id$ +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2003-2007 by Wilson Snyder. This program is free software; you can +# redistribute it and/or modify it under the terms of either the GNU +# General Public License or the Perl Artistic License. + +top_filename("t/t_assert_basic.v"); + +compile ( + v_flags2 => ['+define+FAILING_ASSERTIONS', + $Last_Self->{v3}?'--assert':($Last_Self->{nc}?'+assert':'')], + fails => $Last_Self->{nc}, + ); + +execute ( + fails => 1, + ); + +ok(1); +1; diff --git a/test_regress/t/t_assert_basic_off.pl b/test_regress/t/t_assert_basic_off.pl new file mode 100755 index 000000000..52ac6bafe --- /dev/null +++ b/test_regress/t/t_assert_basic_off.pl @@ -0,0 +1,21 @@ +#!/usr/bin/perl +if (!$::Driver) { use FindBin; exec("./driver.pl", @ARGV, $0); die; } +# $Id$ +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2003-2007 by Wilson Snyder. This program is free software; you can +# redistribute it and/or modify it under the terms of either the GNU +# General Public License or the Perl Artistic License. + +top_filename("t/t_assert_basic.v"); + +compile ( + v_flags2 => [], + ); + +execute ( + check_finished=>1, + ); + +ok(1); +1;