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

Cindy,

I've inserted responses to your points below. I think it will
help if I give a fuller explanation of my view of how a
decision about the mapping from netlists to models can
clarify the question of what sampling policies are valid.
I had not yet done this, as all I wanted to do at this stage
was to get the point recognized as an issue that should be fully
discussed. If this recognition can be confirmed, it may
be best to postpone further technical discussion until the
due time for the topic in the schedule of the extensions
committee.

I'm sending a separate reply to a mail of Erich's, to the
extensions reflector only, containing such an explanation.
I hope that this will show that the approach I suggest
is a way of strenghtening the language definition above
the temporal layer, while avoiding nasty complications.

Regards,

Anthony

Cindy Eisner wrote:
>
> anthony,
>
> i did not see a message on the extensions reflector, so i am responding
> here.
>
> >First, I am not proposing that PSL defines the behaviour of a memory
> >element. I am proposing that it defines the model against which
> >PSL formulae are evaluated.
>
> the model against which psl formulas are evaluated is a trace (formally, a
> finite or infinite word over the alphabet \Sigma as defined in appendix b
> of the lrm). once again, how that trace is obtained is not the business of
> psl.

A PSL formula is evaluated against a trace. It can also be evaluated against
a transition system, by saying that it is true if if it hold for all traces
that are computation paths of the transition system. The semantics of a vunit
is not defined at present, but it is at least plausible to say that the
meaning of a vunit consisting, say, of just two assertions is that both
assertions are true on the transition system associated with the design
the vunit is bound to. The semantics of vunits is the business of PSL.

>
> >I agree that it is for the HDL to define its own simulation semantics.
> >Also, where there is a standard for synthesis associated with the HDL,
> >it is for this standard to define the mapping from HDL to netlist.
> >There is still room for PSL to define the mapping from netlist to
> >transition system.
>
> i do not agree. the mapping from netlist to transition system cannot be
> separated from the simulation semantics. unless you mean that the mapping
> is to be used for formal verification only?

There is a relationship between three things:
- the mapping from netlist to transition system
- the simulation semantics (including internal details about the order in which
things are calculated)
- the sampling policy for evaluating assertions

If the simulation semantics is fixed, then different mappings can be
accommodated by choosing diffent sampling policies.
If the mapping is fixed, then the possible sampling policies depend on the
simulation semantics (and also physical characteristics of the circuit
elements, as Erich pointed out).

>
> >Leaving aside simulation traces, there is an easy opportunity to make
> >a once-for-all choice for formal verification.
>
> i am not sure that i agree that for formal verification, things are so
> simple. what about a tool that wants to incorporate timing information
> into the formal model? or a tool that wants to model tri-states? voltage
> levels? how about a future tool that wants to do any one of a million or
> more things of which i cannot even conceive? why is it our business to
> dictate how a model is built in formal any more than it is our business to
> dictate to a simulation tool how to create its traces?

This is the point of yours that I take most seriously. Why favour one particular
level of detail in the formal model? I would say because there is an
established definition of the synthesized model corresponding to certain
subsets of HDLs. The specific physical circuit elements used to implement
that model don't matter, as long as they satisfy the timing requirements.
The formal model therefore seems to me to be appropriate for defining
the meaning of a vunit when it is bound to a design modelled in
synthesizable HDL, which seems to me to be within the scope of the group.

I don't want to exclude PSL being used in other ways as well.

>
> finally: i do not agree with the following:
>
> > 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.
>
> first, i find it more intuitive to use f@rose(clk) when the mapping is done
> as per johan's proposal. thus, i do not believe that the choices you
> described were forced by psl in any way. second, i repeat: the question
> of the mapping is completely orthogonal to the question of the semantics of
> psl, and has no place in the psl lrm!
>

If the mapping is done according to Johan's proposal, then, whether
intuitive or not, is is not true that, for a formula f with no clocked
subformula, f@rose(clk) holds on a trace if and only if f holds on
the trace sampled at the points where rose(clk) = 1.

> >Your points below suggest that you, and probably others, may be
> >concerned about opening a can of worms.
>
> yes, that is certainly one of my concerns. but if i believed there was a
> hole in the psl definition, i would be for opening the can in order to
> close the hole. in this case, i believe opening the can will serve no good
> purpose.
>

There is no definition of PSL semantics above the temporal layer. I don't
know whether that's best viewed as a hole or a deliberate open roof.
The question is whether there are practical advantages to some additional
formal semantics. Formal specification of the mapping from netlists to
transition systems would
- make properties involving subtle relationships between different clocks
portable between formal verification tools;
- support a concept of a vunit as a statement about a design (i.e. as
a specification);
- provide a foundation for deciding which traces count as possible
tests of a formula, considered as a statement about a design.

It is up to me to convince you that this will not open a can of
worms, indeed that it is a way of fending off endless questions
about how and when to sample assertions. I haven't given up hope
of doing this.

Regards,

Anthony

