RE: [sv-ac] Behaviour of $past under "disable iff"

HI Jonathan,

Past sampled value functions are not affected by disable iff. This
should follow from the formal semantics description in Annex F. I agree
that it would be good to have a more explicit description in the LRM
body, and an example illustrating it.

Would you like to create a Mantis item?

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Jonathan Bromley
Sent: Wednesday, April 23, 2008 2:16 PM
To: sv-ac@server.eda.org
Subject: [sv-ac] Behaviour of $past under "disable iff"

hi AC,

We were asked recently whether the state stored by $past
(and its friends $rose, $fell) is affected by "disable iff".
I couldn't find anything explicit in the LRM about this;
it looks as though the intent is that the sampling for
$past should be unaffected by the disable-iff condition.

Consider

  assert property ( 
    disable iff (Reset) 
    @(posedge Clk) 
    $past(A) |-> B 
  );

Given that $past infers its clock from the context, users 
might imagine it would also respect the reset condition.  
Would it be helpful to describe this behaviour a little
more explicitly?

thanks
-- 
Jonathan Bromley


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