RE: [sv-ac] comments on 2069

Given that there now exists a "restrict" statement, and this is for
formal, do we also need to make it clear that "assumptions" in this
context refers to the set of properties defined by "assume property" and
"restrict property" 

Lisa

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of John
Havlicek
Sent: Thursday, March 13, 2008 10:06 AM
To: dmitry.korchemny@intel.com
Cc: sv-ac@eda.org; sv-champions@eda.org
Subject: [sv-ac] comments on 2069

Hi Dmitry:

From reviewing 2069 for Champions, I have the comments below.

J.H.

  . p. 2, Change "satisfied on each set trace" to "satisfied on each
trace".
  . p. 2, Change "satisfied on at least one set trace" to "satisfied on
at least 
    one trace".
  . p. 2.  The phrases 

       "trace that satisfies all the assumptions associated with the
model" 

    and 
    
       "feasible trace" 

    have not been defined that I can see.  I guess that these are
intended 
    to mean the same thing.  If so, I would change

       The following definitions describe assertion statement
satisfaction on a
       set of traces:
       
       - assert property statement is satisfied on a set of traces if it
is
         satisfied on each set trace that satisfies all the assumptions
         associated with the model.
       
       - assume property statement is satisfied on a set of traces if it
is
         satisfied on each trace of the set.
       
       - cover property statement is satisfied on a set of traces if it
is
         satisfied at least on one set trace satisfying all the
assumptions
         associated with the model.
       
       An assertion statement holds globally if it is satisfied on the
set of
       all feasible traces.

    to something like 

       Given a set of traces and a set of assumptions, the following
definitions
       describe assertion statement satisfaction on the set of traces
predicated
       on the set of assumptions:
       
       - A trace in the set of traces is _feasible_ if every assumption
in the set 
         of assumptions is satisfied on the trace.

       - An assert property statement is satisfied on the set of traces
predicated
         on the set of assumptions if it is satisfied on each feasible
trace.
       
       - A cover property statement is satisfied on a set of traces
predicated on
         the set of assumptions if it is satisfied on at least one
feasible trace.
       
       An assertion statement holds globally on the set of traces
predicated on
       the set of assumptions if it is satisfied on every feasible
trace.

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