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

Hi Ben,

I am removing your attachment.  It seems to be causing a problem  
(detected as a possible virus).  You message should make it through the  
reflector this time for the working group to review.

-Harry

On Mar 13, 2005, at 9:05 PM, ben cohen wrote:

> 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
> ----------------------------------------------------------------------- 
> ----
> <firstmatch2.zip>