Support assert properties, bug785, bug1290.

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]

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

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

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) {}
 };
 
 //======================================================================

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

src/verilog.y

@@ -3716,9 +3716,14 @@ concurrent_assertion_item<nodep>:	// IEEE: concurrent_assertion_item
 	;
 
 concurrent_assertion_statement<nodep>:	// ==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<nodep>:	// Part of concurrent_assertion_statement
+		';'					{ $$ = NULL; }
+	|	yELSE stmtBlock				{ $$ = $2; }
 	;
 
 property_spec<nodep>:			// IEEE: property_spec

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;

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

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;

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;