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.