RE: [sv-ac] RE: Two items for ease of assertion writing

Hi Dave:

I don't think nesting of sampled value functions is expressly forbidden.
I think that the semantics is well defined. One should check carefully,
but I think that

   $past($past(e))

is equivalent to

   $past(e, 2)

In your example, I think

   $past(A && $past(B))

should be equivalent to

   $past(A) && $past(B,2)

In Tom's example,

   $past(txn_valid[txn_id])

does not index with the current value of txn_id -- instead the past
value of the indexed expression txn_valid[txn_id] is what you get. If
you want the current value of txn_id to index into the past value of
txn_valid, then you would want to write something like

   $past(txn_valid)[txn_id]

This looks reasonable to me.

J.H.

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Rich, Dave
Sent: Tuesday, April 13, 2010 11:50 AM
To: Korchemny, Dmitry; Thomas Thatcher
Cc: sv-ac@eda.org
Subject: RE: [sv-ac] RE: Two items for ease of assertion writing

> 2. Is there a way to index an array enclosed by $past() using the
> current sampled value of a variable?
>
> for example
> txn_valid(txn_id) && $past(txn_valid[txn_id])
> ^want to index with the
> current sampled value
> of txn_id
>
> The only way I have figured out to make this work is to explicitly
> create a delayed version of txn_valid and use that instead of the
> $past() function.
>
> Another option I thought of just now would be to extend the $stable()
> system function to take an optional parameter for number of cycles.
>
>
> [Korchemny, Dmitry] If I understand your question correctly, you can
> write it as:
> txn_valid(txn_id) && $past(txn_valid[$sampled(txn_id)])
>
> I can enter Mantis items if either of these turns out to be more than
> just a user education issue.
>

[DR] This raises some serious issues regarding the nesting of sampled
value functions. Can they be nested? If so, does the sampling nest as
well. i.e.

$past(A && $past(B))

Are A and B both 1 cycle in the past or is B 2 cycles in the past?

Dave

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