[sv-ac] 1599

From: John Havlicek <john.havlicek_at_.....>
Date: Thu Apr 26 2007 - 18:42:42 PDT
Hi Bassam:

I think the proposal for Mantis 1599 is in pretty good shape, but
there are a couple of changes that I would recommend to make it
clearer.  I think these changes are consistent with the intention
of what is already there.

I think that discussion of the effects of $assertkill needs to 
be more precise.  $assertkill is like a combination of a disable
and $assertoff.  An attempt can start and be "killed" by $assertkill.
Other attempts may be "turned off" by $assertkill, like $assertoff, 
because the $assertkill is in force.

I recommend changing the wording in 17.13.3 to the following:

  The coverage counters for success, failure, or vacuous success 
  do not include attempts that start but that end as disabled or 
  killed.  The attempt counter includes the attempts that start 
  but that end as disabled or killed.  None of the counters includes
  attempts that do not start because they are turned off as a result
  of $assertoff or $assertkill.

In the changes to 28.3.2, I recommend adding

  cbAssertionKilledEvalutaiont
  An asseriton attempt reaches the killed state as a result of 
  $assertkill executing after the attempt starts.

It is still not completely clear to me how the disable/kill conditions
interplay with the starting of evaluation.  E.g., what should we get
for

  foo:  assert property (
     disable iff (clk)
     @(posedge clk)
     blah
  );

?  Which counter should update?

Best regards,

John H.


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Thu Apr 26 18:43:04 2007

This archive was generated by hypermail 2.1.8 : Thu Apr 26 2007 - 18:43:11 PDT