RE: [sv-ac] 1668 update

Hi John,

Do we really want to support this type of property?

property p;

logic v;

(1,v = 0) ##1 (logic v; (1, v = 1) ##1 (v == 1)) ##1 (v ==0);
endproperty

Although the flow rules hint that this property holds in every
computation (weak semantics), it does not say so explicitly. If we do
want to support it we should define scope rules. If not, we should
forbid declaring the same local variable twice in the same
property/sequence.

Doron

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of John Havlicek
Sent: Saturday, August 18, 2007 5:21 PM
To: sv-ac@server.eda-stds.org
Subject: [sv-ac] 1668 update

Hi Folks:

I have good news about 1668.  I got the intuition last Monday
that introducing the parenthesized, scoped local variable 
declarations to the abstract syntax should be able to give
us a good solution for local variable declaration assignments
even for sequences that admit empty match.

I have spent a lot of time this past week working out the
theory for this, and it looks very good to me.  I have attached
my plain text notes, which I will also put on mantis.

I intend to revise the proposal documents to remove the restriction
disallowing empty match, one which I have never liked.

I also introduced a formal definition of admits_empty at the
level of the abstract syntax to address Dmitry's concerns.  I 
carried out the proof that this definition faithfully represents
at that level the notion of admitting tight satisfaction by the
empty word after local variable declaration assignments and
clocks are eliminated.  This was not as easy as I had hoped, but
maybe the proofs can be simplified.

Please have a look and send any feedback that you have.

J.H.

-- 
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.