[sv-ac] Re: 1599

Hi Bassam:

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

No.  My intention is to make the text clearer, not to eliminate
redundancy.  

My understanding is that "disabled" and "killed" are mutually 
exclusive ending dispositions for an attempt.

The current suggested text for 17.13.3 is

   The coverage counters for success, failure or vacuous success do not
   include disabled evaluations. The attempt counter includes the
   attempts which result in disabled evaluation. None of the counters are
   updated when an assertion is turned off e.g. as a result of
   $assertoff.

The sentences

   The coverage counters for success, failure or vacuous success do not
   include disabled evaluations.  The attempt counter includes the
   attempts which result in disabled evaluation.

invite the questions, "What about the killed evaluations -- are they 
treated the same as disabled or differently, and why are you making 
me think about this?"

> Anyway, should be reasonably clear that if
> something is not attempted it does not go into any of the counts.

Yes, but is it clear when something is not attempted?  If there are
ways to "turn off" attempts other than $assertoff and $assertkill,
then we should alert the reader to that fact.

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

O.k., this looks fine.  What about the content of cb_time in the 
case of a killed attempt?  Does it give the time when the attempt
reached the killed state?

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

O.k., so for my example you are saying that the attempt and disabled
counters both increment at every posedge clk?

And if I have 

   always @(posedge clk)
      $assertkill(foo);

   foo:  cover property (
      @(posedge clk)
      blah
   );

then is it deterministic in the first timestep in which there is a
posedge clk that the $assertkill(foo) executes in the active region 
before the attempt starts in the observed region?

J.H.


> x-mimeole: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Thu, 26 Apr 2007 20:00:09 -0700
> Thread-Topic: 1599
> Thread-Index: AceIbV3L/cd6ag5AQB2v7963vmc0VQABwdhQ
> From: "Bassam Tabbara" <Bassam.Tabbara@synopsys.com>
> Cc: <sv-ac@eda-stds.org>
> X-OriginalArrivalTime: 27 Apr 2007 03:00:09.0755 (UTC) FILETIME=[2AB8B6B0:01C78878]
> 
> Hi John, please see below.=20
> 
> Thx.
> -Bassam.
> 
> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@freescale.com]=20
> 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.