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 > ----------------------------------------------------------------------- > ----
This archive was generated by hypermail 2.1.8 : Sun Mar 13 2005 - 23:41:53 PST