RE: [sv-ac] Sv-AC 1737

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.