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 Wed Dec 15 04:40:27 2004
This archive was generated by hypermail 2.1.8 : Wed Dec 15 2004 - 04:40:28 PST