Mario1159/verilator
1
0
Fork 0
forked from github/verilator
Code Pull Requests Releases 1 Activity

Support trivial SV assertions

Browse Source 
git-svn-id: file://localhost/svn/verilator/trunk/verilator@898 77ca24e4-aefa-0310-84f0-b9a241c72d87
This commit is contained in:
Wilson Snyder 2007-03-06 21:43:38 +00:00
parent 98282114c9
commit 79ab50d84f
19 changed files with 406 additions and 66 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
bin/verilator
View File

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

105
src/V3Assert.cpp
View File

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

2
src/V3Ast.cpp
View File

@ -789,7 +789,7 @@ void AstNode::dumpTreeFile(const string& filename, bool append) {
if (logsp->fail()) v3fatalSrc("Can't write "<<filename);
*logsp<<"Tree Dump from <e"<<dec<<editCountLast()<<">";
*logsp<<" to <e"<<dec<<editCountGbl()<<">"<<endl;
if (editCountGbl()==editCountLast() && 0) { // Off, as messes up tree diffing
if (editCountGbl()==editCountLast() && 1) { // Off, as messes up tree diffing
*logsp<<endl;
*logsp<<"No changes since last dump!\n";
} else {

29
src/V3Ast.h
View File

@ -250,6 +250,34 @@ public:
//######################################################################
class AstDisplayType {
public:
enum en {
DISPLAY,
WRITE,
INFO,
ERROR,
WARNING,
FATAL
};
enum en m_e;
inline AstDisplayType () {};
inline AstDisplayType (en _e) : m_e(_e) {};
explicit inline AstDisplayType (int _e) : m_e(static_cast<en>(_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; }

43
src/V3AstNodes.h
View File

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

3
src/V3Clock.cpp
View File

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

4
src/V3Descope.cpp
View File

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

3
src/V3EmitC.cpp
View File

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

16
src/V3LinkResolve.cpp
View File

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

7
src/V3Width.cpp
View File

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

12
src/Verilator.cpp
View File

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

11
src/verilog.l
View File

@ -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 */
<S05>{
/* 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;}

60
src/verilog.y
View File

@ -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<fileline> yREPORT "report"
%token<fileline> yTRUE "true"
%token<fileline> yPSL_ASSERT "PSL assert"
%token<fileline> yD_BITS "$bits"
%token<fileline> yD_C "$c"
%token<fileline> yD_COUNTONES "$countones"
%token<fileline> yD_DISPLAY "$display"
%token<fileline> yD_ERROR "$error"
%token<fileline> yD_FATAL "$fatal"
%token<fileline> yD_FCLOSE "$fclose"
%token<fileline> yD_FDISPLAY "$fdisplay"
%token<fileline> yD_FINISH "$finish"
%token<fileline> yD_FOPEN "$fopen"
%token<fileline> yD_FWRITE "$fwrite"
%token<fileline> yD_INFO "$info"
%token<fileline> yD_ISUNKNOWN "$isunknown"
%token<fileline> yD_ONEHOT "$onehot"
%token<fileline> yD_ONEHOT0 "$onehot0"
@ -158,6 +168,7 @@ class AstSenTree;
%token<fileline> yD_STOP "$stop"
%token<fileline> yD_TIME "$time"
%token<fileline> yD_UNSIGNED "$unsigned"
%token<fileline> yD_WARNING "$warning"
%token<fileline> yD_WRITE "$write"
%token<fileline> yVL_CLOCK "/*verilator sc_clock*/"
@ -232,7 +243,8 @@ class AstSenTree;
%type<nodep> defpList defpOne
%type<sentreep> sensitivityE
%type<senitemp> senList senitem senitemEdge
%type<nodep> stmtBlock stmtList stmt stateCaseForIf
%type<nodep> stmtBlock stmtList stmt labeledStmt stateCaseForIf
%type<nodep> assertStmt
%type<beginp> beginNamed
%type<casep> caseStmt
%type<caseitemp> caseList
@ -257,6 +269,7 @@ class AstSenTree;
%type<nodep> gateOrList gateNorList gateXorList gateXnorList
%type<assignwp> gateBuf gateNot gateAnd gateNand gateOr gateNor gateXor gateXnor
%type<nodep> gateAndPinList gateOrPinList gateXorPinList
%type<nodep> commaEListE
%type<nodep> pslStmt pslDir pslDirOne pslProp
%type<nodep> 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); }
;

2
test_regress/driver.pl
View File

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

19
test_regress/t/t_assert_basic.pl Executable file
View File

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

48
test_regress/t/t_assert_basic.v Normal file
View File

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

27
test_regress/t/t_assert_basic_cover.pl Executable file
View File

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

23
test_regress/t/t_assert_basic_fail.pl Executable file
View File

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

21
test_regress/t/t_assert_basic_off.pl Executable file
View File

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