[sv-ac] RE: 1599

Hi John, please see below. 

Thx.
-Bassam.

-----Original Message-----
From: John Havlicek [mailto:john.havlicek@freescale.com] 
Sent: Thursday, April 26, 2007 6:43 PM
To: bassam.tabbara@synopsys.COM
Cc: sv-ac@eda-stds.org
Subject: 1599

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.

BT>>> I think this is totally redundant, since "disabled", and "killed"
are now bona fide (result) states. Think of it this way, we don't need
to say that "success" do not include attempts that start but end in
"failure" :) Convinced ? As for last sentence, yes kill doubles up, but
we say  "e.g. assertoff" in text today... I fear if we update it'll make
the kill counting unclear. Anyway, should be reasonably clear that if
something is not attempted it does not go into any of the counts.

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.

BT>>> cbAssertionKill already serves this purpose, I think changing name
is not desirable for backward compatibility.

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?

BT>>> For assert property (@(posedge clk) disable iff (cond) ....) the
attempt counter increments every posedge clk, if cond is enabled then
the final result of this attempt is "disabled" (increment counter). To
kill something, it must've been running ... Basically unless "off", you
always have to start (attempt) to get to any state (disabled, kill,
success, fail, "in progress").

Best regards,

John H.


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