RE: Group A - first draft LRM changes

erich,

>I see where you are going with this, but I don't think it is quite
sufficient. Specifically, in item 5 below,
>you still define the derived path as the path "obtained by extracting from
the given path exactly those cycles
>in which clk holds". But it seems to me that I can write a property that
contains a subproperty that can only
>be satisfied if I consider the sequence of states *between* successive
clock ticks

yes, of course. that is why my number 5 specifies that sub-properties are
calculated before the extraction of the cycles in which clk holds.

>It seems to me that both an implementation and the user's intuitive
understanding would more likely involve
>checking A@CLK on the given path, considering each state in succession,
and for each successive state, ignoring
>it if the 'current clock context' does not hold, where 'current clock
context' switches from time to time as
>different parts of the property a
> re checked.

in general, i like your approach. however, i am a little leary of
cluttering up the document by involving the clock context in the discussion
of the semantics of each operator. i wonder if there is a way to do what
you are suggesting while keeping all the relevant text in the section on
the clock operator?

cindy.

--------------------------------------------------------------------
Cindy Eisner
Formal Methods Group
IBM Haifa Research Laboratory
Haifa 31905, Israel
Tel: +972-4-8296-266
Fax: +972-4-8296-114
e-mail: eisner@il.ibm.com

"Erich Marschner" <erichm@cadence.com>@eda.org on 16/12/2004 06:23:42

Sent by: owner-ieee-1850-extensions@eda.org

To: Cindy Eisner/Haifa/IBM@IBMIL
cc: <ieee-1850-extensions@eda.org>
Subject: RE: Group A - first draft LRM changes

Cindy,

Thanks for the suggestion. I see where you are going with this, but I
don't think it is quite sufficient. Specifically, in item 5 below, you
still define the derived path as the path "obtained by extracting from the
given path exactly those cycles in which clk holds". But it seems to me
that I can write a property that contains a subproperty that can only be
satisfied if I consider the sequence of states *between* successive clock
ticks - e.g.,

   (a -> next {(a && !clk)[+]; clk}@True)@clk

which requires more than just the cycles in which clk holds.

I am beginning to wonder whether this is even the right approach. There
are several reasons:

1. The discussion about the semantics of abort strongly suggests that,
unless all clocked properties are affected by the clock in the same way, it
may be difficult or even inappropriate to try to give a general statement
of the semantics of clocked properties. Instead, it might be better to
simply state that @ defines the clock context for a property, and then
under each different kind of property, specify the semantics of that form
of property under a clock context.

2. This is supposed to be an informal specification of the semantics, not a
formal one, yet we are tending more and more towards a formal (albeit
English) specification of the semantics (i.e., the projection view). The
more formal the 'informal' semantic definition gets, the less accessible it
will be for most users.

