From 1bdf017f9e3867641f9b311739e4ada4ad271e8a Mon Sep 17 00:00:00 2001 From: Wilson Snyder Date: Fri, 14 Mar 2014 21:14:24 -0400 Subject: [PATCH] PSL is no longer supported, please use System Verilog assertions. --- Changes | 2 ++ TODO | 2 ++ bin/verilator | 49 ++--------------------------- src/V3Options.cpp | 4 +-- test_regress/t/t_preproc_psl_on.pl | 2 +- test_regress/t/t_psl_basic.pl | 2 +- test_regress/t/t_psl_basic_cover.pl | 2 +- 7 files changed, 12 insertions(+), 51 deletions(-) diff --git a/Changes b/Changes index 42f3f9244..95c97d840 100644 --- a/Changes +++ b/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] diff --git a/TODO b/TODO index 5a0322521..8accc1f62 100755 --- a/TODO +++ b/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 diff --git a/bin/verilator b/bin/verilator index 6596822e7..81e12ab4f 100755 --- a/bin/verilator +++ b/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[=] Set preprocessor define --debug Enable debugging @@ -311,7 +311,6 @@ descriptions in the next sections for more information. --prefix 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 semantics to be used. =item --assert -Enable all assertions, includes enabling the --psl flag. (If psl is not -desired, but other assertions are, use --assert --nopsl.) +Enable all assertions. 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) - -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, ...); The string will be embedded directly in the output C++ code at the point diff --git a/src/V3Options.cpp b/src/V3Options.cpp index 316deea69..04e97e55f 100644 --- a/src/V3Options.cpp +++ b/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; } diff --git a/test_regress/t/t_preproc_psl_on.pl b/test_regress/t/t_preproc_psl_on.pl index 92bc4fc00..fd818a94a 100755 --- a/test_regress/t/t_preproc_psl_on.pl +++ b/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, ); diff --git a/test_regress/t/t_psl_basic.pl b/test_regress/t/t_psl_basic.pl index 95e70fe4a..21301e528 100755 --- a/test_regress/t/t_psl_basic.pl +++ b/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 ( diff --git a/test_regress/t/t_psl_basic_cover.pl b/test_regress/t/t_psl_basic_cover.pl index 190484a4c..700c38158 100755 --- a/test_regress/t/t_psl_basic_cover.pl +++ b/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 (