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

From: Harry Foster <harrydfoster_at_.....>
Date: Sun Mar 13 2005 - 23:41:47 PST
This didn't make it to the group since it was not sent from the  
standard email address.

Begin forwarded message:

> From: ben cohen <hdlcohen@gmail.com>
> Date: March 13, 2005 9:05:52 PM PST
> To: "Harry D.Foster" <harry@jasper-da.com>
> Cc: ieee-1850@eda.org
> Subject: Re: [$ieee-1850] Third draft (Mar-8) of IEEE-1850 PSL LRM
> Reply-To: ben cohen <hdlcohen@gmail.com>
>
> 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
> ----------------------------------------------------------------------- 
> ----



Received on Sun Mar 13 23:41:52 2005

This archive was generated by hypermail 2.1.8 : Sun Mar 13 2005 - 23:41:53 PST