Modeling

Synchronous and Asynchronous Behavior in VHDL

David M. Russinoff

Computational Logic, Incorporated 1717 West Sixth Street, Suite 290

Austin, Texas 78703-4776 russ@cli.com

Modeling Circuit Behavior

The hardware design process generally involves two distinct models of behavior:

• Sequential machine model – signal representation: waveform

– fundamental operation: event scheduling

– time unit: 10^{−12} sec.

• Event-driven simulation model – signal representation: value sequence

– fundamental operation: state transition

– time unit: 10^{−7} sec. A comprehensive hardware verification system must incorporate both of these models.

Copyright \begin{matrix}c \\ ◯ \end{matrix} 1994 Computational Logic, Inc.  Modeling in VHDL - 17: 2  CLI Research Review, April 1994

Outline of this Talk

• Motivation: an implementation of the biphase mark protocol for asynchronous communication

• Definition: a simple event-driven simulation language (a subset of VHDL)

• Specification: behavioral descriptions of combinational and sequential circuits

• Application: correctness of the biphase mark circuit

Moore’s Model of Asynchrony

Theorem 1 Let s : N → {T , F}, V_{s} = (v_{1} … v_{n}), and V_{r} = (u_{1} … u_{m}). Assume that for all k,

(1) s(t) = v_{k} for some t ∈ [t_{s} + (k − 1)π_{s}, t_{s} + kπ_{s});

(2) s(t) = u_{k} for some t ∈ [t_{r} + (k − 1)π_{r}, t_{r} + kπ_{r});

(3) If v_{k} = v_{k−1}, then s(t) = v_{k} for all t ∈ [t_{s} + (k − 1)π_{s}, t_{s} + kπ_{s}).

Then for some oracle, V_{r} = asynch(V_{s}, t_{s}, t_{r}, π_{s}, π_{r}, oracle).

Biphase Mark Protocol

V_{s} = send(p, msg) consists of a pad of p T ’s followed by sequence of cells corresponding to the bits of msg. Each cell consists of a mark subcell followed by a code subcell.

recv(V_{r}) = msg is computed by recovering the encoded bit from each cell.

Theorem 2 (Moore) If 17π_{r} ≤ 18π_{s} ≤ 19π_{r} and t_{s} ≤ t_{r} < t_{s}+π_{s}, then recv(asynch(send(p, msg), t_{s}, t_{r}, π_{s}, π_{r}, oracle)) = msg.

Biphase Mark Circuit Receiver

Waveforms

A waveform is a list of events, which determines a Boolean-valued function of time.

w = ((T , 8) (F, 7) (T , 5) (F, 4) (T , 2) (F, 0))
w(2) = w(3) = T ; w(4) = F

A packet is a list of waveforms, p = (w_{1} … w_{n}), which determines a vector-valued function of time: p(t) = (w_{1}(t) … w_{n}(t)).

Transport Delay

When an event (v, t) is scheduled on a waveform w, all previously scheduled events of w that occur at or after t are removed.

w

transport(w, T , 6)

Inertial Delay

When an event (v, t) is scheduled on a waveform w at time t_{0}, all previously scheduled events of w that occur after t_{0} are removed.

w

inertial(w, T , 1, 6)

Behavioral Modules

A behavioral module consists of

(1) A list of inputs;

(2) A list of outputs;

(3) A list of terms corresponding to the outputs;

(4) A list of delays corresponding to the outputs;

(5) A list of propagation modes (either TRANSPORT or INERTIAL) corresponding to the outputs.

Examples

A 2-input nand gate:

nand2 = (BEHAV (A B)                     ;inputs
(C)                       ;outputs
((NAND2 A B))             ;terms
(2000)                    ;delays
(INERTIAL))               ;propagation modes

A 1-bit adder:

adder2 = (BEHAV (A B C)                  ;inputs
 (L H)                    ;outputs
 ((XOR3 A B C)            ;terms
  (OR2 (AND2 A (OR2 B C))
       (AND2 B C)))
 (12000 10000)            ;delays
(INERTIAL INERTIAL))      ;propagation modes

Execution of Behavioral Modules

