RE: [sv-ac] Sv-AC 1737

From: Korchemny, Dmitry <dmitry.korchemny_at_.....>
Date: Thu Mar 22 2007 - 07:04:20 PDT
Hi Jonathan,

If the property P is a sequence that the form proposed by Ed is
equivalent to condition ##0 P. Unfortunately, the latter form cannot be
used when P is an arbitrary property: in this case followed_by construct
not (condition |-> not (P)) must be written. Therefore it covers all the
cases.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Jonathan Bromley
Sent: Thursday, March 22, 2007 3:59 PM
To: sv-ac@server.eda-stds.org
Subject: RE: [sv-ac] Sv-AC 1737

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.
Received on Thu Mar 22 07:05:30 2007

This archive was generated by hypermail 2.1.8 : Thu Mar 22 2007 - 07:05:35 PDT