3. The basic assumption in the current approach (that you can derive a path
containing only the cycles in which the clock expression holds, and then
check the property on that derived path) seems to be false in the general
case. Yes, this definition works for singly-clocked properties, where no
clock switching occurs; but it doesn't work for the more general case where
there are multiple clocks (which can include @True as a 'highest possible
frequency' clock). I have a feeling that the problem comes from trying to
define the processing in two stages: first derive path p' from the given
path p; then check A@CLK on p'. It seems to me that both an implementation
and the user's intuitive understanding would more likely involve checking
A@CLK on the given path, considering each state in succession, and for each
successive state, ignoring it if the 'current clock context' does not hold,
where 'current clock context' switches from time to time as different parts
of the property a
 re checked. Perhaps an operational semantics of this sort would make more
sense in an informal semantic presentation.

Am I way off base in thinking the above? If so, why?

Regards,

Erich

| -----Original Message-----
| From: Cindy Eisner [mailto:EISNER@il.ibm.com]
| Sent: Wednesday, December 15, 2004 7:38 AM
| To: Erich Marschner
| Cc: ieee-1850-extensions@eda.org
| Subject: Re: Group A - first draft LRM changes
|
|
|
|
|
| erich,
|
| >- in Clause 6.1.2.5, Clocked SERE, change the informal semantics to
| >read
| as follows:
| > "For unclocked SERE A and Boolean CLK:
| > A@CLK holds tightly on a given path iff CLK holds in the last
| > cycle
| of the given path,
| > and A holds tightly on the path obtained by extracting
| the from
| > the
| given path exactly
| > those cycles in which CLK holds, and any subordinate
| sequences of
| > A
| hold tightly as
| > specified by A on the corresponding sub-paths of the
| given path."
| > ...
| >[Note: I'm not happy with this yet, but this is the best
| I've been able
| >to
| do so far.]
|
| how about the following fix:
|
| 1. split the semantics into two parts, one for seres
| containing no clocked sub-seres, one for seres containing
| clocked sub-seres. for the purposes of this discussion, call
| these two parts "semantics part 1" and "semantics part 2".
|
| 2. modify "for unclocked sere a" above to "for sere a
| containing no clocked sub-seres" in semantics part 1.
|
| 3. take away the phrase "and any subordinate sequences of A
| hold tightly as specified by A on the corresponding sub-paths
| of the given path." from semantics part 1.
|
| 4. add the following note below the semantics part 1: note
| that a@clk is defined for all paths, including those that do
| not begin with a cycle in which clk holds. we make use of
| this fact below in the informal semantics of a@clk, where a
| contains a clocked sub-sere below.
|
| 5. add the following informal semantics as part 2: "for
| sere a containing clocked sub-seres a_1, a_2, ... a_n and
| boolean clk": a@clk holds on a give path iff a' holds on the
| path obtained by extracting from the given path exactly those
| cycles in which clk holds. a' is obtained from a by
| substituting, for each a_i, a new boolean variable a_i',
| which holds on a path iff a_i holds on the path (before the
| extraction of the cycles in which clk holds).
|
| 6. add the following note after the semantics part 2: note
| that in the informal semantics of a sere containing a clocked
| sub-sere, the semantics of the clocked sub-sere is not
| affected by the clock of the outer sere, nor are the
| semantics of the outer sere affected by the clock of the
| inner sub-sere. thus, clocks are not cumulative. that is,
| there is no conjunction of nested clocks.
|
| and the corresponding changes for clocked fl properties.
|
| regards,
|
| cindy.
|
| --------------------------------------------------------------------
| Cindy Eisner
| Formal Methods Group
| IBM Haifa Research Laboratory
| Haifa 31905, Israel
| Tel: +972-4-8296-266
| Fax: +972-4-8296-114
| e-mail: eisner@il.ibm.com
|
| "Erich Marschner" <erichm@cadence.com>@eda.org on 14/12/2004 08:37:58
|
| Sent by: owner-ieee-1850-extensions@eda.org
|
|
| To: <ieee-1850-extensions@eda.org>
| cc:
| Subject: Group A - first draft LRM changes
|
|
|
| Following is a first draft of the changes required for Group A.
| (See http://www.eda.org/ieee-1850/Issues/Group-A.html.)
|
| ================================================================
|
| LRM Changes for Group A
|
| 1. Define "clock context" in the LRM body.
|
| Clause 4.4.1, Clocked vs. unclocked evaluation
| - add the following initial paragraphs (note that this is
| part of a general rewrite of 4.4.1; see below):
|
| "A PSL property, sequence, endpoint, or built-in function
| can be qualified
| by a /clock context/ which causes the property, sequence,
| endpoint, or
| built-in function to apply only to states in which the
| clock context holds.
| A nested property, sequence, endpoint, or built-in
| function within a given
| property or sequence can have a different clock context
| than that of the
|
| parent property or sequence."
|
| "The /base clock context/ is True, i.e., the granularity of
| time as seen by the
| verification tool. Different verification tools may model
| time at different
| levels of granularity. For example, an event-driven
| simulation tool typically
| has a relatively fine-grained model of time, whereas a
| cycle-based simulation
| or formal verification tool typically has a more
| coarse-grained model of time."
|
| "A clock context may be specified explicitly or may be
| inherited implicitly
| from an enclosing construct or region. An explicitly
| specified clock context
| takes precedence over an inherited clock context."
|
|
| 2. Extend built-in functions prev, rose, fell, stable to
| include an optional clock parameter.
|
| - in Clause 5.2.3, Built-in functions, extend the syntax to allow
| Built_In_Function_Call ::=
| prev ( Any_Type [ , Number [ , Clock_Expression ] ] )
| | stable ( Any_Type [ , Clock_Expression ] )
| | rose ( Bit [ , Clock_Expression ] )
| | fell ( Bit [ , Clock_Expression ] )
|
|
| 3. Explain how clock contexts are defined explicitly or
| inherited from an immediately containing construct or region.
|
| - in Clause 5.2.3, Built-in functions, add:
| "For a built-in function reference that specifies a clock
| parameter, the clock
| context is that given by the clock parameter. For a
| built-in function reference
| that does not specify a clock parameter, the clock
| context is that of the clock
| expression, property, sequence, declaration, or directive
| in which the built-in
| function reference is immediately contained."
|
| - in Clause 5.3, Clock expression, add:
| "For any clock expression, the clock context is the base
| clock context."
|
| - in Clause 6.1.2, Sequences, add:
| "For an unclocked sequence, the clock context is that of
| the property, sequence,
| declaration, or directive in which the unclocked sequence
| is immediately
| contained."
|
| - in Clause 6.1.2.5, Clocked SERE, add:
| "For a clocked SERE, i.e., a braced SERE that is the left
| operand of the @
| operator, the clock context is given by the right operand
| of the @ operator."
|
| - in Clause 6.1.3.2, Sequence instantiation, add:
| "For an unclocked sequence instance, the clock context is
| that of the property,
| sequence, declaration, or directive in which the
| unclocked sequence instance
| is immediately contained."
|
| - in Clause 6.1.4.2, Endpoint instantiation, add:
| "For an unclocked endpoint instance, the clock context is
| that of the property,
| sequence, declaration, or directive in which the
| unclocked endpoint instance
| is immediately contained."
|
| - in Clause 6.2.1, FL Properties, add:
| "For a given unclocked property, the clock context is that
| of the property, sequence,
| declaration, or directive in which the given property is
| immediately contained."
|
| - in Clause 6.2.1.2, Clocked FL properties, add:
| "For a clocked FL property, i.e., one that is the left
| operand of the @
| operator, the clock context is given by the right operand
| of the @ operator."
|
| - in Clause 6.2.4.2, Property instantiation, add:
| "For an unclocked property instance, the clock context is
| that of the property,
| sequence, declaration, or directive in which the
| unclocked property instance is
| immediately contained."
|
| - in Clause 7.1, Verification directives, add:
| "For a directive, the clock context is given by the
| applicable default
| clock declaration, if any; otherwise the clock context is
| the base clock context."
|
| If we do not want the modeling layer to define a clock
| context, we should also add the following:
|
| - in Clause 8, Modeling layer, add:
| "For modeling layer code, no clock context is defined. Any
| reference to built-in
| function calls prev(), stable(), rose(), or fell() must
| therefore include an explicit
| clock parameter to specify the clock context."
|
| If we want to allow the modeling layer to define a clock
| context, and therefore allow use of built-in functions within
| the modeling layer without explicitly passing a clock
| parameter to each one, then we should instead add the following:
|
| - in Clause 8, Modeling layer, add:
| "For modeling layer code, the clock context is the base
| clock context."
|
|
| 4. Correct the informal semantics of '@' to allow for a
| nested subelement that has a different clock context.
|
| - in Clause 6.1.2.5, Clocked SERE, change the informal
| semantics to read as
| follows:
| "For unclocked SERE A and Boolean CLK:
| A@CLK holds tightly on a given path iff CLK holds in
| the last cycle of the given path,
| and A holds tightly on the path obtained by extracting
| the from the given path exactly
| those cycles in which CLK holds, and any subordinate
| sequences of A hold tightly as
| specified by A on the corresponding sub-paths of the
| given path."
|
| - in clause 6.2.1.2, Clocked FL properties, change the
| informal semantics to read as follows:
| "For unclocked FL property A and Boolean CLK:
| A@CLK holds on a given path iff A holds on the path
| obtained by extracting
| from the given path exactly those cycles in which CLK
| holds, and any subordinate
| properties of A hold as specified by A at the
| corresponding cycles of the given path."
|
| [Note: I'm not happy with this yet, but this is the best I've
| been able to do so far.]
|
|
| 5. Update Default Clock Declaration semantics to link it to
| the discussion of clock context.
|
| - in Clause 5.4, Default clock declaration, change the
| informal semantics (first two paragraphs) to say:
| "The clock context of a directive is defined by the
| applicable default clock declaration,
| if any; otherwise the clock context of the directive is
| the base clock context."
|
| [Note that the clock context of a directive such as "assert
| (always a)@c"
| may be True, even though the directive's clock context is
| superceded, or hidden, by the clock context of the property
| that is at the top level of the directive - in this case, c.]
|
|
| 6. Clarify how outer clock contexts affect references to
| prev/rose/fell/stable differently depending upon where those
| function references appear.
|
| [This is accomplished by the addition of the explanation in
| clause 5.2.3 above, together with the removal of the repeated
| paragraphs representing the previous explanation, as follows.]
|
| - in Clause 5.2.3.1, prev(), remove the paragraph starting
| "The clock context ..."
| - in Clause 5.2.3.3, stable(), remove the paragraph starting
| "The clock context ..."
| - in Clause 5.2.3.4, rose(), remove the paragraph starting
| "The clock context ..."
| - in Clause 5.2.3.5, fell(), remove the paragraph starting
| "The clock context ..."
|
| [We also need to clarify the equivalences given in these
| sections, roughly as follows.]
|
| [Define the following equivalences, probably in a Note,
| because these are consequences of other rules:
|
| prev(e,n,c) <==> prev(e,n) in the clock context c
| prev(e,1) <==> prev(e)
|
| as a Boolean (not a clock expression):
| stable(a) within a clock context c <==> (prev(a,1,c)==a)
| rose(a) within a clock context c <==> (prev(a,1,c)==0 && a==1)
| fell(a) within a clock context c <==> (prev(a,1,c)==1 && a==0)
|
| as a clock expression:
| stable(a) within a clock context c <==> (prev(a,1,True)==a)
| rose(a) within a clock context c <==> (prev(a,1,True)==0 && a==1)
| fell(a) within a clock context c <==> (prev(a,1,True)==1 && a==0)
|
| ]
|
|
| =====================================================
|
| The above includes part of a proposed general rewrite of
| section 4.4.1, the goal of which is to also explain more
| precisely what kinds of properties must give the same results
| in simulation and in formal verification. A current draft of
| the full section 4.4.1 is below. The issue of equivalence
| between simulation and formal verification is partly related
| to the definitions of rose and fell, which are addressed
| above, and partly related to Group M, clocking and sampling.
|
| 4.4.1 Clocked vs. unclocked evaluation
|
| A PSL property, sequence, endpoint, or built-in function can
| be qualified by a /clock context/ which causes the property,
| sequence, endpoint, or built-in function to apply only to
| states in which the clock context holds.
| A nested property, sequence, endpoint, or built-in function
| within a given property or sequence can have a different
| clock context than that of the parent property or sequence.
|
| The /base clock context/ is True, i.e., the granularity of
| time as seen by the verification tool. Different
| verification tools may model time at different levels of
| granularity. For example, an event-driven simulation tool
| typically has a relatively fine-grained model of time,
| whereas a cycle-based simulation or formal verification tool
| typically has a more coarse-grained model of time.
|
| A clock context may be specified explicitly or may be
| inherited implicitly from an enclosing construct or region.
| An explicitly specified clock context takes precedence over
| an inherited clock context.
|
| A PSL property or sequence whose clock context is specified
| explicitly by a clock expression attached to the property or
| sequence (via the @ operator; see Clause ...) is a /clocked/
| property or sequence, respectively; otherwise it is an
| /unclocked/ property or sequence. An unclocked property or
| sequence inherits its clock context from an enclosing
| construct or region.
|
| A PSL property, sequence, endpoint, or built-in function
| whose clock context is equivalent to True is an
| /asynchronous/ property, sequence, endpoint, or built-in
| function; otherwise it is a /synchronous/ property, sequence,
| endpoint, or built-in function, respectively.
|
| A synchronous PSL property that contains no nested
| asynchronous properties, sequences, endpoints, or built-in
| functions shall give the same result in cycle-based and
| event-based verification tools, provided that there is a
| one-to-one, in-order correspondence between (a) the
| succession of event-based states in which a clock context of
| the property holds, and (b) the succession of cycle-based
| states in which the same clock context holds.
|
|
| =====================================================
|
| Some issues with this draft that remain to be addressed:
|
| 1. Need to ensure that the definition of "unclocked ...
| instance" is clear
| - it is intended to mean an instance of a declaration that is
| unclocked.
| 2. Need to ensure that it is clear that the clock context of
| a property/sequence in which an instance appears flows into
| the (virtual)
| *instance* of the referenced declaration, not into the
| referenced declaration itself (which can be referenced from
| many different clock contexts).
| 3. May need to make it clear that clock expressions are by
| nature asynchronous, and that their asynchronicity does not
| affect the synchronousness of clocked properties (and
| therefore the expectation that, under appropriate
| circumstances, clocked properties will give the same result
| in both simulation and formal verification).
| 4. Need to detail the changes required to clarify the
| equivalences of prev/rose/fell/stable.
|
|
|
|
|
|
|
|
Received on Thu Dec 16 01:33:48 2004