Execution of behavioral modules is defined by a function exec(M, p_{in}, p_{out}, t), where

(1) M is a behavioral module;

(2) p_{in} is a packet of input waveforms for M;

(3) p_{out} is a packet of output waveforms for M;

(4) t is the current time. The returned value is an updated output packet, produced by scheduling an event on each waveform of p_{out}.

Structural Modules

A structural module consists of

(1) A list of (global) inputs;

(2) A list of (global) outputs;

(3) A list of submodules;

(4) Corresponding to each submodule, a list of local inputs;

(5) Corresponding to each submodule, a list of local outputs. Each global output is a local output; each local input is either a global input or a local output.

A structural version of the adder:

adder2
=
(STRUCT (A B C) (L H)
(nand2 nand2 nand2 nand2 nand2 nand2 nand2 nand2 nand2)
((A B) (A T1) (B T1) (T2 T3) (C T4) (T5 T4) (C T5) (T5 T1) (T7 T6))
((T1) (T2) (T3) (T4) (T5) (T6) (T7) (H) (L)))

A synchronous resettable D-flip-flop:

dff
=
(STRUCT (CLK RST D) (Q QN)
(not1 and2 nand2 nand2 nand3 nand2 nand2 nand2)
((RST) (RN D) (B2 B1) (A1 CLK) (B1 CLK B2) (A2 DD) (B1 QN) (Q A2))
((RN) (DD) (A1) (B1) (A2) (B2) (Q) (QN)))

Circuit Diagrams

Simulation

Simulation is defined by a function sim(M, p, t_{f}), where

(1) M is any module module;

(2) p is an input packet for M;

(3) t_{f} is the termination time.

The returned value consists of an output packet corresponding to each behavioral component of M, computed by the following procedure:

(1) Initialize each waveform to the trivial waveform ((F, 0)).

(2) Execute each behavioral component at t_{0} = 0.

(3) Reset t_{0} to the time of the earliest event that occurs after t_{0}. If t_{0} > t, then terminate; otherwise, execute each component for which some input has an event at t_{0}, and repeat.

Example

Combinational Modules

M is combinational if either (a) M is behavioral or (b) M is structural with no loops and all its submodules are combinational.

Given a signal s of a combinational module M and a vector V of input values, we may compute the combinational value cv(s, V, M):

cv(C, (a b), nand2) = nand(a, b)

cv(L, (a b c), adder1) = xor(a, b, c)
cv(L, (a b c), adder2) = xor(a, b, c)

How can the behavior of M be described in terms of cv?

Specification of Behavioral Modules

The relationship between the behavior of a signal s and its combinational value depends on the delay of s:

Lemma 1 Let s be an output of a behavioral module M with delay d. Let w be the corresponding waveform of sim(M, p, t_{f})). Suppose that cv(s, p(t), M) has a constant value v on the interval [t_{1}, t_{2}), where t_{2} − t_{1} ≥ d. Then for all t ∈ [t_{1} + d, t_{2} + d), w(t) = v.

Specification of Combinational Modules

Each signal s of a combinational M is associated with minimum and maximum delays, which are computed by comparing the total delays along all paths to s. For example,

dmin(L, adder2) = 4000 and dmax(L, adder2) = 12000.

The relationship between the behavior of a signal s and its combinational value depends on the delay of s:

Lemma 2 Let s be an output of a combinational module M. Let dmin(s, M) = d and dmax(s, M) = D. Let w be the corresponding waveform of sim(M, p, t_{f})). Suppose that p(t) is constant and that cv(s, p(t), M) = v on the interval [t_{1}, t_{2}), where t_{2} − t_{1} ≥ D. Then for all t ∈ [t_{1} + D, t_{2} + d), w(t) = v.

Sequential Modules

Let M be a structural module, two inputs of which are distinguished as the clock and the reset. M is a sequential module with mult(M) = q if either (a) q = 0 and M = dff, or (b) q > 0 and the following conditions hold:

(1) q of the submodules of M are sequential and the rest are combinational;

(2) The clock input of M is connected to the clock input of each sequential submodule, and not to any other submodule input;

(3) The reset input of M is connected to the reset input of each sequential submodule, and not to any other submodule input;

