Indeed thx Johan, I proposed 39, it is similar in spirit to what Anthony
raised in 22 but really the intent is to clearly address the sampling
semantics so that "tools" (users' and vendors') can be consistent; I see
your comments speak to that too. Since I had to leave early (and no minutes
yet) I have no idea what its current disposition is.
Thx.
-Bassam.
--
Dr. Bassam Tabbara
Architect, R&D
Novas Software, Inc.
(408) 467-7893
-----Original Message-----
From: owner-ieee-1850@eda.org [mailto:owner-ieee-1850@eda.org] On Behalf Of
Johan Mårtensson
Sent: Thursday, October 14, 2004 3:30 AM
To: ieee-1850@eda.org
Subject: [$ieee-1850] Sampling semantics for DFFs
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 Thu Oct 14 08:31:36 2004
This archive was generated by hypermail 2.1.8 : Thu Oct 14 2004 - 08:31:41 PDT