From 500dc2170fe9f7ec481906c4529f02e7b217803e Mon Sep 17 00:00:00 2001 From: Wilson Snyder Date: Wed, 6 Aug 2008 12:52:39 -0400 Subject: [PATCH] Support SystemVerilog "cover property" statements. --- Changes | 2 + bin/verilator | 3 +- nodist/dot_importer | 13 +-- nodist/dot_pruner | 13 +-- nodist/invoke_iccr | 58 +++++++++++++ nodist/invoke_ncverilog | 13 +-- nodist/vtree_importer | 13 +-- src/V3Assert.cpp | 24 +++++- src/V3AssertPre.cpp | 39 +++++++-- src/V3AstNodes.h | 34 +++++++- src/V3Width.cpp | 7 +- src/verilog.l | 20 ++--- src/verilog.y | 72 ++++++++++++----- test_regress/t/t_assert_cover.pl | 42 ++++++++++ test_regress/t/t_assert_cover.v | 117 +++++++++++++++++++++++++++ test_regress/t/t_assert_cover_off.pl | 20 +++++ 16 files changed, 396 insertions(+), 94 deletions(-) create mode 100755 nodist/invoke_iccr create mode 100755 test_regress/t/t_assert_cover.pl create mode 100644 test_regress/t/t_assert_cover.v create mode 100755 test_regress/t/t_assert_cover_off.pl diff --git a/Changes b/Changes index df0128c3d..390a82298 100644 --- a/Changes +++ b/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. diff --git a/bin/verilator b/bin/verilator index e260bb005..559492c98 100755 --- a/bin/verilator +++ b/bin/verilator @@ -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 diff --git a/nodist/dot_importer b/nodist/dot_importer index 76f5e09c8..598c3eec5 100755 --- a/nodist/dot_importer +++ b/nodist/dot_importer @@ -1,16 +1,5 @@ #!/usr/bin/perl -w -###################################################################### -# -# Copyright 2005-2008 by Wilson Snyder . 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; diff --git a/nodist/dot_pruner b/nodist/dot_pruner index 46806d056..097d67e1b 100755 --- a/nodist/dot_pruner +++ b/nodist/dot_pruner @@ -1,16 +1,5 @@ #!/usr/bin/perl -w -###################################################################### -# -# Copyright 2005-2008 by Wilson Snyder . 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; diff --git a/nodist/invoke_iccr b/nodist/invoke_iccr new file mode 100755 index 000000000..d51975d21 --- /dev/null +++ b/nodist/invoke_iccr @@ -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 + +=head1 SEE ALSO + +=cut + +###################################################################### +### Local Variables: +### compile-command: "./invoke_iccr -help" +### End: diff --git a/nodist/invoke_ncverilog b/nodist/invoke_ncverilog index d4a5c2691..77705108f 100755 --- a/nodist/invoke_ncverilog +++ b/nodist/invoke_ncverilog @@ -1,16 +1,5 @@ #!/usr/bin/perl -w -###################################################################### -# -# Copyright 2007-2008 by Wilson Snyder . 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; diff --git a/nodist/vtree_importer b/nodist/vtree_importer index beb39edf0..fa51bb005 100755 --- a/nodist/vtree_importer +++ b/nodist/vtree_importer @@ -1,16 +1,5 @@ #!/usr/bin/perl -w -###################################################################### -# -# Copyright 2005-2008 by Wilson Snyder . 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; diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp index 3dcbb7643..1adebd183 100644 --- a/src/V3Assert.cpp +++ b/src/V3Assert.cpp @@ -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 diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 9b580c666..44374ff62 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -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"<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); } diff --git a/src/V3AstNodes.h b/src/V3AstNodes.h index 9d6aea2e8..ea068bb28 100644 --- a/src/V3AstNodes.h +++ b/src/V3AstNodes.h @@ -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 }; //====================================================================== diff --git a/src/V3Width.cpp b/src/V3Width.cpp index 2a4ec3303..fb4209b9b 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -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*) { diff --git a/src/verilog.l b/src/verilog.l index e35c376b8..72cd3be2b 100644 --- a/src/verilog.l +++ b/src/verilog.l @@ -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]+ { /* 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);} */ diff --git a/src/verilog.y b/src/verilog.y index a288f38d3..9228f5d94 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -163,17 +163,20 @@ class AstSenTree; %token yCASE "case" %token yCASEX "casex" %token yCASEZ "casez" -%token yCLOCK "clock" +%token yCLOCKING "clocking" %token yCOVER "cover" %token yDEFAULT "default" %token yDEFPARAM "defparam" +%token yDISABLE "disable" %token yDO "do" %token yELSE "else" %token yEND "end" %token yENDCASE "endcase" +%token yENDCLOCKING "endclocking" %token yENDFUNCTION "endfunction" %token yENDGENERATE "endgenerate" %token yENDMODULE "endmodule" +%token yENDPROPERTY "endproperty" %token yENDSPECIFY "endspecify" %token yENDTASK "endtask" %token yFINAL "final" @@ -182,6 +185,7 @@ class AstSenTree; %token yGENERATE "generate" %token yGENVAR "genvar" %token yIF "if" +%token yIFF "iff" %token yINITIAL "initial" %token yINOUT "inout" %token yINPUT "input" @@ -196,9 +200,8 @@ class AstSenTree; %token yOUTPUT "output" %token yPARAMETER "parameter" %token yPOSEDGE "posedge" -%token yPSL "psl" +%token yPROPERTY "property" %token yREG "reg" -%token yREPORT "report" %token ySCALARED "scalared" %token ySIGNED "signed" %token ySPECIFY "specify" @@ -248,7 +251,11 @@ class AstSenTree; %token yD_WARNING "$warning" %token yD_WRITE "$write" +%token yPSL "psl" %token yPSL_ASSERT "PSL assert" +%token yPSL_CLOCK "PSL clock" +%token yPSL_COVER "PSL cover" +%token yPSL_REPORT "PSL report" %token yVL_CLOCK "/*verilator sc_clock*/" %token yVL_CLOCK_ENABLE "/*verilator clock_enable*/" @@ -628,6 +635,8 @@ modOrGenItem: | 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: assertStmt { $$ = $1; } ; +clocking_declaration: // IEEE: clocking_declaration (INCOMPLETE) + yDEFAULT yCLOCKING '@' '(' senitemEdge ')' ';' clocking_item yENDCLOCKING + { $$ = new AstClocking($1, $5, $8); } + ; + +clocking_item: // IEEE: clocking_item (INCOMPLETE) + concurrent_assertion_item { $$ = $1; } + | clocking_item concurrent_assertion_item { $$ = $1->addNext($2); } + ; + +concurrent_assertion_item: // IEEE: concurrent_assertion_item (complete) + concurrent_assertion_statement { $$ = $1; } + | yaID ':' concurrent_assertion_statement { $$ = new AstBegin($2,*$1,$3); } + ; + +concurrent_assertion_statement: // IEEE: concurrent_assertion_statement (INCOMPLETE) + cover_property_statement { $$ = $1; } + ; + +cover_property_statement: // IEEE: cover_property_statement (complete) + yCOVER yPROPERTY '(' property_spec ')' stmtBlock { $$ = new AstPslCover($1,$4,$6); } + ; + +property_spec: // 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: + /* empty */ { $$ = NULL; } + | yDISABLE yIFF '(' expr ')' { $$ = $4; } + ; + assertStmt: 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: ; pslDir: - yaID ':' pslDirOne { $$ = $3; } // ADD: Create label on $1 + yaID ':' pslDirOne { $$ = $3; } | pslDirOne { $$ = $1; } ; -//ADD: | yRESTRICT pslSequence ';' { $$ = PSLUNSUP(new AstPslRestrict($1,$2)); } pslDirOne: - 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: - 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: pslProp: 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: 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: pslExpr { $$ = $1; } | pslSequence { $$ = $1; } // Sequence containing sequence @@ -1478,8 +1514,6 @@ pslSere: // 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: exprPsl { $$ = new AstPslBool($1->fileline(), $1); } | yTRUE { $$ = new AstPslBool($1, new AstConst($1, V3Number($1,1,1))); } diff --git a/test_regress/t/t_assert_cover.pl b/test_regress/t/t_assert_cover.pl new file mode 100755 index 000000000..eed0c29f9 --- /dev/null +++ b/test_regress/t/t_assert_cover.pl @@ -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; diff --git a/test_regress/t/t_assert_cover.v b/test_regress/t/t_assert_cover.v new file mode 100644 index 000000000..23b4d621c --- /dev/null +++ b/test_regress/t/t_assert_cover.v @@ -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 ___X__ + cross cyc_value, toggle; + endgroup + counter1 c1 = new(); +`endif + +endmodule diff --git a/test_regress/t/t_assert_cover_off.pl b/test_regress/t/t_assert_cover_off.pl new file mode 100755 index 000000000..076b05408 --- /dev/null +++ b/test_regress/t/t_assert_cover_off.pl @@ -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;