Remove PSL support

Changes

@@ -5,6 +5,9 @@ indicates the contributor was also the author of the fix; Thanks!
 
 * Verilator 3.867 devel
 
+**    PSL support was removed, please use System Verilog assertions.
+
+
 * Verilator 3.866 2014-11-15
 
 ***   Fix +define+A+B to define A and B to match other simulators, bug847. [Adam Krolnik]

src/V3Assert.cpp

@@ -131,19 +131,13 @@ private:
 		if (message!="") covincp->declp()->comment(message);
 		bodysp = covincp;
 	    }
-	} else if (nodep->castPslAssert()) {
-	    bodysp = newFireAssert(nodep,message);
-	    // We assert the property is always true... so report when it fails
-	    // (Note this is opposite the behavior of coverage statements.)
-	    // Need: 'never' operator: not hold in current or any future cycle
-	    propp = new AstLogNot (nodep->fileline(), propp);
 	} 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::BP_UNLIKELY);
+	if (nodep->castVAssert()) ifp->branchPred(AstBranchPred::BP_UNLIKELY);
 	//
 	AstNode* newp = new AstAlways (nodep->fileline(),
 				       VAlwaysKwd::ALWAYS,
@@ -309,12 +303,6 @@ private:
 			nodep->stmtsp(), nodep->name()); nodep=NULL;
 	++m_statAsCover;
     }
-    virtual void visit(AstPslAssert* nodep, AstNUser*) {
-	nodep->iterateChildren(*this);
-	newPslAssertion(nodep, nodep->propp(), nodep->sentreep(),
-			NULL, nodep->name()); nodep=NULL;
-	++m_statAsPsl;
-    }
     virtual void visit(AstVAssert* nodep, AstNUser*) {
 	nodep->iterateChildren(*this);
 	newVAssertion(nodep, nodep->propp()); nodep=NULL;
@@ -339,14 +327,6 @@ private:
 	m_beginp = lastp;
     }
 
-    // VISITORS  //========== Temporal Layer
-
-    // VISITORS  //========== Boolean Layer
-    virtual void visit(AstPslBool* nodep, AstNUser*) {
-	nodep->replaceWith(nodep->exprp()->unlinkFrBack());
-	pushDeletep(nodep); nodep=NULL;
-    }
-
     virtual void visit(AstNode* nodep, AstNUser*) {
 	nodep->iterateChildren(*this);
     }

src/V3AssertPre.cpp

@@ -73,14 +73,6 @@ private:
     }
 
     // VISITORS  //========== Statements
-    virtual void visit(AstPslDefClock* nodep, AstNUser*) {
-	nodep->iterateChildren(*this);
-	// Store the new default clock, reset on new module
-	m_seniDefaultp = nodep->sensesp();
-	// Trash it
-	nodep->unlinkFrBack();
-	pushDeletep(nodep); nodep=NULL;
-    }
     virtual void visit(AstClocking* nodep, AstNUser*) {
 	UINFO(8,"   CLOCKING"<<nodep<<endl);
 	// Store the new default clock, reset on new module
@@ -101,13 +93,6 @@ private:
 	nodep->sentreep(newSenTree(nodep));
 	clearAssertInfo();
     }
