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.