Subject: sampling at clock edges
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Fri Mar 07 2003 - 06:33:39 PST
Compatibility of PSL semantics with SVA sampling at clock edges
(can this please be forwarded to sv-ac?)
I have some comments about the definition, in 11.3 of the SVA 0.8 proposal,
of the traces on which sequential expressions are evaluated. In particular,
what values are taken by the clock variables themselves, and any other
inputs that are synchronized with the clock variables.
According to the account in 11.3, the value of all variables are sampled
just before clock ticks. Applying this to the clock variables themselves,
the value of a clock variable at a rising clock edge is sampled as 0. This
is not inconsistent in itself; and if there is only a single clock, one
can abstract away the clock input from the design, so that its values
are irrelevant as far as property formulations are concerned.
However, if there are multiple clocks, one may want to use clock values
in properties. Further, PSL defines the values of clocked properties in
terms of clock values. For a property clocked on rose(clk), one really
does have to take the value of clk as 1 when values are sampled. Otherwise,
if a trace includes points other than rising edges of clk, one will sample
at the wrong points.
I would ask that consideration be given to how values of clocks at their
own rising edges are defined in SVA. Two suggestions:
- special treatment could be given to clocks at their own rising edges:
their sampled values could be defined as 1 here. This may give problems with
other clock inputs that are synchronized with the clocks in question -
and may indeed be effectively duplicates of them. They should take the same
values as the clocks they are synchronized with.
- from a specification point of view, the sampled values of signals could
be defined as those immediately after the clock edge, before any values
have changed as a result of the clock edge. This would not necessarily
make a significant difference to the way sampling is implemented in the
simultor scheduling, for all the signals that hold their values over the
clock edge.
The discussion below indicates how the PSL semantics could be more explicit
about the models with respect to which formulae are evaluated; this
will in turn help to clarify what simulation traces are consistent with
these models.
PSL does not define the traces on which properties are evaluated. It
simply defines how properties are evaluated on traces, regardless of how these
traces are produced. It also defines how properties are evaluated on
"models",that is, transition systems describing the possible evolutions
of a design. A property is true on a model if it is true on all infinite
traces that are computation paths of the model.
In my view, this approach is strongly to be recommended as a starting point
for a semantics of properties that is consistent between simulation and
formal verification, and independent of specific simulator implementations.
It is not the whole story: a fuller account is as follows.
1. Given a synthesizable HDL model, the synthesis semantics for the HDL maps
it to a netlist consisting of flip-flop and latches (and possibly
tristates), and combinational logic. PSL has nothing to contribute here.
2. A netlist as above can be mapped to a transition system (a set of states,
and a relation determining which transitions between pairs of successive states
are possible). This mapping is independent of any particular design language,
and should be standardized. It would be useful for PSL to define this mapping
explicitly. There aren't many possible choices, but where there is a choice,
it is important that everyone makes the same choice.
3. For formal verification, a property is satisfied for a design if it is
satisfied on every infinite computation path of the transition system
representing that design.
4. For simulation, a formula is checked on an evaluation path produced by
the simulation tool. Different tools may produce different evaluation
paths, but it should be possible to state sufficient conditions for an
evalaution path to be consistent with the transition system derived from
the netlist as in 2 above. Then a safety property that passes in formal
verification will also pass in simulation.
Logically, it makes sense to establish the definition of the model
associated with a netlist as in point 2 first, with no reference to any
particular language or simulation model; and then for each particular
design language and tool, to ensure that properties are evaluated in such
a way that, if they fail on a trace, that is evidence that they may fail in
the model.
For netlists containing only flip-flops and combinational logic, the only
real choice is when the state variables are updated. If the flip-flops are
clocked on the rising clock edge, do the state variables take their new
values at the same time as the clock takes the value 1, after having been
0 previously, or after one further transition of the system? (Note that
such a transition is not in general a cycle of the clock in question; the
model does not specify the behaviour of the clocks as inputs, only how state
variables behave in relation to the clocks.)
In fact, there is only one viable choice for PSL. Suppose that the state
variables take their new values at the same points as the clock takes the
value 1, after having been 0 previously. If the clock input c takes the
sequence of values 00110011...., then a formula f@rose(c), where f has no
clocked subformulae, should hold on a trace if and only if f holds on that
trace sampled at times 3, 7, .... But the points at which the input and state
variable values that determine the next states of flip-flops are stabilized
are times 2,6, ..... By times 3,7, etc., the state values will have changed
(but not the input values). So this model won't work. If the state values
are updated one point later, we can assume that the state and input values
remain stable over the rising edge, so that sampling at times 3,7, ..
will give the correct behaviour. This is therefore how the model should
be defined.
A formal definition of this model is as follows.
Let V be the set of all design variables, plus extra variables rose_c and
fell_c for each variable c that is a clock for a flip-flop in the netlist.
The set of states S is the set of all possible ways that values can be
assigned to the variables in V.
The transition relation R is determined by defining the next value v' of
each variable v.
If v is an input, v' may have any value.
If v is the output of a flip-flop with input u, clocked on the rising edge
of c, then v' = u if rose_c = 1, else v
If v is the output of a flip-flop with input u, clocked on the falling edge
of c, then v' = u if fell_c = 1, else v
If v is combinationally determined as v = f(v1,...,vn), then v' = f(v1',...,vn').
It will be possible to define v' for every variable v if there are no
combinational loops.
If v is rose_c, then v' = 1 if c = 0 and c' = 1, else 0
If v is fell_c, then v' = 1 if c = 0 and c' = 1, else 1
(This definition has to be extended if there are latches.)
Informally, this means that memory elements are updated one evaluation
cycle after the active clock edge. All variables are assumed to have
stabilized before theclock edge, and to hold their values over the clock edge.
A design satisfies a formula f if f is satisfied on every infinite
computation path of the model associated with the design.
Formal verification can check whether a formula is satisfied by a design. In
simulation, a formula is checked on an evaluation path as produced by the
verification tool. An evaluation path will be a computation path of the
design if the simulation is sampled according to the following rules:
- sample just once after each active clock edge, before any values have
changed as a consquence of the edge
- do not sample between a change in value of a variable and the consequent
changes in value of variables that depend combinationally on it (directly or
indirectly)
- sample at any number of other points
A special case is when there is only one clock, and only one edge is active.
In this case, a trace will be consistent with the model if the values are
sampled just after each edge (rising and falling), before any values have
changed as a result of the edge. But, since nothing changes on the inactive edge,
the trace consisting of the samples values just after each active edge
is also consistent with the model, if one abstracts the clock (i.e. replaces the
variables clk and rose_clk with just one variable rose_clk, which is always 1).
Although this special case is very common, it is a special case, and the
general semantics should demonstrate how it fits into a scheme where the
values of the clock inputs are significant.
-- Anthony McIsaacSTMicroelectronics Limited 1000 Aztec West Almondsbury Bristol BS32 4SQ
Tel: ++44 (0)1454 462466 Fax: ++44 (0)1454 617910
Email: Anthony.McIsaac@st.com
This archive was generated by hypermail 2b28 : Fri Mar 07 2003 - 06:48:07 PST