-    virtual void visit(AstPslAssert* nodep, AstNUser*) {
-	if (nodep->sentreep()) return;  // Already processed
-	clearAssertInfo();
-	nodep->iterateChildren(*this);
-	nodep->sentreep(newSenTree(nodep));
-	clearAssertInfo();
-    }
     virtual void visit(AstPslClocked* nodep, AstNUser*) {
 	nodep->iterateChildren(*this);
 	if (m_senip) {

src/V3AstNodes.h

@@ -4520,19 +4520,6 @@ public:
 //======================================================================
 // PSL
 
-class AstPslDefClock : public AstNode {
-    // Set default PSL clock
-    // Parents:  MODULE
-    // Children: SENITEM
-public:
-    AstPslDefClock(FileLine* fl, AstNodeSenItem* sensesp)
-	: AstNode(fl) {
-	addNOp1p(sensesp);
-    }
-    ASTNODE_NODE_FUNCS(PslDefClock, PSLDEFCLOCK)
-    AstNodeSenItem* sensesp() const { return op1p()->castNodeSenItem(); }	// op1 = Sensitivity list
-};
-
 class AstPslClocked : public AstNode {
     // A clocked property
     // Parents:  ASSERT|COVER (property)
@@ -4551,27 +4538,6 @@ public:
     AstNode*	propp()		const { return op3p(); }	// op3 = property
 };
 
-class AstPslAssert : public AstNodeStmt {
-    // Psl Assertion
-    // Parents:  {statement list}
-    // Children: expression, report string
-private:
-    string	m_name;		// Name to report
-public:
-    AstPslAssert(FileLine* fl, AstNode* propp, const string& name="")
-	: AstNodeStmt(fl)
-	, m_name(name) {
-	addOp1p(propp);
-    }
-    ASTNODE_NODE_FUNCS(PslAssert, PSLASSERT)
-    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(); }
-    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
-};
-
 class AstPslCover : public AstNodeStmt {
     // Psl Cover
     // Parents:  {statement list}
@@ -4598,29 +4564,6 @@ public:
     AstNode*	stmtsp()	const { return op4p(); }	// op4 = statements
 };
 
-//======================================================================
-// PSL Expressions
-
-class AstPslBool : public AstNode {
-    // Separates PSL Sere/sequences from the normal expression boolean layer below.
-    // Note this excludes next() and similar functions; they are time domain, so not under AstPslBool.
-    // Parents: Sequences, etc.
-    // Children: math
-public:
-    AstPslBool(FileLine* fileline, AstNode* exprp)
-	: AstNode(fileline) {
-	addOp1p(exprp);
-    }
-    ASTNODE_NODE_FUNCS(PslBool, PSLBOOL)
-    AstNode*	exprp()	const { return op1p()->castNode(); }	// op1= expression
-    virtual bool hasDType() const { return true; }
-    virtual bool isGateOptimizable() const { return false; }	// Not relevant
-    virtual bool isPredictOptimizable() const { return false; }	// Not relevant
-    virtual int instrCount()	const { return 0; }
-    virtual V3Hash sameHash() const { return V3Hash(); }
-    virtual bool same(AstNode* samep) const { return true; }
-};
-
 //======================================================================
 // Text based nodes
 

src/V3Options.cpp

@@ -754,7 +754,6 @@ void V3Options::parseOptsList(FileLine* fl, const string& optdir, int argc, char
 	    else if ( onoff   (sw, "-pins-uint8", flag/*ref*/) ){ m_pinsUint8 = flag; }
 	    else if ( !strcmp (sw, "-private") )		{ m_public = false; }
 	    else if ( onoff   (sw, "-profile-cfuncs", flag/*ref*/) )	{ m_profileCFuncs = flag; }
-	    else if ( onoff   (sw, "-psl-deprecated", flag/*ref*/) )	{ m_psl = flag; }  // Undocumented
 	    else if ( onoff   (sw, "-public", flag/*ref*/) )		{ m_public = flag; }
 	    else if ( onoff   (sw, "-report-unoptflat", flag/*ref*/) )	{ m_reportUnoptflat = flag; }
 	    else if ( onoff   (sw, "-savable", flag/*ref*/) )		{ m_savable = flag; }
@@ -1226,7 +1225,6 @@ V3Options::V3Options() {
     m_profileCFuncs = false;
     m_preprocOnly = false;
     m_preprocNoLine = false;
-    m_psl = false;
     m_public = false;
     m_savable = false;
     m_skipIdentical = true;

src/V3Options.h

@@ -82,7 +82,6 @@ class V3Options {
     bool	m_pinsScBigUint;// main switch: --pins-sc-biguint
     bool	m_pinsUint8;	// main switch: --pins-uint8
     bool	m_profileCFuncs;// main switch: --profile-cfuncs
-    bool	m_psl;		// main switch: --psl
     bool	m_public;	// main switch: --public
     bool	m_savable;	// main switch: --savable
     bool	m_systemC;	// main switch: --sc: System C instead of simple C++
@@ -230,7 +229,6 @@ class V3Options {
     bool pinsScBigUint() const { return m_pinsScBigUint; }
     bool pinsUint8() const { return m_pinsUint8; }
     bool profileCFuncs() const { return m_profileCFuncs; }
-    bool psl() const { return m_psl; }
     bool allPublic() const { return m_public; }
     bool l2Name() const { return m_l2Name; }
     bool lintOnly() const { return m_lintOnly; }

src/V3ParseImp.h

@@ -131,7 +131,6 @@ public:
 
     // Functions called by lex rules:
     int yylexThis();
-    static bool optPsl() { return v3Global.opt.psl(); }
     static bool optFuture(const string& flag) { return v3Global.opt.isFuture(flag); }
 
     void ppline (const char* text);
@@ -190,8 +189,6 @@ public:
     // Interactions with lexer
     void lexNew(int debug);
     void lexDestroy();
-    void stateExitPsl();	// Parser -> lexer communication
-    void statePushVlg();	// Parser -> lexer communication
     void statePop();		// Parser -> lexer communication
     static int stateVerilogRecent();	// Parser -> lexer communication
     int	prevLexToken() { return m_prevLexToken; } // Parser -> lexer communication

src/V3ParseLex.cpp

@@ -47,13 +47,6 @@ public:
     V3Lexer() : V3LexerBase(NULL) {}
     ~V3Lexer() {}
     // METHODS
-    void stateExitPsl() {
-	if (YY_START != PSL) yyerrorf("Internal error: Exiting PSL state when not in PSL state");
-	yy_pop_state();
-    }
-    void statePushVlg() {
-	yy_push_state(STATE_VERILOG_RECENT);
-    }
     void statePop() {
 	yy_pop_state();
     }
@@ -65,8 +58,6 @@ public:
 	}
     }
 };
-void V3ParseImp::stateExitPsl() { parsep()->m_lexerp->stateExitPsl(); }
-void V3ParseImp::statePushVlg() { parsep()->m_lexerp->stateExitPsl(); }
 void V3ParseImp::statePop()	{ parsep()->m_lexerp->statePop(); }
 
 void V3ParseImp::unputString(const char* textp, size_t length) { parsep()->m_lexerp->unputString(textp, length); }

src/V3PreLex.h

@@ -166,8 +166,6 @@ class V3PreLex {
     // State from lexer
     int		m_formalLevel;	// Parenthesis counting inside def formals
     int		m_parenLevel;	// Parenthesis counting inside def args
-    int		m_pslParenLevel;// PSL Parenthesis (){} counting, so we can find final ;
-    bool	m_pslMoreNeeded;// Next // comment is really psl
     bool	m_defCmtSlash;	// /*...*/ comment in define had \ ending
     bool	m_defQuote;	// Definition value inside quote
     string	m_defValue;	// Definition value being built.
@@ -186,8 +184,6 @@ class V3PreLex {
 	m_defCmtSlash = false;
 	m_tokFilelinep = filelinep;
 	m_enterExit = 0;
-	m_pslParenLevel = 0;
-	m_pslMoreNeeded = false;
 	initFirstBuffer(filelinep);
     }
     ~V3PreLex() {

src/V3PreLex.l

@@ -42,24 +42,14 @@ void yyourtext(const char* textp, size_t size) { yytext=(char*)textp; yyleng=siz
 
 // Prevent conflicts from perl version
 static void linenoInc()  {LEXP->linenoInc();}
-static bool optPsl() { return V3PreProc::optPsl(); }
 static bool pedantic() { return LEXP->m_pedantic; }
 static void yyerror(char* msg) { LEXP->curFilelinep()->v3error(msg); }
 static void yyerrorf(const char* msg) { LEXP->curFilelinep()->v3error(msg); }
 static void appendDefValue(const char* t, size_t l) { LEXP->appendDefValue(t,l); }
-static int  pslParenLevel()    { return LEXP->m_pslParenLevel; }
-static void pslParenLevelInc() { LEXP->m_pslParenLevel++; }
-static void pslParenLevelDec() { if (pslParenLevel()) LEXP->m_pslParenLevel--; }
-static bool pslMoreNeeded()    { return LEXP->m_pslMoreNeeded; }
-static void pslMoreNeeded(bool flag) { LEXP->m_pslMoreNeeded = flag; }
 
 /**********************************************************************/
 %}
 
-%x PSLONEM
-%x PSLONEE
-%x PSLMULM
-%x PSLMUL1
 %x CMTONEM
 %x CMTBEGM
 %x CMTMODE
@@ -86,7 +76,6 @@ symb		([a-zA-Z_][a-zA-Z0-9_$]*|\\[^ \t\f\r\n]+)
 symbdef		([a-zA-Z_][a-zA-Z0-9_$]*|\\[^ \t\f\r\n`]+)
 word		[a-zA-Z0-9_]+
 drop		[\032]
-psl		[p]sl
 
 	/**************************************************************/
 %%
@@ -117,7 +106,7 @@ psl		[p]sl
 <INITIAL>"`error"	{ if (!pedantic()) return (VP_ERROR); else return(VP_DEFREF); }
 
 	/* Pass-through strings */
-<INITIAL,PSLMULM,PSLONEM>{quote}	{ yy_push_state(STRMODE); yymore(); }
+<INITIAL>{quote}	{ yy_push_state(STRMODE); yymore(); }
 <STRMODE><<EOF>>	{ linenoInc(); yyerrorf("EOF in unterminated string"); yyleng=0; yyterminate(); }
 <STRMODE>{crnl}		{ linenoInc(); yyerrorf("Unterminated string"); BEGIN(INITIAL); }
 <STRMODE>{word}		{ yymore(); }
@@ -233,57 +222,36 @@ psl		[p]sl
 <ARGMODE>.		{ appendDefValue(yytext,yyleng); }
 
 	/* One line comments. */
-<INITIAL>"//"{ws}*{psl} { if (optPsl())        { pslMoreNeeded(true); yy_push_state(PSLONEM); return(VP_PSL); }
-			  else { yy_push_state(CMTONEM); yymore(); } }
 <INITIAL>"//"{ws}*{crnl} { linenoInc(); yytext=(char*)"\n"; yyleng=1; return (VP_WHITE); }
-<INITIAL>"//" 		{ if (pslMoreNeeded()) { pslMoreNeeded(true); yy_push_state(PSLONEM); return(VP_PSL); }
+<INITIAL>"//" 		{ yy_push_state(CMTONEM); yymore(); }
-			  else { yy_push_state(CMTONEM); yymore(); } }
 <CMTONEM>[^\n\r]* 	{ yy_pop_state(); return (VP_COMMENT); }
 
-	/* Psl oneline comments */
-<PSLONEM>[{(]		{ pslParenLevelInc(); return (VP_TEXT); }
-<PSLONEM>[})]		{ pslParenLevelDec(); return (VP_TEXT); }
-<PSLONEM>[;]		{ if (!pslParenLevel()) {BEGIN PSLONEE; pslMoreNeeded(false);} return (VP_TEXT); }
-<PSLONEM>{crnl}		{ linenoInc(); yy_pop_state(); yytext=(char*)"\n"; yyleng=1; return(VP_WHITE); }
-
-	/* Completed psl oneline comments */
-<PSLONEE>{crnl}		{ linenoInc(); yy_pop_state(); yytext=(char*)"\n"; yyleng=1; return(VP_WHITE); }
-<PSLONEE>{ws}+		{ yymore(); }
-<PSLONEE>.		{ yyerrorf("Unexpected text following psl assertion\n"); }
-
 	/* C-style comments. */
 	/**** See also DEFCMT */
-	/* We distinguish between the start of a comment, and later, so we may find a "psl" prefix */
+	/* We distinguish between the start of a comment, and later, to look for prefix comments (deprecated) */
-<INITIAL>"/*"		{ yy_push_state(optPsl() ? CMTBEGM : CMTMODE); yymore(); }
+<INITIAL>"/*"		{ yy_push_state(CMTMODE); yymore(); }
-<CMTBEGM>{psl}		{ yyleng -= 3; BEGIN PSLMUL1; return (VP_COMMENT); }
 <CMTBEGM>{ws}+		{ yymore(); }
 <CMTBEGM,CMTMODE>"*/"		{ yy_pop_state(); return(VP_COMMENT); }
 <CMTBEGM,CMTMODE>{crnl}		{ linenoInc(); yymore(); }
 <CMTBEGM,CMTMODE><<EOF>>	{ yyerrorf("EOF in '/* ... */' block comment\n"); yyleng=0; yyterminate(); }
 <CMTMODE>{word}			{ yymore(); }
-<CMTBEGM>.			{ BEGIN CMTMODE; yymore(); }	/* Non 'psl' beginning in comment */
+<CMTBEGM>.			{ BEGIN CMTMODE; yymore(); }	/* beginning in comment */
 <CMTMODE>.			{ yymore(); }
 
-	/* Psl C-style comments. */
-	/* EOFs are normal because / * `foo(..) * / hits a unputString EOF */
-<PSLMUL1>.|{crnl}	{ yyless(0); BEGIN PSLMULM; return(VP_PSL); }
-<PSLMULM>"*/"		{ yy_pop_state(); return(VP_COMMENT); }
-<PSLMULM>"//"[^\n\r]*	{ return (VP_COMMENT); }	/* Comments inside block comments get literal inclusion (later removal) */
-
 	/* Define calls */
 	/* symbdef prevents normal lex rules from making `\`"foo a symbol {`"foo} instead of a BACKQUOTE */
-<INITIAL,PSLMULM,PSLONEM>"`"{symbdef}	{ return (VP_DEFREF); }
+<INITIAL>"`"{symbdef}	{ return (VP_DEFREF); }
-<INITIAL,PSLMULM,PSLONEM>"`"{symbdef}`` { yyleng-=2; return (VP_DEFREF_JOIN); }
+<INITIAL>"`"{symbdef}`` { yyleng-=2; return (VP_DEFREF_JOIN); }
 
 	/* Generics */
-<INITIAL,PSLMULM>{crnl}		{ linenoInc(); yytext=(char*)"\n"; yyleng=1; return(VP_WHITE); }
+<INITIAL>{crnl}		{ linenoInc(); yytext=(char*)"\n"; yyleng=1; return(VP_WHITE); }
-<INITIAL,PSLMULM,PSLONEM><<EOF>>  { yyterminate(); }  /* A "normal" EOF */
+<INITIAL><<EOF>>	{ yyterminate(); }  /* A "normal" EOF */
-<INITIAL,PSLMULM,PSLONEM>{symb}	  { return (VP_SYMBOL); }
+<INITIAL>{symb} 	{ return (VP_SYMBOL); }
-<INITIAL,PSLMULM,PSLONEM>{symb}`` { yyleng-=2; return (VP_SYMBOL_JOIN); }
+<INITIAL>{symb}``	{ yyleng-=2; return (VP_SYMBOL_JOIN); }
-<INITIAL,PSLMULM,PSLONEM>{wsn}+	{ return (VP_WHITE); }
+<INITIAL>{wsn}+		{ return (VP_WHITE); }
-<INITIAL,PSLMULM,PSLONEM>{drop}	{ }
+<INITIAL>{drop}		{ }
-<INITIAL,PSLMULM,PSLONEM>[\r]	{ }
+<INITIAL>[\r]		{ }
-<INITIAL,PSLMULM,PSLONEM>.	{ return (VP_TEXT); }
+<INITIAL>.		{ return (VP_TEXT); }
 %%
 
 void V3PreLex::pushStateDefArg(int level) {

src/V3PreProc.cpp

@@ -282,10 +282,6 @@ V3PreProc* V3PreProc::createPreProc(FileLine* fl) {
     return preprocp;
 }
 
-bool V3PreProc::optPsl() {
-    return v3Global.opt.psl();
-}
-
 //*************************************************************************
 // Defines
 
@@ -483,7 +479,6 @@ const char* V3PreProcImp::tokenName(int tok) {
     case VP_IFNDEF	: return("IFNDEF");
     case VP_INCLUDE	: return("INCLUDE");
     case VP_LINE	: return("LINE");
-    case VP_PSL		: return("PSL");
     case VP_STRIFY	: return("STRIFY");
     case VP_STRING	: return("STRING");
     case VP_SYMBOL	: return("SYMBOL");
@@ -1103,7 +1098,7 @@ int V3PreProcImp::getStateToken() {
 		// Value of building argument is data before the lower defref
 		// we'll append it when we push the argument.
 		break;
-	    } else if (tok==VP_SYMBOL || tok==VP_STRING || VP_TEXT || VP_WHITE || VP_PSL) {
+	    } else if (tok==VP_SYMBOL || tok==VP_STRING || VP_TEXT || VP_WHITE) {
 		string rtn; rtn.assign(yyourtext(),yyourleng());
 		refp->nextarg(refp->nextarg()+rtn);
 		goto next_tok;
@@ -1340,7 +1335,6 @@ int V3PreProcImp::getStateToken() {
 	    goto next_tok;
 	case VP_SYMBOL:
 	case VP_STRING:
-	case VP_PSL:
 	case VP_TEXT: {
 	    m_defDepth = 0;
 	    if (!m_off) return tok;
@@ -1436,9 +1430,6 @@ string V3PreProcImp::getline() {
 	    }
 	    gotEof = true;
 	}
-	else if (tok==VP_PSL) {
-	    m_lineChars.append(" psl ");
-	}
 	else {
 	    m_lineChars.append(buf);
 	}

src/V3PreProc.h

@@ -75,7 +75,6 @@ public:
 	return !(v3Global.opt.preprocOnly() && v3Global.opt.preprocNoLine());
     }
     static bool pedantic() { return false; }		// Obey standard; Don't substitute `error
-    static bool optPsl();
 
     // CALLBACK METHODS
     // This probably will want to be overridden for given child users of this class.

src/V3Width.cpp

@@ -189,7 +189,6 @@ private:
 
     // Widths: 1 bit out, lhs 1 bit; Real: converts via compare with 0
     virtual void visit(AstLogNot* nodep, AstNUser* vup) {	visit_log_not(nodep,vup); }
-    virtual void visit(AstPslBool* nodep, AstNUser* vup) {	visit_log_not(nodep,vup); }
     // Widths: 1 bit out, lhs 1 bit, rhs 1 bit; Real: converts via compare with 0
     virtual void visit(AstLogAnd* nodep, AstNUser* vup) {	visit_log_and_or(nodep,vup); }
     virtual void visit(AstLogOr* nodep, AstNUser* vup) {	visit_log_and_or(nodep,vup); }
@@ -1810,10 +1809,6 @@ private:
 	iterateCheckBool(nodep,"Property",nodep->propp(),BOTH);	// it's like an if() condition.
 	nodep->stmtsp()->iterateAndNext(*this);
     }
-    virtual void visit(AstPslAssert* nodep, AstNUser* vup) {
-	assertAtStatement(nodep,vup);
-	iterateCheckBool(nodep,"Property",nodep->propp(),BOTH);	// it's like an if() condition.
-    }
     virtual void visit(AstVAssert* nodep, AstNUser* vup) {
 	assertAtStatement(nodep,vup);
 	iterateCheckBool(nodep,"Property",nodep->propp(),BOTH);	// it's like an if() condition.
@@ -2131,8 +2126,7 @@ private:
     }
 
     void visit_log_not(AstNode* nodep, AstNUser* vup) {
-	// CALLER: LogNot, PslBool
+	// CALLER: LogNot
-	// Note AstPslBool isn't a AstNodeUniop, or we'd only allow that here
 	// Width-check: lhs 1 bit
 	// Real: Allowed; implicitly compares with zero
 	// We calculate the width of the UNDER expression.

src/verilog.l

@@ -103,8 +103,6 @@ void V3ParseImp::verilatorCmtBad(const char* textp) {
 }
 
 // See V3Read.cpp
-//void V3ParseImp::stateExitPsl() { BEGIN VLG; }
-//void V3ParseImp::statePushVlg() { yy_push_state(VLG); }
 //void V3ParseImp::statePop() { yy_pop_state(); }
 
 //======================================================================
@@ -138,7 +136,7 @@ void yyerrorf(const char* format, ...) {
 
 %s V95 V01 V05 S05 S09 S12
 %s STRING ATTRMODE TABLE
-%s VA5 SAX PSL VLT
+%s VA5 SAX VLT
 %s SYSCHDR SYSCINT SYSCIMP SYSCIMPH SYSCCTOR SYSCDTOR
 %s IGNORE
 
@@ -179,7 +177,7 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
 
   /************************************************************************/
   /* Verilog 1995 */
-<V95,V01,V05,VA5,S05,S09,S12,SAX,PSL>{
+<V95,V01,V05,VA5,S05,S09,S12,SAX>{
   {ws}			{ }	/* otherwise ignore white-space */
   {crnl}		{ NEXTLINE(); }		/* Count line numbers */
   /*     Extensions to Verilog set, some specified by PSL */
@@ -352,7 +350,7 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
 }
 
   /* Verilog 2001 */
-<V01,V05,VA5,S05,S09,S12,SAX,PSL>{
+<V01,V05,VA5,S05,S09,S12,SAX>{
   /*     System Tasks */
   "$signed"		{ FL; return yD_SIGNED; }
   "$unsigned"		{ FL; return yD_UNSIGNED; }
@@ -383,13 +381,13 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
 }
 
   /* Verilog 2005 */
-<V05,S05,S09,S12,SAX,PSL>{
+<V05,S05,S09,S12,SAX>{
   /*     Keywords */
   "uwire"		{ FL; return yWIRE; }
 }
 
   /* System Verilog 2005 */
-<S05,S09,S12,SAX,PSL>{
+<S05,S09,S12,SAX>{
   /*     System Tasks */
   "$bits"		{ FL; return yD_BITS; }
   "$clog2"		{ FL; return yD_CLOG2; }
@@ -414,18 +412,21 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
   "always_comb"		{ FL; return yALWAYS_COMB; }
   "always_ff"		{ FL; return yALWAYS_FF; }
   "always_latch"	{ FL; return yALWAYS_LATCH; }
+  "assert"		{ FL; return yASSERT; }
   "bind"		{ FL; return yBIND; }
   "bit"			{ FL; return yBIT; }
   "break"		{ FL; return yBREAK; }
   "byte"		{ FL; return yBYTE; }
   "chandle"		{ FL; return yCHANDLE; }
   "clocking"		{ FL; return yCLOCKING; }
+  "const"		{ FL; return yCONST__LEX; }
   "context"		{ FL; return yCONTEXT; }
   "continue"		{ FL; return yCONTINUE; }
+  "cover"		{ FL; return yCOVER; }
   "do"			{ FL; return yDO; }
   "endclocking"		{ FL; return yENDCLOCKING; }
-  "endpackage"		{ FL; return yENDPACKAGE; }
   "endinterface"	{ FL; return yENDINTERFACE; }
+  "endpackage"		{ FL; return yENDPACKAGE; }
   "endprogram"		{ FL; return yENDPROGRAM; }
   "endproperty"		{ FL; return yENDPROPERTY; }
   "enum"		{ FL; return yENUM; }
@@ -434,8 +435,8 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
   "iff"			{ FL; return yIFF; }
   "import"		{ FL; return yIMPORT; }
   "inside"		{ FL; return yINSIDE; }
-  "interface"		{ FL; return yINTERFACE; }
   "int"			{ FL; return yINT; }
+  "interface"		{ FL; return yINTERFACE; }
   "logic"		{ FL; return yLOGIC; }
   "longint"		{ FL; return yLONGINT; }
   "modport"		{ FL; return yMODPORT; }
@@ -443,6 +444,7 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
   "packed"		{ FL; return yPACKED; }
   "priority"		{ FL; return yPRIORITY; }
   "program"		{ FL; return yPROGRAM; }
+  "property"		{ FL; return yPROPERTY; }
   "pure"		{ FL; return yPURE; }
   "rand"		{ FL; return yRAND; }
   "randc"		{ FL; return yRANDC; }
@@ -454,6 +456,7 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
   "timeprecision"	{ FL; return yTIMEPRECISION; }
   "timeunit"		{ FL; return yTIMEUNIT; }
   "typedef"		{ FL; return yTYPEDEF; }
+  "union"		{ FL; return yUNION; }
   "unique"		{ FL; return yUNIQUE; }
   "var"			{ FL; return yVAR; }
   "void"		{ FL; return yVOID; }
@@ -461,6 +464,8 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
   /* Note assert_strobe was in SystemVerilog 3.1, but removed for SystemVerilog 2005 */
   "$root"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
   "alias"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
+  "assume"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
+  "before"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
   "bins"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
   "binsof"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
   "class"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
@@ -492,6 +497,7 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
   "randomize"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
   "randsequence"	{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
   "ref"			{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
+  "sequence"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
   "shortreal"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
   "solve"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
   "super"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
@@ -503,25 +509,11 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
   "wait_order"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
   "wildcard"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
   "with"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
-}
+  "within"		{ yyerrorf("Unsupported: SystemVerilog 2005 reserved word not implemented: %s",yytext); }
-
-  /* SystemVerilog 2005 ONLY not PSL; different rules for PSL as specified below */
-<S05,S09,S12,SAX>{
-  /*     Keywords */
-  "assert"		{ FL; return yASSERT; }
-  "const"		{ FL; return yCONST__LEX; }
-  "cover"		{ FL; return yCOVER; }
-  "property"		{ FL; return yPROPERTY; }
-  "union"		{ FL; return yUNION; }
-  /*     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); }
-  "sequence"		{ 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); }
 }
 
   /* SystemVerilog 2009 */
-<S09,S12,SAX,PSL>{
+<S09,S12,SAX>{
   /*     Keywords */
   "global"	 	{ FL; return yGLOBAL__LEX; }
   "unique0"	 	{ FL; return yUNIQUE0; }
@@ -550,7 +542,7 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
 }
 
   /* System Verilog 2012 */
-<S12,SAX,PSL>{
+<S12,SAX>{
   /*     Keywords */
   "implements"	 	{ yyerrorf("Unsupported: SystemVerilog 2012 reserved word not implemented: %s",yytext); }
   "interconnect" 	{ yyerrorf("Unsupported: SystemVerilog 2012 reserved word not implemented: %s",yytext); }
@@ -559,7 +551,7 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
 }
 
   /* Default PLI rule */
-<V95,V01,V05,VA5,S05,S09,S12,SAX,PSL>{
+<V95,V01,V05,VA5,S05,S09,S12,SAX>{
   "$"[a-zA-Z_$][a-zA-Z0-9_$]*	{ string str (yytext,yyleng);
 				  yylval.strp = PARSEP->newString(AstNode::encodeName(str));
 				  // Lookup unencoded name including the $, to avoid hitting normal signals
@@ -662,100 +654,11 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
    "zi_zp"		{ yyerrorf("Unsupported: AMS reserved word not implemented: %s",yytext); }
 }
 
-  /************************************************************************/
-  /* PSL */
-
-  /*Entry into PSL; mode change */
-<V95,V01,V05,VA5,S05,S09,S12,SAX>{
-  "psl"			{ yy_push_state(PSL); FL; return yPSL; }
-}
-
-<PSL>{
-  /*     Special things */
-  "psl"			{ ; }	// 'psl' may occur in middle of statement, so easier just to suppress
-  /*     Keywords */
-  "assert"		{ FL; return yPSL_ASSERT; }
-  "assume"		{ FL; return yPSL_ASSERT; } //==assert
-  "before_!"		{ yyerrorf("Illegal syntax, use before!_ instead of %s",yytext); }
-  "clock"		{ FL; return yPSL_CLOCK; }
-  "countones"		{ FL; return yD_COUNTONES; }
-  "cover"		{ FL; return yPSL_COVER; }
-  "isunknown"		{ FL; return yD_ISUNKNOWN; }
-  "onehot"		{ FL; return yD_ONEHOT; }
-  "onehot0"		{ FL; return yD_ONEHOT0; }
-  "until_!"		{ yyerrorf("Illegal syntax, use until!_ instead of %s",yytext); }
-  "report"		{ FL; return yPSL_REPORT; }
-  "true"		{ FL; return yTRUE; }
-  /*     Generic unsupported warnings */
-  /*"A"			{ yyerrorf("Unsupported: PSL branching reserved word not implemented: %s",yytext); } */
-  /*"AF"		{ yyerrorf("Unsupported: PSL branching reserved word not implemented: %s",yytext); } */
-  /*"AG"		{ yyerrorf("Unsupported: PSL branching reserved word not implemented: %s",yytext); } */
-  /*"AX"		{ yyerrorf("Unsupported: PSL branching reserved word not implemented: %s",yytext); } */
-  /*"E"			{ yyerrorf("Unsupported: PSL branching reserved word not implemented: %s",yytext); } */
-  /*"EF"		{ yyerrorf("Unsupported: PSL branching reserved word not implemented: %s",yytext); } */
-  /*"EG"		{ yyerrorf("Unsupported: PSL branching reserved word not implemented: %s",yytext); } */
-  /*"EX"		{ yyerrorf("Unsupported: PSL branching reserved word not implemented: %s",yytext); } */
-  /*"F"			{ FL; return yEVENTUALLYB; } */
-  /*"G"			{ FL; return yALWAYS; } */
-  /*"U"			{ FL; return yUNTILB; } */
-  /*"W"			{ FL; return yUNTIL; } */
-  /*"X"			{ FL; return yNEXT; } */
-  /*"X!"		{ FL; return yNEXTB; } */
-  /*"restrict"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); } S09 instead */
-  /*"strong"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); } S09 instead */
-  /*"until"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); } S09 instead */
-  "%for"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "%if"			{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "abort"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "assume_guarantee"	{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); } //Unsup in other tools
-  "before"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "before!"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "before!_"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "before_"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "boolean"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "const"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "endpoint"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "eventually!"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "fairness"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); } //Unsup in other tools
-  "fell"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "forall"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); } //Unsup in other tools
-  "in"			{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "inf"			{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "inherit"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); } //Unsup in other tools
-  "never"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "next"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "next!"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "next_a"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "next_a!"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "next_e"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "next_e!"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "next_event"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "next_event!"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "next_event_a"	{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "next_event_a!"	{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "next_event_e"	{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "next_event_e!"	{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "prev"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "property"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "restrict_guarantee"	{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); } //Unsup in other tools
-  "rose"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "sequence"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "stable"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "union"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "until!"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "until!_"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "until_"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "vmode"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); } //Unsup in other tools
-  "vprop"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); } //Unsup in other tools
-  "vunit"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-  "within"		{ yyerrorf("Unsupported: PSL reserved word not implemented: %s",yytext); }
-}
-
   /************************************************************************/
   /* Meta comments */
 
   /* Converted from //{cmt}verilator ...{cmt} by preprocessor */
-<V95,V01,V05,VA5,S05,S09,S12,SAX,PSL>{
+<V95,V01,V05,VA5,S05,S09,S12,SAX>{
   "/*verilator"{ws}*"*/"		{}	/* Ignore empty comments, may be `endif // verilator */
   "/*verilator clock_enable*/"		{ FL; return yVL_CLOCK_ENABLE; }
   "/*verilator coverage_block_off*/"	{ FL; return yVL_COVERAGE_BLOCK_OFF; }
@@ -793,8 +696,6 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
 <V95,V01,V05,VA5,S05,S09,S12,SAX>{
   "{"			{ FL; return yytext[0]; }
   "}"			{ FL; return yytext[0]; }
-}
-<V95,V01,V05,VA5,S05,S09,S12,SAX,PSL>{
   "!"			{ FL; return yytext[0]; }
   "#"			{ FL; return yytext[0]; }
   "$"			{ FL; return yytext[0]; }
@@ -826,7 +727,7 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
   /* Operators and multi-character symbols */
 
   /* Verilog 1995 Operators */
-<V95,V01,V05,VA5,S05,S09,S12,SAX,PSL>{
+<V95,V01,V05,VA5,S05,S09,S12,SAX>{
   "&&"			{ FL; return yP_ANDAND; }
   "||"			{ FL; return yP_OROR; }
   "<="			{ FL; return yP_LTE; }
@@ -848,7 +749,7 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
 }
 
   /* Verilog 2001 Operators */
-<V01,V05,VA5,S05,S09,S12,SAX,PSL>{
+<V01,V05,VA5,S05,S09,S12,SAX>{
   "<<<"			{ FL; return yP_SLEFT; }
   ">>>"			{ FL; return yP_SSRIGHT; }
   "**"			{ FL; return yP_POW; }
@@ -891,23 +792,8 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
   "["{ws}*"->"		{ FL; return yP_BRAMINUSGT; }
 }
 
-  /* PSL Operators */
-<PSL>{
-  "{"			{ FL; return yPSL_BRA; }	// Avoid parser hitting concatenate.
-  "}"			{ FL; return yPSL_KET; }	// Avoid parser hitting concatenate.
-  "<->"			{ yyerrorf("Unsupported: PSL operator not implemented: %s",yytext); } //Unsup in other tools
-  "[*"			{ yyerrorf("Unsupported: PSL operator not implemented: %s",yytext); } // yP_BRA_STAR
-  "[*]"			{ yyerrorf("Unsupported: PSL operator not implemented: %s",yytext); } // yP_BRA_STAR_KET
-  "[+]"			{ yyerrorf("Unsupported: PSL operator not implemented: %s",yytext); } // yP_BRA_PLUS_KET
-  "[->"			{ yyerrorf("Unsupported: PSL operator not implemented: %s",yytext); } // yP_BRA_MINUS_GT
-  "[->]"		{ yyerrorf("Unsupported: PSL operator not implemented: %s",yytext); } // yP_BRA_MINUS_GT_KET
-  "[="			{ yyerrorf("Unsupported: PSL operator not implemented: %s",yytext); } // yP_BRA_EQ
-  "|->"			{ yyerrorf("Unsupported: PSL operator not implemented: %s",yytext); } // yP_ORMINUSGT
-  "|=>"			{ yyerrorf("Unsupported: PSL operator not implemented: %s",yytext); } // yP_OREQGT
-}
-
   /* Identifiers and numbers */
-<V95,V01,V05,VA5,S05,S09,S12,SAX,PSL,VLT>{
+<V95,V01,V05,VA5,S05,S09,S12,SAX,VLT>{
   {escid}		{ FL; yylval.strp = PARSEP->newString
 	  			(AstNode::encodeName(string(yytext+1))); // +1 to skip the backslash
 			  return yaID__LEX;
@@ -997,7 +883,7 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
   /* Preprocessor */
   /* Common for all SYSC header states */
   /* OPTIMIZE: we return one per line, make it one for the entire block */
-<V95,V01,V05,VA5,S05,S09,S12,SAX,PSL,VLT,SYSCHDR,SYSCINT,SYSCIMP,SYSCIMPH,SYSCCTOR,SYSCDTOR,IGNORE>{
+<V95,V01,V05,VA5,S05,S09,S12,SAX,VLT,SYSCHDR,SYSCINT,SYSCIMP,SYSCIMPH,SYSCCTOR,SYSCDTOR,IGNORE>{
   "`accelerate"				{ } // Verilog-XL compatibility
   "`autoexpand_vectornets"		{ } // Verilog-XL compatibility
   "`celldefine"				{ PARSEP->inCellDefine(true); }
@@ -1026,7 +912,6 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
   "`portcoerce"				{ }
   "`pragma"{ws}+[^\n\r]*		{ } // Verilog 2005
   "`protect"				{ }
-  "`psl"				{ if (PARSEP->optPsl()) { BEGIN PSL; } else { BEGIN IGNORE; } }
   "`remove_gatenames"			{ } // Verilog-XL compatibility
   "`remove_netnames"			{ } // Verilog-XL compatibility
   "`resetall"				{ PARSEP->fileline()->warnOn(V3ErrorCode::I_DEF_NETTYPE_WIRE,true); } // Rest handled by preproc
@@ -1073,7 +958,7 @@ vnum	{vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5}
   /************************************************************************/
   /* Default rules - leave last */
 
-<V95,V01,V05,VA5,S05,S09,S12,SAX,PSL,VLT>{
+<V95,V01,V05,VA5,S05,S09,S12,SAX,VLT>{
   "`"[a-zA-Z_0-9]+	{ FL; yyerrorf("Define or directive not defined: %s",yytext); }
   "//"[^\n]*		{ }  /* throw away single line comments */
   .			{ FL; return yytext[0]; }	/* return single char ops. */

src/verilog.y

@@ -488,12 +488,6 @@ class AstSenTree;
 %token<fl>		yD_WARNING	"$warning"
 %token<fl>		yD_WRITE	"$write"
 
-%token<fl>		yPSL		"psl"
-%token<fl>		yPSL_ASSERT	"PSL assert"
-%token<fl>		yPSL_CLOCK	"PSL clock"
-%token<fl>		yPSL_COVER	"PSL cover"
-%token<fl>		yPSL_REPORT	"PSL report"
-
 %token<fl>		yVL_CLOCK		"/*verilator sc_clock*/"
 %token<fl>		yVL_CLOCK_ENABLE	"/*verilator clock_enable*/"
 %token<fl>		yVL_COVERAGE_BLOCK_OFF	"/*verilator coverage_block_off*/"
@@ -566,8 +560,6 @@ class AstSenTree;
 %token<fl>		yP_SRIGHTEQ	">>="
 %token<fl>		yP_SSRIGHTEQ	">>>="
 
-%token<fl>		yPSL_BRA	"{"
-%token<fl>		yPSL_KET	"}"
 %token<fl>	 	yP_LOGIFF
 
 // [* is not a operator, as "[ * ]" is legal
@@ -578,7 +570,6 @@ class AstSenTree;
 // PSL op precedence
 %right	 	yP_MINUSGT  yP_LOGIFF
 %right		yP_ORMINUSGT  yP_OREQGT
-%left<fl>	prPSLCLK
 
 // Verilog op precedence
 %right		'?' ':'
@@ -637,20 +628,6 @@ class AstSenTree;
 %start source_text
 
 %%
-//**********************************************************************
-// Feedback to the Lexer
-// Note we read a parenthesis ahead, so this may not change the lexer at the right point.
-
-stateExitPsl:			// For PSL lexing, return from PSL state
-		/* empty */			 	{ PARSEP->stateExitPsl(); }
-	;
-statePushVlg:			// For PSL lexing, escape current state into Verilog state
-		/* empty */			 	{ PARSEP->statePushVlg(); }
-	;
-statePop:			// Return to previous lexing state
-		/* empty */			 	{ PARSEP->statePop(); }
-	;
-
 //**********************************************************************
 // Files
 
@@ -1698,8 +1675,6 @@ module_common_item<nodep>:	// ==IEEE: module_common_item
 	|	yALWAYS_LATCH event_controlE stmtBlock	{ $$ = new AstAlways($1,VAlwaysKwd::ALWAYS_LATCH, $2,$3); }
 	|	loop_generate_construct			{ $$ = $1; }
 	|	conditional_generate_construct		{ $$ = $1; }
-	//			// Verilator only
-	|	pslStmt 				{ $$ = $1; }
 	//
 	|	error ';'				{ $$ = NULL; }
 	;
@@ -2987,7 +2962,7 @@ expr<nodep>:			// IEEE: part of expression/constant_expression/primary
 	|	~noPar__IGNORE~'(' expr ')'		{ $$ = $2; }
 	//UNSUP	~noPar__IGNORE~'(' expr ':' expr ':' expr ')'	{ $$ = $4; }
 	//			// PSL rule
-	|	'_' '(' statePushVlg expr statePop ')'	{ $$ = $4; }	// Arbitrary Verilog inside PSL
+	|	'_' '(' expr ')'			{ $$ = $3; }	// Arbitrary Verilog inside PSL
 	//
 	//			// IEEE: cast/constant_cast
 	|	casting_type yP_TICK '(' expr ')'	{ $$ = new AstCast($2,$4,$1); }
@@ -3087,11 +3062,6 @@ fexprScope<nodep>:		// exprScope, For use as first part of statement (disambigua
 		BISONPRE_COPY(exprScope,{s/~l~/f/g})	// {copied}
 	;
 
-// Psl excludes {}'s by lexer converting to different token
-exprPsl<nodep>:
-		expr					{ $$ = $1; }
-	;
-
 // PLI calls exclude "" as integers, they're strings
 // For $c("foo","bar") we want "bar" as a string, not a Verilog integer.
 exprStrText<nodep>:
@@ -3622,56 +3592,6 @@ package_scopeIdFollows<packagep>:	// IEEE: package_scope
 	//UNSUP	/*cont*/	yP_COLONCOLON	{ UNSUP }
 	;
 
-//************************************************
-// PSL Statements
-
-pslStmt<nodep>:
-		yPSL pslDir  stateExitPsl		{ $$ = $2; }
-	|	yPSL pslDecl stateExitPsl 		{ $$ = $2; }
-	;
-
-pslDir<nodep>:
-		id ':' pslDirOne			{ $$ = $3; }
-	|	pslDirOne		       		{ $$ = $1; }
-	;
-
-pslDirOne<nodep>:
-		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 yPSL_CLOCK '=' senitemEdge ';'		{ $$ = new AstPslDefClock($3, $4); }
-	|	yDEFAULT yPSL_CLOCK '=' '(' senitemEdge ')' ';'	{ $$ = new AstPslDefClock($3, $5); }
-	;
-
-//************************************************
-// PSL Properties, Sequences and SEREs
-// Don't use '{' or '}'; in PSL they're yPSL_BRA and yPSL_KET to avoid expr concatenates
-
-pslProp<nodep>:
-		pslSequence				{ $$ = $1; }
-	|	pslSequence '@' %prec prPSLCLK '(' senitemEdge ')' { $$ = new AstPslClocked($2,$4,NULL,$1); }  // or pslSequence @ ...?
-	;
-
-pslSequence<nodep>:
-		yPSL_BRA pslSere yPSL_KET		{ $$ = $2; }
-	;
-
-pslSere<nodep>:
-		pslExpr					{ $$ = $1; }
-	|	pslSequence				{ $$ = $1; }  // Sequence containing sequence
-	;
-
-// Undocumented PSL rule is that {} is always a SERE; concatenation is not allowed.
-// This can be bypassed with the _(...) embedding of any arbitrary expression.
-pslExpr<nodep>:
-		exprPsl					{ $$ = new AstPslBool($1->fileline(), $1); }
-	|	yTRUE					{ $$ = new AstPslBool($1, new AstConst($1, AstConst::LogicTrue())); }
-	;
-
 //**********************************************************************
 // VLT Files
 

test_regress/t/t_preproc_psl.v

@@ -1,72 +0,0 @@
-// DESCRIPTION: Verilator: Verilog Test module
-//
-//
-// This file ONLY is placed into the Public Domain, for any use,
-// without warranty, 2005 by Wilson Snyder.
-
-// verilator metacomment preserved
-/**/
-/*verilator metacomment also_preserved*/
-
-Hello in t_preproc_psl.v
-   // Psl capitalized not relevant
-   // Double commented ignored // psl not ok
-   // You can't have multiple statements on one // psl line.
-   // Inline /*cmt*/ comments not allowed inside psl comments
-
-   // psl default clock = (posedge clk);
-   // psl fails1: cover {cyc==10};
-   // psl assert always cyc!=10;
-   // psl assert always cyc==3 -> mask==8'h2;
-   // psl failsx: cover {cyc==3 && mask==8'h1};
-   /* psl fails2:
-        cover {
-	    cyc==3 && mask==8'h9};
-        // Ignore this comment-in-between-statements  (however not legal inside a statement)
-	fails3: always assert {
-	    cyc==3 && mask==8'h10 };
-    */
- `__LINE__
-
-   // Note the PSL statement can be on a unique line
-   // There can also be multiple "psl" keywords per line.
-   /*
-   psl
-      fails_ml:
-        assert always
-  	    cyc==3 -> mask==8'h21;
-    psl
-      fails_mlalso:  assert always cyc==3 -> mask==8'h21;
-    */
- `__LINE__
-
-   // psl assert never (cyc==1 && reset_l);
-
-   // psl fails3: assert always
-   //	    cyc==3 -> mask==8'h21;
-   //	syntax_error, not_part_of_above_stmt;
-
-// We need to count { and ( when looking for ; that terminate a PSL expression
-   // psl assert always
-   //       {[*]; cyc==3;
-   //        cyc==4; cyc==6};
-   //	syntax_error, not_part_of_above_stmt;
-
-// However /**/ pairs can't be split as above.
-
-`ifdef NEVER
-   // psl ifdefs have precedence;
-`endif
-
-// Macros are expanded...
-`define define_sig cyc
-   // psl assert always `define_sig!=10;
-
-`ifdef verilator
-  `psl
-psl assert always sig!=90;
-  `verilog
-`endif
-
-// Did we end up right?
-`__LINE__

test_regress/t/t_preproc_psl_off.out

@@ -1,99 +0,0 @@
-`line 1 "t/t_preproc_psl.v" 1
- 
-
-
-`line 4 "t/t_preproc_psl.v" 0
- 
- 
-
-`line 7 "t/t_preproc_psl.v" 0
-/*verilator metacomment preserved*/ 
- 
-/*verilator metacomment also_preserved*/ 
-
-`line 11 "t/t_preproc_psl.v" 0
-Hello in t_preproc_psl.v
-    
-    
-    
-    
-
-`line 17 "t/t_preproc_psl.v" 0
-    
-    
-    
-    
-    
-   
-
-`line 28 "t/t_preproc_psl.v" 0
-
-`line 28 "t/t_preproc_psl.v" 0
-
-`line 28 "t/t_preproc_psl.v" 0
-
-`line 28 "t/t_preproc_psl.v" 0
-
-`line 28 "t/t_preproc_psl.v" 0
- 
- 29
-
-`line 31 "t/t_preproc_psl.v" 0
-    
-    
-   
-
-`line 40 "t/t_preproc_psl.v" 0
-
-`line 40 "t/t_preproc_psl.v" 0
-
-`line 40 "t/t_preproc_psl.v" 0
-
-`line 40 "t/t_preproc_psl.v" 0
-
-`line 40 "t/t_preproc_psl.v" 0
-
-`line 40 "t/t_preproc_psl.v" 0
- 
- 41
-
-`line 43 "t/t_preproc_psl.v" 0
-    
-
-`line 45 "t/t_preproc_psl.v" 0
-    
-    
-    
-
-`line 49 "t/t_preproc_psl.v" 0
- 
-    
-    
-    
-    
-
-`line 55 "t/t_preproc_psl.v" 0
- 
-
-`line 57 "t/t_preproc_psl.v" 0
- 
-   
-
-
-`line 61 "t/t_preproc_psl.v" 0
- 
- 
-    
-
-`line 65 "t/t_preproc_psl.v" 0
- 
-  `psl
-psl assert always sig!=90;
-  `verilog
-
-
-`line 71 "t/t_preproc_psl.v" 0
- 
-72
-
-`line 74 "t/t_preproc_psl.v" 2

test_regress/t/t_preproc_psl_off.pl

@@ -1,24 +0,0 @@
-#!/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.
-
-$Self->{vlt} or $Self->skip("Verilator only test");
-
-my $stdout_filename = "$Self->{obj_dir}/$Self->{name}__test.vpp";
-
-top_filename("t/t_preproc_psl.v");
-
-compile (
-    verilator_flags2 => ['-E'],
-    verilator_make_gcc=>0,
-    stdout_filename => $stdout_filename,
-    );
-
-ok(files_identical($stdout_filename, "t/$Self->{name}.out"));
-
-1;

test_regress/t/t_preproc_psl_on.out

@@ -1,88 +0,0 @@
-`line 1 "t/t_preproc_psl.v" 1
- 
-
-
-`line 4 "t/t_preproc_psl.v" 0
- 
- 
-
-`line 7 "t/t_preproc_psl.v" 0
-/*verilator metacomment preserved*/ 
- 
-/*verilator metacomment also_preserved*/ 
-
-`line 11 "t/t_preproc_psl.v" 0
-Hello in t_preproc_psl.v
-    
-    
-    
-    
-
-`line 17 "t/t_preproc_psl.v" 0
-    psl  default clock = (posedge clk);
-    psl  fails1: cover {cyc==10};
-    psl  assert always cyc!=10;
-    psl  assert always cyc==3 -> mask==8'h2;
-    psl  failsx: cover {cyc==3 && mask==8'h1};
-     psl  fails2:
-        cover {
-	    cyc==3 && mask==8'h9};
-         
-	fails3: always assert {
-	    cyc==3 && mask==8'h10 };
-     
- 29
-
-`line 31 "t/t_preproc_psl.v" 0
-    
-    
-   
-  psl 
-      fails_ml:
-        assert always
-  	    cyc==3 -> mask==8'h21;
-    psl
-      fails_mlalso:  assert always cyc==3 -> mask==8'h21;
-     
- 41
-
-`line 43 "t/t_preproc_psl.v" 0
-    psl  assert never (cyc==1 && reset_l);
-
-`line 45 "t/t_preproc_psl.v" 0
-    psl  fails3: assert always
-    psl 	    cyc==3 -> mask==8'h21;
-    
-
-`line 49 "t/t_preproc_psl.v" 0
- 
-    psl  assert always
-    psl        {[*]; cyc==3;
-    psl         cyc==4; cyc==6};
-    
-
-`line 55 "t/t_preproc_psl.v" 0
- 
-
-`line 57 "t/t_preproc_psl.v" 0
- 
-      
-
-
-`line 61 "t/t_preproc_psl.v" 0
- 
- 
-    psl  assert always cyc!=10;
-
-`line 65 "t/t_preproc_psl.v" 0
- 
-  `psl
-psl assert always sig!=90;
-  `verilog
-
-
-`line 71 "t/t_preproc_psl.v" 0
- 
-72
-
-`line 74 "t/t_preproc_psl.v" 2

test_regress/t/t_preproc_psl_on.pl

@@ -1,24 +0,0 @@
-#!/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.
-
-$Self->{vlt} or $Self->skip("Verilator only test");
-
-my $stdout_filename = "$Self->{obj_dir}/$Self->{name}__test.vpp";
-
-top_filename("t/t_preproc_psl.v");
-
-compile (
-    verilator_flags2 => ['-psl-deprecated -E'],
-    verilator_make_gcc=>0,
-    stdout_filename => $stdout_filename,
-    );
-
-ok(files_identical($stdout_filename, "t/$Self->{name}.out"));
-
-1;

test_regress/t/t_psl_basic.pl

@@ -1,19 +0,0 @@
-#!/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 (
-	 v_flags2 => [$Self->{v3}?'--assert --psl-deprecated':($Self->{nc}?'+assert':'')],
-	 );
-
-execute (
-	 check_finished=>1,
-	 );
-
-ok(1);
-1;

test_regress/t/t_psl_basic.v

@@ -1,54 +0,0 @@
-// DESCRIPTION: Verilator: Verilog Test module
-//
-// This file ONLY is placed into the Public Domain, for any use,
-// without warranty, 2005 by Wilson Snyder.
-
-module t (/*AUTOARG*/
-   // Inputs
-   clk
-   );
-
-   input clk;
-
-   reg 	 toggle;
-
-   integer cyc; initial cyc=1;
-   wire [7:0] cyc_copy = cyc[7:0];
-
-   // psl cover  {cyc==3 || cyc==4} @ (posedge clk);
-   // psl assert {cyc<100} @ (posedge clk) report "AssertionFalse1";
-`ifdef FAILING_ASSERTIONS
-   // psl assert {toggle} @ (posedge clk) report "AssertionShouldFail";
-`endif
-
-   // psl default clock = negedge clk;
-//FIX   // psl assert always {cyc<99};
-   // psl cover {cyc==9} report "DefaultClock,expect=1";
-
-   // psl assert {(cyc==5)->toggle};
-   // psl cover  {(cyc==5)->toggle} report "ToggleLogIf,expect=1";
-`ifdef NOT_SUP
-   // psl assert {toggle<->cyc[0]};
-   // psl cover  {toggle<->cyc[0]} report "CycsLogIff,expect=10";
-`endif
-   
-   // Test {{..}} == Sequence of sequence...
-   // psl assert {{true}};
-
-   always @ (negedge clk) begin
-      //if (!(cyc==5) || toggle) $write("%d: %s\n", cyc, "ToggleLogIf,expect=1");
-      //if (toggle&&cyc[0] || ~toggle&&~cyc[0]) $write("%d: %s\n", cyc, "CycsLogIff,expect=10");
-   end
-
-   always @ (posedge clk) begin
-      if (cyc!=0) begin
-	 cyc <= cyc + 1;
-	 toggle <= !cyc[0];
-	 if (cyc==10) begin
-	    $write("*-* All Finished *-*\n");
-	    $finish;
-	 end
-      end
-   end
-
-endmodule

test_regress/t/t_psl_basic_cover.pl

@@ -1,26 +0,0 @@
-#!/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_psl_basic.v");
-
-compile (
-	 verilator_flags2 => ['--psl-deprecated --sp --coverage-user'],
-	 );
-
-execute (
-	 check_finished=>1,
-	 );
-
-# Allow old Perl format dump, or new binary dump
-file_grep ($Self->{coverage_filename}, qr/(,o=>'cover'.*,c=>2\)|o.cover.* 2\n)/);
-file_grep ($Self->{coverage_filename}, qr/(DefaultClock.*,c=>1\)|DefaultClock.* 1\n)/);
-file_grep ($Self->{coverage_filename}, qr/(ToggleLogIf.*,c=>9\)|ToggleLogIf.* 9\n)/);
-
-ok(1);
-1;

test_regress/t/t_psl_basic_off.pl

@@ -1,21 +0,0 @@
-#!/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_psl_basic.v");
-
-compile (
-	 v_flags2 => [],
-	 );
-
-execute (
-	 check_finished=>1,
-	 );
-
-ok(1);
-1;