Support SystemVerilog "cover property" statements.
This commit is contained in:
parent
a76ae67a81
commit
500dc2170f
2
Changes
2
Changes
|
|
@ -5,6 +5,8 @@ indicates the contributor was also the author of the fix; Thanks!
|
|||
|
||||
* Verilator 3.6***
|
||||
|
||||
*** Support SystemVerilog "cover property" statements.
|
||||
|
||||
*** When warnings are disabled on signals that are flattened out, disable
|
||||
the warnings on the signal(s) that replace it.
|
||||
|
||||
|
|
|
|||
|
|
@ -1050,7 +1050,8 @@ always_ff, always_latch, do-while, and final.
|
|||
|
||||
It also supports .name and .* interconnection.
|
||||
|
||||
Verilator partially supports assert.
|
||||
Verilator partially supports concurrent assert and cover statements; see
|
||||
the enclosed coverage tests for the syntax which is allowed.
|
||||
|
||||
=head1 SUGAR/PSL SUPPORT
|
||||
|
||||
|
|
|
|||
|
|
@ -1,16 +1,5 @@
|
|||
#!/usr/bin/perl -w
|
||||
######################################################################
|
||||
#
|
||||
# Copyright 2005-2008 by Wilson Snyder <wsnyder@wsnyder.org>. This
|
||||
# program is free software; you can redistribute it and/or modify it under
|
||||
# the terms of either the GNU Lesser General Public License or the Perl
|
||||
# Artistic License.
|
||||
#
|
||||
# This program is distributed in the hope that it will be useful,
|
||||
# but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
# GNU General Public License for more details.
|
||||
#
|
||||
# See copyright, etc in below POD section.
|
||||
######################################################################
|
||||
|
||||
require 5.006_001;
|
||||
|
|
|
|||
|
|
@ -1,16 +1,5 @@
|
|||
#!/usr/bin/perl -w
|
||||
######################################################################
|
||||
#
|
||||
# Copyright 2005-2008 by Wilson Snyder <wsnyder@wsnyder.org>. This
|
||||
# program is free software; you can redistribute it and/or modify it under
|
||||
# the terms of either the GNU Lesser General Public License or the Perl
|
||||
# Artistic License.
|
||||
#
|
||||
# This program is distributed in the hope that it will be useful,
|
||||
# but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
# GNU General Public License for more details.
|
||||
#
|
||||
# See copyright, etc in below POD section.
|
||||
######################################################################
|
||||
|
||||
require 5.006_001;
|
||||
|
|
|
|||
|
|
@ -0,0 +1,58 @@
|
|||
#!/usr/bin/perl -w
|
||||
# See copyright, etc in below POD section.
|
||||
######################################################################
|
||||
|
||||
require 5.006_001;
|
||||
use strict;
|
||||
|
||||
#======================================================================
|
||||
# main
|
||||
|
||||
delete $ENV{MODULE_VERSION};
|
||||
_setup_modules();
|
||||
module('add','cadence_verif');
|
||||
exec('iccr',@ARGV);
|
||||
|
||||
#######################################################################
|
||||
# Modules package
|
||||
|
||||
sub _setup_modules {
|
||||
# Load the 'module' command into the environment
|
||||
my $init = "/sicortex/$ENV{DIRPROJECT_ARCH}/lib/Modules/default/init/perl";
|
||||
(-f $init) or die "%Error: Script not found: $init,";
|
||||
require $init;
|
||||
}
|
||||
|
||||
#######################################################################
|
||||
__END__
|
||||
|
||||
=pod
|
||||
|
||||
=head1 NAME
|
||||
|
||||
invoke_iccr - Invoke tool under "modules" command
|
||||
|
||||
=head1 SYNOPSIS
|
||||
|
||||
invoke_iccr {ncv arguments}
|
||||
|
||||
=head1 DESCRIPTION
|
||||
|
||||
=head1 DISTRIBUTION
|
||||
|
||||
Copyright 2007-2008 by Wilson Snyder. This package is free software; you
|
||||
can redistribute it and/or modify it under the terms of either the GNU
|
||||
Lesser General Public License or the Perl Artistic License.
|
||||
|
||||
=head1 AUTHORS
|
||||
|
||||
Wilson Snyder <wsnyder@wsnyder.org>
|
||||
|
||||
=head1 SEE ALSO
|
||||
|
||||
=cut
|
||||
|
||||
######################################################################
|
||||
### Local Variables:
|
||||
### compile-command: "./invoke_iccr -help"
|
||||
### End:
|
||||
|
|
@ -1,16 +1,5 @@
|
|||
#!/usr/bin/perl -w
|
||||
######################################################################
|
||||
#
|
||||
# Copyright 2007-2008 by Wilson Snyder <wsnyder@wsnyder.org>. This
|
||||
# program is free software; you can redistribute it and/or modify it under
|
||||
# the terms of either the GNU Lesser General Public License or the Perl
|
||||
# Artistic License.
|
||||
#
|
||||
# This program is distributed in the hope that it will be useful,
|
||||
# but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
# GNU General Public License for more details.
|
||||
#
|
||||
# See copyright, etc in below POD section.
|
||||
######################################################################
|
||||
|
||||
require 5.006_001;
|
||||
|
|
|
|||
|
|
@ -1,16 +1,5 @@
|
|||
#!/usr/bin/perl -w
|
||||
######################################################################
|
||||
#
|
||||
# Copyright 2005-2008 by Wilson Snyder <wsnyder@wsnyder.org>. This
|
||||
# program is free software; you can redistribute it and/or modify it under
|
||||
# the terms of either the GNU Lesser General Public License or the Perl
|
||||
# Artistic License.
|
||||
#
|
||||
# This program is distributed in the hope that it will be useful,
|
||||
# but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
# GNU General Public License for more details.
|
||||
#
|
||||
# See copyright, etc in below POD section.
|
||||
######################################################################
|
||||
|
||||
require 5.006_001;
|
||||
|
|
|
|||
|
|
@ -43,6 +43,7 @@ private:
|
|||
|
||||
// STATE
|
||||
AstModule* m_modp; // Last module
|
||||
AstBegin* m_beginp; // Last begin
|
||||
V3Double0 m_statAsCover; // Statistic tracking
|
||||
V3Double0 m_statAsPsl; // Statistic tracking
|
||||
V3Double0 m_statAsFull; // Statistic tracking
|
||||
|
|
@ -100,9 +101,11 @@ private:
|
|||
return bodysp;
|
||||
}
|
||||
|
||||
void newPslAssertion(AstNode* nodep, AstNode* propp, AstSenTree* sentreep, const string& message) {
|
||||
void newPslAssertion(AstNode* nodep, AstNode* propp, AstSenTree* sentreep,
|
||||
AstNode* stmtsp, const string& message) {
|
||||
propp->unlinkFrBack();
|
||||
sentreep->unlinkFrBack();
|
||||
if (stmtsp) stmtsp->unlinkFrBack();
|
||||
//
|
||||
AstNode* bodysp = NULL;
|
||||
bool selfDestruct = false;
|
||||
|
|
@ -126,6 +129,7 @@ private:
|
|||
} else {
|
||||
nodep->v3fatalSrc("Unknown node type");
|
||||
}
|
||||
if (stmtsp) bodysp = bodysp->addNext(stmtsp);
|
||||
AstIf* ifp = new AstIf (nodep->fileline(), propp, bodysp, NULL);
|
||||
bodysp = ifp;
|
||||
if (nodep->castPslAssert()) ifp->branchPred(AstBranchPred::UNLIKELY);
|
||||
|
|
@ -232,12 +236,15 @@ private:
|
|||
|
||||
virtual void visit(AstPslCover* nodep, AstNUser*) {
|
||||
nodep->iterateChildren(*this);
|
||||
newPslAssertion(nodep, nodep->propp(), nodep->sentreep(), nodep->name()); nodep=NULL;
|
||||
if (m_beginp && nodep->name() == "") nodep->name(m_beginp->name());
|
||||
newPslAssertion(nodep, nodep->propp(), nodep->sentreep(),
|
||||
nodep->stmtsp(), nodep->name()); nodep=NULL;
|
||||
m_statAsCover++;
|
||||
}
|
||||
virtual void visit(AstPslAssert* nodep, AstNUser*) {
|
||||
nodep->iterateChildren(*this);
|
||||
newPslAssertion(nodep, nodep->propp(), nodep->sentreep(), nodep->name()); nodep=NULL;
|
||||
newPslAssertion(nodep, nodep->propp(), nodep->sentreep(),
|
||||
NULL, nodep->name()); nodep=NULL;
|
||||
m_statAsPsl++;
|
||||
}
|
||||
virtual void visit(AstVAssert* nodep, AstNUser*) {
|
||||
|
|
@ -253,6 +260,16 @@ private:
|
|||
// Reset defaults
|
||||
m_modp = NULL;
|
||||
}
|
||||
virtual void visit(AstBegin* nodep, AstNUser*) {
|
||||
// This code is needed rather than a visitor in V3Begin,
|
||||
// because V3Assert is called before V3Begin
|
||||
AstBegin* lastp = m_beginp;
|
||||
{
|
||||
m_beginp = nodep;
|
||||
nodep->iterateChildren(*this);
|
||||
}
|
||||
m_beginp = lastp;
|
||||
}
|
||||
|
||||
// VISITORS //========== Temporal Layer
|
||||
|
||||
|
|
@ -268,6 +285,7 @@ private:
|
|||
public:
|
||||
// CONSTRUCTORS
|
||||
AssertVisitor(AstNetlist* nodep) {
|
||||
m_beginp = NULL;
|
||||
m_modp = NULL;
|
||||
// Process
|
||||
AstNode::userClearTree(); // userp() used on entire tree
|
||||
|
|
|
|||
|
|
@ -60,6 +60,9 @@ private:
|
|||
if (!senip) nodep->v3error("Unsupported: Unclocked assertion");
|
||||
return newp;
|
||||
}
|
||||
void clearAssertInfo() {
|
||||
m_senip = NULL;
|
||||
}
|
||||
|
||||
// VISITORS //========== Statements
|
||||
virtual void visit(AstPslDefClock* nodep, AstNUser*) {
|
||||
|
|
@ -70,28 +73,48 @@ private:
|
|||
nodep->unlinkFrBack();
|
||||
pushDeletep(nodep); nodep=NULL;
|
||||
}
|
||||
virtual void visit(AstClocking* nodep, AstNUser*) {
|
||||
UINFO(8," CLOCKING"<<nodep<<endl);
|
||||
AstSenItem* lastp = m_seniDefaultp;
|
||||
{
|
||||
// Store the new default clock only in this scope
|
||||
m_seniDefaultp = nodep->sensesp();
|
||||
nodep->iterateChildren(*this);
|
||||
}
|
||||
m_seniDefaultp = lastp;
|
||||
// Trash it
|
||||
nodep->replaceWith(nodep->bodysp()->unlinkFrBack());
|
||||
pushDeletep(nodep); nodep=NULL;
|
||||
}
|
||||
|
||||
virtual void visit(AstPslCover* nodep, AstNUser*) {
|
||||
// Prep
|
||||
m_senip = NULL;
|
||||
if (nodep->sentreep()) return; // Already processed
|
||||
clearAssertInfo();
|
||||
nodep->iterateChildren(*this);
|
||||
nodep->sentreep(newSenTree(nodep));
|
||||
m_senip = NULL;
|
||||
clearAssertInfo();
|
||||
}
|
||||
virtual void visit(AstPslAssert* nodep, AstNUser*) {
|
||||
// Prep
|
||||
m_senip = NULL;
|
||||
if (nodep->sentreep()) return; // Already processed
|
||||
clearAssertInfo();
|
||||
nodep->iterateChildren(*this);
|
||||
nodep->sentreep(newSenTree(nodep));
|
||||
m_senip = NULL;
|
||||
clearAssertInfo();
|
||||
}
|
||||
virtual void visit(AstPslClocked* nodep, AstNUser*) {
|
||||
nodep->iterateChildren(*this);
|
||||
if (m_senip) {
|
||||
nodep->v3error("Unsupported: Only one PSL clock allowed per assertion\n");
|
||||
}
|
||||
// Unlink and just keep a pointer to it, convert to sentree as needed
|
||||
// Block is the new expression to evaluate
|
||||
AstNode* blockp = nodep->propp()->unlinkFrBack();
|
||||
if (nodep->disablep()) {
|
||||
blockp = new AstAnd(nodep->disablep()->fileline(),
|
||||
new AstNot(nodep->disablep()->fileline(),
|
||||
nodep->disablep()->unlinkFrBack()),
|
||||
blockp);
|
||||
}
|
||||
// Unlink and just keep a pointer to it, convert to sentree as needed
|
||||
m_senip = nodep->sensesp();
|
||||
nodep->replaceWith(blockp);
|
||||
pushDeletep(nodep); nodep=NULL;
|
||||
|
|
@ -108,8 +131,8 @@ private:
|
|||
public:
|
||||
// CONSTRUCTORS
|
||||
AssertPreVisitor(AstNetlist* nodep) {
|
||||
m_senip = NULL;
|
||||
m_seniDefaultp = NULL;
|
||||
clearAssertInfo();
|
||||
// Process
|
||||
nodep->accept(*this);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -2830,6 +2830,27 @@ struct AstVAssert : public AstNodeStmt {
|
|||
AstNode* failsp() const { return op3p(); } // op3 = if fails
|
||||
};
|
||||
|
||||
//======================================================================
|
||||
// Assertions
|
||||
|
||||
struct AstClocking : public AstNode {
|
||||
// Set default clock region
|
||||
// Parents: MODULE
|
||||
// Children: Assertions
|
||||
public:
|
||||
AstClocking(FileLine* fl, AstSenItem* sensesp, AstNode* bodysp)
|
||||
: AstNode(fl) {
|
||||
addOp1p(sensesp);
|
||||
addNOp2p(bodysp);
|
||||
}
|
||||
virtual ~AstClocking() {}
|
||||
virtual AstType type() const { return AstType::CLOCKING;}
|
||||
virtual AstNode* clone() { return new AstClocking(*this); }
|
||||
virtual void accept(AstNVisitor& v, AstNUser* vup=NULL) { v.visit(this,vup); }
|
||||
AstSenItem* sensesp() const { return op1p()->castSenItem(); } // op1 = Sensitivity list
|
||||
AstNode* bodysp() const { return op2p(); } // op2 = Body
|
||||
};
|
||||
|
||||
//======================================================================
|
||||
// PSL
|
||||
|
||||
|
|
@ -2854,17 +2875,19 @@ struct AstPslClocked : public AstNode {
|
|||
// Parents: ASSERT|COVER (property)
|
||||
// Children: SENITEM, Properties
|
||||
public:
|
||||
AstPslClocked(FileLine* fl, AstSenItem* sensesp, AstNode* propp)
|
||||
AstPslClocked(FileLine* fl, AstSenItem* sensesp, AstNode* disablep, AstNode* propp)
|
||||
: AstNode(fl) {
|
||||
addNOp1p(sensesp);
|
||||
addOp2p(propp);
|
||||
addNOp2p(disablep);
|
||||
addOp3p(propp);
|
||||
}
|
||||
virtual ~AstPslClocked() {}
|
||||
virtual AstType type() const { return AstType::PSLCLOCKED;}
|
||||
virtual AstNode* clone() { return new AstPslClocked(*this); }
|
||||
virtual void accept(AstNVisitor& v, AstNUser* vup=NULL) { v.visit(this,vup); }
|
||||
AstSenItem* sensesp() const { return op1p()->castSenItem(); } // op1 = Sensitivity list
|
||||
AstNode* propp() const { return op2p(); } // op2 = property
|
||||
AstNode* disablep() const { return op2p(); } // op2 = disable
|
||||
AstNode* propp() const { return op3p(); } // op3 = property
|
||||
};
|
||||
|
||||
struct AstPslAssert : public AstNodeStmt {
|
||||
|
|
@ -2898,10 +2921,11 @@ struct AstPslCover : public AstNodeStmt {
|
|||
private:
|
||||
string m_name; // Name to report
|
||||
public:
|
||||
AstPslCover(FileLine* fl, AstNode* propp, const string& name="")
|
||||
AstPslCover(FileLine* fl, AstNode* propp, AstNode* stmtsp, const string& name="")
|
||||
: AstNodeStmt(fl)
|
||||
, m_name(name) {
|
||||
addOp1p(propp);
|
||||
addNOp4p(stmtsp);
|
||||
}
|
||||
virtual ~AstPslCover() {}
|
||||
virtual AstType type() const { return AstType::PSLCOVER;}
|
||||
|
|
@ -2910,11 +2934,13 @@ public:
|
|||
virtual string name() const { return m_name; } // * = Var name
|
||||
virtual V3Hash sameHash() const { return V3Hash(name()); }
|
||||
virtual bool same(AstNode* samep) const { return samep->name() == name(); }
|
||||
void name(const string& flag) { m_name = flag; }
|
||||
AstNode* propp() const { return op1p(); } // op1 = property
|
||||
AstSenTree* sentreep() const { return op2p()->castSenTree(); } // op2 = clock domain
|
||||
void sentreep(AstSenTree* sentreep) { addOp2p(sentreep); } // op2 = clock domain
|
||||
AstNode* coverincp() const { return op3p(); } // op3 = coverage node
|
||||
void coverincp(AstCoverInc* nodep) { addOp3p(nodep); } // op3 = coverage node
|
||||
AstNode* stmtsp() const { return op4p(); } // op4 = statements
|
||||
};
|
||||
|
||||
//======================================================================
|
||||
|
|
|
|||
|
|
@ -462,7 +462,11 @@ private:
|
|||
}
|
||||
virtual void visit(AstPslClocked* nodep, AstNUser*) {
|
||||
nodep->propp()->iterateAndNext(*this,WidthVP(1,1,BOTH).p());
|
||||
nodep->sensesp()->iterate(*this);
|
||||
nodep->sensesp()->iterateAndNext(*this);
|
||||
if (nodep->disablep()) {
|
||||
nodep->disablep()->iterateAndNext(*this,WidthVP(1,1,BOTH).p());
|
||||
widthCheckReduce(nodep,"Disable",nodep->disablep(),1,1); // it's like a if() condition.
|
||||
}
|
||||
widthCheckReduce(nodep,"Property",nodep->propp(),1,1); // it's like a if() condition.
|
||||
nodep->width(1,1);
|
||||
}
|
||||
|
|
@ -635,6 +639,7 @@ private:
|
|||
virtual void visit(AstPslCover* nodep, AstNUser*) {
|
||||
// TOP LEVEL NODE
|
||||
nodep->propp()->iterateAndNext(*this,WidthVP(1,1,BOTH).p());
|
||||
nodep->stmtsp()->iterateChildren(*this,WidthVP(ANYSIZE,0,BOTH).p());
|
||||
widthCheckReduce(nodep,"Property",nodep->propp(),1,1); // it's like a if() condition.
|
||||
}
|
||||
virtual void visit(AstPslAssert* nodep, AstNUser*) {
|
||||
|
|
|
|||
|
|
@ -187,6 +187,7 @@ escid \\[^ \t\f\r\n]+
|
|||
"casez" {yylval.fileline = CRELINE(); return yCASEZ;}
|
||||
"default" {yylval.fileline = CRELINE(); return yDEFAULT;}
|
||||
"defparam" {yylval.fileline = CRELINE(); return yDEFPARAM;}
|
||||
"disable" {yylval.fileline = CRELINE(); return yDISABLE;}
|
||||
"edge" {yylval.fileline = CRELINE(); return yaTIMINGSPEC;}
|
||||
"else" {yylval.fileline = CRELINE(); return yELSE;}
|
||||
"end" {yylval.fileline = CRELINE(); return yEND;}
|
||||
|
|
@ -243,7 +244,6 @@ escid \\[^ \t\f\r\n]+
|
|||
"bufif1" {yyerrorf("Unsupported: Verilog 1995 reserved word not implemented: %s",yytext);}
|
||||
"cmos" {yyerrorf("Unsupported: Verilog 1995 reserved word not implemented: %s",yytext);}
|
||||
"deassign" {yyerrorf("Unsupported: Verilog 1995 reserved word not implemented: %s",yytext);}
|
||||
"disable" {yyerrorf("Unsupported: Verilog 1995 reserved word not implemented: %s",yytext);}
|
||||
"endprimitive" {yyerrorf("Unsupported: Verilog 1995 reserved word not implemented: %s",yytext);}
|
||||
"endtable" {yyerrorf("Unsupported: Verilog 1995 reserved word not implemented: %s",yytext);}
|
||||
"event" {yyerrorf("Unsupported: Verilog 1995 reserved word not implemented: %s",yytext);}
|
||||
|
|
@ -349,8 +349,12 @@ escid \\[^ \t\f\r\n]+
|
|||
"always_comb" {yylval.fileline = CRELINE(); return yALWAYS;}
|
||||
"always_ff" {yylval.fileline = CRELINE(); return yALWAYS;}
|
||||
"always_latch" {yylval.fileline = CRELINE(); return yALWAYS;}
|
||||
"clocking" {yylval.fileline = CRELINE(); return yCLOCKING;}
|
||||
"do" {yylval.fileline = CRELINE(); return yDO;}
|
||||
"endclocking" {yylval.fileline = CRELINE(); return yENDCLOCKING;}
|
||||
"endproperty" {yylval.fileline = CRELINE(); return yENDPROPERTY;}
|
||||
"final" {yylval.fileline = CRELINE(); return yFINAL;}
|
||||
"iff" {yylval.fileline = CRELINE(); return yIFF;}
|
||||
"static" {yylval.fileline = CRELINE(); return ySTATIC;}
|
||||
/* Generic unsupported warnings */
|
||||
/* Note assert_strobe was in SystemVerilog 3.1, but removed for SystemVerilog 2005 */
|
||||
|
|
@ -363,7 +367,6 @@ escid \\[^ \t\f\r\n]+
|
|||
"byte" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"chandle" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"class" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"clocking" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"constraint" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"context" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"continue" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
|
|
@ -372,12 +375,10 @@ escid \\[^ \t\f\r\n]+
|
|||
"cross" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"dist" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"endclass" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"endclocking" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"endgroup" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"endinterface" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"endpackage" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"endprogram" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"endproperty" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"endsequence" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"enum" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"expect" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
|
|
@ -387,7 +388,6 @@ escid \\[^ \t\f\r\n]+
|
|||
"first_match" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"foreach" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"forkjoin" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"iff" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"ignore_bins" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"illegal_bins" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
"import" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext);}
|
||||
|
|
@ -442,12 +442,12 @@ escid \\[^ \t\f\r\n]+
|
|||
<S05>{
|
||||
/* Keywords */
|
||||
"assert" {yylval.fileline = CRELINE(); return yASSERT;}
|
||||
"cover" {yylval.fileline = CRELINE(); return yCOVER;}
|
||||
"property" {yylval.fileline = CRELINE(); return yPROPERTY;}
|
||||
/* Generic unsupported warnings */
|
||||
"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);}
|
||||
"cover" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented in non-PSL context: %s",yytext);}
|
||||
"property" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented in non-PSL context: %s",yytext);}
|
||||
"sequence" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented in non-PSL context: %s",yytext);}
|
||||
"union" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented in non-PSL context: %s",yytext);}
|
||||
"within" {yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented in non-PSL context: %s",yytext);}
|
||||
|
|
@ -473,14 +473,14 @@ escid \\[^ \t\f\r\n]+
|
|||
"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;}
|
||||
"clock" {yylval.fileline = CRELINE(); return yPSL_CLOCK;}
|
||||
"countones" {yylval.fileline = CRELINE(); return yD_COUNTONES;}
|
||||
"cover" {yylval.fileline = CRELINE(); return yCOVER;}
|
||||
"cover" {yylval.fileline = CRELINE(); return yPSL_COVER;}
|
||||
"isunknown" {yylval.fileline = CRELINE(); return yD_ISUNKNOWN;}
|
||||
"onehot" {yylval.fileline = CRELINE(); return yD_ONEHOT; }
|
||||
"onehot0" {yylval.fileline = CRELINE(); return yD_ONEHOT0; }
|
||||
"until_!" {yyerrorf("Illegal syntax, use until!_ instead of %s",yytext);}
|
||||
"report" {yylval.fileline = CRELINE(); return yREPORT; }
|
||||
"report" {yylval.fileline = CRELINE(); return yPSL_REPORT; }
|
||||
"true" {yylval.fileline = CRELINE(); return yTRUE; }
|
||||
/* Generic unsupported warnings */
|
||||
/*"A" {yyerrorf("Unsupported: PSL branching reserved word not implemented: %s",yytext);} */
|
||||
|
|
|
|||
|
|
@ -163,17 +163,20 @@ class AstSenTree;
|
|||
%token<fileline> yCASE "case"
|
||||
%token<fileline> yCASEX "casex"
|
||||
%token<fileline> yCASEZ "casez"
|
||||
%token<fileline> yCLOCK "clock"
|
||||
%token<fileline> yCLOCKING "clocking"
|
||||
%token<fileline> yCOVER "cover"
|
||||
%token<fileline> yDEFAULT "default"
|
||||
%token<fileline> yDEFPARAM "defparam"
|
||||
%token<fileline> yDISABLE "disable"
|
||||
%token<fileline> yDO "do"
|
||||
%token<fileline> yELSE "else"
|
||||
%token<fileline> yEND "end"
|
||||
%token<fileline> yENDCASE "endcase"
|
||||
%token<fileline> yENDCLOCKING "endclocking"
|
||||
%token<fileline> yENDFUNCTION "endfunction"
|
||||
%token<fileline> yENDGENERATE "endgenerate"
|
||||
%token<fileline> yENDMODULE "endmodule"
|
||||
%token<fileline> yENDPROPERTY "endproperty"
|
||||
%token<fileline> yENDSPECIFY "endspecify"
|
||||
%token<fileline> yENDTASK "endtask"
|
||||
%token<fileline> yFINAL "final"
|
||||
|
|
@ -182,6 +185,7 @@ class AstSenTree;
|
|||
%token<fileline> yGENERATE "generate"
|
||||
%token<fileline> yGENVAR "genvar"
|
||||
%token<fileline> yIF "if"
|
||||
%token<fileline> yIFF "iff"
|
||||
%token<fileline> yINITIAL "initial"
|
||||
%token<fileline> yINOUT "inout"
|
||||
%token<fileline> yINPUT "input"
|
||||
|
|
@ -196,9 +200,8 @@ class AstSenTree;
|
|||
%token<fileline> yOUTPUT "output"
|
||||
%token<fileline> yPARAMETER "parameter"
|
||||
%token<fileline> yPOSEDGE "posedge"
|
||||
%token<fileline> yPSL "psl"
|
||||
%token<fileline> yPROPERTY "property"
|
||||
%token<fileline> yREG "reg"
|
||||
%token<fileline> yREPORT "report"
|
||||
%token<fileline> ySCALARED "scalared"
|
||||
%token<fileline> ySIGNED "signed"
|
||||
%token<fileline> ySPECIFY "specify"
|
||||
|
|
@ -248,7 +251,11 @@ class AstSenTree;
|
|||
%token<fileline> yD_WARNING "$warning"
|
||||
%token<fileline> yD_WRITE "$write"
|
||||
|
||||
%token<fileline> yPSL "psl"
|
||||
%token<fileline> yPSL_ASSERT "PSL assert"
|
||||
%token<fileline> yPSL_CLOCK "PSL clock"
|
||||
%token<fileline> yPSL_COVER "PSL cover"
|
||||
%token<fileline> yPSL_REPORT "PSL report"
|
||||
|
||||
%token<fileline> yVL_CLOCK "/*verilator sc_clock*/"
|
||||
%token<fileline> yVL_CLOCK_ENABLE "/*verilator clock_enable*/"
|
||||
|
|
@ -628,6 +635,8 @@ modOrGenItem<nodep>:
|
|||
| varDecl { $$ = $1; }
|
||||
//No: | tableDecl // Unsupported
|
||||
| pslStmt { $$ = $1; }
|
||||
| concurrent_assertion_item { $$ = $1; } // IEEE puts in modItem; seems silly
|
||||
| clocking_declaration { $$ = $1; }
|
||||
;
|
||||
|
||||
//************************************************
|
||||
|
|
@ -1421,6 +1430,39 @@ labeledStmt<nodep>:
|
|||
assertStmt { $$ = $1; }
|
||||
;
|
||||
|
||||
clocking_declaration<nodep>: // IEEE: clocking_declaration (INCOMPLETE)
|
||||
yDEFAULT yCLOCKING '@' '(' senitemEdge ')' ';' clocking_item yENDCLOCKING
|
||||
{ $$ = new AstClocking($1, $5, $8); }
|
||||
;
|
||||
|
||||
clocking_item<nodep>: // IEEE: clocking_item (INCOMPLETE)
|
||||
concurrent_assertion_item { $$ = $1; }
|
||||
| clocking_item concurrent_assertion_item { $$ = $1->addNext($2); }
|
||||
;
|
||||
|
||||
concurrent_assertion_item<nodep>: // IEEE: concurrent_assertion_item (complete)
|
||||
concurrent_assertion_statement { $$ = $1; }
|
||||
| yaID ':' concurrent_assertion_statement { $$ = new AstBegin($2,*$1,$3); }
|
||||
;
|
||||
|
||||
concurrent_assertion_statement<nodep>: // IEEE: concurrent_assertion_statement (INCOMPLETE)
|
||||
cover_property_statement { $$ = $1; }
|
||||
;
|
||||
|
||||
cover_property_statement<nodep>: // IEEE: cover_property_statement (complete)
|
||||
yCOVER yPROPERTY '(' property_spec ')' stmtBlock { $$ = new AstPslCover($1,$4,$6); }
|
||||
;
|
||||
|
||||
property_spec<nodep>: // IEEE: property_spec
|
||||
'@' '(' senitemEdge ')' property_spec_disable expr { $$ = new AstPslClocked($1,$3,$5,$6); }
|
||||
| property_spec_disable expr { $$ = new AstPslClocked(CRELINE(),NULL,$1,$2); }
|
||||
;
|
||||
|
||||
property_spec_disable<nodep>:
|
||||
/* empty */ { $$ = NULL; }
|
||||
| yDISABLE yIFF '(' expr ')' { $$ = $4; }
|
||||
;
|
||||
|
||||
assertStmt<nodep>:
|
||||
yASSERT '(' expr ')' stmtBlock %prec prLOWER_THAN_ELSE { $$ = new AstVAssert($1,$3,$5, V3Parse::createDisplayError($1)); }
|
||||
| yASSERT '(' expr ')' yELSE stmtBlock { $$ = new AstVAssert($1,$3,NULL,$6); }
|
||||
|
|
@ -1436,21 +1478,20 @@ pslStmt<nodep>:
|
|||
;
|
||||
|
||||
pslDir<nodep>:
|
||||
yaID ':' pslDirOne { $$ = $3; } // ADD: Create label on $1
|
||||
yaID ':' pslDirOne { $$ = $3; }
|
||||
| pslDirOne { $$ = $1; }
|
||||
;
|
||||
|
||||
//ADD: | yRESTRICT pslSequence ';' { $$ = PSLUNSUP(new AstPslRestrict($1,$2)); }
|
||||
pslDirOne<nodep>:
|
||||
yPSL_ASSERT pslProp ';' { $$ = new AstPslAssert($1,$2); }
|
||||
| yPSL_ASSERT pslProp yREPORT yaSTRING ';' { $$ = new AstPslAssert($1,$2,*$4); }
|
||||
| yCOVER pslProp ';' { $$ = new AstPslCover($1,$2); }
|
||||
| yCOVER pslProp yREPORT yaSTRING ';' { $$ = new AstPslCover($1,$2,*$4); }
|
||||
yPSL_ASSERT pslProp ';' { $$ = new AstPslAssert($1,$2); }
|
||||
| yPSL_ASSERT pslProp yPSL_REPORT yaSTRING ';' { $$ = new AstPslAssert($1,$2,*$4); }
|
||||
| yPSL_COVER pslProp ';' { $$ = new AstPslCover($1,$2,NULL); }
|
||||
| yPSL_COVER pslProp yPSL_REPORT yaSTRING ';' { $$ = new AstPslCover($1,$2,NULL,*$4); }
|
||||
;
|
||||
|
||||
pslDecl<nodep>:
|
||||
yDEFAULT yCLOCK '=' senitemEdge ';' { $$ = new AstPslDefClock($3, $4); }
|
||||
| yDEFAULT yCLOCK '=' '(' senitemEdge ')' ';' { $$ = new AstPslDefClock($3, $5); }
|
||||
yDEFAULT yPSL_CLOCK '=' senitemEdge ';' { $$ = new AstPslDefClock($3, $4); }
|
||||
| yDEFAULT yPSL_CLOCK '=' '(' senitemEdge ')' ';' { $$ = new AstPslDefClock($3, $5); }
|
||||
;
|
||||
|
||||
//************************************************
|
||||
|
|
@ -1459,18 +1500,13 @@ pslDecl<nodep>:
|
|||
|
||||
pslProp<nodep>:
|
||||
pslSequence { $$ = $1; }
|
||||
| pslSequence '@' %prec prPSLCLK '(' senitemEdge ')' { $$ = new AstPslClocked($2, $4, $1); } // or pslSequence @ ...?
|
||||
| pslSequence '@' %prec prPSLCLK '(' senitemEdge ')' { $$ = new AstPslClocked($2,$4,NULL,$1); } // or pslSequence @ ...?
|
||||
;
|
||||
|
||||
//ADD: | pslCallSeq { $$ = PSLUNSUP($1); }
|
||||
//ADD: | pslRepeat { $$ = PSLUNSUP($1); }
|
||||
pslSequence<nodep>:
|
||||
yPSL_BRA pslSere yPSL_KET { $$ = $2; }
|
||||
;
|
||||
|
||||
//ADD: | pslSere ';' pslSere %prec prPSLCONC { $$ = PSLUNSUP(new AstPslSeqConcat($2, $1, $3)); }
|
||||
//ADD: | pslSere ':' pslSere %prec prPSLFUS { $$ = PSLUNSUP(new AstPslSeqFusion($2, $1, $3)); }
|
||||
//ADD: | pslSereCpnd { $$ = $1; }
|
||||
pslSere<nodep>:
|
||||
pslExpr { $$ = $1; }
|
||||
| pslSequence { $$ = $1; } // Sequence containing sequence
|
||||
|
|
@ -1478,8 +1514,6 @@ pslSere<nodep>:
|
|||
|
||||
// Undocumented PSL rule is that {} is always a SERE; concatenation is not allowed.
|
||||
// This can be bypassed with the _(...) embedding of any arbitrary expression.
|
||||
//ADD: | pslFunc { $$ = UNSUP($1); }
|
||||
//ADD: | pslExpr yUNION pslExpr { $$ = UNSUP(new AstPslUnion($2, $1, $3)); }
|
||||
pslExpr<nodep>:
|
||||
exprPsl { $$ = new AstPslBool($1->fileline(), $1); }
|
||||
| yTRUE { $$ = new AstPslBool($1, new AstConst($1, V3Number($1,1,1))); }
|
||||
|
|
|
|||
|
|
@ -0,0 +1,42 @@
|
|||
#!/usr/bin/perl
|
||||
if (!$::Driver) { use FindBin; exec("./driver.pl", @ARGV, $0); die; }
|
||||
# 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_cover.v");
|
||||
|
||||
compile (
|
||||
v_flags2 => [$Last_Self->{v3}?'--assert --sp --coverage-user':''],
|
||||
nc_flags2 => ["+nccovoverwrite +nccoverage+all +nccovtest+$Last_Self->{name}"]
|
||||
);
|
||||
|
||||
execute (
|
||||
check_finished=>1,
|
||||
);
|
||||
|
||||
if ($Last_Self->{nc}) {
|
||||
my $name = $Last_Self->{name};
|
||||
my $cf = "obj_dir/${name}__nccover.cf";
|
||||
{
|
||||
my $fh = IO::File->new(">$cf") or die "%Error: $! writing $cf,";
|
||||
$fh->printf("report_summary -module *\n");
|
||||
$fh->printf("report_detail -both -module *\n");
|
||||
$fh->printf("report_html -both -module * > obj_dir/${name}__nccover.html\n");
|
||||
$fh->close;
|
||||
}
|
||||
$Last_Self->_run (logfile=>"obj_dir/${name}__nccover.log",
|
||||
tee=>0,
|
||||
cmd=>[($ENV{VERILATOR_ICCR}||'iccr'),
|
||||
"-test ${name} ${cf}"]);
|
||||
}
|
||||
|
||||
file_grep ("obj_dir/$Last_Self->{name}_simx.log", qr/COVER: Cyc==4/);
|
||||
file_grep ("obj_dir/$Last_Self->{name}_simx.log", qr/COVER: Cyc==5/);
|
||||
file_grep ("obj_dir/$Last_Self->{name}_simx.log", qr/COVER: Cyc==6/);
|
||||
file_grep ($Last_Self->{coverage_filename}, qr/cyc_eq_5.*,c=>[^0]/);
|
||||
|
||||
ok(1);
|
||||
1;
|
||||
|
|
@ -0,0 +1,117 @@
|
|||
// 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;
|
||||
|
||||
Test test (/*AUTOINST*/
|
||||
// Inputs
|
||||
.clk (clk),
|
||||
.toggle (toggle),
|
||||
.cyc (cyc[31:0]));
|
||||
|
||||
always @ (posedge clk) begin
|
||||
if (cyc!=0) begin
|
||||
cyc <= cyc + 1;
|
||||
toggle <= !cyc[0];
|
||||
if (cyc==9) begin
|
||||
end
|
||||
if (cyc==10) begin
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
end
|
||||
end
|
||||
|
||||
endmodule
|
||||
|
||||
module Test
|
||||
(
|
||||
input clk,
|
||||
input toggle,
|
||||
input [31:0] cyc
|
||||
);
|
||||
|
||||
// Simple cover
|
||||
cover property (@(posedge clk) cyc==3);
|
||||
|
||||
// With statement, in generate
|
||||
generate if (1) begin
|
||||
cover property (@(posedge clk) cyc==4) $display("*COVER: Cyc==4");
|
||||
end
|
||||
endgenerate
|
||||
|
||||
// Labeled cover
|
||||
cyc_eq_5:
|
||||
cover property (@(posedge clk) cyc==5) $display("*COVER: Cyc==5");
|
||||
|
||||
// Using default clock
|
||||
default clocking @(posedge clk);
|
||||
cover property (cyc==6) $display("*COVER: Cyc==6");
|
||||
endclocking
|
||||
|
||||
// Disable statement
|
||||
// Note () after disable are required
|
||||
cover property (@(posedge clk) disable iff (toggle) cyc==8)
|
||||
$display("*COVER: Cyc==8");
|
||||
cover property (@(posedge clk) disable iff (!toggle) cyc==8)
|
||||
$stop;
|
||||
|
||||
`ifndef verilator // Unsupported
|
||||
// Using a more complicated property
|
||||
property C1;
|
||||
@(posedge clk)
|
||||
disable iff (!toggle)
|
||||
cyc==5;
|
||||
endproperty
|
||||
cover property (C1) $display("*COVER: Cyc==5");
|
||||
|
||||
// Using covergroup
|
||||
// Note a covergroup is really inheritance of a special system "covergroup" class.
|
||||
covergroup counter1 @ (posedge cyc);
|
||||
// Automatic methods: stop(), start(), sample(), set_inst_name()
|
||||
|
||||
// Each bin value must be <= 32 bits. Strange.
|
||||
cyc_value : coverpoint cyc {
|
||||
}
|
||||
|
||||
cyc_bined : coverpoint cyc {
|
||||
bins zero = {0};
|
||||
bins low = {1,5};
|
||||
// Note 5 is also in the bin above. Only the first bin matching is counted.
|
||||
bins mid = {[5:$]};
|
||||
// illegal_bins // Has precidence over "first matching bin", creates assertion
|
||||
// ignore_bins // Not counted, and not part of total
|
||||
}
|
||||
toggle : coverpoint (toggle) {
|
||||
bins off = {0};
|
||||
bins on = {1};
|
||||
}
|
||||
cyc5 : coverpoint (cyc==5) {
|
||||
bins five = {1};
|
||||
}
|
||||
|
||||
// option.at_least = {number}; // Default 1 - Hits to be considered covered
|
||||
// option.auto_bin_max = {number}; // Default 64
|
||||
// option.comment = {string}
|
||||
// option.goal = {number}; // Default 90%
|
||||
// option.name = {string}
|
||||
// option.per_instance = 1; // Default 0 - each instance separately counted (cadence default is 1)
|
||||
// option.weight = {number}; // Default 1
|
||||
|
||||
// CROSS
|
||||
value_and_toggle: // else default is __<firstlabel>_X_<secondlabel>_<n>
|
||||
cross cyc_value, toggle;
|
||||
endgroup
|
||||
counter1 c1 = new();
|
||||
`endif
|
||||
|
||||
endmodule
|
||||
|
|
@ -0,0 +1,20 @@
|
|||
#!/usr/bin/perl
|
||||
if (!$::Driver) { use FindBin; exec("./driver.pl", @ARGV, $0); die; }
|
||||
# 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_cover.v");
|
||||
|
||||
compile (
|
||||
v_flags2 => [],
|
||||
);
|
||||
|
||||
execute (
|
||||
check_finished=>1,
|
||||
);
|
||||
|
||||
ok(1);
|
||||
1;
|
||||
Loading…
Reference in New Issue