RE: [sv-ac] Annex F document for 1549

Hi John,

This proposal looks very good to me.

Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of John Havlicek
Sent: Monday, August 06, 2007 4:00 PM
To: sv-ac@server.eda-stds.org
Subject: [sv-ac] Annex F document for 1549

Hi Folks:

I have uploaded the .pdf for the Annex F document for 1549
and attached it below.

This version differs from the one I sent out last night in one 
place--in flatten_property the last step has been corrected to refer
to property_spec, which is the body of a property, rather than
property_expr.

I thought I should highlight the more substantial changes that I
made from the last version by Doron.

. I changed the perspective of the rewriting algorithm from rewriting
  assertions to rewriting properties.  I did this because I don't
  think the rewriting has anything to do with what is going on in the
  semantics at the level of assertion directive in Annex F.  In
  F.3.3.1, the concern is with the implicit "always" that comes with
  an assertion directive and with the meaning of the inferred enabling
  condition.

. Regarding the term "property", we use this term in Annex F and
  distinguish "top-level properties" as the ones in which a 
  "disable iff" may appear.  Therefore I kept the term "property" and 
  avoided the terms "property_spec" and "property_expr" except when
  referring to the body property_spec (as corrected) in flatten_property
  and in the definition of p[0].

. I changed the perspective of the definition of the k-fold
  approximation in the changes for F.5 from assertions to properties.
  Again, I don't think the part of the semantics that deals with
  assertion directives has anything to do with the k-fold
  approximations.  If you follow the semantics definitions from the
  top down, you have to account for the implicit "always" from the
  assertion directive and the enabling condition in F.3.3.1 Then you
  get to the point where you need to understand what it means to
  satisfy a top-level property.  At that point, you can use the k-fold
  approximations if the property depends on instances of recursive
  properties (perhaps through a chain of instances of nonrecursive
  properties).

. I changed the procedures flatten_property and flatten_sequence to be 
  functions.  Previously, these procedures referred to the enveloping 
  assertion, which is now gone.

. I got rid of the steps in flatten_property and flatten_sequence that
  make the local variable identifiers unique.  With the local variables
  in the abstract syntax, I don't think we need this.  We could still
  do it, but it is another step and more text.

. I changed the example in F.1 to illustrate more details of why $var 
  is needed.

I am not entirely sure that syntax like

  (logic[3:0])'({a,b})

is legal in Draft3a.  It would be good to check on this.  I think this
syntax 
ought to be legal, but I can only get things like

  logic'({a,b})

from the BNF.

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.