(4) There is no combinational path in M (i.e., path through only combinational submodules) from an input to an output;

(5) There is no combinational loop in M.

Sequential Values

Given a signal s of a sequential module M and a list V of data input vectors, we may compute the sequential value list sv(s, V, M):

sv(Q, ((T ) (T ) (F) (T )), dff) = (F T T F T ) sv(Q, (T T ) (T T ) (F F) (F T )), edff) = (F T T T T ) sv(Q0, ((T ) (T ) (F) (T )), count3) = (F T F F T )

How can the behavior of M be described in terms of sv?

Flip-Flop Specification

Lemma 3 Let p = (wCLK wRST wD), where

(a) wCLK is a periodic clock pulse with high ≥ 4000, low ≥ 6000, and successive rising edges at t_{1}, t_{2}, t_{3}, …

(b) wRST(t) = r for all t ∈ [t_{1} − 8000, t_{1})

(c) wD(t) = d for all t ∈ [t_{1} − 6000, t_{1}). Let wQ and wQN be the output waveforms of sim(dff, p, t_{f}), and let v = and(not(r), d). Then wQ(t) = v and wQN(t) = not(v) on [t_{1} + 6000, t_{2} + 4000). Moreover, if these same values hold on [t_{2} + 6000, t_{3} + 4000), then they also hold on [t_{2}, t_{3}).

Sequential Parameters

The behavior of a sequential module may be characterized in terms of the following parameters:

• The minimum clock period, high time, and low time;

• The setup time of a signal is the duration over which the signal is required to hold constant prior to a rising edge.

• The minimum and maximum delay of a signal determine an interval during which the signal’s value may change following a rising edge.

Input Constraints

Suppose w(t) = v_{k} for all t ∈ [t_{0} + kπ − u, t_{0} + kπ), k = 1, …, n. Then w is stable w.r.t. u, based at t_{0} with effective value list (v_{1} … v_{n}) and period π.

We impose the following constraints:

• Clock parameters are respected. Assume period π and rising edge at t_{0};

• Each data input is stable w.r.t. its setup, based at t_{0} with period π and effective value list of length n;

• Reset is stable w.r.t. its setup, based at t_{0} − π with period π and effective value list (T F F … F) of length n + 1.

Main Theorem

Theorem 3 Let s be an output of a sequential module M with maximum delay D. Let w be the corresponding waveform of sim(M, p, t_{f}), where p satisfies the input constraints for M with period π. Let V be the list of vectors of effective data input values. Then w is stable w.r.t. π − D, based at t_{0} with effective value list sv(s, V, M) and period π. Suppose that s is a registered signal of M and that its effective values on two successive cycles coincide. Then w is constant on the second cycle.

Eliminating Metastability

Theorem 4 Let p = (wCLK wD), where wCLK is a periodic clock pulse with high ≥ 7000, low ≥ 7000, and successive rising edges at t_{1} and t_{3}, with intervening falling edge at t_{2}. Let wS2 be the output waveform of sim(dlatch, p, t_{f}). Then wS2 has a constant value v on [t_{2} + 7000, t_{3}). If wD has a constant value u on the cycle [t_{1}, t_{3}), then u = v.

Final Circuit

Correctness Theorem (Sketch)

Theorem 5 Assume all inputs meet stability constraints and the two clock periods are sufficiently close. Suppose SEND has effective value T on exactly 1 cycle, on which the other inputs have effective values (d_{0} … d_{7}). Then the outputs are stable. On the first cycle on which DONE has effective value T , the other outputs have effective values (d_{0} … d_{7}).

Proof (Sketch)

• Theorem 3 ⇒ output of sndr is stable with effective value list V_{r} = send(m, (d_{7} … d_{0})).

• Theorem 4 ⇒ input to rcvr is stable with effective value list V_{r}.

• Theorem 1 ⇒ V_{r} = asynch(V_{s}, t_{s}, t_{r}, π_{s}, π_{r}, oracle).

• Theorem 2 ⇒ recv(V_{r}) = (d_{7} … d_{0}).

• Theorem 3 ⇒ conclusion.