[sv-ac] RE: 1599

Hi John, my comments below. I updated the proposal (also to draft3
citations). 

Thx.
-Bassam.

-----Original Message-----
From: John Havlicek [mailto:john.havlicek@freescale.com] 
Sent: Friday, April 27, 2007 4:55 AM
To: Bassam.Tabbara@synopsys.COM
Cc: john.havlicek@freescale.com; sv-ac@eda-stds.org
Subject: 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?"


BT>> I added more context into the proposal, this section is talking
about coverage for properties and the history of this (805) meant to
emphasize that disabled is not an interesting / tracked state here and
does not get folded into one of the other counts except for attempt
hence the wording and why killed (applies to assertion attempt) is not
mentioned.

> 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>> Done. I replaced that confusing incomplete line at the end with a
reference to 39.5.3 with the equation. This is NOT the place to think
about attempts states etc ... Rather paragraph here is meant to focus on
listing the coverage property required results.

> BT>>> cbAssertionKill already serves this purpose, I think changing 
> BT>>> 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?

BT>> Yes see end of 38.4.2.

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

BT >> Yes first attempt and then "disabled" is a result of the
assertion.

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?

BT >> I would think so yes. Anyway kill applies to the in-flight
assertion if the scheduling were different.

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