> 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
>
> Anthony MCISAAC <anthony.mcisaac@st.com>@st.com> on 09/11/2004 16:02:42
>
> To: Cindy Eisner/Haifa/IBM@IBMIL
> cc: Johan Mårtensson <johan@safelogic.se>, ieee-1850@eda.org,
> Anthony.McIsaac@st.com
> Subject: Re: [$ieee-1850] Sampling semantics for DFFs
>
> Cindy,
>
> You won't be surprised that I don't accept your arguments.
>
> I'll give a brief comment here and leave the details of
> my points for a mail to the extensions subcommittee.
> [note added later - but see below!]
>
> Event-driven simulation:
> Yes, event-driven simulators produce different traces from each
> other, and different traces from cycle-driven simulators.
> But all these traces can be consistent with the transition systems
> derived in the way that either Johan or I described. The
> advantage of establishing the definition of the transition
> system corresponding to a netlist is that you can work out which
> traces are consistent with the transition system, even if you
> have a variety of simulators with different ways of modelling
> the hardware elements.
>
> HDL semantics:
> First, I am not proposing that PSL defines the behaviour of a memory
> element. I am proposing that it defines the model against which
> PSL formulae are evaluated.
> I agree that it is for the HDL to define its own simulation semantics.
> Also, where there is a standard for synthesis associated with the HDL,
> it is for this standard to define the mapping from HDL to netlist.
> There is still room for PSL to define the mapping from netlist to
> transition system.
>
> Different tools:
> Leaving aside simulation traces, there is an easy opportunity to make
> a once-for-all choice for formal verification. In essence, it is a
> trivial choice about whether the clock is evaluated at 0 or 1 when
> it rises. It may or may not matter which choice is made, but it
> will be a nuisance if different vendors make different choices,
> especially when there are different but related clocks, etc.
> This may not appear as a problem to developers or users of a
> single tool, but it is a real problem for users who want to write
> properties portable betweem different tools.
>
> rise(clk):
> I agree that there could be separate reasons for introducing a
> "rise" function, but there is also a case arising from this
> discussion. If Johan's sytem is preferable to mine (and he makes
> a good case for it), then there is a strong argument for
> introducing "rise".
> It may only shift observations by one cycle in the simplest
> case, but this is a nuisance in itself. Users don't want it,
> and this is why we participate in committees like this one.
> An inexperienced group using a new tool may waste days on
> just such small points.
>
> Concession:
> I do agree that it would be possible to restrict the scope of
> PSL semantics to defining the interpretation on traces, or on
> traces and on transition systems. But I believe it would
> restrict its usefulness, when we are trying to establish a standard
> so that properties can be reused. The scope of this working group
> includes clarifying how PSL interfaces with various electronic system
> design languages; Johan's proposal appears to be consistent with this.
>
> Consequences:
> Your points below suggest that you, and probably others, may be
> concerned about opening a can of worms. This is a very reasonable
> fear, but the proposals are limited:
> - There is no proposal to attempt to define HDL semantics.
> - The proposal does not go directly into defining how to sample
> traces, but it will provide a foundation for making decisions
> about how to sample traces.
> - The proposal need not, I believe, require defining the
> contribution to a transition system from every type of memory
> element. Once the pattern is established for one or two, it
> can be followed for others.
>
> Apologies for not being brief as I planned. I will restrict further
> comments to the extensions committee, if the whole committee does
> indeed agree that it is an issue for the extensions subcommittee.
>
> Regards,
>
> Anthony
>
> Cindy Eisner wrote:
> >
> > anthony, johan, all,
> >
> > this discussion has been very interesting, but i completely disagree that
> > it has anything to do with psl semantics.
> >
> > both anthony's original proposal as well as johan's counter-proposal give
> > semantics to v', where v' is the output of a memory element. this is
> > beyond the scope of psl or indeed even of a hardware description
> language.
> > if you legislate the behavior of v', you will put most simulation tools
> out
> > of the running vis a vis psl: while cycle-based simulators behave more
> or
> > less as you have described, event-based simulators do not - there may be
> > many steps between v and v'. thus anthony's comment that different tools
> > may adopt different mappings from netlists to transition systems is not a
> > "maybe" - it is already an established fact, and one that we have to live
> > with.
> >
> > even if you are willing to give up on event-driven simulation (which i am
> > not!), what is the point of defining formally the behavior of a memory
> > element without formally defining the behavior of the rest of the hdl?
> and
> > in any case, if this is done, then it is part of the definition of the
> hdl,
> > not of psl or any other assertion language.
> >
> > a trace is created by a verification tool. it is highly desirable that
> two
> > verification tools create the same trace from the same netlist and input
> > sequence. however, it is already a given that this is not guaranteed.
> it
> > is also highly desirable that given the same trace, two psl tools will
> > interpret it in the same way. this is already guaranteed by the formal
> > semantics of psl.
> >
> > the question of whether or not psl supplies another operator, @rise(clk),
> > as discussed by johan and anthony, is completely orthogonal. in the
> simple
> > case of one clock and no glitches, both will work the same, except that
> the
> > numbering of the cycles is shifted by one. (to see this: assume that
> > rose(clk) holds at time X, and the next time after X that rise(clk) holds
> > is at time X+k. then in the absence of glitches, the value of signal "a"
> > at time X and at time X+k is the same.)
> >
> > 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
> >
> > Anthony MCISAAC <anthony.mcisaac@st.com>@eda.org on 08/11/2004 12:55:20
> >
> > Sent by: owner-ieee-1850@eda.org
> >
> > To: Johan Mårtensson <johan@safelogic.se>
> > 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
> > >
> > > --
> > > ------------------------------------------------------------
> > > Johan Martensson, PhD Office: +46 31 7451913
> > > R&D Mobile: +46 703749681
> > > Safelogic AB Fax: +46 31 7451939
> > > Arvid Hedvalls Backe 4 johan.martensson@safelogic.se
> > > SE-411 33 Gothenburg, SWEDEN
> > > PGP key ID A8857A60
> > > www.safelogic.se
> > > ------------------------------------------------------------
> >
Received on Mon Nov 15 09:15:25 2004