PSL is no longer supported, please use System Verilog assertions.

Changes

@@ -5,6 +5,8 @@ indicates the contributor was also the author of the fix; Thanks!
 
 * Verilator 3.857 devel
 
+**    PSL is no longer supported, please use System Verilog assertions.
+
 ***   Add --no-trace-params.
 
 ****  Documentation fixes, bug723. [Glen Gibb]

TODO

@@ -31,11 +31,13 @@ Configure/Make/Install
 	* Distribute with flex/bison already expanded?
 	  Flex library not needed.  Probably too difficult to be worth it.
 	* Integrate SystemPerl coverage
+	      see the SystemPerl git branch coverage_only
     	      (Note in /usr/include there are no upper cased include files.)
 		Coverage.pm		-- Need all functionality, but in C?
 		Coverage/Item.pm	-- Need all functionality, but in C?
 		Coverage/ItemKey.pm	-- Need all functionality, but in C?
 		sp_preproc		-- Some steps in here need to be moved to generated C
+		--			   -- note uses Verilog::Getopt
 		src/Sp.cpp		-- n/a
 		src/SpCommon.h		-- mostly overlaps verilatedos.h
 		src/SpCoverage.cpp/h	-- All needed

bin/verilator

@@ -209,7 +209,7 @@ Verilator - Convert Verilog code to C++/SystemC
 =head1 DESCRIPTION
 
 Verilator converts synthesizable (not behavioral) Verilog code, plus some
-Synthesis, SystemVerilog and a small subset of Verilog AMS and Sugar/PSL
+Synthesis, SystemVerilog and a small subset of Verilog AMS
 assertions, into C++, SystemC or SystemPerl code.  It is not a complete
 simulator, just a compiler.
 
@@ -259,7 +259,7 @@ descriptions in the next sections for more information.
     --coverage                  Enable all coverage
     --coverage-line             Enable line coverage
     --coverage-toggle           Enable toggle coverage
-    --coverage-user             Enable PSL/SVL user coverage
+    --coverage-user             Enable SVL user coverage
     --coverage-underscore       Enable coverage of _signals
      -D<var>[=<value>]          Set preprocessor define
     --debug                     Enable debugging
@@ -311,7 +311,6 @@ descriptions in the next sections for more information.
     --prefix <topname>          Name of top level class
     --profile-cfuncs            Name functions for profiling
     --private                   Debugging; see docs
-    --psl                       Enable PSL parsing
     --public                    Debugging; see docs
     --report-unoptflat          Extra diagnostics for UNOPTFLAT
     --savable			Enable model save-restore
@@ -410,8 +409,7 @@ C<+1364-1995ext+> etc. specify both the syntax I<and> semantics to be used.
 
 =item --assert
 
-Enable all assertions, includes enabling the --psl flag.  (If psl is not
+Enable all assertions.
-desired, but other assertions are, use --assert --nopsl.)
 
 See also --x-assign and --x-initial-edge; setting "--x-assign unique"
 and/or "--x-initial-edge" may be desirable.
@@ -902,12 +900,6 @@ statements.
 Opposite of --public.  Is the default; this option exists for backwards
 compatibility.
 
-=item --psl
-
-Enable PSL parsing.  Without this switch, PSL meta-comments are ignored.
-See the --assert flag to enable all assertions, and --coverage-user to
-enable functional coverage.
-
 =item --public
 
 This is only for historical debug use.  Using it may result in
@@ -1987,34 +1979,6 @@ AMS parsing is enabled with "--language VAMS" or "--language 1800+VAMS".
 At present Verilator implements ceil, exp, floor, ln, log, pow, sqrt,
 string, and wreal.
 
