RE: [sv-ac] Sv-AC 1737

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.