Re: [$ieee-1850] Sampling semantics for DFFs

Erich,

I agree that consideration of the physical characteristics of the circuit
elements is important.

I'd like to explain my view of the relationship between the definition
of a netlist to transition system mapping and sampling policies for
assertions. I hope this will make it clearer where I see physical
characteristics as being relevant.

I am not proposing that the language definition should include a direct
specification of where simulation results are sampled.

I am proposing that the language definition should include a definition
of the model associated with a netlist synthesized from an HDL design,
by specifying how a number of abstract memory elements contribute to
the transition system. I believe thios is the way to avoid as many
complications as possible.

Given such a definition, it is possible to deduce the conditions under
which a trace of sampled values is a computation path of the model
(i.e. is consistent with the model). A violation of a formula on such a
trace means that the formula does not hold of the design (i.e. does not
hold on the model). It will be useful for the LRM to contain a section
indicating what sampling policies can be expected to produce traces that
are consistent with the model, though this will not be part of the
formal definition.

Traces sampled around (whether just before, or at, just after, at an
intermediate stage of the computations following, ...) a clock edge will
not be the only ones that are consistent with the model. In particular,
suppose that you have a trace consisting of the values sampled at each
rising clock edge, that is consistent with the model. Suppose that an
input has changed at a point somewhere between two clock edges, with
a resultant change in certain internal signals and outputs. You can add
an additional sampling point to the trace at the point where all the
resultant changes have happened. The trace with the additional point
will still be consistent with the model.

Consideration of the points you discuss is relevant in determining
which samplings are consistent with the model. For example, you
cannot expect to get a trace consistent with the model if you sample
the output of a gate within the gate delay of a change of its inputs.
And there will be rules about which points within the zero-time
computations following a signal change are valid for sampling values.
There may also be rules about the circuit: to take your example,
a sampling policy may be consistent with the model only if inputs
are constant over clock edges. These rules can be kept separate
from the language definition.

An aside about unclocked formulae.
Only certain styles of formulae with no clocked subformulae are likely
to be true of a design (i.e. to be true for all traces consistent
with the model). Formulae such as never(p && q) may well be true
of a design, but not formulae that depend on counting cycles,
such as p -> next[4](q). If you are not thinking in terms of clocks,
you probably won't want to write formulae that depend on counting cycles,
but rather formulae describing the relationships between events,
such as p -> next_event(q)(r). Such formulae will often be true
of all traces consistent with the model, including those with
sampling points between clock edges.

From a formal point of view, it doesn't matter whether the mapping
from netlists to transition systems follows Johan's definition
or mine. However, it's worth pointing out that the valid sampling
policies that emerge from one choice of the definition may be
preferable to those that emerge from the other choice. Although
I believe that the choice of mapping comes first from a logical
point of view, it may be that in practice one knows what criteria
for sampling one wants to end up with, and chooses the mapping
accordingly.

Regards,

Anthony