-=head2 Sugar/PSL Support
-
-Most future work is being directed towards improving SystemVerilog
-assertions instead of PSL.  If you are using these PSL features, please
-contact the author as they may be depreciated in future versions.
-
-With the --assert switch, Verilator enables support of the Property
-Specification Language (PSL), specifically the simple PSL subset without
-time-branching primitives.  Verilator currently only converts PSL
-assertions to simple "if (...) error" statements, and coverage statements
-to increment the line counters described in the coverage section.
-
-Verilator implements these keywords: assert, assume (same as assert),
-default (for clocking), countones, cover, isunknown, onehot, onehot0,
-report, and true.
-
-Verilator implements these operators: -> (logical if).
-
-Verilator does not support SEREs yet.  All assertion and coverage
-statements must be simple expressions that complete in one cycle.  PSL
-vmode/vprop/vunits are not supported.  PSL statements must be in the module
-they reference, at the module level where you would put an
-initial... statement.
-
-Verilator only supports (posedge CLK) or (negedge CLK), where CLK is the
-name of a one bit signal.  You may not use arbitrary expressions as
-assertion clocks.
-
 =head2 Synthesis Directive Assertion Support
 
 With the --assert switch, Verilator reads any "//synopsys full_case" or
@@ -2055,13 +2019,6 @@ supported by Verilator since 2006!)
 
 This will report an error when encountered, like C++'s #error.
 
-=item _(I<expr>)
-
-A underline followed by an expression in parenthesis returns a Verilog
-expression.  This is different from normal parenthesis in special contexts,
-such as PSL expressions, and can be used to embed bit concatenation ({})
-inside of PSL statements.
-
 =item $c(I<string>, ...);
 
 The string will be embedded directly in the output C++ code at the point

src/V3Options.cpp

@@ -715,7 +715,7 @@ void V3Options::parseOptsList(FileLine* fl, const string& optdir, int argc, char
 	    else if ( !strcmp (sw, "-E") )			{ m_preprocOnly = true; }
 	    else if ( onoff   (sw, "-MMD", flag/*ref*/) )	{ m_makeDepend = flag; }
 	    else if ( onoff   (sw, "-MP", flag/*ref*/) )	{ m_makePhony = flag; }
-	    else if ( onoff   (sw, "-assert", flag/*ref*/) )	{ m_assert = flag; m_psl = flag; }
+	    else if ( onoff   (sw, "-assert", flag/*ref*/) )	{ m_assert = flag; }
 	    else if ( onoff   (sw, "-autoflush", flag/*ref*/) )	{ m_autoflush = flag; }
 	    else if ( onoff   (sw, "-bbox-sys", flag/*ref*/) )	{ m_bboxSys = flag; }
 	    else if ( onoff   (sw, "-bbox-unsup", flag/*ref*/) ) { m_bboxUnsup = flag; }
@@ -745,7 +745,7 @@ 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", flag/*ref*/) )		{ m_psl = 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; }

test_regress/t/t_preproc_psl_on.pl

@@ -14,7 +14,7 @@ my $stdout_filename = "$Self->{obj_dir}/$Self->{name}__test.vpp";
 top_filename("t/t_preproc_psl.v");
 
 compile (
-    verilator_flags2 => ['-psl -E'],
+    verilator_flags2 => ['-psl-deprecated -E'],
     verilator_make_gcc=>0,
     stdout_filename => $stdout_filename,
     );

test_regress/t/t_psl_basic.pl

@@ -8,7 +8,7 @@ if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); di
 # Version 2.0.
 
 compile (
-	 v_flags2 => [$Self->{v3}?'--assert':($Self->{nc}?'+assert':'')],
+	 v_flags2 => [$Self->{v3}?'--assert --psl-deprecated':($Self->{nc}?'+assert':'')],
 	 );
 
 execute (

test_regress/t/t_psl_basic_cover.pl

@@ -10,7 +10,7 @@ if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); di
 top_filename("t/t_psl_basic.v");
 
 compile (
-	 verilator_flags2 => ['--psl --sp --coverage-user'],
+	 verilator_flags2 => ['--psl-deprecated --sp --coverage-user'],
 	 );
 
 execute (