RE: [sv-ac] Sv-AC 1737

Doron,

Thanks for the clarification. 

-Jiang 

-----Original Message-----
From: Doron Bustan [mailto:dbustan@freescale.com] 
Sent: Friday, March 23, 2007 2:27 PM
To: Long, Jiang
Cc: Havlicek John-r8aaau; sv-ac@eda-stds.org
Subject: Re: [sv-ac] Sv-AC 1737

Hi Long,

the idea in the double negation is that in case that (a != 1), the
property does not succeeds and does not count as a cover hit.

We do not want to make the distinction between vacuous and non-vacuous
coverage hits, so we provide a mechanism that will not pass when the
antecedent does not hold.

I agree that double negation is not nice, and we plan to have a
followed_by operator to replace it.

regards

Doron

Long, Jiang wrote:

> Doron and John,
>
> Thanks for the pointers. I read the latest P1800-2008 draft in Annex
> F.3.3.3 vacuity and section 16.13.3 ( John, I think the new LRM draft 
> changed section ordering).
>
> Yes, it is consistent now with translation of "double negation" form.
>
> With the latest Annex F.3.3.3. treatment of vacuity, it seems that a 
> direct coversion of the cover statement is the same as the double 
> negation form in this context. If that is the case, I would suggest 
> not using double negation, because it is not as intuitive.
>
> > > property r4_cover;
> > >       @(posedge mclk) not((a==1) |-> not ((q != d) ##1 ack)); 
> > > endproperty
> r4_c: cover property ( r4_cover);
>
> v.s.
>
> property r4_cover;
> @(posedge mclk)  (a==1) |-> ( (q!=d) ##1 ack)) ; endproperty
> r4_c: cover property ( r4_cover);
>
> Anyway, I think the double negatioin form is not very intuitive for 
> the readers/users. The question is : is it possible to fit it with 
> direct translation, the same way as for those concurrent procedural
"assert"
> statements?
>
> -Jiang
>
> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@freescale.com]
> Sent: Friday, March 23, 2007 5:33 AM
> To: Long, Jiang
> Cc: sv-ac@eda-stds.org
> Subject: Re: [sv-ac] Sv-AC 1737
>
> Hi Jiang:
>
> > 1737 suppose to complete proposal 1381, which had already passed and

> > which redefine vacuity. I think that
> > 1737 is consistent with 1381.
>
> Was this explanation sufficient? 
>
> If you look at P1800-2008-draft1 in 17.13.6 and E.3.3.3, you will see 
> the recursive definitions of non-vacuous (and hence also of vacuous) 
> evaluation attempt.  The "not" operator does not affect the vacuity of

> an attempt, i.e. an attempt of "P" is non-vacuous iff an attempt of 
> "not P" starting from the same point is non-vacuous.
>
> J.H.
>
> > Date: Thu, 22 Mar 2007 13:47:18 -0500
> > From: Doron Bustan <dbustan@freescale.com>
> > X-Accept-Language: en-us, en
> > CC: Havlicek John-r8aaau <john.havlicek@freescale.com>,
> >         jonathan.bromley@doulos.com, sv-ac@eda-stds.org
> > X-OriginalArrivalTime: 22 Mar 2007 18:47:19.0556 (UTC) 
> > FILETIME=[850D2C40:01C76CB2]
> >
> > Hi Long,
> >
> > 1737 suppose to complete proposal 1381, which had already passed and

> > which redefine vacuity. I think that
> > 1737 is consistent with 1381.
> >
> > Doron
> >
> >
> > Long, Jiang wrote:
> >
> > > Hello all,
> > >
> > > Please excuse the intrusion too.
> > >
> > > I have a question about the 'equivalent' translation of cover 
> > > statement through "double negation".
> > >
> > > property r4;
> > >       @(posedge mclk)((q != d) ##1 ack); endproperty
> > >
> > > always @(posedge mclk) begin
> > >       case (a)
> > >             1: begin q <= d1;
> > >                   r4_p: assert property (r4);
> > >                   r4_c: cover property (r4);
> > >             end
> > >             default: q1 <= d1;
> > >       endcase
> > > end
> > > property r4_cover;
> > >       @(posedge mclk) not((a==1) |-> not ((q != d) ##1 ack)); 
> > > endproperty
> > > r4_c: cover property (r4_cover);
> > >
> > > In the above example from the proposal, I suspect the use of 
> > > double negation is to avoid the 'vacuous pass' of the antecedent 
> > > inferred from the context. However, the double negation makes 
> > > unclear what is
>
> > > a pass/vacuous pass for the original cover property ( in this 
> > > case, it is r4).
> > >
> > > For example, if r4 is defined as
> > >
> > > property r4;
> > > @(posedge mclk)  ( q!=d ) |=> ##[1:2] ack; endproperty
> > >
> > > //double negation:
> > > property r4_cover;
> > > not ( ( a==1) |-> not (r4)  ) ;
> > > endproperty ;
> > > r4_c : cover property (r4_cover);
> > >
> > > It seems that the double negation form will make it non-intuitive 
> > > (if not inconsistent) with regard to  what is to count as a 
> > > vacuous pass, non-vacuous pass or number of attempts as defined in

> > > the LRM (
>
> > > version published 22 Nov 2005)  page  288.
> > >
> > > Thanks in advance,
> > >
> > > -Jiang
> > >
> > >
>
> --
> This message has been scanned for viruses and dangerous content by 
> MailScanner, and is believed to be clean.
>
>


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