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.