Re: [sv-ac] Sv-AC 1737

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
>
>
> -----Original Message-----
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
> Behalf Of John Havlicek
> Sent: Thursday, March 22, 2007 10:24 AM
> To: jonathan.bromley@doulos.com
> Cc: sv-ac@server.eda-stds.org
> Subject: Re: [sv-ac] Sv-AC 1737
>
> Hi Jonathan:
>
> I know you have already received several responses that have explained
> that "b ##0 P" is not legal for a general property expression P and that
> the double negation expresses the dual of "|->", which has the desired
> semantics.
>
> I think it would be nice if we could get away with overloading "##0" to
> stand for the dual of "|->", so that the form "b ##0 P" would be legal
> for general P, but this might cause the grammar to become too ambiguous
> or to have other bad technical properties.
>
> J.H.
>
> >
> > SV-AC,
> > 
> > Please excuse the intrusion.  I've been following the 1737 discussion
> > and wanted to ask a question that will probably expose my ignorance
> > and/or stupidity.
> > 
> > When creating "cover property" with an inferred antecedent,
> > 
> >   ... if (condition) begin
> >         cover property (P);
> >   ...
> > is rewritten as
> > 
> > cover property (not (condition |-> not (P)));
> > 
> > I understand and agree with this, but I can't see any difference
> > between
> >   cover property (not (condition |-> not (P))); and the
> > easier-to-understand
> >   cover property (condition ##0 P);
> > 
> > Can someone kindly explain why the double-negation form is preferable?
> >
> > Thanks in advance
> > --
> > Jonathan Bromley
> > 
> >
> > -- This message has been scanned for viruses anddangerous content by
> MailScanner, and isbelieved to be clean.
> >
>
> --
> 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.
>
>


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