diff --git a/Changes b/Changes index 0b29e3d61..bda43c901 100644 --- a/Changes +++ b/Changes @@ -8,6 +8,8 @@ The contributors that suggested a given feature are shown in []. Thanks! *** Support calling system functions as tasks, bug1285. [Joel Holdsworth] +*** Support assert properties, bug785, bug1290. [John Coiner, et al] + *** Add --no-debug-leak to reduce memory use under debug. [John Coiner] **** On convergence errors, show activity. [John Coiner] diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp index 7b23a4e80..9168a31d7 100644 --- a/src/V3Assert.cpp +++ b/src/V3Assert.cpp @@ -88,11 +88,17 @@ private: return newp; } - AstNode* newFireAssert(AstNode* nodep, const string& message) { + AstNode* newFireAssertUnchecked(AstNode* nodep, const string& message) { + // Like newFireAssert() but omits the asserts-on check AstDisplay* dispp = new AstDisplay (nodep->fileline(), AstDisplayType::DT_ERROR, message, NULL, NULL); AstNode* bodysp = dispp; replaceDisplay(dispp, "%%Error"); // Convert to standard DISPLAY format bodysp->addNext(new AstStop (nodep->fileline())); + return bodysp; + } + + AstNode* newFireAssert(AstNode* nodep, const string& message) { + AstNode* bodysp = newFireAssertUnchecked(nodep, message); bodysp = newIfAssertOn(bodysp); return bodysp; } @@ -105,7 +111,9 @@ private: // AstNode* bodysp = NULL; bool selfDestruct = false; + AstIf* ifp = NULL; if (AstPslCover* snodep = nodep->castPslCover()) { + ++m_statAsCover; if (!v3Global.opt.coverageUser()) { selfDestruct = true; } else { @@ -116,14 +124,30 @@ private: if (message!="") covincp->declp()->comment(message); bodysp = covincp; } + + if (bodysp && stmtsp) bodysp = bodysp->addNext(stmtsp); + ifp = new AstIf (nodep->fileline(), propp, bodysp, NULL); + bodysp = ifp; + + } else if (nodep->castPslAssert()) { + ++m_statAsPsl; + // Insert an automatic error message and $stop after + // any user-supplied statements. + AstNode* autoMsgp = newFireAssertUnchecked(nodep, "'assert property' failed."); + if (stmtsp) { + stmtsp->addNext(autoMsgp); + } else { + stmtsp = autoMsgp; + } + ifp = new AstIf(nodep->fileline(), propp, NULL, stmtsp); + // It's more LIKELY that we'll take the NULL if clause + // than the sim-killing else clause: + ifp->branchPred(AstBranchPred::BP_LIKELY); + bodysp = newIfAssertOn(ifp); } else { nodep->v3fatalSrc("Unknown node type"); } - if (bodysp && stmtsp) bodysp = bodysp->addNext(stmtsp); - AstIf* ifp = new AstIf (nodep->fileline(), propp, bodysp, NULL); - bodysp = ifp; - if (nodep->castVAssert()) ifp->branchPred(AstBranchPred::BP_UNLIKELY); - // + AstNode* newp = new AstAlways (nodep->fileline(), VAlwaysKwd::ALWAYS, sentreep, @@ -294,12 +318,11 @@ private: } } - virtual void visit(AstPslCover* nodep) { + virtual void visit(AstNodePslCoverOrAssert* nodep) { nodep->iterateChildren(*this); if (m_beginp && nodep->name() == "") nodep->name(m_beginp->name()); newPslAssertion(nodep, nodep->propp(), nodep->sentreep(), nodep->stmtsp(), nodep->name()); VL_DANGLING(nodep); - ++m_statAsCover; } virtual void visit(AstVAssert* nodep) { nodep->iterateChildren(*this); diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 20bfcd1ec..f61887a11 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -86,7 +86,7 @@ private: pushDeletep(nodep); VL_DANGLING(nodep); } - virtual void visit(AstPslCover* nodep) { + virtual void visit(AstNodePslCoverOrAssert* nodep) { if (nodep->sentreep()) return; // Already processed clearAssertInfo(); nodep->iterateChildren(*this); diff --git a/src/V3AstNodes.h b/src/V3AstNodes.h index 1a08415a9..c6b19f6f7 100644 --- a/src/V3AstNodes.h +++ b/src/V3AstNodes.h @@ -3986,6 +3986,7 @@ class AstNodeSystemUniop : public AstNodeUniop { public: AstNodeSystemUniop(FileLine* fl, AstNode* lhsp) : AstNodeUniop(fl, lhsp) { dtypeSetDouble(); } + ASTNODE_BASE_FUNCS(NodeSystemUniop) virtual bool cleanOut() {return true;} virtual bool cleanLhs() {return false;} virtual bool sizeMattersLhs() {return false;} virtual int instrCount() const { return instrCountDoubleTrig(); } @@ -5260,30 +5261,44 @@ public: AstNode* propp() const { return op3p(); } // op3 = property }; -class AstPslCover : public AstNodeStmt { +class AstNodePslCoverOrAssert : public AstNodeStmt { // Psl Cover // Parents: {statement list} // Children: expression, report string private: string m_name; // Name to report public: - AstPslCover(FileLine* fl, AstNode* propp, AstNode* stmtsp, const string& name="") + AstNodePslCoverOrAssert(FileLine* fl, AstNode* propp, AstNode* stmtsp, const string& name="") : AstNodeStmt(fl) , m_name(name) { addOp1p(propp); addNOp4p(stmtsp); } - ASTNODE_NODE_FUNCS(PslCover) - virtual string name() const { return m_name; } // * = Var name + ASTNODE_BASE_FUNCS(NodePslCoverOrAssert) + virtual string name() const { return m_name; } // * = Var name virtual V3Hash sameHash() const { return V3Hash(name()); } virtual bool same(const AstNode* samep) const { return samep->name() == name(); } virtual void name(const string& name) { m_name = name; } - 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 + 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* stmtsp() const { return op4p(); } // op4 = statements +}; + +class AstPslCover : public AstNodePslCoverOrAssert { +public: + ASTNODE_NODE_FUNCS(PslCover) + AstPslCover(FileLine* fl, AstNode* propp, AstNode* stmtsp, const string& name="") + : AstNodePslCoverOrAssert(fl, propp, stmtsp, name) {} + AstNode* coverincp() const { return op3p(); } // op3 = coverage node + void coverincp(AstCoverInc* nodep) { addOp3p(nodep); } // op3 = coverage node +}; + +class AstPslAssert : public AstNodePslCoverOrAssert { +public: + ASTNODE_NODE_FUNCS(PslAssert) + AstPslAssert(FileLine* fl, AstNode* propp, AstNode* stmtsp, const string& name="") + : AstNodePslCoverOrAssert(fl, propp, stmtsp, name) {} }; //====================================================================== diff --git a/src/V3Width.cpp b/src/V3Width.cpp index 01fe26cb5..522ca4b48 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -2226,7 +2226,7 @@ private: assertAtStatement(nodep); userIterateChildren(nodep, WidthVP(SELF,BOTH).p()); } - virtual void visit(AstPslCover* nodep) { + virtual void visit(AstNodePslCoverOrAssert* nodep) { assertAtStatement(nodep); iterateCheckBool(nodep,"Property",nodep->propp(),BOTH); // it's like an if() condition. userIterateAndNext(nodep->stmtsp(), NULL); diff --git a/src/verilog.y b/src/verilog.y index 140ba1502..8bf478df9 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -3716,9 +3716,14 @@ concurrent_assertion_item: // IEEE: concurrent_assertion_item ; concurrent_assertion_statement: // ==IEEE: concurrent_assertion_statement - //UNSUP: assert/assume + yASSERT yPROPERTY '(' property_spec ')' elseStmtBlock { $$ = new AstPslAssert($1,$4,$6); } // // IEEE: cover_property_statement - yCOVER yPROPERTY '(' property_spec ')' stmtBlock { $$ = new AstPslCover($1,$4,$6); } + | yCOVER yPROPERTY '(' property_spec ')' stmtBlock { $$ = new AstPslCover($1,$4,$6); } + ; + +elseStmtBlock: // Part of concurrent_assertion_statement + ';' { $$ = NULL; } + | yELSE stmtBlock { $$ = $2; } ; property_spec: // IEEE: property_spec diff --git a/test_regress/t/t_assert_property.pl b/test_regress/t/t_assert_property.pl new file mode 100755 index 000000000..5dc691360 --- /dev/null +++ b/test_regress/t/t_assert_property.pl @@ -0,0 +1,19 @@ +#!/usr/bin/perl +if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; } +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2003-2009 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 Version 3 or the Perl Artistic License +# Version 2.0. + +compile ( + verilator_flags2 => ['--assert --cc'], + ); + +execute ( + check_finished=>1, + ); + +ok(1); +1; diff --git a/test_regress/t/t_assert_property.v b/test_regress/t/t_assert_property.v new file mode 100644 index 000000000..ed6d8b799 --- /dev/null +++ b/test_regress/t/t_assert_property.v @@ -0,0 +1,51 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed into the Public Domain, for any use, +// without warranty, 2018 by Wilson Snyder. + +module t (/*AUTOARG*/ + // Inputs + clk + ); + + input clk; + integer cyc; initial cyc=1; + + Test test (/*AUTOINST*/ + // Inputs + .clk (clk), + .cyc (cyc[31:0])); + + always @ (posedge clk) begin + if (cyc!=0) begin + cyc <= cyc + 1; + if (cyc==10) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end + end + +endmodule + +module Test + ( + input clk, + input [31:0] cyc + ); + +`ifdef FAIL_ASSERT_1 + assert property (@(posedge clk) cyc==3) + else $display("cyc != 3, cyc == %0d", cyc); +`endif + +`ifdef FAIL_ASSERT_2 + assert property (@(posedge clk) cyc!=3); +`endif + + assert property (@(posedge clk) cyc < 100); + +// Unclocked is not supported: +// assert property (cyc != 6); + +endmodule diff --git a/test_regress/t/t_assert_property_fail_1.pl b/test_regress/t/t_assert_property_fail_1.pl new file mode 100755 index 000000000..69035746b --- /dev/null +++ b/test_regress/t/t_assert_property_fail_1.pl @@ -0,0 +1,26 @@ +#!/usr/bin/perl +if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; } +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2003-2009 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 Version 3 or the Perl Artistic License +# Version 2.0. + +top_filename("t/t_assert_property.v"); + +compile ( + v_flags2 => ['+define+FAIL_ASSERT_1'], + verilator_flags2 => ['--assert --cc'], + ); + +execute ( + fails => 1 + ); + +file_grep ($Self->{run_log_filename}, qr/'assert property' failed/); +# We expect to get a message when this assert fires: +file_grep ($Self->{run_log_filename}, qr/cyc != 3/); + +ok(1); +1; diff --git a/test_regress/t/t_assert_property_fail_2.pl b/test_regress/t/t_assert_property_fail_2.pl new file mode 100755 index 000000000..c348e60ab --- /dev/null +++ b/test_regress/t/t_assert_property_fail_2.pl @@ -0,0 +1,24 @@ +#!/usr/bin/perl +if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; } +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2003-2009 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 Version 3 or the Perl Artistic License +# Version 2.0. + +top_filename("t/t_assert_property.v"); + +compile ( + v_flags2 => ['+define+FAIL_ASSERT_2'], + verilator_flags2 => ['--assert --cc'], + ); + +execute ( + fails => 1 + ); + +file_grep ($Self->{run_log_filename}, qr/'assert property' failed/); + +ok(1); +1;