Re: [$ieee-1850] Third draft (Mar-8) of IEEE-1850 PSL LRM

The LRM does not address the "first_match" function.  
For compatability to SVA and for use, it would be a good idea to add
the "first_match" function a la SVA.
I simulated the following code: 
  // psl default clock= posedge clk;
  // psl property p_a23b_c= 
  //  always {rose(a); [*1:2]; b} |-> {c};
  // psl assert p_a23b_c; 
  //  always {rose(a); [*1:2]; b} |-> {c};

A simulator yielded the fillowing error: 
  //  always {rose(a); [*1:2]; b} |-> {c};
                                       |
 (./firstmatch.sv,24): (time 360 NS) Assertion firstmatch.p_a23b_c has
failed (4 cycles, starting 180 NS)
360 NS + 0 (Assertion output stop: firstmatch.p_a23b_c = failed)

Attached is a copy of the  code and the error log. Contact me if you
need the simulation waveform.
 
/* -----\/----- EXCLUDED -----\/-----
// I also sImulated the equivalent code in sva, and the results 
// without the first_match were the same as PSL.  However, the use of the 
// first_match removed that unexpected anbiguity. 
// SVA tested code 
  property p_a23b_c;
  @(posedge clk) $rose(a) ##[2:3] b |-> c;
  endproperty : p_a23b_c
  ap_a23b_c : assert property (p_a23b_c);

  property p_FMa23b_c;
  @(posedge clk) first_match($rose(a) ##[2:3] b) |-> c;
  endproperty : p_FMa23b_c
  ap_FMa23b_c : assert property (p_FMa23b_c);
 -----/\----- EXCLUDED -----/\----- */

I strongly believe that the first_match function is a needed function
because without a first_match in the antecedent, unexpected results
may occur, and there is no method to remove that ambiguity.  If it is
too late to incorporate it in this revision, then we need to keep it
in mind for the next update of the lrm.
--------------------------------------------------------------------------
Ben Cohen Trainer, Consultant, Publisher (310) 721-4830 
http://www.vhdlcohen.com/  ben_ f rom _abv-sva.org
* Co-Author: SystemVerilog Assertions Handbook, 2005 ISBN 0-9705394-7-9
* Co-Author: Using PSL/SUGAR for Formal and Dynamic Verification 2nd
Edition, 2004, ISBN 0-9705394-6-0
* Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn
0-9705394-2-8
* Component Design by Example ", 2001 isbn 0-9705394-0-1
* VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn 0-7923-8474-1
* VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn 0-7923-8115
---------------------------------------------------------------------------