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.