Subject: [sv-ac] Fw: sampling at clock edges
From: Faisal Haque (fhaque@cisco.com)
Date: Fri Mar 07 2003 - 07:38:49 PST
----- Original Message -----
From: "Faisal Haque" <fhaque@cisco.com>
To: <sv-ac@eda.org>
Sent: Friday, March 07, 2003 7:36 AM
Subject: Fw: sampling at clock edges
> Forwarding for Anthony McIsaac.
> -Faisal
> ----- Original Message -----
> From: "Anthony McIsaac" <anthony.mcisaac@st.com>
> To: <vfv@eda.org>
> Cc: <fhaque@cisco.com>
> Sent: Friday, March 07, 2003 6:33 AM
> Subject: sampling at clock edges
>
>
> > 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 McIsaac
> >
> >
> > STMicroelectronics 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 - 07:39:42 PST