RE: [sv-ac] FW: Difference between PSL prev() and SVA $past()

You might be referring to Mantis 1550 and Mantis 1698.

Shalom
 

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On
> Behalf Of Havlicek John-R8AAAU
> Sent: Tuesday, June 15, 2010 6:43 AM
> To: Korchemny, Dmitry; sv-ac@eda.org
> Cc: Avigail Orni
> Subject: RE: [sv-ac] FW: Difference between PSL prev() and SVA $past()
>
> Hi Folks:
>
> I believe that when we considered the semantics of
> $past(e,@c) we tried
> to align it with the behavior of $sampled(past_e_at_c) where
>
> type(e) past_e_at_c;
> always @(c)
> past_e_at_c <= $sampled(e);
>
> For reasonably behaved c, this leads to a straightforward
> implementation
> such that
>
> @(d) $past(e,@(c))
>
> is left-continuous as d -> c, but not right-continuous.
>
> The PSL-2010 definition of prev is aligned with a pasttime version of
> the clocked nexttime (involving first a backward alignment to
> the clock
> and then backward traversal to the next previous clock).
> This operator
> is right-continuous, but not left-continuous. I'm not sure what
> goodness criteria it satisfies, and it is getting too late
> for me to try
> to write down an HDL implementation.
>
> If anyone remembers the Mantis ID from when we worked on this
> previously, please send it along ... there may be some useful notes.
>
> J.H.
>
> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
> Korchemny, Dmitry
> Sent: Sunday, June 06, 2010 12:46 AM
> To: sv-ac@eda.org
> Cc: Avigail Orni
> Subject: [sv-ac] FW: Difference between PSL prev() and SVA $past()
>
> Hi all,
>
> Forwarding the note from Avigail.
>
> Thanks,
> Dmitry
>
> -----Original Message-----
> From: Avigail Orni [mailto:ORNIA@il.ibm.com]
> Sent: Thursday, June 03, 2010 9:24 PM
> To: Korchemny, Dmitry
> Subject: Difference between PSL prev() and SVA $past()
>
>
> Hi Dmitry,
>
> I've written the note below for the SV-AC committee.
> I think I can't send it to the committee mailing list, so I
> hope you can
> pass on this information to the others.
>
> Many thanks,
> Avigail
>
> --------------------------------------------------------------
> ----------
> ------------------------
>
> Dear SV-AC,
>
> I would like to bring to your attention a misalignment between PSL and
> SVA, which was introduced by developments in the SV-2009 and PSL-2010
> standards.
>
> Generally, the difference is in cases where prev/$past is
> clocked with a
> slower clock than the property (or statement) in which it appears.
> As a running example, consider the one from the PSL-2005 LRM, section
> 5.2.3.1 (p. 39):
>
> time 0 1 2 3 4 5 6 7
> -----------------------
> clk 0 1 0 1 0 1 0 1
> a 0 0 1 1 0 1 0 0
>
> The general question is: what is the value of prev(a, clk) between the
> ticks of 'clk'?
>
>
> History (2005 LRMs)
> ---------------------------
> PSL:
> (*) No formal semantics
> (*) The LRM text gives an example (the one mentioned above).
> According to the example, the value of prev(a, clk) is always 0
> between ticks of 'clk'.
>
> SVA:
> (*) The formal semantics don't explicitly address this case.
> (*) The LRM text gives a restriction:
> "When these functions are used in an assertion, the
> clocking event
> argument of the functions, if specified,shall be identical to the
> clocking event of the expression in the assertion."
> I take this to mean that the case we are dealing with is illegal
> (we
> can only use $past(a, clk) inside a property that is clocked with
> 'clk'), so the question is irrelevant.
>
>
> Current status (2009/10 LRMs)
> ----------------------------------------
> PSL
> (*) New formal semantics: for prev(a, clk), go to the last tick of
> 'clk' (which may be the current tick), and then go back to the
> preceding
> tick of 'clk'. Take the value of 'a' at that time point.
> (*) In our running example, at time tick 4 we should have prev(a,
> clk)=0
>
> SVA
> (*) The LRM restriction has been removed, so the case we are
> discussing
> is legal.
> (*) Formal semantics: for $past(a, clk), if we are not on a tick of
> 'clk' then take the value of 'a' at the last tick of
> 'clk'. If we are
> on
> a tick of 'clk' then take the value at the previous tick of 'clk'
> (*) In our running example, at time tick 4 we should have $past(a,
> clk)=1
>
> Here is a diagram to illustrate the difference in the 2009/10 LRMs.
> We use a1, a2, a3,... to denote the value of 'a' at time
> ticks 1, 2, 3,
> ...
> aH is the init value that 'a' should get according to the simulation
> semantics of the HDL.
>
> time 0 1 2 3 4 5 6 7 8 9 10 11
> ------------------------------------------------------------------
> clk 0 0 1 0 0 1 0 0 1 0 0 1
> a a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
>
> prev(a,clk) aH aH aH aH aH a2 a2 a2 a5 a5 a5 a8
>
> $past(a,clk) aH aH aH a2 a2 a2 a5 a5 a5 a8 a8 a8
>
>
> I think it is important to be aware of this difference.
> The committee can also consider whether to take some action to solve
> this misalignment.
>
>
> Best regards,
> Avigail
> _______________________________________________________
> Avigail Orni
> Formal Verification Group
> IBM Haifa Research Laboratory
> Phone: 972-4-829-6396 email: ornia@il.ibm.com
>
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
>
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or
> distribution by
> others is strictly prohibited. If you are not the intended recipient,
> please contact the sender and delete all copies.
>
>
> --
> This message has been scanned for viruses and dangerous content by
> MailScanner, and is believed to be clean.
>
>
>
>
> --
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
>
>
>
---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.