Erich Marschner wrote:
>
> Johan, Anthony,
>
> Here are my two cents about this issue. (Note that I've moved this discussion to the Extensions reflector.)
>
> I believe this discussion needs to be grounded in the physical objects that we are modeling (transistors, gates, FFs), their timing characteristics, the design rules that are universally followed to produce predictable designs, and the verification steps that we perform (both timing and functional) to verify a design. Reasoning about a particular abstract model of a FF without taking the above into account is going to be misleading and confusing.
>
> In particular, I claim that standard design and verification methodologies have built-in mechanisms for avoiding race conditions and verifying that they don't occur. For example, in both synthesis and standard-cell-based custom design, flipflop cells are carefully characterized to identify their setup and hold times w.r.t. the active clock edge, and part of the verification process is a timing verification step that checks to make sure those constraints are not violated - i.e., that the input data is stable across the clock edge. If a designer were to wire the same signal to the clock and data inputs of a FF, then he would have to juggle the capacitance or the wire lengths or add buffers along the clock path to ensure that the clock edge occurred after the data was set up, or else the timing verification step would fail. The key point is that functional verification does not stand alone; functional verification results are valid iff timing verification has also been perf
 or
> med, and timing verification would preclude the race condition issue raised in the FF example below.
>
> I believe that Anthony's original statement is correct - that there is only one solution that satisfies PSL's abstract semantics (which involves sampling a trace at points where the clock expression is true). This solution also satisfies our desire to have a given property give equivalent results in simulation and in formal verification, modulo the timing abstraction difference. It requires the stability assumption for inputs of a FF (i.e., that the data is stable before the clock edge, and that it doesn't change simultaneous with the clock), and as I've argued above, this assumption is in fact consistent with current design and verification practice. The assumption allows us to sample either just before, at, or just after the clock edge (assuming a fine-grained model of time, and provided that no other signal updates occur between the sampling point and the clock edge), and still expect to get the same result. This is important because event-driven simulation must reac
 t
> to a clock edge (i.e., sample just after it), whereas cycle-driven simulation/formal verification must effectively sample just before the clock edge. So the only way event-driven simulation and formal verification will give equivalent results is if we require that data stabilizes before the clock edge and stays stable until after the clock edge. Fortunately, this assumption is already built into current design and verification practice.
>
> The discussion below also assumes that 'now' is an indivisible quantum of time. In fact, both simulation and formal verification are performed by algorithms which advance in a sequence of micro-steps "during" each time point. A complete discussion of this issue needs to recognize verification tools' implicit division of a time point into substeps, otherwise it will lead to conclusions that are perhaps mathematically defensible but are nonetheless incorrect in practice.
>
> Regards,
>
> Erich
>
> | -----Original Message-----
> | From: owner-ieee-1850@eda.org
> | [mailto:owner-ieee-1850@eda.org] On Behalf Of Anthony MCISAAC
> | Sent: Monday, November 08, 2004 5:55 AM
> | To: Johan Mårtensson
> | Cc: ieee-1850@eda.org
> | Subject: Re: [$ieee-1850] Sampling semantics for DFFs
> |
> | Johan,
> |
> | Apologies for late reply to your message: I have only just
> | joined the mailing list.
> |
> | I have no reason for preferring the scheme I described to the
> | Safelogic one, except that I believe that the choices I
> | described were forced by PSL as it is now. At least, it is
> | forced by a presumption that, for a formula p = f@rose(clk),
> | where f has no clocked subformulae, the value of p on any
> | trace is equal to the value of f on the subtrace sampled at
> | those points where
> | rose(clk) is true.
> |
> | In many ways, your scheme seems preferable. If it were to be
> | adopted, we would need another keyword "rise" (where
> | rise(clk) is true if clk is 0 in this state and 1 in the next
> | state), and the way to write a property for designs clocked
> | on the rising edge would typically be f@rise(clk).
> |
> | In my original message, I did not want to argue for a
> | particular way of defining the mapping from netlists to
> | transition systems.
> | But I strongly believe that it is necessary to make a
> | decision on what this mapping is. Otherwise, different tools
> | may adopt different mappings. I also believe that
> | establishing this mapping is the best foundation for
> | answering questions like Ben's (issue 22) on what the meaning
> | of an unclocked formula should be, or more generally, where a
> | formula should be sampled in simulation.
> |
> | I notice that issue 22 was rejected by the issues subcommittee.
> | I'm not sure to what extent the netlist to transition system
> | mapping question is associated with issue 22. Although there
> | were a large number of zero priority votes for issue 22,
> | these did not represent a broad range of participants, and
> | I'm not convinced that the issue is fully appreciated. The
> | fact that one company is adopting a scheme inconsistent with
> | PSL seems to me to be prima facie case for concern.
> |
> | The new issue 39 is related to issue 22, and could be taken
> | to subsume it. However, it does not mention the question of
> | the mapping from netlist to transition system, on which I
> | believe it depends.
> |
> | Anthony
> |
> |
> |
> |
> |
> |
> | Johan Mårtensson wrote:
> | >
> | > Hi All,
> | >
> | > I'm not sure whether item on sampling semantics (# 39) was dropped or
> | > not? I didn't argue at the Issues meeting that it should stay but I
> | > have second thoughts. I now think we shold discuss this in the
> | > extensions committee. Or what is perhaps a related thing, namely what
> | > Anthony McIsaac brought up a while ago, that is, standardization of
> | > the mapping between netlist and transition system.
> | >
> | > At Safelogic we have chosen a somewhat different such mapping for DFFs
> | > than the one McIsaac suggested, and we feel it would be unfortunate if
> | > others were to adopt something different. I have started to work on a
> | > formal statement of the Safelogic mapping in the same terms as McIsaac
> | > did together with a criticism of McIsaacs suggestion:
> | >
> | > > 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
> | >
> | > McIsaac sample semantics (as stated).
> | > ====================================
> | >
> | > * If v is an input then v' is independent of v.
> | >
> | > * If v is output of a flipflop with input u then
> | >
> | > / u, if rose_c = 1 and
> | > v' = <
> | > \ v, otherwise.
> | >
> | >
> | > * If v is (rose_c) then
> | >
> | > / 1, if c = 0 and c' = 1
> | > v' = <
> | > \ 0, otherwise.
> | >
> | >
> | > So we have the following situation (d is an input)
> | >
> | > D-flip-flop
> | > _________
> | > | |
> | > d ---| |--- q
> | > | |
> | > c ---|> |
> | > |_________|
> | >
> | > A D-flip-flop will take the last value on d before a positive
> | > (/negative) clock flank and hold it on q from that clock flank until
> | > the next positive (/negative) one. (In the following 'a' and 'b' are
> | > binary varibles and 'x' is "don't care".) So we have the following
> | > behavior, for example:
> | >
> | > Actual behavior
> | > ----------------
> | > t 0123456
> | > c 0001100
> | > d xxaxxxx
> | > q xxxaaaa
> | >
> | > McIsaac behavior (without constancy requirement)
> | > ------------------------------------------------
> | > t 0123456
> | > c 0001100
> | > rose c 0001000
> | > d xxabxxx <= is not required to be constant over the clock flank
> | > q xxxxbbb
> | >
> | > This is clearly not correct. A suggested solution is to require that
> | > all signals (except the clock) are constant over the clock flank. This
> | > can be achieved by requiring that inputs (except the clock) are
> | > constant over the clock flank. McIsaac mentions this in his informal
> | > account (but not in the formal one it seems). This suggests the
> | > following change to the clause for inputs:
> | >
> | > * If v is an input not occurring in the definition of the clock c
> | >
> | > / v, if rose_c' = 1 and
> | > v' = <
> | > \ any value, otherwise.
> | >
> | > (Clearly we cannot require that the clock signal is constant over the
> | > clock flank.)
> | >
> | > McIsaac behavior (with constancy requirement)
> | > ---------------------------------------------
> | > t 0123456
> | > c 0001100
> | > rose c 0001000
> | > d xxaaxxx <= is "forced" to be constant over the clock flank
> | > q xxxxaaa
> | >
> | > So this now better reflects the actual behaviour.
> | >
> | > But then there is the following problem: If an input signal is both
> | > occurring as a input to a flip-flop and in the definition of the clock
> | > signal then we can not help ourselves to the constancy assumption.
> | >
> | > D-flip-flop with gated clock
> | > _________
> | > | |
> | > d ---| |--- q
> | > | |
> | > c&d ---|> |
> | > |_________|
> | >
> | > Actual behavior
> | > ----------------
> | > t 0123456
> | > c 1111111
> | > d 0001xxx
> | > q xxx0000
> | >
> | > (I will use v_n to refer to v at t=n). So q_4=0 and d_3=1, but on
> | > McIsaac's model, without the constancy requirement: q_4=(q_3)'=d_3=1.
> | > If McIsaac's model is strengthened with the requirement that all input
> | > signals (also d) are stable over the clock edge, then of course, one
> | > gets a flat contradiction.
> | >
> | > McIsaac behavior (without constancy requirement)
> | > ------------------------------------------------
> | > t 0123456
> | > c 1111111
> | > d 0001xxx
> | > rose (c&d) 00010xx
> | > q xxxx111
> | >
> | > So I think there are at least two related problems with this model.
> | > 1) There is an "artificial" requirement that input signals are
> | > constant over the clock flank.
> | > 2) Input signals that are input to a DFF and occur in the definition
> | > of its clock expression will not be treated correctly.
> | >
> | > I suggest the following mapping as a solution to those problems:
> | >
> | > Safelogic sample semantics.
> | > ===========================
> | >
> | > If v is an input then v' is independent of v.
> | >
> | > If v is output of a flipflop with input u then
> | >
> | > / u, if rise_c = 1 and
> | > v' = <
> | > \ v, otherwise.
> | >
> | >
> | > If v is (rise_c) then
> | >
> | > / 1, if c = 0 and c' = 1
> | > v = <
> | > \ 0, otherwise.
> | >
> | >
> | > So we have the following situation (d is an input)
> | >
> | > D-flip-flop
> | > _________
> | > | |
> | > d ---| |--- q
> | > | |
> | > c ---|> |
> | > |_________|
> | >
> | > Actual behavior
> | > ----------------
> | > t 0123456
> | > c 0001100
> | > d xxaxxxx
> | > q xxxaaaa
> | >
> | > Safelogic behavior
> | > ----------------
> | > t 0123456
> | > c 0001100
> | > rise c 001000x
> | > d xxaxxxx <= no requirement of constancy
> | > q xxxaaaa
> | >
> | > If an input signal is both occurring as a input to a flip-flop and in
> | > the definition of the clock signal then there is no problem in the
> | > following example:
> | >
> | > D-flip-flop with gated clock
> | > _________
> | > | |
> | > d ---| |--- q
> | > | |
> | > c&d ---|> |
> | > |_________|
> | >
> | > Actual behavior
> | > ----------------
> | > t 0123456
> | > c 1111111
> | > d 0001xxx
> | > q xxx0000
> | >
> | > (I will refer to v at t=n with v_n). So q_4=0 and d_3=1,
> | >
> | > Safelogic behavior
> | > ----------------
> | > t 0123456
> | > c 1111111
> | > rise (c&d) 0010xxx
> | > d 0001xxx
> | > q xxx0000
> | >
> | > On the Safelogic model q_4=q_3=d_2, and since d_2=0 and d_3=1 this is
> | > in accordance with the actual behavior.
> | >
> | > PSL clocking.
> | > =============
> | >
> | > To get the intended meaning for clocked PSL formulas the clock edge
> | > must not be expressed using rose_c but using rise_c, defined as above.
> | > In this way the last value before the clock edge will be referred to
> | > rather than the first one after the edge.
> | >
> | > I see this as just a beginning. There are other kinds of state
> | > elements that need to be mapped to PSL models in a suitable way. There
> | > is also perhaps a need to reformulate the solution for simulation
> | > where next values of signals are not available.
> | >
> | > Best Regards,
> | >
> | > Johan Martensson
> | >
> | > --
Received on Mon, 15 Nov 2004 17:14:51 +0000