Specification and Verification of Gate-Level VHDL Models of Synchronous and Asynchronous Circuits

David M. Russinoff

Technical Report 99 May 10, 1994

Computational Logic, Inc. 1717 West Sixth Street, Suite 290 Austin, Texas 78703-4776

TEL: +1 512 322 9951 FAX: +1 512 322 0656

EMAIL: russ@cli.com

This work was sponsored in part at Computational Logic, Inc. by National Aeronautics and Space Administration Langley Research Center (NAS1-18878). The views and conclusions contained in this document are those of the author(s) and should not be interpreted as representing the official policies, either expressed or implied, of Computational Logic, Inc., NASA Langley Research Center or the U.S. Government.

Abstract

We present a mathematical definition of a hardware description language (HDL) that admits a semantics-preserving translation to a subset of VHDL. Our HDL includes the basic VHDL propagation delay mechanisms and gate-level circuit descriptions. We also develop formal procedures for deriving and verifying concise behavioral specifications of combinational and sequential devices. The HDL and the specification procedures have been formally encoded in the computational logic of Boyer and Moore, which provides a LISP implementation as well as a facility for mechanical proof-checking. As an application, we design, specify, and verify a circuit that achieves asynchronous communication by means of the biphase mark protocol.

1 Introduction

During the course of the design process, a typical hardware device is modeled at various levels of abstraction. The most abstract representation is generally a sequential machine, which is initially derived from a given behavioral specification. This model is then gradually refined to produce a concrete representation, such as a network of gates, which is more amenable to implementation.

A hardware design is validated by demonstrating the equivalence of these representations. This is most commonly effected through simulation. The VHSIC Hardware Description Language (VHDL), which is rapidly becoming an industry standard, supports modeling and simulation of circuits at all stages of the design process. In VHDL, a circuit component is represented as an entity, which may be associated with various alternative architectures. An architecture may either specify an abstract behavioral description of a device, or provide a concrete structural definition in terms of simpler components. The equivalence of architectures may be confirmed through comparative simulations. Once a sufficiently low-level VHDL architecture has been derived and validated in this manner, it may be implemented directly, even automatically.

However, since exhaustive testing of complex circuits is impractical, the effectiveness of simulation as a validation method is limited. An alternative approach is provided by formal hardware verification. The object of formal verification is to prove mathematically that a given model of a hardware device satisfies a given behavioral specification. Once this is accomplished, the design problem is reduced to that of implementing the model.

Naturally, the utility of this approach requires that the specification is sufficiently abstract to provide a comprehensive description of functionality, and that the model is sufficiently concrete to allow straightforward implementation. Unfortunately, hardware verification techniques have been deficient in this regard: proofs of of high-level specifications generally depend on similarly high-level implicit assumptions. In particular, verification of sequential machine behavior has been achieved only by basing the hardware model itself on the sequential machine concept.

For the purpose of addressing this problem, we have designed a formal hardware simulation language that admits a semantics-preserving translation to a subset of VHDL. The language is based on the paradigm of event-driven simulation and the basic signal propagation and delay mechanisms of VHDL. In particular, it includes the VHDL “delta-delay” mechanism, which complicates its definition considerably. Since this mechanism is irrelevant to our present purpose, we shall present here a simplified version of the language, in which all delays are required to be positive. The full language definition may be found in [6].

The language that we shall describe includes behavioral modules as primitives, which we use to model gates, and structural modules, with which we represent hierarchically constructed circuits. Our goal is to derive and verify abstract specifications of these gate-level models.

First, we consider the relatively simple class of combinational circuits, i.e., circuits that are free of cyclic paths. Each output of such a circuit is naturally associated with a certain Boolean function of the inputs. This association is commonly stated as follows: the value of an output at any time may be computed by applying the associated function to the current input values. Obviously, this description is valid only with respect to hardware models that ignore propagation delay. We shall derive a more accurate specification of combinational circuits and verify its validity in the context of our model.

The analysis of sequential circuits is considerably more complicated. While the abstract sequential machine model is well understood, its precise relationship with the actual behavior of the hardware that it is intended to describe is not. The sequential machine characterization is traditionally based on the extravagant assumption that signal values may change only at discrete points occurring at regular time intervals. This allows the behavior of a signal to be represented abstractly as a sequence of values. The value of an output over a given interval is then expressed as a function of the sequence of past input values. Of course, the underlying model again must disregard propagation delay. This approximation seems questionable, since the functionality of the basic state-holding elements generally depends critically on the presence of delays.

We shall treat a class of sequential circuits that may be characterized as synchronous resettable rising-edge-triggered devices. The basic memory element employed in their construction is a resettable clocked d-flip-flop, composed of nand gates. After verifying a precise specification of the behavior of this component, we establish a procedure for deriving high-level sequential machine descriptions for this class of circuits, and prove a theorem that gives a precise statement of the relationship between the sequential machine description of a circuit and its behavior as defined by our gate-level semantics.

One advantage of our approach is that we can effectively model asynchronous communication between individually synchronous processors. In fact, we shall present the definition of a circuit in our language that consists of two independently clocked sequential modules, and prove that communication between them is achieved by means of the well known biphase mark protocol [5]. The circuit design and the proof are both based on Moore’s work on asynchrony [4], which includes a formal model of asynchronous communication and a rigorous formulation of the protocol.

The syntax and semantics of our language are both based on the S-expressions of LISP. This decision was motivated by our desire to support its analysis with the use of the Nqthm system of Boyer and Moore [1]. Nqthm is based on a constructive formal logic for which the intended model is the domain of S-expressions. Thus, there is a correspondence between the formulas of this logic and informal propositions about S-expressions. A user of the system may extend the logic by adding axioms that correspond to definitions of computable functions over this domain.

Mechanical support for the Nqthm logic is provided by a LISP implementation that includes (1) an evaluator that computes values of functions defined in the logic, and (2) a theorem prover that may be used to derive logical consequences of the axioms. Since these theorems may be interpreted as propositions about functions of S-expressions, the prover may be used to verify mechanically the correctness of properties of these functions that have been derived by traditional (informal) mathematical methods.

All of the functions involved in the construction of our language, which we describe informally, meet the computability requirement for encoding as Nqthm definitions [1]. In fact, we have developed an Nqthm theory that formalizes these functions, including the module recognizers that form the syntax of the language, the interpreter that constitutes its semantics, and various procedures for deriving behavioral specifications of its programs. Thus, we have a complete LISP implementation of our language, provided by the Nqthm evaluator.

Moreover, all of our results, which are justified by informal (but mathematically rigorous) proofs, correspond in a natural way to Nqthm formulas. Thus, these proofs could, in principle, be checked mechanically by the Nqthm prover, thereby increasing our confidence in their validity at the the expense of some effort. In general, we have found it practical to employ the prover to check those proofs that involve extensive computation or detailed case analysis, while relying instead on the conventional social review process to detect any errors in our more intelligible proofs. In this instance, most of the results pertaining to specific circuits, including the components of the biphase mark implementation, have been mechanically verified, but at the time of this writing, most of the more general theorems have not.

Another benefit of the Nqthm formalization is that it provides a basis for a LISP implementation of the translator from our language to VHDL [3]. This potentially allows commercial VHDL synthesis tools to be used to implement our programs in silicon. As another application of more immediate interest, we have executed the translations of many of our programs using the Vantage VHDL simulator. For the simulations that we have tested, which include all of those described herein, the Vantage results were identical to those produced by our LISP-based interpreter. Aside from the practical advantage of increased efficiency, this offers evidence that we have achieved our goal of semantically capturing the VHDL subset in which we are interested. Indeed, in the absence of any comprehensive formal semantics for VHDL itself, these empirical observations provide the most convincing evidence possible.

2 Definition of the Language

2.1 S-expressions

Along with the set N of natural numbers, we posit a set B = {T , F} and an infinite set L, the elements of which are called Boolean and literal atoms, respectively. These three sets are assumed to be pairwise disjoint, and any element of their union is called an atom. We further assume that no atom is an ordered pair of atoms, and we recursively define an S-expression to be an atom or an ordered pair of Sexpressions. S denotes the set of all S-expressions. Three basic operations on S are defined: If z = (x, y) ∈ S × S, then car(z) = x, cdr(z) = y, and cons(x, y) = z.

We also assume the existence of various distinct literal atoms, which we shall mention as we proceed. Among these is the atom NIL. A list is an S-expression that is either NIL or an ordered pair z ∈ S × S such that cdr(z) is a list. The list NIL is denoted alternatively as (), and a non-NIL list z is denoted as (a_{1} … a_{n}), where a_{1} = car(z) and (a_{2} … a_{n}) denotes cdr(z). In this case, n is the length of z, and a_{1}, …, a_{n} are its members. For 1 ≤ i ≤ n, nth(i, z) is defined to be a_{i}. A list is a bit vector if each of its members is a Boolean atom.

A function f : B^{n} → B is an n-ary Boolean function. The following Boolean functions are called elementary: the 0-ary functions t0 and f0, with values T and F, respectively; the unary function not1; the binary functions and2, or2, nand2, nor2, xor2; the ternary functions and3, or3, nand3, nor3, xor3; the quaternary functions and4, or4, nand4, nor4, and xor4; and the quinary functions and5, or5, nand5, nor5, and xor5. The definitions of these functions are assumed to be understood.

For the purpose of encoding Boolean function calls, we also assume that each elementary Boolean function f is associated with a unique literal atom f̄ that is denoted with the same name as f. Thus, the function not1 is associated with the literal atom \overline{not1} = NOT1. We define a Boolean term over a list L of distinct literal atoms to be an S-expression that is either (a) a member of L, or (b) a list (f̄τ_{1} … τ_{n}), where f is an n-ary elementary Boolean function and each τ_{i} is an Boolean term over L.

Let L = (s_{1} … s_{k}) be a list of distinct literal atoms and let V = (v_{1} … v_{k}) be a bit vector. Then pairlist(L, V) is the list A = ((s_{1}, v_{1}) … (s_{k}, v_{k})), which is called an association list. If τ is a Boolean term over L, then we define eval(τ, A) to be (a) v_{i}, if τ = s_{i}, or (b) f(eval(τ_{1}, A), …, eval(τ_{n}, A)), if τ = (f̄τ_{1} … τ_{n}).

2.2 Waveforms

In the simplified version of our language on which the present work is based, our model of time is the set N. Thus, a moment is represented by a natural number, which we take arbitrarily to be the number of picoseconds elapsed since the beginning of a simulation. For t_{1}, t_{2} ∈ N, the interval {t ∈ N : t_{1} ≤ t < t_{2}} will be denoted as [t_{1}, t_{2}).

An event is an ordered pair e = (v, t), where v = value(e) ∈ B and t = time(e) ∈ N. Let w = ((v_{n}, t_{n}) … (v_{0}, t_{0})) be a list of events. If t_{i} > t_{i−1} and v_{i} ≠ v_{i−1} for 0 < i ≤ n, and t_{0} = 0, then w is a waveform. We define ŵ : T → B by ŵ(t) = v_{j}, where j is the greatest value of i satisfying t_{i} ≤ t; ŵ(t) is called the value of w at t. Note that ŵ_{1} = ŵ_{2} iff w_{1} = w_{2}. If t = t_{j}, then we shall say that w has a new value at t. We also define the history of w relative to t to be the waveform hist(w, t) = ((v_{j}, t_{j}) … (v_{0}, t_{0})).

A packet is a list of waveforms, p = (w_{1} … w_{n}), n ≥ 0. For any t ∈ N, the value of p at t is the bit vector p̂(t) = (ŵ_{1}(t) … ŵ_{n}(t)); p has a new value at t if any member of p does. The history of p relative to t is the packet hist(p, t) = (hist(w_{1}, t) … hist(w_{n}, t)).

The behavior of each signal occurring in a circuit will be modeled as a waveform. When a waveform is considered in the context of a current time t_{0}, each of its members e is viewed as a past, current, or future event, according to the relationship between time(e) and t_{0}. Past and present events are immutable, but future events are subject to deletion as they are superceded by newly scheduled events.

The fundamental operation of the simulator is the updating of a waveform w at a time t_{0} by scheduling a new event e = (v, t_{v}), where t_{0} < t_{v}. This may be performed by either of two procedures, corresponding to the transport and inertial delay modes of VHDL. The simpler of these is transport mode, in which each event (v′, t′) with t′ ≥ t_{v} is deleted from w, and e is then consed to the result, unless that result already has value v at t_{v}. The updated waveform w′ is computed as the value of transport(w, v, t_{v}), which is defined recursively as follows:

(1) Let car(w) = (v_{f}, t_{f}). If t_{f} ≥ t_{v}, then w′ = transport(cdr(w), v, t_{v}); otherwise:

(2) If v_{f} = v, then w′ = w; otherwise:

(3) w′ = cons((v, t_{v}), w).

Figure 1: Transport and Inertial Delay

Alternatively, w′ may be described in terms of the function ŵ′:

ŵ′(t) = \{ \begin{matrix}v & if t ≥ t_{v} \\ ŵ(t) & if t < t_{v}. \end{matrix}

Inertial mode is somewhat more complicated: every event (v′, t′) with t′ > t_{0} is deleted from w, and if ŵ(t_{0}) ≠ v, then a single event with value v is consed to the result. If ŵ(t_{v}) = v, then the time of this event is the time of the last event of w that precedes t_{v}; otherwise, it is t_{v}. Note that this procedure takes the current time t_{0} as an additional argument, and requires that t_{0} < t_{v}. The recursive definition of w′ = inertial(w, v, t_{0}, t_{v}) is given as follows:

(1) Let w̄ = hist(w, t_{0}). If ŵ(t_{0}) = v, then w′ = w̄; otherwise:

(2) Let car(w) = (v_{f}, t_{f}). If t_{f} ≥ t_{v}, then w′ = inertial(cdr(w), v, t_{0}, t_{v}); otherwise:

(3) If v_{f} = v, then w′ = cons((v, t_{f}), w̄); otherwise:

(4) w′ = cons((v, t_{v}), w̄).

The difference between the two propagation modes is illustrated in Fig. 1. The diagram labelled (a) represents the waveform

w = ((T , 9) (F, 8) (T , 6) (F, 5) (T , 3) (F, 1) (T , 0)).

The results of updating w at time 1 by scheduling an event with time 7 and value T , in both transport and inertial modes, are

transport(w, T , 7) = ((T , 6) (F, 5) (T , 3) (F, 1) (T , 0))

and

inertial(w, T , 1, , 7) = ((T , 6) (F, 1) (T , 0)),

as shown in (b) and (c), respectively.

Transport mode is often used to model wires (along which pulses of arbitrarily small duration are propagated to the delayed signal), while gate outputs are generally modeled by inertial delay. The latter, which is the VHDL default mode, will be used in all of our examples.

The following is a useful summary of both propagation functions. Each result may be proved by a straightforward induction. Note that (b) is consistent with our earlier informal observation that past and present events are immutable:

Lemma 2.1 Let w be a waveform, let t_{0}, t_{1}, and t_{v} be time objects with t_{0} < t_{v}, and let w′ be either transport(w, v, t_{v}) or inertial(w, v, t_{0}, t_{v}). Then

(a) ŵ′(t) = v for t ≥ t_{v};

(b) ŵ′(t) = ŵ(t) for t ≤ t_{0};

(c) if t_{1} ≤ t_{0} ≤ t_{2} ≤ t_{v} and ŵ(t) = u for t ∈ [t_{1}, t_{2}), then ŵ′(t) = u for t ∈ [t_{1}, t_{2}).

A similar induction shows that both procedures are “idempotent” in the following sense:

Lemma 2.2 If w is a waveform and t_{0}, t_{v}, t′_{0}, t′_{v} are time objects with t_{0} < t_{v}, t′_{0} < t′_{v}, t_{0} < t′_{0}, and t_{v} < t′_{v}, then

(a) transport(transport(w, v, t_{v}), v, t′_{v}) = transport(w, v, t_{v});

(b) inertial(inertial(w, v, t_{0}, t_{v}), v, t′_{0}, t′_{v}) = inertial(w, v, t_{0}, t_{v}).

2.3 Behavioral Modules

The simplest programs of our language are the behavioral modules, which contain explicit information concerning propagation delay and the functional dependence of outputs on inputs.

A behavioral module is a list M = (BEHAV I O T P D), where

(1) BEHAV is the identifying literal atom for modules of this type;

(2) I = I(M) = (r_{1} … r_{m}) is a list of literal atoms called the inputs of M;

(3) O = O(M) = (s_{1} … s_{n}) is a list of literal atoms called the outputs of M;

(4) T = T (M) = (τ_{1} … τ_{n}) is a list of elementary Boolean terms over I(M), called the output terms of M; (5) D = D(M) = (d_{1} … d_{n}) is a list of positive natural numbers, the delays of

M;

(6) P = P (M) = (p_{1} … p_{n}) is a list of literal atoms called the propagation modes of M, each of which is either TRANSPORT or INERTIAL.

The members of the list (r_{1} … r_{m} s_{1} … s_{n}) are required to be distinct and are called the signals of M.

Note that each output is associated with a term, a mode, and a delay. If every term is either an atom or a list of atoms, (i.e., contains no nested function calls), then M is primitive.

Gates are generally modeled as primitive modules with inertial delays. For example, we represent a simple 2-input nand gate as the primitive module nand2:

(BEHAV (A B) (C) ((NAND2 A B)) (2000) (INERTIAL))

We may define a similar behavioral module, with n inputs and 1 output, corresponding to each elementary n-ary Boolean function, arbitrarily taking the delay to be 2000 in each case. In the sequel, we shall refer to these primitive modules without explicitly listing their definitions.

Another example of a behavioral module is the 1-bit adder adder1:

(BEHAV (A B C) (L H)
  ((XOR3 A B C) (OR2 (AND2 A (OR2 B C)) (AND2 B C)))
  (12000 10000)
  (INERTIAL INERTIAL))

The two outputs of this module represent the 2-bit sum of the three input bits. Since the higher-order “carry” output bit is not expressed as an elementary function of the inputs, this is not a primitive module.

Let s = nth(j, O(M)) be an output of a behavioral module M and let τ = nth(j, T (M)) be the corresponding term. For any bit vector V of the same length as I(M), we define the combinational value of s w.r.t. V as

cv(s, V, M) = eval(τ, pairlist(I(M), V)).

We shall say that a list of waveforms is an input (resp., output) packet for a module M if it has the same length as I(M) (resp., O(M)). The semantics of behavioral modules are defined by a function exec of four arguments: (1) a module M, (2) an input packet p_{in} for M, (3) an output packet p_{out} = (w_{1} … w_{n}) for M, and (4) a time object t_{0}. The value of exec(M, p_{in}, p_{out}, t_{0}) is the updated output packet p′_{out} = (w′_{1} … w′_{n}) that results from “executing” M at t_{0}. It is defined as follows: For i = 1, …, n, let v_{i} be the combinational value of nth(i, O(M)) w.r.t. p̂_{in}(t_{0}), and let t_{i} = t_{0} + nth(i, D(M)). Then w′_{i} is either transport(w_{i}, v_{i}, t_{i}) or inertial(w_{i}, v_{i}, t_{0}, t_{i}), according to nth(i, P (M)).

Our first observation concerning the behavior of exec is that its value depends only on the current values of the input:

Lemma 2.3 Let p_{1} and p_{2} be input packets and let p_{out} be an output packet for a behavioral module M. For any t_{0} ∈ T, if p̂_{1}(t_{0}) = p̂_{2}(t_{0}), then exec(M, p_{1}, p_{out}, t_{0}) = exec(M, p_{2}, p_{out}, t_{0}).

Two other basic properties may be derived as consequences of Lemmas 2.1(b) and 2.2:

Lemma 2.4 Let p_{in} and p_{out} be an input packet and an output packet for a behavioral module M. For any t_{0} ∈ T, hist(exec(M, p_{in}, p_{out}, t_{0}), t_{0}) = hist(p_{out}, t_{0}).

Lemma 2.5 Let p_{in} and p_{out} be an input packet and an output packet for a behavioral module M and let t_{0} and t_{1} be time objects. If t_{0} < t_{1} and p̂_{in}(t_{0}) = p̂_{in}(t_{1}), then exec(M, p_{in}, exec(M, p_{in}, p_{out}, t_{0}), t_{1}) = exec(M, p_{in}, p_{out}, t_{0}).

2.4 Structural Modules

Our language also includes modules that represent hierarchically constructed circuits. These structures contain information concerning interconnections among the modules of which they are composed.

A structural module is a list M = (STRUCT I O S LI LO), where

(1) STRUCT is the identifying literal atom for modules of this type;

(2) I = I(M) = (r_{1} … r_{m}) is a list of literal atoms called the (global) inputs of M;

(3) O = O(M) = (s_{1} … s_{n}) is a list of literal atoms called the (global) outputs of M;

(4) S = S(M) = (μ_{1} … μ_{k}) is a list of (structural or behavioral) modules, called the submodules of M;

(5) LI = LI(M) = (A_{1} … A_{k}), where for j = 1, …, k, A_{j} = (a_{j1} … a_{jm_{j}}) is a list of literal atoms called the j^{th} local inputs of M, and m_{j} is the length of I(μ_{j}); (6) LO = (B_{1} … B_{k}), where for j = 1, …, k, B_{j} = (b_{j1} … b_{jn_{j}}) is a list of literal

atoms called the j^{th} local outputs of M, and n_{j} is the length of O(μ_{j}).

The members of the list (r_{1} … r_{m}b_{11} … b_{1n_{1}} … b_{k1} … b_{kn_{k}}), consisting of the global inputs and all local outputs, are required to be distinct and are called the signals of M. There is no such constraint on the global outputs or local inputs, but each local input must be a signal of M, and each global output must be a local output.

Note that the local inputs and outputs of M correspond to its submodules. Thus, intuitively, the submodules of a structure generate signals that are distinct from each other and from the structure’s inputs. Each signal may be connected to arbitrarily many submodule inputs. A signal other than a global input may serve as any number of global outputs, but global inputs and outputs are distinct.

Our first example is the structural module adder2, composed of nine nand gates and intended as a gate-level “implementation” of the behavioral module adder1:

(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 circuit diagram for adder2 appears in Fig. 2(b). Later, we shall compare its behavior with that of the behavioral module adder1.

An important feature of our language is that it allows cyclic signal paths, thereby providing for the modeling of state-holding devices. Figure 2(a) shows a clocked resettable d-flip-flop, which is modeled by the structural module 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)))

In addition to five 2-input nand gates, the submodules of dff include an inverter not1, an a 2-input and gate and2, and a 3-input nand gate nand3, the definitions of which are assumed to be understood.

We shall define the semantics of structural modules by means of a function step, based on the exec function of the preceding subsection. Note that the notions of input and output packets may be naturally applied to any module. For a structural module M, however, instead of a simple output packet, the third argument of step must be an object that consists of a waveform corresponding to each signal generated by each component of M. Thus, for any module M, we define a bundle for M to be a list B such that (a) if M is behavioral, then B is an output packet for M; (b) if M

Figure 2:  (a) D-Flip-Flop  (b) 1-Bit Adder

is a structure with S(M) = (μ_{1} … μ_{k}), then B = (β_{1} … β_{k}), where β_{i} is a bundle for μ_{i}, i = 1, …, k.

Let B be a bundle for a module M and let s be a signal of M that is not an input of M. The waveform for s determined by B is the waveform w that is computed as follows: (a) if M is behavioral and s = nth(j, O(M)), then w = nth(j, B);

(b) if M is structural and s = nth(j, nth(i, LO(M))), then w is the waveform for nth(j, O(nth(i, S(M))) determined by nth(i, B).

The output packet for M determined by B, denoted as outp(M, B), is defined as follows: (a) if M is behavioral, then outp(M, B) = B; (b) if M is structural with O(M) = (s_{1} … s_{n}), then outp(M, B) = (w_{1} … w_{n}), where for 1 ≤ j ≤ n, w_{j} is the waveform for s_{j} determined by B.

Let M be a structural module with nth(i, LI(M)) = (a_{i1} … a_{in_{i}}). Let p be an input packet and let B be a bundle for M. The i^{th} input packet determined by p and B, denoted as inp(i, M, p, B), is the input packet (w_{1} … w_{m}) for nth(i, S(M)), where for 1 ≤ j ≤ m, w_{j} is computed as follows: (a) if s_{j} is a global input nth(k, I(M)), then w_{j} = nth(k, p); (b) if s_{j} is a local output, then w_{j} is the waveform for s_{j} determined by B.

We may now define step. Let p and B be an input packet and a bundle, respectively, for an arbitrary module M, and let t ∈ T. Then step(M, p, B, t) is the bundle B′, defined as follows: (a) if M is behavioral, then B′ = exec(M, p, B, t) if p has a new value at t, and B′ = B if not; (b) if M is structural with S(M) = (μ_{1} … μ_{k}) and B = (β_{1} … β_{k}), then B′ = (β′_{1} … β′_{k}), where β′_{i} = step(μ_{i}, inp(i, M, p, B), β_{i}, t).

Thus, the execution of a structure at time t amounts to the execution of each behavioral component for which the value of some input signal changes at t.

We have the following generalization of Lemma 2.3:

Lemma 2.6 Let p_{1} and p_{2} be input packets and let B be a bundle for a module M. Let t_{0} ∈ T. If hist(p_{1}, t_{0}) = hist(p_{2}, t_{0}), then step(M, p_{1}, B, t_{0}) = step(M, p_{2}, B, t_{0}).

The history of a structural bundle (β_{1} … β_{k}) relative to a time t is recursively defined as hist(B, t) = (hist(β_{1}, t) … hist(β_{k}, t)). Lemma 2.4 may be generalized as follows:

Lemma 2.7 Let p and B be an input packet and a bundle for a module M. For any t_{0} ∈ T, hist(step(M, p, B, t_{0}), t_{0}) = hist(B, t_{0}).

2.5 Simulation

Let p and B be an input packet and a bundle for a module M. For any t ∈ N, we define t_{next}(t, p, B, M) to be the minimum element of the set of all t′ ∈ N that occur as times of events in the waveforms of p and B and that satisfy t′ > t, if this set is nonempty; otherwise, t_{next}(t, p, B, M) is undefined.

A simulation of M consists of repeated applications of step, which are performed by the function run. For t_{0}, t_{f} ∈ T, we define run(M, p, B, t_{0}, t_{f}) to be the bundle B′ that is computed recursively as follows: Let t_{next} = t_{next}(t_{0}, p, B, M). If t_{next} is defined and t_{next} ≤ t_{f}, then B′ = run(M, p, step(M, p, B, t_{next}), t_{next}, t_{f}); otherwise, B′ = B.

The definition of our top-level simulation function sim depends on run as well as a function init, which generates an initial bundle from a module and an input packet. First, for a given module M, we define the bundle B_{0}(M):

(1) If M is behavioral, then B_{0}(M) is the output packet (w_{0} … w_{0}) for M, where w_{0} = ((F, 0)).

(2) If M is structural and S(M) = (μ_{1} … μ_{k}), then B_{0}(M) = (B_{0}(μ_{1}) … B_{0}(μ_{k})).

Thus, every waveform of B_{0}(M) is the trivial w_{0}, which has the constant value ŵ_{0}(t) = F. Prior to simulation, each of these waveforms is updated by executing every behavioral component of M. The result is the bundle init(M, p), defined as follows:

(1) If M is behavioral, then init(M, p) = exec(M, p, B_{0}(M), 0);

(2) If M is structural with S(M) = (μ_{1} … μ_{k}), then init(M, p) = (init(μ_{1}, inp(1, M, p, B_{0}(M))) … init(μ_{k}, inp(k, M, p, B_{0}(M)))).

Specification and Verification of VHDL Models Technical Report #99 13

Figure 3: Simulation of adder1 and adder2

Now, given an input packet p for M and a time object t, we define

sim(M, p, t) = run(M, p, init(M, p), 0, t).

As an example, simulations of the modules adder1 and adder2 are illustrated in Fig. 3. The waveforms corresponding to the inputs A, B, and C are

w_{A} = ((F, 80000) (T , 12000) (F, 10000) (T , 0)),

w_{B} = ((F, 60000) (T , 20000) (F, 0)),

and

w_{C} = ((T , 60000) (F, 40000) (T , 0)),

respectively. The resulting output of the behavioral module adder1 is

sim(adder1, (w_{A} w_{B} w_{C}), 100000) = (w_{L} w_{H}),

where

w_{L} = (((T , 92000) (F, 52000) (T , 32000) (F, 0)))

and

w_{H} = ((F, 90000) (T , 10000) (F, 0)).

This example exhibits a fundamental characteristic of inertial delay, as distinguished from transport delay: an input pulse of duration less than the delay, as occurs in w_{A} over the interval [10000, 12000), is not reflected in the output.

The corresponding simulation of the circuit adder2 produces a bundle of the form

sim(adder2, (w_{A}w_{B}w_{C}), 100000) = ((w′_{T 1})(w′_{T 2})(w′_{T 3})(w′_{T 4})(w′_{T 5})(w′_{T 6})(w′_{T 7})(w′_{H})(w′_{L})),

of which we illustrate the output waveforms w′_{L} and w′_{H}. Note that the behavior of adder2 is somewhat more complicated than that of adder1, although for stable inputs, the two modules eventually produce the same values.

Some basic properties of the simulator that will be critical in the subsequent development are summarized in the following three lemmas. The first of these provides for the decomposition of a simulation interval:

Lemma 2.8 If p is an input packet for a module M, and t_{1} ≤ t_{2}, then sim(M, p, t_{2}) = run(M, p, sim(M, p, t_{1}), t_{1}, t_{2}).

An equally important result is the following, which describes the behavior of a structural module in terms of that of its components. Its proof (which appears in [6]) depends on the two properties of step that are stated in Lemmas 2.6 and 2.7, namely that module execution is neither predictive (with respect to input) nor retroactive (with respect to output):

Lemma 2.9 Let p be an input packet for a structural module M with S(M) = (μ_{1} … μ_{k}). Let t ∈ N and B = (β_{1} … β_{k}) = sim(M, p, t). Then β_{i} = sim(μ_{i}, b_{i}, t), where b_{i} = inp(i, M, p, B), i = 1, …, k.

Finally, as a consequence of Lemma 2.5, we observe that at any time during a simulation of a behavioral module, the output packet is the result of executing the module at that time, regardless of whether the execution actually occurs, i.e., whether there is change in input:

Lemma 2.10 Let p be an input packet for a behavioral module M, let t ∈ N, and let B = sim(M, p, t). Then B = exec(M, p, B, t).

3 Specification of Synchronous Circuits

3.1 Combinational Modules

Before undertaking a characterization of synchronous sequential circuits, we shall consider the relatively simple class of combinational circuits. Let ρ = (s_{1} … s_{p}) be a list of signals of a structural module M such that for each i, 1 < i ≤ p, there exists j such that s_{i−1} is a member of nth(j, LI(M)) and s_{i} is a member of nth(j, LO(M)). Then ρ is a path in M from s_{1} to s_{p}. If s_{1} = s_{p}, then ρ is a loop in M. An arbitrary module M is combinational if either (a) M is behavioral or (b) M is structural with no loops and all of its submodules are combinational.

The notion of combinational value, which previously applied only to outputs of behavioral modules, may be extended to combinational modules. Let s be any signal of a combinational module M and let V be a bit vector of the same length as I(M).

(1) If s = nth(j, I(M)), then cv(s, V, M) = nth(j, V);

(2) If M is structural and s = nth(j, nth(i, LO(M))), where μ = nth(i, S(M)) and (a_{1} … a_{m}) = nth(i, LI(M)), then

cv(s, V, M) = cv(nth(j, O(μ)), (cv(a_{1}, V, M) … cv(a_{m}, V, M)), μ).

We shall describe the behavior of combinational modules in terms of the function cv. Our analysis begins with the following characterization of behavioral modules:

Lemma 3.1 Let s = nth(j, O(M)) be the j^{th} output of a behavioral module M, let d = nth(j, D(M)) be the corresponding delay, and let w = nth(j, sim(M, p, t_{f})).

Assume that for all t ∈ [t_{1}, t_{2}), the combinational value of s w.r.t. p̂(t) is v, where t_{1} + d ≤ t_{2} and t_{1} ≤ t_{f}. Then for all t ∈ [t_{1} + d, t_{2} + d), ŵ(t) = v.

Proof: Let p_{1} = sim(M, p, t_{1}). Then according to Lemma 2.10,

p_{1} = exec(M, p, p_{1}, t_{1}).

It follows from Lemma 2.1(a) that the value of nth(j, p_{1}) is v for all t ≥ t_{1} + d.

We claim that if p′ is any output packet for M such that nth(j, p′) has value v throughout [t_{1} + d, t_{2} + d), then so does nth(j, run(M, p, p′, t′, t_{f})), for any t′ ≥ t_{1}. Once this claim is proved, the lemma will follow from Lemma 2.8 upon substituting p_{1} and t_{1} for p′ and t′.

The claim is proved by induction. It suffices to show that if p has a new value at t′′ = t_{next}(t′, p, p′, M), and p′′ = exec(M, p, p′, t′′), then nth(j, p′′) has value v throughout [t_{1} + d, t_{2} + d).

If t′′ ≥ t_{2}, then the desired result follows from Lemma 2.1(c). Thus, we may assume t′′ < t_{2} and hence, the combinational value of s w.r.t. p̂(t′′) is v. In this case, nth(j, p′′) has value v on [t_{1} + d, t′′ + d) by Lemma 2.1(c), and on [t′′ + d, t_{2} + d) by Lemma 2.1(a). □

Lemma 3.1 is illustrated by the simulation of adder1 shown in Fig. 3. Note, for example, that the output L of adder1, with corresponding term (XOR3 A B C), has the combinational value F throughout the interval from 40000 to 80000, and thus, since its delay is 12000, the actual value of the signal is F from 52000 to 92000. Note also that this simple behavior is not shared by the combinational module adder2.

However, we shall derive a generalization of Lemma 3.1 that provides similar (although somewhat weaker) behavioral specifications of arbitrary combinational modules. First, we associate each signal s of a combinational module M with two parameters, called the minimum and maximum delays of s, which represent the range of total delays along all paths connecting the inputs of M to s. These are defined as follows:

(1) If s is a member of I(M), then dmin(s, M) = dmax(s, M) = 0;

(2) If M is behavioral and s = nth(j, O(M)), then dmin(s, M) = dmax(s, M) = nth(j, D(M));

(3) If M is structural and s = nth(j, nth(i, LO(M))), where μ = nth(i, S(M)) and (a_{1} … a_{m}) = nth(i, LI(M)), then

dmin(s, M) = dmin(nth(j, O(μ)), μ) + min(dmin(a_{1}, M), …, dmin(a_{m}, M)),

dmax(s, M) = dmax(nth(j, O(μ)), μ)+max(dmax(a_{1}, M), …, dmax(a_{m}, M)).

Lemma 3.2 Let s = nth(j, O(M)) be the j^{th} output of a combinational module M, d = dmin(s, M), d′ = dmax(s, M), and w = nth(j, outp(M, sim(M, p, t_{f}))).

Assume that p̂ is constant on the interval [t_{1}, t_{2}), where t_{1} + d′ ≤ t_{2} and t_{1} ≤ t_{f}. Let v = cv(s, p̂(t_{1}), M). Then for all t ∈ [t_{1} + d′, t_{2} + d), ŵ(t) = v.

Proof: For behavioral M, the conclusion follows from Lemma 3.1. For structural M, we shall show that it holds more generally for any local output s of M and the waveform w for s determined by B = sim(M, p, t_{f}). The proof is by induction on the length of the longest path in M terminating at s.

Suppose s = nth(j, nth(i, LO(M))). Let μ = nth(i, S(M)), β = nth(i, B), (a_{1} … a_{m}) = nth(i, LI(M)), and b = inp(i, M, p, B) = (w_{1} … w_{m}). Then w = nth(j, outp(μ, β)), and by Lemma 2.9, β = sim(μ, b, t_{f}).

For 1 ≤ ℓ ≤ m, let d_{ℓ} = dmin(a_{ℓ}, M), d′_{ℓ} = dmax(a_{ℓ}, M), and v_{ℓ} = cv(a_{ℓ}, p̂(t_{1}), M). If a_{ℓ} is a local output of M, then by inductive hypothesis, ŵ_{ℓ}(t) = v_{ℓ} for all t ∈ [t_{1} + d′_{ℓ}, t_{2} + d_{ℓ}); otherwise, a_{ℓ} is an input, and the same is true trivially. Thus, b̂(t) = (v_{1} … v_{m}) for all t ∈ [t_{1} + Δ, t_{2} + δ), where Δ = max(d′_{1}, …, d′_{m}) and δ = min(d_{1}, …, d_{m}).

By the definition of cv,

v = cv(nth(j, O(μ)), (v_{1} … v_{m}), μ) = cv(nth(j, O(μ)), b̂(t_{1} + Δ), μ).

Since μ is combinational,ŵ(t) = v for all

t ∈ [t_{1} + Δ + dmax(nth(j, O(μ)), μ), t_{2} + δ + dmin(nth(j, O(μ)), μ))
= [t_{1} + d′, t_{2} + d). □

As an example, consider the output signal L of the combinational module adder2. By tracing all paths from the inputs to L, we may compute cv(L, (a b c), adder2) as a nested nand2 expression that may be shown to be tautologically equivalent to xor3(a, b, c). By a similar calculation, we have

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

Thus, according to Lemma 3.2, if t_{1} + 12000 ≤ t_{2}, t_{1} ≤ t_{f}, and the input packet p for adder2 has the constant value p̂(t) = (a b c) for t ∈ [t_{1}, t_{2}), then

w = nth(1, outp(adder2, sim(adder2, p, t_{2})))

has the value ŵ(t) = xor3(a, b, c) for t ∈ [t_{1} + 12000, t_{2} + 4000). This result is illustrated in Fig. 3: since the input packet has the constant value (T T T ) on the interval [20000, 40000), the value of the first output is xor3(T , T , T ) = T on the interval [32000, 44000).

3.2 Sequential Modules

We shall describe a class of sequential circuits that may be characterized as synchronous resettable rising-edge-triggered devices. The flip-flop dff of Subsection 2.4 will be used as a primitive in the construction of these circuits.

Let M be a structural module with I(M) = (r_{1} … r_{m}), where m ≥ 2, S(M) = (μ_{1} … μ_{k}), and for i = 1, …, k, nth(i, LI(M)) = (a_{i1} … a_{im_{i}}) and nth(i, LO(M)) = (b_{i1} … b_{in_{i}}). Let q ∈ N. Then M is a sequential module with multiplicity q = mult(M) if either (a) q = 0 and M = dff, or (b) 0 < q ≤ k and the following conditions hold:

(1) For 1 ≤ i ≤ q, μ_{i} is a sequential module;

(2) For q < i ≤ k, μ_{i} is a combinational module;

(3) For 1 ≤ i ≤ k and 1 ≤ j ≤ m_{i}, a_{ij} = r_{1} iff i ≤ q and j = 1;

(4) For 1 ≤ i ≤ k and 1 ≤ j ≤ m_{i}, a_{ij} = r_{2} iff i ≤ q and j = 2; (5) If (s_{1} … s_{p}) is a path in M with s_{1} = s_{p}, then for some i and j, where

1 ≤ i ≤ p and 1 ≤ j ≤ q, s_{i} is a member of nth(j, LO(M));

(6) If (s_{1} … s_{p}) is a path in M with s_{1} a global input and s_{p} a global output of M, then for some i and j, where 1 ≤ i ≤ p and 1 ≤ j ≤ q, s_{i} is a member of nth(j, LO(M)).

Throughout the remainder of this section, we shall assume that M is a sequential module with I(M), S(M), LI(M), and LO(M) as denoted above. Note that M must have at least two inputs, r_{1} and r_{2}, which we call the clock and reset, respectively; the other inputs are called data. According to (3) and (4), if M ≠ dff, then the clock and reset of M are connected to the clock and reset, respectively, of each sequential submodule of M, and to no other submodule inputs.

We define a path in M to be combinational if it contains no signal that is a local output of a sequential submodule. According to (5) of the definition, M contains no combinational loop; according to (6), no combinational path connects an input to an output.

We define a signal s of M to be native if there is no combinational path from any global input to s; the signals Q and QN of dff are also defined to be native. Thus, all outputs of M are native signals.

A native signal s of M is registered if either (a) M = dff and s is an output of M, or (b) M ≠ dff and s is a local output b_{ij} where i ≤ q and nth(j, O(μ_{i})) is a registered signal of μ_{i}. This property will have special significance in connection with asynchronous communication.

Two examples of sequential modules are diagrammed in Fig. 4. The enabled d-flip-flop, edff, is defined to be the following structure:

(STRUCT
  (CLK RST EN D)
  (Q QN)
  (dff not1 nand2 nand2 nand2)
  ((CLK RST S4) (EN) (S1 Q) (D EN) (S2 S3))
  ((Q QN) (S1) (S2) (S3) (S4)))

Clearly, this module satisfies the definition, with mult(edff) = 1.

The 3-bit counter count3 is a sequential module of multiplicity 3, defined as follows:

(STRUCT
  (CLK RST EN)
  (Q0 Q1 Q2)

  (edff edff edff and2 xor2 xor2)
  ((CLK RST EN QN0) (CLK RST EN S3) (CLK RST EN S2)
   (Q0 Q1) (S1 Q2) (Q0 Q1))
  ((Q0 QN0) (Q1 QN1) (Q2 QN2) (S1) (S2) (S3)))

Note that all outputs of both of these modules are registered.

3.3 Sequential Values

Our description of the behavior of sequential modules will be based on a function that computes a sequence of values for each output corresponding to a given sequence of input values. The definition of this function the notion of state. An object Σ is a state of M if

(1) M = dff and Σ ∈ B,

(2) mult(M) = 1 and Σ is a state of μ_{1}, or

(3) mult(M) = q > 1 and Σ = (σ_{1} … σ_{q}), where for i = 1, …, q, σ_{i} is a state of μ_{i}.

Thus, a state associates a Boolean value with each flip-flop. The reset state Σ_{0}(M) is the state for which each of these values is F:

(1) Σ_{0}(dff) = F;

(2) If mult(M) = 1, then Σ_{0}(M) = Σ_{0}(μ_{1});

(3) If mult(M) = q > 1, then Σ_{0}(M) = (Σ_{0}(μ_{1}) … Σ_{0}(μ_{q})).

A data vector for M is a bit vector of length m − 2, the components of which correspond to the data inputs of M. We shall define a function next(V, Σ, M) that computes a state of M from a data vector V and a state Σ. This definition requires two auxiliary functions.

First, for a native signal s and a state Σ of M, we define the native value of s determined by Σ, denoted as nv(s, Σ, M), as follows:

(1) nv(Q, Σ, dff) = Σ and nv(QN, Σ, dff) = not1(Σ);

(2) If mult(M) = 1 and s = b_{1j}, then nv(s, Σ, M) = nv(nth(j, O(μ_{1})), Σ, μ_{1});

(3) If mult(M) = q > 1 and s = b_{ij}, where i ≤ q, then

nv(s, Σ, M) = nv(nth(j, O(μ_{i})), nth(i, Σ), μ_{i});

(4) If mult(M) = q ≥ 1 and s = b_{ij}, where i > q, then

nv(s, Σ, M) = cv(nth(j, O(μ_{i})), (nv(a_{i1}, Σ, M) … nv(a_{im_{i}}, Σ, M)), μ_{i}).

Now, let V = (v_{3} … v_{m}) and Σ be a data vector and a state of M, respectively. We define the resultant value of a signal s determined by V and Σ, denoted as rv(s, V, Σ, M), as follows:

(1) If s = r_{i} is a data input of M, then rv(s, V, Σ, M) = v_{i};

(2) If s is native to M, then rv(s, V, Σ, M) = nv(s, Σ, M);

(3) If mult(M) = q > 0 and s = b_{ij}, where i > q, then

rv(s, V, Σ, M) = cv(nth(j, O(μ_{i})), (rv(a_{i1}, V, Σ, M) … rv(a_{im_{i}}, V, Σ, M)), μ_{i}).

We may now define the function next. Let mult(M) = q and for i = 1, …, q, let L_{i} = (rv(a_{i1}, V, Σ, M) … rv(a_{im_{i}}, V, Σ, M)). Then next(V, Σ, M) = Σ′, where

(1) If q = 0 (i.e., M = dff), then Σ′ = v_{3};

(2) If q = 1, then Σ′ = next(L_{1}, Σ, μ_{1});

(3) If q > 1 and Σ = (σ_{1} … σ_{q}), then Σ′ = (next(L_{1}, σ_{1}, μ_{1}) … next(L_{q}, σ_{q}, μ_{q})).

Now, let V = (V_{3} … V_{m}), where for i = 3, …, m, V_{i} = (v_{i1} … v_{in}) is a bit vector of length n. V may be viewed as a Boolean matrix, the rows of which correspond to the data inputs of M. Each column of this matrix, V̄_{j} = (v_{3j} … v_{mj}), where j = 1, …, n, is a data vector for M. A sequence of n + 1 states is determined by V as follows:

state(j, V, M) = \{ \begin{matrix}Σ_{0}(M) if j = 0 \\ next(V̄_{j}, , state(j − 1, V, M), M) if 0 < j ≤ n. \end{matrix}

For any native signal s of M, the j^{th} sequential value of s determined by V is defined as

sv(j, s, V, M) = nv(s, state(j, V, M), M).

Thus, the sequential values corresponding to a given matrix of input values are determined by the functions nv and next. As an illustration, we shall analyze the behavior of these functions for the modules edff and count3. Clearly, a state of

Figure 4:  (a) edff  (b) count3

edff is a state of dff, i.e., a Boolean value. If Σ is such a state and V = (v_{3} v_{4}) is a data vector, then

rv(Q, V, Σ, edff) = nv(Q, V, Σ, edff) = nv(Q, Σ, dff) = Σ

and

rv(QN, V, Σ, edff) = nv(QN, V, Σ, edff) = nv(QN, Σ, dff) = not1(Σ).

Expanding the definition of rv, we have

rv(S4, V, Σ, edff) = nand2(nand2(not1(v_{3}), Σ), nand2(v_{3}, v_{4})),

which is also the value of next(V, Σ, edff). A trivial calculation yields the following:

Proposition 3.1 Let Σ and V = (v_{3} v_{4}) be a state and a data vector for edff. Then

nv(Q, V, Σ, edff) = Σ and nv(QN, V, Σ, edff) = not1(Σ);

next(V, Σ, edff) = \{ \begin{matrix}v_{4} & if v_{3} = T \\ Σ & if v_{3} = F. \end{matrix}

A state of count3 is a vector of 3 Boolean values, corresponding to the

mult(count3) = 3

occurrences of edff. If Σ = (σ_{0} σ_{1} σ_{2}) and V = (v_{3}) are a state and a data vector, then

rv(S1, V, Σ, count3) = and2(σ_{0}, σ_{1}),
rv(S2, V, Σ, count3) = xor2(and2(σ_{0}, σ_{1}), σ_{2}),
rv(S3, V, Σ, count3) = xor2(σ_{0}, σ_{1}),

and it follows from Proposition 3.1 that

next(V, Σ, count3) = \{ \begin{matrix}(not1(σ_{0}) xor2(σ_{0}, σ_{1}) xor2(and2(σ_{0}, σ_{1}), σ_{2}) if v_{3} = T \\ Σ if v_{3} = F. \end{matrix}

This result is conveniently expressed in terms of the function inc(W), defined as follows for an arbitrary bit vector W:

(1) If W = NIL, then inc(W) = NIL; otherwise:

(2) If car(W) = T , then inc(W) = cons(F, inc(cdr(W))); otherwise:

(3) inc(W) = cons(T , cdr(W)).

Proposition 3.2 Let Σ = (σ_{0} σ_{1} σ_{2}) and V = (v_{3}) be a state and a data vector for

count3. Then

nv(Q0, V, Σ, count3) = σ_{0}, nv(Q1, V, Σ, count3) = σ_{1}, nv(Q2, V, Σ, count3) = σ_{2};

next(V, Σ, count3) = \{ \begin{matrix}inc(Σ) & if v_{3} = T \\ Σ & if v_{3} = F. \end{matrix}

3.4 Behavior of dff

Naturally, the behavior of sequential modules depends on that of the primitive dff. A precise behavioral specification of dff is given by the following lemma, the proof of which is an elaboration of the informal argument found in [7]:

Lemma 3.3 Let t_{1}+4000 ≤ t_{−}, t_{−}+6000 ≤ t_{2}, and t_{1} ≤ t_{f}. Let p = (w_{CLK}w_{RST}w_{D}) be an input packet for dff, and suppose that

ŵ_{CLK}(t) = \{ \begin{matrix}F for all t ∈ [t_{1} − 6000, t_{1}) ∪ [t_{−}, t_{2}) \\ T for all t ∈ [t_{1}, t_{−}), \end{matrix}

ŵ_{RST}(t) = r for all t ∈ [t_{1} − 8000, t_{1}), and

ŵ_{D}(t) = d for all t ∈ [t_{1} − 6000, t_{1}).

Let sim(dff, p, t_{f}) = ((w_{RN}) (w_{DD}) (w_{A1}) (w_{B1}) (w_{A2}) (w_{B2}) (w_{Q}) (w_{QN})) and let v = and2(not1(r), d). Then ŵ_{Q}(t) = v and ŵ_{Q}(t) = not1(v) for all t ∈ [t_{1} + 6000, t_{2} + 4000). Moreover, if these same values hold for all t ∈ [t_{1}, t_{1} + 4000), then they also hold for all t ∈ [t_{1} + 4000, t_{1} + 6000).

Proof: By Lemmas 3.1 and 2.9, we have ŵ_{RN}(t) = not1(r) for all t ∈ [t_{1} − 6000, t_{1} + 2000). Applying the same two lemmas again, we have ŵ_{DD}(t) = v for all t ∈ [t_{1}−4000, t_{1}+2000). Similarly, ŵ_{A2}(t) = ŵ_{B1}(t) = T for t ∈ [t_{1}−4000, t_{1}+2000), ŵ_{B2}(t) = not1(v) for t ∈ [t_{1} − 2000, t_{1} + 4000), and hence ŵ_{A1}(t) = v for t ∈ [t_{1}, t_{1} + 4000).

We shall consider the case v = F; the case v = T is similar. In this case, ŵ_{B1}(t) = T for t ∈ [t_{1} + 2000, t_{1} + 6000), and hence ŵ_{A2}(t) = F for t ∈ [t_{1} + 2000, t_{1} + 6000).

Let t′ be the least time such that t′ > t_{1} + 2000 and some waveform in the set {w_{A1}, w_{B1}, w_{A2}, w_{B2}} assumes a new value at t′. Then ŵ_{A1}(t) = ŵ_{A2}(t) = F and ŵ_{B1}(t) = ŵ_{B2}(t) = T for t ∈ [t_{1} + 2000, t′). Since t′ ≥ t_{1} + 4000, it follows that ŵ_{B1}(t) = ŵ_{B2}(t) = T and ŵ_{A1}(t) = F for t ∈ [t_{1} + 4000, t′ + 2000). Similarly, ŵ_{A2}(t) = F for t ∈ [t_{1} +4000, min(t′ +4000, t_{−} +2000)). Thus, only w_{A2} can possibly assume a new value at t′, and this requires that t′ ≥ t_{−} + 2000.

Hence, ŵ_{B1}(t) = T and ŵ_{A2}(t) = F for t ∈ [t_{1} + 2000, t_{−} + 2000). It follows that ŵ_{QN}(t) = T for t ∈ [t_{1} + 4000, t_{−} + 4000), and hence ŵ_{Q}(t) = F for t ∈ [t_{1} + 6000, t_{−} + 4000).

Let t′′ be the least time such that t′′ > t_{1} + 6000 and either w_{Q} or w_{QN} assumes a new value at t′′. By an argument similar to the above, it is easily shown that t′′ ≥ t_{2} + 4000. Thus, ŵ_{Q}(t) = F = u_{r} for t ∈ [t_{1} + 6000, t_{2} + 4000), and ŵ_{QN}(t) = T = not1(u_{r}) for t ∈ [t_{1} + 4000, t_{2} + 4000).

Now suppose that ŵ_{Q}(t) = F and ŵ_{QN}(t) = T for t ∈ [t_{1}, t_{1} + 4000). Then ŵ_{QN}(t) = T for t ∈ [t′_{1}, t_{2} + 4000). It follows that ŵ_{Q}(t) = F for t ∈ [t_{1} + 4000, t_{2} + 4000). □

3.5 Parameters

Our objective is to impose constraints on the input to a sequential module that will allow its outputs to be described in terms of sequential values. In particular, the clock input will be required to exhibit periodic behavior. We shall call each event of its associated waveform a rising or falling edge, according to whether its value is T or F. An interval between two successive rising edges is called a cycle. Each of the remaining inputs will be required to maintain a stable value over a prescribed interval preceding each rising edge. For the reset input r_{2}, this value is T for an initial cycle, and F for every cycle thereafter.

Under these constraints, we shall show that the behavior of M admits a fairly simple description. A state of M will be associated with each rising edge. This state may computed from the data values prior to the edge and the previous state by the function next. The values of the outputs, which may change only during a short interval following a rising edge, are the corresponding sequential values.

We shall describe the behavior of the signals of M in terms of several parameters. First, we associate with each input other than the clock a setup time, which represents the duration over which the signal is required to hold constant prior to a rising edge. For the case M = dff, as suggested by Lemma 3.3, we define

setup(RST, dff) = 8000 and setup(D, dff) = 6000.

Now suppose mult(M) = q > 0 and let s be any signal of M other than r_{1}. Assume setup(s′, M) has been defined for each s′ ≠ s that lies on a combinational path starting at s. For i = 1, …, k, let ζ_{i} be defined as follows:

(1) If s ≠ a_{ij} for all j, 1 ≤ j ≤ m_{i}, then ζ_{i} = 0; otherwise:

(2) If i ≤ q, then ζ_{i} is the maximum setup(nth(j, I(μ_{i})), μ_{i}) such that s = a_{ij}, j = 2, …, m_{i}; otherwise:

(3) i > q, and ζ_{i} is the maximum sum dmax(nth(j, O(μ_{i})), μ_{i}) + setup(b_{ij}, M) such that setup(b_{ij}, M) > 0, j = 1, …, n_{i}.

Then setup(s, M) = max(ζ_{1}, …, ζ_{k}).

Each native signal of M is associated with a minimum and a maximum delay, which determine an interval during which the signal’s value may change following a rising edge. For the case M = dff, we define

dmin(Q, dff) = dmin(QN, dff) = 4000,

dmax(Q, dff) = dmax(QN, dff) = 6000.

Now suppose mult(M) = q > 0 and let s = b_{ij} be any native signal of M.

(1) If i ≤ q, then

dmin(s, M) = dmin(nth(j, O(μ_{i})), μ_{i}),
dmax(s, M) = dmax(nth(j, O(μ_{i})), μ_{i});

(2) If i > q, then

dmin(s, M) = dmin(nth(j, O(μ_{i})), μ_{i})+min(dmin(a_{i1}, M), …, dmin(a_{im_{i}}, M)),

dmax(s, M) = dmax(nth(j, O(μ_{i})), μ_{i})+max(dmax(a_{i1}, M), …, dmax(a_{im_{i}}, M)).

We also define three parameters pertaining to the behavior of the clock input of M, called the clock high, the clock low, and the minimum period of M. These represent the minimum durations between a rising edge and the next falling edge, a falling edge and the next rising edge, and successive rising edges, respectively. First, we define high(dff) = 4000, low(dff) = 6000, and per(dff) = 10000. For mult(M) = q > 0, we define

high(M) = max(high(μ_{1}), …, high(μ_{q}));

low(M) = max(low(μ_{1}), …, low(μ_{q}));

per(M) = max(P_{1}, P_{2}, P_{3}), where P_{1} = max{per(μ_{i}) : 1 ≤ i ≤ q}; P_{2} = max{setup(r_{i}, M) : 2 ≤ i ≤ m}; P_{3} = max{setup(b_{ij}, M) + dmax(nth(j, O(μ_{i})), μ_{i}) : 1 ≤ i ≤ q, 1 ≤ j ≤ n_{i}}.

Consider, for example, the circuits edff and count3. First, the setup times for the signals of edff may be computed directly from the definitions, by tracing along all combinational paths. For example,

setup(RST, edff) = 8000,
setup(EN, edff) = 12000,
setup(D, edff) = 10000;

The setups for count3 follow trivially:

setup(RST, count3) = 8000,
setup(EN, count3) = 12000.

In fact, it follows from our definitions that the reset input of every sequential module is 8000.

All outputs of both of these devices are registered. It follows that the minimum and maximum delay of each output are 4000 and 6000, respectively.

Similarly, the clock high and low of each device (in fact, of any sequential device) are 4000 and 6000, respectively, as determined by dff. Calculation of the minimum period, on the other hand, involves a comparison of various setups and delays. In the case of edff, the minimum period is found to be

setup(Q, edff) + dmax(Q, dff) = 10000 + 6000 = 16000;

for count3, it is

setup(Q0, count3) + dmax(Q, edff) = 14000 + 6000 = 20000.

3.6 The Main Theorem

The input constraints for sequential modules will be expressed in terms of the functions setup, high, low, and per. First, we define a waveform w to be an n-cycle pulse based at t_{0} with high h, low ℓ, and period π = h + ℓ if for k = 0, …, n − 1,

ŵ(t) = \{ \begin{matrix}T for all t ∈ [t_{0} + kπ, t_{0} + kπ + h) \\ F for all t ∈ [t_{0} + kπ + h, t_{0} + (k + 1)π). \end{matrix}

If h ≥ high(M), ℓ ≥ low(M), and π ≥ per(M), then w is an admissible pulse for M.

Let V = (v_{1} … v_{n}) be a bit vector and let π ≥ u > 0. Let w be a waveform such that for k = 1, …, n, ŵ(t) = v_{k} for all t ∈ [t_{0} + kπ − u, t_{0} + kπ). Then w is a stable n-cycle waveform based at t_{0} with setup u, value list V, and period π. If u = setup(r_{2}, M), v_{1} = T , and v_{2} = … = v_{r} = F, then w is an admissible reset waveform for M.

For i = 1, …, k, let w_{i} be a stable n-cycle waveform based at t_{0} with value list V_{i}, setup u_{i}, and period π. Let V = (V_{1} … V_{k}), U = (u_{1} … u_{k}), and W = (w_{1} … w_{k}). Then W is a stable n-cycle packet based at t_{0} with value matrix V, setup list U, and period π. If k = m − 2 and u_{i} = setup(r_{i+2}, M) for i = 1, …, k, then W is an admissible data packet for M.

Let w_{1} be an admissible (n + 2)-cycle pulse for M based at t_{0} with period π. Let w_{2} be an admissible (n + 1)-cycle reset waveform for M based at t_{0} with period π. Let w_{3} … w_{m}) be an admissible n-cycle data packet for M based at t_{0}+π with value matrix V and period π. Then (w_{1} … w_{m}) is an admissible n-cycle input packet for M based at t_{0} with value matrix V and period π.

We may now state a behavioral specification for sequential modules:

Theorem 3.1 Let s = nth(j, O(M)) be the j^{th} output of a sequential module M, d′ = dmax(s, M), and w = nth(j, outp(M, sim(M, p, t_{f}))).

Assume that p is an admissible n-cycle input packet for M based at t_{0} with value matrix V and period π, where t_{f} ≥ t_{0} + (n + 1)π. For i = 0, …, n, let v_{i} = sv(i, s, V, M). Then w is a stable (n + 1)-cycle waveform based at t_{0} + π with setup π − d′, value list (v_{0} … v_{n}), and period π;

Assume further that s is a registered signal of M and v_{i−1} = v_{i}, for some i, 1 ≤ i ≤ n. Then ŵ(t) = v_{i} for all t ∈ [t_{0} + (i + 1)π, t_{0} + (i + 2)π).

Theorem 3.1 is an immediate consequence of the following:

Lemma 3.4 Let s = nth(j, O(M)) be the j^{th} output of a sequential module M, d = dmin(s, M), d′ = dmax(s, M), and w = nth(j, outp(M, sim(M, p, t_{f}))).

Assume that p is an admissible n-cycle input packet for M based at t_{0} with value matrix V and period π. Let t_{0} + (n + 1)π = t_{1}, t_{1} + π = t_{2}, and assume t_{1} ≤ t_{f}. Let v = sv(n, s, V, M). Then ŵ(t) = v for all t ∈ [t_{1} + d′, t_{2} + d).

Suppose further that s is a registered signal of M. If n > 0 and sv(n − 1, s, V, M) = v, then ŵ(t) = v for all t ∈ [t_{1} + d, t_{2} + d).

Proof: For the case M = dff, the lemma is simply a restatement of Lemma 3.3. Thus, we may assume that M ≠ dff and proceed by induction on the structure of M. Let V = (V_{3} … V_{m}), where for i = 3, …, m, V_{i} = (v_{i1} … v_{ir}). For j = 0, …, n, let Σ_{j} = state(j, V, M).

Let B = sim(M, p, t_{f}), and for each signal s of M, let

w_{s} = \{ \begin{matrix}nth(i, p) if s is a global input r_{i} \\ the waveform for s determined by B if s is a local output b_{ij}, \end{matrix}

If s is not r_{1} or r_{2}, then for 0 ≤ ℓ < n, let

val(s, ℓ) = rv(s, (v_{3(ℓ+1)} … v_{m(ℓ+1)}), Σ_{ℓ}, M).

If s is native, then by definition we have

val(s, ℓ) = nv(s, Σ_{ℓ}, M) = sv(ℓ, s, V, M).

Thus, for native s, we extend the definition to ℓ = n by

val(s, n) = sv(n, s, V, M).

For any ℓ ∈ N, let t^{ℓ} = t_{0} + (ℓ + 1)π, so that t_{1} = t^{n} and t_{2} = t^{n+1} = t^{n} + π. We shall prove, by induction on ℓ, that the following three statements hold for each ℓ ≤ n:

(a) For each i, 1 ≤ i ≤ q, inp(i, M, p, B) is an admissible ℓ-cycle input packet for μ_{i} based at t_{0} with value matrix

((val(a_{i3}, 0) … val(a_{i3}, ℓ − 1)) … (val(a_{im_{i}}, 0) … val(a_{im_{i}}, ℓ − 1)))

and period π.

(b) For each native signal s = b_{ij} of M,

ŵ_{s}(t) = val(s, ℓ) for all t ∈ [t^{ℓ} + dmax(s, M), t^{ℓ+1} + dmin(s, M));

if s is a registered signal of M, then the same is true for the interval

[t^{ℓ} + dmin(s, M), t^{ℓ+1} + dmin(s, M));

(c) If ℓ < n, then for each signal s of M other than r_{1} and r_{2},

ŵ_{s}(t) = val(s, ℓ) for all t ∈ [t^{ℓ+1} − setup(s, M), t^{ℓ+1}).

The lemma will then follow from (b), taking ℓ = n.

Proof of (a): For ℓ = 0, this follows from (3) and (4) in the definition of sequential module. For ℓ > 0, we must also invoke the inductive hypothesis that (c) holds with ℓ replaced by ℓ − 1.

Proof of (b): We induct on the length of the longest combinational path terminating at s. Let s = b_{ij}. In the base case, where i ≤ q, the result follows from the inductive assumption that the lemma holds for the sequential submodule μ_{i}, Lemma 2.9, and (a). In the inductive case, where i > q, it follows from Lemmas 2.9 and 3.2.

Proof of (c): This is similarly proved by induction on the length of the longest combinational path terminating at s. In the base case, s is either a global input r_{i}, i ≥ 3, or a local output b_{ij}, i ≤ q. If s = r_{i}, then the claim follows directly from the admissibility of the input packet p. Suppose s = b_{ij}, i ≤ q. It follows from (b) that

ŵ_{s}(t) = val(s, ℓ) for all t ∈ [t^{ℓ} + dmax(s, M), t^{ℓ+1}).

According to the definition of per(M),

π ≥ setup(b_{ij}, , M) + dmax(nth(j, O(μ_{i})), μ_{i}).

Hence,

t^{ℓ} + dmax(s, M) = t^{ℓ+1} − π + dmax(nth(j, O(μ_{i})), μ_{i}) ≤ t^{ℓ+1} − setup(b_{ij}, M).

The induction is completed as in the proof of (b). □

4 Asynchronous Communication

Suppose we have a circuit in which an output of one sequential module, called the sender, is connected to a data input of another, called the receiver. Under suitable conditions on the sender’s input, its output waveform is guaranteed by Theorem 3.1 to be stable with respect to the period of the sender’s clock. On the other hand, in order to apply the results of Section 3 to the behavior of the receiver, we must be able to assume that its input is stable with respect to the period of its own clock. In general, this is true only for a synchronous circuit, in which the two modules are driven by the same clock. In this section, we shall examine the asynchronous case, in which the two clock inputs have different periods.

Our treatment of this problem is based on Moore’s model of asynchrony [4]. In this model, the behavior of a signal is characterized abstractly by three quantities: a base time, a period, and a bit vector (representing the values assumed on successive cycles). Moore postulates that the receiver’s input vector is determined by a function asynch, the arguments of which include the sender’s output vector, the two periods, and the two base times. In this section, we shall present Moore’s function asynch and establish the applicability of his model to certain circuits represented in our language. In Section 5, we shall employ a theorem of Moore to show that if the sender’s and receiver’s periods are known to be approximately equal, then communication may be achieved by means of a well known protocol.

4.1 Smooth and Quasi-Smooth Waveforms

The communication protocol is motivated by the observation that if the time at which the receiver samples its input may be approximated by the sender, then the sender may successfully communicate a value by redundantly writing the value on sufficiently many successive cycles to guarantee that it is the value read by the receiver. For this purpose, the assumption that the sender’s output waveform is stable is too weak; the waveform must be known to be constant on each cycle during some critical interval. With this requirement in mind, we define a stable waveform to be smooth if its setup time coincides with its period. Thus, w is a smooth n-cycle waveform based at t_{0} with value list V = (v_{1} … v_{n}) and period π if for i = 1, …, n, ŵ(t) = v_{i} for all t ∈ [t_{0} + (k − 1)π, t_{0} + kπ).

A somewhat weaker notion of smoothness is needed to describe waveforms that are constant over some but not all cycles. First, we define a list V = (v_{1} … v_{n}) to be a generalized bit vector if each v_{i} is either Boolean or the literal atom Q. In this case, we shall call w a quasi-smooth n-cycle waveform based at t_{0} with value list V and period π if for i = 1, …, n, either v_{i} = Q or ŵ(t) = v_{i} for all t ∈ [t_{0}+(k−1)π, t_{0}+kπ). (Thus, the value Q corresponds to cycles of unknown behavior.)

Our first objective is to derive a nontrivial representation of an output waveform of a sequential device as a quasi-smooth waveform. For this purpose, we make the following definition: If v is a Boolean atom and V is a bit vector, then smooth(v, V) is the generalized bit vector V′, where

(1) If V = NIL, then V′ = NIL; otherwise:

(2) If car(V) = v, then V′ = cons(v, smooth(v, cdr(V))); otherwise:

(3) V′ = cons(Q, smooth(car(V), cdr(V))).

Thus, if v = v_{0} and V = (v_{1} … v_{n}), then V′ = (v′_{1} … v′_{n}), where for i = 1, …, n,

v′_{i} = \{ \begin{matrix}v_{i} if v_{i} = v_{i−1} \\ Q if v_{i} ≠ v_{i−1}. \end{matrix}

Lemma 4.1 Let s = nth(j, O(M)) be a registered output of a sequential module M. Let w = nth(j, outp(M, sim(M, p, t_{f}))), where p is an admissible n-cycle input packet for S based at t_{0} with value matrix V and period π, and t_{f} ≥ t_{0} + (n + 1)π.

Let U = (sv(0, s, V, M) … sv(n, s, V, M)). Then w is an n-cycle quasi-smooth waveform based at t_{0} + 2π with value list smooth(car(U), cdr(U)) and period π.

Proof: For 0 ≤ k ≤ n, let U_{k} = (sv(n − k, s, V, M) … sv(n, s, V, M)) and V_{k} = smooth(car(U_{k}), cdr(U_{k})). We shall prove, by induction on k, that w is a k-cycle quasi-smooth waveform based at t_{0} + (n − k + 2)π with value list V_{k} and period π.

The base case k = 0 holds vacuously. For k > 0, since cdr(V_{k}) = V_{k−1}, we need only consider car(V_{k}) and the behavior of w on [t_{0} +(n−k+2)π, t_{0} +(n−k+3)π). If car(V_{k}) = Q, there is nothing to prove. In the remaining case, car(V_{k}) = car(U_{k}) = car(U_{k−1}), i.e., sv(n − k, s, V, M) = sv(n − k + 1, s, V, M), and the result follows from Theorem 3.1. □

4.2 Describing Output as Input

Next, for a given quasi-smooth waveform with period π_{s} (representing that of the sender’s clock), we would like to derive an alternative representation as a quasismooth waveform with a given period π_{r} (that of the receiver’s clock). Let w be an n-cycle quasi-smooth waveform based at t_{s} (a rising edge of the sender’s clock) with value list V = (v_{1} … v_{n}) and period π_{s}. Assume t_{s} ≤ t_{r} < t_{s} + π_{s} (where t_{r} represents a rising edge of the receiver’s clock). We shall construct a list of values V′ = warp(V, t_{s}, t_{r}, π_{s}, π_{r}) such that w is a quasi-smooth waveform based at t_{r} with value list V′ and period π_{r}. The definition of warp requires several auxiliary functions.

Let t satisfy t_{s} < t ≤ t_{s} + nπ_{s}. Choose k so that t_{s} + (k − 1)π_{s} < t ≤ t_{s} + kπ_{s}. Then 1 ≤ k ≤ n. (k represents the number of cycles of the sender that intersect the interval [t_{r}, t).) We define

sig(V, t_{s}, t, π_{s}) = \{ \begin{matrix}v_{1} if v_{1} = v_{2} = … = v_{k} \\ Q if not. \end{matrix}

Under the same constraints on t, choose ℓ so that t_{s} + ℓπ_{s} ≤ t < t_{s} + (ℓ + 1)π_{s}. Then 0 ≤ ℓ ≤ n. (t_{s} + ℓπ_{s} represents the maximum sender’s rising edge that is not exceeded by t.) We define

t_{s}^{+}(V, t_{s}, t, π_{s}) = t_{s} + ℓπ_{s}

and

lst^{+}(V, t_{s}, t, π_{s}) = (v_{ℓ+1} … v_{n}).

Now we may define V′ = warp(V, t_{s}, t_{r}, π_{s}, π_{r}): If t_{r} + π_{r} > t_{s} + nπ_{s}, then V′ = NIL; otherwise,

V′ = cons(sig, warp(lst^{+}, t_{s}^{+}, t_{r} + π_{r}, π_{s}, π_{r})),

where sig = sig(V, t_{s}, t_{r}+π_{r}, π_{s}), lst^{+} = lst^{+}(V, t_{s}, t_{r}+π_{r}, π_{s}), and t_{s}^{+} = t_{s}^{+}(V, t_{s}, t_{r}+ π_{r}, π_{s}).

Lemma 4.2 Let w be a quasi-smooth n-cycle waveform based at t_{s} with value list V and period π_{s}. Let π_{r} > 0 and t_{s} ≤ t_{r} < t_{s} + π_{s}. Let V′ = warp(V, t_{s}, t_{r}, π_{s}, π_{r}) and let n′ be the length of V′. Then w is a quasi-smooth n′-cycle waveform based at t_{r} with value list V′ and period π_{r}.

Proof: We may assume t_{r} + π_{r} ≤ t_{s} + nπ_{s}, for otherwise, n′ = 0. Let V = (v_{1} … v_{n}) and let sig, lst^{+}, and t_{s}^{+} be defined as in the definition of warp. By induction, we may further assume that w is a quasi-smooth (n′ − 1)-cycle waveform based at t_{r} + π_{r} with value list cdr(V′) = warp(lst^{+}, t_{s}^{+}, t_{r} + π_{r}, π_{s}, π_{r}) and period π_{r}. We need only show that either car(V′) = sig = Q, or ŵ has the constant value sig on the cycle [t_{r}, t_{r} + π_{r}).

Suppose sig ≠ Q. Choose k so that t_{s} +(k −1)π_{s} < t_{r} +π_{r} ≤ t_{s} +kπ_{s}. According to the definition of sig, sig = v_{1} = v_{2} = … = v_{k}, and hence, ŵ(t) = sig for all t ∈ [t_{s}, t_{s} + kπ_{s}) ⊇ [t_{r}, t_{r} + π_{r}). □

4.3 Eliminating Metastability

Lemmas 4.1 and 4.2 together provide a representation of a registered output waveform from the sender as a quasi-smooth waveform with respect to the receiver’s clock. In order to achieve communication, we shall design a clocked state-holding device, called a d-latch, that converts a quasi-smooth input to a stable output. In our asynchronous circuit, this device will share the receiver’s clock, and its output will be connected to the receiver’s input.

The d-latch will consist of an inverter and three nand gates. Its functionality will depend on the relative delays of these components. Thus, along with our standard gates not1 and nand2, both of which have delay 2000, we shall require the following faster nand gate, fnand2:

(BEHAV (A B) ((NAND2 A B)) (1000) (INERTIAL))

We define dlatch to be the following module, which is diagrammed in Fig. 5:

(STRUCT (CLK D) (S2)
  (not1 nand2 nand2 fnand2)
  ((CLK) (CLK D) (S1 S3) (S0 S2))
  ((S0) (S1) (S2) (S3)))

Unlike all other circuits that we have encountered, the specified behavior of dlatch will also depend on the unique character of inertial delay. In particular, we shall need the following result:

Lemma 4.3 Let M be a behavioral module with nth(j, O(M)) = s, nth(j, D(M)) = d, and nth(j, P (M)) = INERTIAL. Let p be an input packet for M, let v be the combinational value of s w.r.t. p̂(t_{0}), and let w = nth(j, sim(M, p, t_{0}).

(a) If ŵ(t_{0}) = v, then w = hist(w, t_{0});

(a) If ŵ(t_{0}) ≠ v, then w = cons((v, t_{1}), hist(w, t_{0})), where t_{0} < t_{1} ≤ t_{0} + d.

Proof: By Lemma 2.10 and the definition of exec, w = inertial(w, v, t_{0}, t_{0} + d). The lemma follows from the definition of inertial. □

The behavioral specification of dlatch is an instance of the following, with d_{0} = d_{1} = d_{2} = 2000 and d_{3} = 1000.

Lemma 4.4 Let G_{0} be the inverter

                      (BEHAV (A) (NOT1 A) (d_{0}) (INERTIAL))

and for i = 1, 2, 3, let G_{i} be the nand gate

                    (BEHAV (A B) (NAND2 A B) (d_{i}) (INERTIAL)),

where d_{1} ≤ d_{0} and d_{0} + d_{3} < d_{1} + d_{2}. Let D = d_{0} + d_{1} + d_{2} + d_{3}. Let L be the module

                      (STRUCT (CLK) (D)

(G_{0} G_{1} G_{2} G_{3})

                        ((CLK) (CLK D) (S1 S3) (S2 S0))
                        ((S0) (S1) (S2) (S3))).

Let p = (w_{CLK} w_{D}) be an input packet for L, and assume that

ŵ_{CLK}(t) = \{ \begin{matrix}T for all t ∈ [t_{+}, t_{−}) \\ F for all t ∈ [t_{−}, t_{f}), \end{matrix}

where t_{−} > t_{+} + D and t_{f} > t_{−} + D. Let ((w_{0}) (w_{1}) (w_{2}) (w_{3})) = sim(L, p, t_{f}). Then ŵ_{2} has a constant value v on [t_{−} + D, t_{f}). If ŵ_{D} has a constant value u on [t_{+}, t_{f}), then u = v.

Proof: For each t ∈ N, let B_{t} = ((w_{0,t}) (w_{1,t}) (w_{2,t}) (w_{3,t})) = sim(L, p, t). Then for i = 0, …, 3, w_{i} = w_{i,t_{f}}. Let t_{0} = t_{−} + d_{0}. For each t ≥ t_{0}, the following results may be derived from Lemmas 3.1 and 2.9:

(a) ŵ_{0,t} has the constant value F on [t_{+} + d_{0}, t_{0});

(b) ŵ_{3,t} has the constant value T on [t_{+} + d_{0} + d_{3}, t_{0} + d_{3});

(c) ŵ_{0,t} has the constant value T on [t_{0}, t_{f} + d_{0});

(d) ŵ_{1,t} has the constant value T on [t_{−} + d_{1}, t_{f} + d_{1}). In particular, for each t ≥ t_{0}, ŵ_{0,t} and ŵ_{1,t} are both constant on [t_{0}, t_{f}).

By Lemma 2.9, (w_{2,t}) = sim(G_{2}, (w_{1,t} w_{3,t}), t) and (w_{3,t}) = sim(G_{3}, (w_{0,t} w_{2,t}), t). We shall apply Lemma 4.3 to both G_{2} and G_{3}.

We shall show that for some t_{1} ∈ [t_{0}, t_{−} + D) and some v ∈ B, ŵ_{2,t_{1}}(t_{1}) = v and ŵ_{3,t_{1}}(t_{1}) = not1(v). Let w_{2,t_{0}}(t_{0}) = v_{2} and w_{3,t_{0}}(t_{0}) = v_{3}. We consider the following cases:

Case 1: v_{3} = not1(v_{2}). In this case, we take t_{1} = t_{0} and v = v_{2}.

Case 2: v_{3} = v_{2}. By Lemma 4.3(b), w_{2,t_{0}} = cons((not1(v_{2}), t_{2}), hist(w_{2,t_{0}}, t_{0})), where t_{0} < t_{2} ≤ t_{0} + d_{2}, and w_{3,t_{0}} = cons((not1(v_{2}), t_{t}), hist(w_{3,t_{0}}, t_{0})), where t_{0} < t_{3} ≤ t_{0} + d_{3}.

Subcase 2a: t_{3} < t_{2}. Here, t_{next}(t_{0}, p, B_{t_{0}}, L) = t_{3}. By Lemma 2.7,ŵ_{2,t_{3}}(t_{3}) = ŵ_{2,t_{0}}(t_{3}) = v_{2} and ŵ_{3,t_{3}}(t_{3}) = ŵ_{3,t_{0}}(t_{3}) = not1(v_{2}). Thus, we have t_{1} = t_{3} and v = v_{2}.

Subcase 2b: t_{2} < t_{3}. In this case, t_{next}(t_{0}, p, B_{t_{0}}, L) = t_{3}, and we have ŵ_{2,t_{2}}(t_{2}) = ŵ_{2,t_{0}}(t_{2}) = not1(v_{2}) and ŵ_{3,t_{2}}(t_{2}) = ŵ_{3,t_{0}}(t_{2}) = v_{2}. In this case, t_{1} = t_{2} and v = not1(v_{2}).

Subcase 2c: t_{2} = t_{3}. We have ŵ_{2,t_{2}}(t_{2}) = ŵ_{3,t_{2}}(t_{2}) = not1(v_{2}). By Lemma 4.3(b), w_{2,t_{2}} = cons((v_{2}, t_{2} + d_{2}), w_{2,t_{0}}), and w_{3,t_{2}} = cons((v_{2}, t_{2} + d_{3}), w_{3,t_{0}}). It follows from our hypotheses that d_{3} < d_{2}. Hence, ŵ_{2,t_{2}+d_{3}}(t_{2} + d_{3}) = not1(v_{2}) and ŵ_{3,t_{2}+d_{3}}(t_{2} + d_{3}) = v_{2}. Thus, t_{1} = t_{2} + d_{3} and v = not1(v_{2}).

Now, by Lemma 4.3(a), ŵ_{2,t_{1}} = hist(ŵ_{2,t_{1}}, t_{1}) and ŵ_{3,t_{1}} = hist(ŵ_{3,t_{1}}, t_{1}). Hence, t_{next}(t_{1}, p, B_{t_{1}}, L) ≥ t_{f}. It follows that for any t′ ∈ [t_{1}, t_{f}), B_{t′} = B_{t_{1}}, and in particular, w_{2,t_{f}} (t′) = w_{2,t′}(t′) = w_{2,t_{1}}(t′) = v. Thus, w_{2,t_{f}} has the constant value v on [t_{1}, t_{f}) ⊇ [t_{−} + D, t_{f}).

Figure 5: (a) dlatch (b) bpm

Finally, suppose that ŵ_{D} has a constant value u on [t_{+}, t_{f}). Then ŵ_{1}(t) = not1(u) for t ∈ [t_{+} + d_{1}, t_{−} + d_{1}). Since ŵ_{3}(t) = T on [t_{+} + d_{0} + d_{3}, t_{0} + d_{3}), the combinational value corresponding to S2 is u on the intersection of these intervals, [max(t_{+} + d_{1}, t_{+} + d_{0} + d_{3}), min(t_{−} + d_{1}, t_{0} + d_{3})). Thus, by Lemma 3.1, ŵ_{2}(t) = u for t ∈ [max(t_{+} + d_{1} + d_{2}, t_{+} + d_{0} + d_{3} + d_{2}), min(t_{−} + d_{1} + d_{2}, t_{0} + d_{3} + d_{2})). In particular, ŵ_{2}(t) = u for t ∈ [t_{0}, t_{0} + d_{3} + d_{2}). Thus, v_{2} = u. Moreover, Subcases 2b and 2c, in which ŵ assumes the value not1(v_{2}) at some point in this interval, are eliminated. In the remaining cases, v = v_{2} = u. □

In order to avail ourselves of the results of [4], we must restate Lemma 4.4 in terms of Moore’s function det. If V is a generalized bit vector and oracle is a bit vector, then det(V, oracle) is the bit vector V′, defined as follows:

(1) If V = NIL, then V′ = NIL; otherwise:

(2) If car(V) ∈ B, then V′ = cons(car(V), det(cdr(V), oracle)); otherwise:

(3) If oracle = NIL, then V′ = cons(T , det(cdr(V), oracle)); otherwise:

(4) V′ = cons(car(oracle), det(cdr(V), cdr(oracle))).

Lemma 4.5 Let p = (w_{CLK} w_{D}) be an input packet for dlatch, where w_{CLK} is an n-cycle pulse based at t_{0} with high h > 7000, low ℓ > 7000, and period π = h+ℓ, and w_{D} is a quasi-smooth n-cycle waveform based at t_{0} with value list V and period π. Let ((w_{0}) (w_{1}) (w_{2}) (w_{3})) = sim(dlatch, p, t_{f}), where t_{f} ≥ t_{0} + nπ. Then for some bit vector oracle, w_{2} is a stable n-cycle waveform based at t_{0} with setup ℓ − 7000, value list det(V, oracle), and period π.

Proof: We induct on n. For n = 0, the statement is vacuous. For n > 0, we may assume that w_{2} is a stable (n − 1)-cycle waveform based at t_{0} + π with setup ℓ − 7000, value list det(cdr(V), oracle′), and period π. By Lemma 4.4, ŵ_{2} has a constant value v on [t_{0} + h + 7000, t_{0} + π) = [t_{0} + π − (ℓ − 7000), t_{0} + π), and if car(V) ≠ Q, then car(V) = v. If car(V) = Q, then let oracle = cons(v, oracle′); otherwise, let oracle = oracle′. In either case, w_{2} is a stable n-cycle waveform based at t_{0} with setup ℓ − 7000, value list det(V, oracle), and period π. □

4.4 The Main Theorem

In Section 5, we shall apply the results of this section to a circuit bpm, consisting of two sequential submodules, sndr and rcvr, and a dlatch: According to the definitions that we shall present later, sndr has 9 data inputs and one registered output, SOUT, while rcvr has one data input, SIN, and 9 outputs. The circuit bpm, which is diagrammed in Fig. 5, is defined as follows:

  (STRUCT
    (CLKS RSTS CLKR RSTR SEND I0 I1 I2 I3 I4 I5 I6 I7)
    (DONE O0 O1 O2 O3 O4 O5 O6 O7)
    (sndr dlatch rcvr)
    ((CLKS RSTS SEND I0 I1 I2 I3 I4 I5 I6 I7) (CLKR SOUT) (CLKR RSTS LOUT))
    ((SOUT) (LOUT) (DONE O0 O1 O2 O3 O4 O5 O6 O7)))

The following theorem summarizes our results on asynchrony, as they pertain to the module bpm. The theorem refers to Moore’s function asynch, which is defined as follows: Let V and oracle be bit vectors and let t_{s}, t_{r}, π_{s}, π_{r} ∈ N such that π_{s} > 0, π_{r} > 0, and t_{s} ≤ t_{r} < t_{s} + π_{s}. Then

asynch(V, t_{s}, t_{r}, π_{s}, π_{r}, oracle) = det(warp(smooth(T , V), t_{s}, t_{r}, π_{s}, π_{r}), oracle).

Theorem 4.1 Let p = (w_{CLKS} w_{RSTS} w_{CLKR} w_{RSTR} w_{SEND} w_{0} … w_{7}) be an input packet for bpm, where

(a) (w_{CLKS} w_{RSTS} w_{SEND} w_{0} … w_{7}) is an admissible n_{s}-cycle input packet for sndr based at b_{s} with value matrix V and period π_{s};

(b) w_{CLKR} is an admissible (n_{r} + 2)-cycle pulse for rcvr based at b_{r} with high h > 7000, low ℓ > 7000 + setup(SIN, rcvr), and period π_{r} = h + ℓ;

(c) w_{RSTR} is an admissible (n_{r} + 1)-cycle reset waveform for rcvr based at b_{r} with period π_{r}. Let t_{r} = b_{r} + π_{r}. Assume that b_{s} + 2π_{s} ≤ t_{r} ≤ b_{s} + (n_{s} + 2)π_{s} ≤ t_{r} + n_{r}π_{r}. Choose j so that b_{s} + jπ_{s} ≤ t_{r} < b_{s} + (j + 1)π_{s} and let t_{s} = b_{s} + jπ_{s}. Assume sv(j − 2, SOUT, V, sndr) = T .

Let U = (sv(j − 1, SOUT, V, sndr) … sv(n_{s}, SOUT, V, sndr)). Let w_{LOUT} be the waveform for LOUT determined by sim(bpm, p, t_{f}), where t_{f} ≥ t_{r} + n_{r}π_{r}. Then for some bit vector oracle, (w_{CLKR} w_{RSTR} w_{LOUT}) is an admissible input packet for rcvr based at b_{r} with value matrix (asynch(U, t_{s}, t_{r}, π_{s}, π_{r}, oracle)) and period π_{r}.

Proof: Let w_{SOUT} be the waveform for SOUT determined by sim(bpm, p, t_{f}). According to Lemma 4.1, w_{SOUT} is a quasi-smooth waveform based at t_{s} with value list smooth(T , U) and period π_{s}. It follows from Lemma 4.2 that w_{SOUT} is also a quasi-smooth waveform based at t_{r} with value list warp(smooth(T , U), t_{s}, t_{r}, π_{s}, π_{r}) and period π_{r}. Finally, by Lemma 4.5, w_{LOUT} is a stable waveform based at t_{r} with setup ℓ − 7000 > setup(SIN, rcvr), value list

det(warp(smooth(T , U), t_{s}, t_{r}, π_{s}, π_{r}), oracle) = asynch(U, t_{s}, t_{r}, π_{s}, π_{r}, oracle)),

for some oracle, and period π_{r}. □

5 Biphase Mark

Moore’s formulation [4] of the biphase mark protocol is based on two functions, send and recv, which represent the computations performed by the sender and the receiver, respectively. After presenting the definitions of these functions, we shall implement them in the design of the sequential modules sndr and rcvr. Then, using a theorem of Moore in combination with results of Section 4, we shall show that the circuit bpm achieves communication between these modules.

5.1 Sending

The function send returns a bit vector that represents an encoding of a given input bit vector msg. Each bit of msg is encoded as a bit vector called a cell, computed as the value of cell(x, n, k, b), where b is the bit of msg to be encoded, x is the final bit of the preceding cell, and n and k are parameters of the protocol. A cell consists of two subcells, each of which is a uniform bit vector: a mark subcell of length n, followed by a code subcell of length k. The mark subcell is intended as a signal to the receiver that a new cell has been entered: each of its bits is not1(x). The code subcell is the region in which the receiver is expected to look for information from which it will derive the value b of the encoded bit: if b = T , then each bit of this subcell is x; if b = F, each bit is not1(x).

The definition of cell requires three auxiliary functions. First, the subcells are constructed by the function listn: for any n ∈ N and any x, listn(n, x) is the uniform vector (x … x) of length n. Next, the two subcells are combined by the function app: for any two lists L = (a_{1} … a_{n}) and M = (b_{1} … b_{m}), app(L, M) = (a_{1} … a_{n}b_{1} … b_{m}). Finally, the bit occurring in the code subcell is determined by the Boolean function equal, where equal(x, y) = T iff x = y, i.e., equal(x, y) = not1(xor2(x, y)).

Now, we may define

cell(x, n, k, b) = app(listn(n, not1(x)), listn(k, equal(x, b))),

and cells(x, n, k, msg) is defined as

(1) NIL, if msg = NIL;

(2) app(cell(x, n, k, car(msg)), cells(equal(x, car(msg)), n, k, cdr(msg))), if msg ≠

     NIL.

The protocol includes the convention that the value T is transmitted until the encoded message is sent. Thus, the encoded bit vector constructed by send includes “pads” consisting arbitrarily many copies of T on both sides of the cells. The arguments of send include the lengths p_{1} and p_{2} of these pads:

send(msg, p_{1}, n, k, p_{2}) = app(listn(p_{1}, T ), app(cells(T , n, k, msg), listn(p_{2}, T ))).

5.2 Receiving

Next, we define recv(i, x, j, L)^{1}, which may be shown, under suitable assumptions, to be the inverse of send. This function recovers a bit of the encoded message from each cell by first detecting the beginning of the mark subcell, and then reading and decoding a bit at a predetermined location within the cell, which has been calculated to lie within the code subcell. Its arguments are interpreted as follows: i is the number of bits of the original message yet to be recovered, x is the last bit to have been read (from the preceding cell), j is the location within the cell of the bit to be read, and L is the remaining input stream.

The beginning of a new cell is detected by the function scan(x, L), which successively removes bits from the beginning of the list L until a value different from x is found. The recursive definition follows:

(1) If L = NIL, then scan(x, L) = NIL; otherwise:

(2) If car(L) = x, then scan(x, L) = scan(x, cdr(L)); otherwise:

1For technical reasons, we shall slightly modify Moore’s original definition of this function. Our modification does not affect the validity of any of his results.

(3) scan(x, L) = L.

We shall require one other auxiliary function: If n ∈ N and L is a list, then cdrn(n, L) is defined to be

(1) L, if n = 0;

(2) cdrn(n − 1, cdr(L)), if n > 0.

Finally, we define recv(i, x, j, L) to be the bit vector msg, where

(1) If i = 0, then msg = NIL; otherwise:

(2) Let S = scan(x, L). If length(S) ≤ k, then msg = NIL; otherwise:

(3) Let b = nth(k + 1, S) and L′ = cdrn(k + 1, S). If b = x, then msg = cons(T , recv(i − 1, b, j, L′); otherwise:

(4) msg = cons(F, recv(i − 1, b, j, L′).

5.3 Moore’s Theorem

Moore has proved a statement of correctness of the protocol for certain values of the parameters. The lengths of the mark and code subcells generated by send are taken to be n = 5 and k = 13, respectively. The index of the bit read by recv following the detection of an edge is j = 10, i.e., the eleventh bit after the edge is sampled. The theorem also depends on an assumption concerning the proximity of the two clock periods:

Theorem 5.1 (Moore) Let π_{s} > 0, π_{r} > 0, and 17π_{r} ≤ 18π_{s} ≤ 19π_{r}. Let t_{s} ≤ t_{r} < t_{s} + π_{s}. Let msg be a bit vector of length k. Then for any bit vector oracle and any numbers p_{1} and p_{2},

recv(k, T , 10, asynch(send(msg, p_{1}, 5, 13, p_{2}), t_{s}, t_{r}, π_{s}, π_{r}, oracle)) = msg.

We shall apply Moore’s theorem to the specification of the circuit bpm. The sequential submodules sndr and rcvr of bpm remain to be defined. As we present the definitions of the these modules and their components, which are diagrammed in Figs. 6–10, we shall derive characterizations of their behavior that are analogous to Propositions 3.1 and 3.2. The proofs of these results are based on straightforward calculations and have all been mechanically checked. Therefore, the details of these proofs are omitted here.

5.4 Basic Components

The message that is transmitted from sndr to rcvr will consist of eight bits. It is stored (by both sndr and rcvr) in a shift register, shift8, which is constructed from eight copies of the following 3-port cell, port3:

(STRUCT
  (CLK RST SHIFT SIN LOAD DIN)
  (Q)
  (edff nand2 nand2 or2 nand2)
  ((CLK RST S3 S4) (DIN LOAD) (SIN SHIFT) (LOAD SHIFT) (S1 S2))
  ((Q QN) (S1) (S2) (S3) (S4)))

The behavior of port3 may be derived easily from that of edff (Proposition 3.1):

Proposition 5.1 Let Σ and V = (shift sin load din) be a state and a data vector for port3. Assume that shift and load are not both T . Then

nv(Q, V, Σ, port3) = Σ;

next(V, Σ, port3) = \{ \begin{matrix}sin & if shift = T and load = F \\ din & if shift = F and load = T \\ Σ & if shift = F and load = F. \end{matrix}

The register shift8 is defined as follows:

(STRUCT
  (CLK RST LOAD SHIFT SIN D0 D1 D2 D3 D4 D5 D6 D7)
  (Q0 Q1 Q2 Q3 Q4 Q5 Q6 Q7)
  (port3 port3 port3 port3 port3 port3 port3 port3)
  ((CLK RST SHIFT SIN LOAD D0)
   (CLK RST SHIFT Q0 LOAD D1)
   (CLK RST SHIFT Q1 LOAD D2)
   (CLK RST SHIFT Q2 LOAD D3)
   (CLK RST SHIFT Q3 LOAD D4)
   (CLK RST SHIFT Q4 LOAD D5)
   (CLK RST SHIFT Q5 LOAD D6)
   (CLK RST SHIFT Q6 LOAD D7))
  ((Q0) (Q1) (Q2) (Q3) (Q4) (Q5) (Q6) (Q7)))

40 Figure 6: (b) shift8 Proposition 5.2 Let Σ = (σ_{0} … σ_{7}) and V = (load shift sin d_{0} … d_{7}) be a state and a data vector for shift8. Assume that shift and load are not both T . Then

nv(Qi, V, Σ, shift8) = σ_{i}, i = 0, …, 7;

next(V, Σ, shift8) = \{ \begin{matrix}(sin σ_{0} … σ_{6}) & if shift = T and load = F \\ (d_{0} … d_{7}) & if shift = F and load = T \\ Σ & if shift = F and load = F. \end{matrix}

In order to describe the shifting operation that is performed by shift8, we define, for any b ∈ B and any bit vector V,

shift(b, V) = \{ \begin{matrix}NIL & if V = NIL \\ cons(b, shift(car(V), cdr(V))) & if V ≠ NIL. \end{matrix}

Thus, shift(sin, (σ_{0} … σ_{7})) = (sin σ_{0} … σ_{6}).

In addition to dff and edff, we shall require two other versions of the flip-flop. The first of these, cdff, has an input CLR, which may be used to override the other data input D and reinitialize the state:

(STRUCT
  (CLK RST CLR D)
  (Q QN)
  (dff not1 nand2)
  ((CLK RST DCN) (CLR) (D CN))
  ((Q QN) (CN) (DCN)))

Proposition 5.3 Let Σ and V = (clr d) be a state and a data vector for cdff. Then

nv(Q, V, Σ, cdff) = Σ and nv(QN, V, Σ, cdff) = not1(Σ);

next(V, Σ, cdff) = \{ \begin{matrix}F & if clr = T \\ d & if clr = F. \end{matrix}

The second, cedff, is a combination of edff and cdff:

(STRUCT
  (CLK RST CLR EN D)
  (Q QN)
  (dff not1 not1 nand3 nand3 nand2)
  ((CLK RST S5) (EN) (CLR) (Q S1 S2) (D S2 EN) (S3 S4))
  ((Q QN) (S1) (S2) (S3) (S4) (S5)))

Figure 7:  (a) cdff  (b) cedff

Proposition 5.4 Let Σ and V = (clr en d) be a state and a data vector for cedff. Then

nv(Q, V, Σ, cedff) = Σ and nv(QN, V, Σ, cedff) = not1(Σ);

next(V, Σ, cedff) = \{ \begin{matrix}F & if clr = T \\ d & if clr = F and en = T \\ Σ & if clr = F and en = F. \end{matrix}

Using cedff, we construct the following 5-bit counter, count5:

(STRUCT
  (CLK RST CLR EN)
  (Q0 Q1 Q2 Q3 Q4)
  (cedff cedff cedff cedff cedff
   and2 and2 and2 xor2 xor2 xor2 xor2)
  ((CLK RST CLR EN QN0)
   (CLK RST CLR EN X1)
   (CLK RST CLR EN X2)
   (CLK RST CLR EN X3)
   (CLK RST CLR EN X4)
   (Q0 Q1) (A1 Q2) (A2 Q3) (Q0 Q1) (Q2 A1) (Q3 A2) (Q4 A3))
  ((Q0 QN0) (Q1 QN1) (Q2 QN2) (Q3 QN3) (Q4 QN4)
   (A1) (A2) (A3) (X1) (X2) (X3) (X4)))

Proposition 5.5 Let Σ = (σ_{0} … σ_{4}) and V = (clr en) be a state and a data vector for count5. Then

nv(Qi, V, Σ, count5) = σ_{i}, i = 0, …, 4;

Figure 8:  (a) count5  (b) comp5

next(V, Σ, count5) = \{ \begin{matrix}listn(5, F) & if clr = T \\ inc(cnt) & if clr = F and en = T \\ Σ & if clr = F and en = F. \end{matrix}

For convenience in representing states of both count3 and count5, we define, for k ∈ N and n ∈ N,

bv_{k}(n) = \{ \begin{matrix}listn(k, F) & if n = 0 \\ inc(bv_{k}(n − 1)) & if n > 0. \end{matrix}

Thus, bv_{k}(n) is the k-bit vector that represents the number n.

We shall also require a combinational module, the following 5-bit comparator

comp5:
(STRUCT
  (C0 B0 C1 B1 C2 B2 C3 B3 C4 B4)
  (MATCH)
  (xor2 xor2 xor2 xor2 xor2 nor5)
  ((C0 B0) (C1 B1) (C2 B2) (C3 B3) (C4 B4) (S1 S2 S3 S4 S5))
  ((S1) (S2) (S3) (S4) (S5) (MATCH)))

This module simply determines whether two given 5-bit vectors are equal, i.e.,

cv(MATCH, (c_{0} b_{0} c_{1} b_{1} … c_{4} b_{4}), comp5) = \{ \begin{matrix}T & if (c_{0} … c_{4}) = (b_{0} … b_{4}) \\ F & if not. \end{matrix}

5.5 The Sender

The action of sndr is controlled by the submodule scount, which is defined as follows:

(STRUCT
  (CLK RST STOP BIT)
  (MARK CODE)
  (cdff count5 or2 or2 t0 f0 comp5 comp5)
  ((CLK RST STOP S1) (CLK RST S2 Q) (BIT Q) (STOP BIT) () ()
   (F Q0 F Q1 T Q2 F Q3 F Q4) (T Q0 F Q1 F Q2 F Q3 T Q4))
  ((Q QN) (Q0 Q1 Q2 Q3 Q4) (S1) (S2) (T) (F) (MARK) (CODE)))

A state of scount is a list (on cnt) of two components, corresponding to the two sequential submodules, cdff and count5. As long as both data inputs are F, the value of on remains constant. While on = T , cnt is incremented repreatedly; while on = F, cnt remains unchanged. If either input is T , then on is set accordingly and cnt is reset to bv_{5}(0). The output values are both determined by cnt:

Proposition 5.6 Let Σ = (on cnt) and V = (stop bit) be a state and a data vector for scount. Then

nv(MARK, V, Σ, scount) = \{ \begin{matrix}T & if cnt = bv_{5}(4) \\ F & if cnt ≠ bv_{5}(4); \end{matrix}

nv(CODE, V, Σ, scount) = \{ \begin{matrix}T & if cnt = bv_{5}(17) \\ F & if cnt ≠ bv_{5}(17); \end{matrix}

next(V, Σ, scount) = \{ \begin{matrix}(F bv_{5}(0)) & if stop = T \\ (T bv_{5}(0)) & if stop = F and bit = T \\ (T inc(cnt)) & if stop = bit = F and on = T \\ (F cnt) & if stop = bit = F and on = F. \end{matrix}

The definition of sndr is as follows:

Figure 9:  (a) scount  (b) sndr

(STRUCT
  (CLK RST SEND I0 I1 I2 I3 I4 I5 I6 I7)
  (SOUT)
  (scount shift8 count3 edff or2 and2 and4 or3 f0)
  ((CLK RST A4 O2) (CLK RST SEND CODE F I0 I1 I2 I3 I4 I5 I6 I7)
   (CLK RST MARK) (CLK RST O3 SOUT) (CODE SEND) (Q7 MARK)
   (MARK C0 C1 C2) (A2 SEND CODE) ())
  ((MARK CODE) (Q0 Q1 Q2 Q3 Q4 Q5 Q6 Q7) (C0 C1 C2)
   (Q SOUT) (O2) (A2) (A4) (O3) (F)))

This module has two modes of operation. In one mode, it waits dormantly for the SEND input to become T . When this occurs, the current values of the other eight data inputs are loaded into the shift register, the state of the flip-flop edff (which determines the output value) changes, and the controller scount begins counting. This mode is described by the following:

Proposition 5.7 Let V = (s d_{0} … d_{7}) be a data vector for sndr, and let Σ = (σ_{1} σ_{2} σ_{3} σ_{4}) be a state of sndr, where σ_{1} = (on cnt). Assume that on = F and cnt = bv_{5}(0). Let Σ′ = next(V, Σ, sndr).

(a) If s = T , then Σ′ = ((T bv_{5}(0)) (d_{0} … d_{7}) σ_{3} not1(σ_{4}));

(b) If s = F, then Σ′ = Σ.

In the other mode of operation, the register contents are encoded and transmitted. Each register bit is encoded as a cell consisting of a 5-bit mark subcell and a 13-bit code subcell, as measured by scount. The number of cells that have been transmitted is recorded as the contents of count3. At the end of each mark subcell, this number is incremented. At the end of each code subcell, the scount counter is reset and the register contents are shifted:

Proposition 5.8 Let V = (s d_{0} … d_{7}) be a data vector for sndr, and let Σ = (σ_{1} σ_{2} σ_{3} σ_{4}) be a state of sndr, where σ_{1} = (on cnt) and σ_{2} = (q_{0} … q_{7}). Assume that s = F and on = T . Let Σ′ = next(V, Σ, sndr).

(a) If cnt = bv_{5}(4) and σ_{3} = bv_{3}(7), then Σ′ = ((F bv_{5}(0))σ_{2} inc(σ_{3})xor2(q_{7}, σ_{4}));

(b) If cnt = bv_{5}(4) and σ_{3} ≠ bv_{3}(7), then Σ′ = ((T bv_{5}(5))σ_{2} inc(σ_{3})xor2(q_{7}, σ_{4}));

(c) If cnt = bv_{5}(17), then Σ′ = ((T bv_{5}(0)) shift(F, σ_{2}) σ_{3} not1(σ_{4}));

(d) If cnt ≠ bv_{5}(4) and cnt ≠ bv_{5}(17), then Σ′ = ((T inc(cnt)) σ_{2} σ_{3} σ_{4}).

Our main theorem on sndr is the following specification:

Proposition 5.9 Let V = (V_{SEND} V_{I0} … V_{I7}) be a list of bit vectors, each of length n ≥ 144. Let m = n − 144. Assume that for j = 1, …, n,

nth(j, V_{SEND}) = \{ \begin{matrix}T & if j = m \\ F & if j ≠ m. \end{matrix}

For i = 0, …, 7, let d_{i} = nth(m, V_{Ii}). For j = 1, …, n, let sv_{j} = sv(j, SOUT, V, sndr). Then (sv_{1} … sv_{n}) = send((d_{7} … d_{0}), m, 5, 13, 0).

Proof: Let Σ_{j} = state(j, V, sndr), j = 0, …, n. By Proposition 5.7(b), for j = 0, …, m,

Σ_{j} = Σ_{0}(sndr) = ((F bv_{5}(0)) listn(8, F) bv_{3}(0) F)

and hence (sv_{1} … sv_{m}) = listn(m, T ). It remains to show that (sv_{m+1} … sv_{n}) = cells(T , 5, 13, (d_{7} … d_{0})).

By Proposition 5.7(a),

Σ_{m+1} = ((T bv_{5}(0)) (d_{0} … d_{7}) bv_{3}(0) T ).

We shall show that for all k, 0 ≤ k ≤ 7, if

Σ_{m+1+18k} = ((T bv_{5}(0)) app(listn(k, F), (d_{0} … d_{7−k})) bv_{3}(k) x),

then

(sv_{m+1+18k} … sv_{n}) = cells(x, 5, 13, (d_{7−k} … d_{0})).

The proposition will follow from this result upon setting k = 0.

The proof is by induction on 7 − k. In the base case, k = 7, our assumption is that

Σ_{m+1+18k} = Σ_{m+127} = ((T bv_{5}(0)) app(listn(7, F), (d_{0})) bv_{3}(7) x).

By Proposition 5.8(d), for ℓ = 0, …, 4,

Σ_{m+127+ℓ} = ((T bv_{5}(ℓ)) app(listn(7, F), (d_{0})) bv_{3}(7) x),

and by Proposition 5.8(a),

Σ_{m+127+5} = Σ_{m+132} = ((F bv_{5}(0)) app(listn(7, F), (d_{0})) bv_{3}(0) xor2(d_{0}, x)). By Proposition 5.7(b), Σ_{m+132+ℓ} = Σ_{m+132} for ℓ = 0, …, 12. It follows that

(sv_{m+127} … sv_{n}) = app(listn(5, not1(x)), listn(13, equal(d_{0}, x)))
= cell(x, 5, 13, d_{0})
= cells(x, 5, 13, (d_{0})).

In the inductive case, k < 7, we again have, for ℓ = 0, …, 4,

Σ_{m+1+18k+ℓ} = ((T bv_{5}(ℓ)) app(listn(k, F), (d_{0} … d_{7−k})) bv_{3}(k) x) by Proposition 5.8(d). By Proposition 5.8(b) and (d), for ℓ = 5, …, 17, Σ_{m+1+18k+ℓ} = ((T bv_{5}(ℓ)) app(listn(k, F), (d_{0} … d_{7−k})) bv_{3}(k + 1) xor2(d_{7−k}, x)). Thus, (sv_{m+1+18k} … sv_{m+1+18k+17}) is

app(listn(5, not1(x)), listn(13, equal(d_{7−k}, x))) = cell(x, 5, 13, d_{7−k}). By Proposition 5.8(c), Σ_{m+1+18(k+1)} is ((T bv_{5}(0)) app(listn(k + 1, F), (d_{0} … d_{7−(k+1)})) bv_{3}(k + 1) equal(d_{7−k}, x)).

It follows from our inductive hypothesis that

(sv_{m+1+18(k+1)} … sv_{n}) = cells(equal(d_{7−k}, x), 5, 13, (d_{7−(k+1)} … d_{0})), and hence (sv_{m+1+18k} … sv_{n}) is

app(cell(x, 5, 13, d_{7−k}), cells(equal(d_{7−k}, x), 5, 13, (d_{7−(k+1)} … d_{0}))

= cells(x, 5, 13, (d_{7−k} … d_{0})). □

5.6 The Receiver

Its action of the receiver is controlled by a submodule, rcount, which is defined as follows:

(STRUCT
  (CLK RST STOP START)
  (BIT)
  (cdff count5 or2 t0 f0 comp5)
  ((CLK RST STOP S1) (CLK RST STOP Q) (START Q)
   () () (T Q0 F Q1 F Q2 T Q3 F Q4))
  ((Q QN) (Q0 Q1 Q2 Q3 Q4) (S1) (T) (F) (BIT)))

The functionality of rcount is similar to that of scount. A state is again a list (on cnt) of two components, corresponding to the two sequential submodules, cdff and count5. As long as both data inputs are F, the value of on remains constant. While on = T , cnt is incremented repreatedly; while on = F, cnt remains unchanged. If STOP is T , then on and cnt are reset to F and bv_{5}(0); otherwise, if START is T , then on is set to T . The output value is determined by comparing cnt with bv_{5}(9):

Proposition 5.10 Let Σ = (on cnt) and V = (stop start) be a state and a data vector for rcount. Then

nv(BIT, V, Σ, rcount) = \{ \begin{matrix}T & if cnt = bv_{5}(9) \\ F & if cnt ≠ bv_{5}(9); \end{matrix}

next(V, Σ, rcount) = \{ \begin{matrix}(F bv_{5}(0)) & if stop = T \\ (T inc(cnt)) & if stop = F and start = on = T \\ (T cnt) & if stop = F and start = T and on = F \\ (T inc(cnt)) & if stop = F and start = F and on = T \\ (T cnt) & if stop = start = on = F. \end{matrix}

The definition of rcvr is as follows:

(STRUCT
  (CLK RST SIN)
  (O0 O1 O2 O3 O4 O5 O6 O7 DONE)
  (rcount edff count3 shift8 dff not1 not1 xor2 and4 f0)
  ((CLK RST BIT N2) (CLK RST BIT N1)
   (CLK RST BIT) (CLK RST F BIT X F F F F F F F F)
   (CLK RST A) (SIN) (X) (SIN Q) (Q0 Q1 Q2 BIT) ())
  ((BIT) (Q QN) (Q0 Q1 Q2) (O0 O1 O2 O3 O4 O5 O6 O7)
   (DONE DONEN) (N1) (N2) (X) (A) (F)))

Figure 10:  (a) rcount  (b) rcvr

Like sndr, rcvr has two modes of operation. In the first mode, it waits for an edge, i.e., a change in input. This is detected by comparing the input with the state of the flip-flop edff, which is the negation of the most recently read value. In this mode, the controller rcount is turned off. When an edge is detected, rcount is turned on and its counter is reset:

Proposition 5.11 Let V = (sin) be a data vector for rcvr, and let Σ = (σ_{1}σ_{2}σ_{3}σ_{4}σ_{5}) be a state of rcvr, where σ_{1} = (on cnt). Assume that on = F, cnt = bv_{5}(0), and σ_{5} = F. Let Σ′ = next(V, Σ, rcvr).

(a) If sin = σ_{2}, then Σ′ = ((T bv_{5}(0)) σ_{2} σ_{3} σ_{4} F);

(b) If sin ≠ σ_{2}, then Σ′ = Σ.

In its second mode, the receiver counts until it reaches the input bit to be sampled. At this point, the appropriate value is shifted into the register shift8, the bit counter count3 is incremented, the current input value is stored in edff, and rcount is turned off. When the eighth bit has been computed, the state of dff is altered to indicate termination:

Proposition 5.12 Let V = (sin) be a data vector for rcvr, and let Σ = (σ_{1}σ_{2}σ_{3}σ_{4}σ_{5}) be a state of rcvr, where σ_{1} = (on cnt). Assume that on = T and σ_{5} = F. Let Σ′ = next(V, Σ, rcvr).

(a) If cnt = bv_{5}(9) and σ_{3} = bv_{3}(7), then

Σ′ = ((F bv_{5}(0)) not1(sin) bv_{3}(0)) shift(xor2(σ_{2}, sin), σ_{4}) T ); (b) If cnt = bv_{5}(9) and σ_{3} ≠ bv_{3}(7), then

Σ′ = ((F bv_{5}(0)) not1(sin) inc(σ_{3}) shift(xor2(σ_{2}, sin), σ_{4}) F);

(c) If cnt ≠ bv_{5}(9), then Σ′ = ((T inc(cnt)) σ_{2} σ_{3} σ_{4} F).

The specification of rcvr is given by the following lemma. For its proof, we require the following definition: If L and M are two bit vectors, then

push(L, M) = \{ \begin{matrix}M & if L = NIL \\ push(cdr(L), shift(car(L), M)) & if L ≠ NIL. \end{matrix}

Thus, if L = (x_{1} … x_{ℓ}) and M = (y_{1} … y_{m}), where ℓ ≤ m, then

push(L, M) = (x_{ℓ} … x_{1} y_{1} … y_{m−ℓ}).

Proposition 5.13 Let V = (V), where V is a bit vector of length n. Assume that length(recv(8, T , 10, V)) = 8. Then for some m, 1 ≤ m ≤ n,

sv(j, DONE, V, rcvr) = \{ \begin{matrix}T & if j = m \\ F & if j < m. \end{matrix}

For i = 1, …, 7, let d_{i} = sv(m, Oi, V, rcvr). Then (d_{7} … d_{0}) = recv(8, T , 10, V).

Proof: Let V = (v_{1} … v_{n}). For j = 0, …, n, let V_{j} = (v_{j+1} … v_{n}) and

Σ_{j} = state(j, V, rcvr) = ((on_{j} cnt_{j}) flg_{j} bits_{j} reg_{j} done_{j}).

We shall prove the following generalization of the desired result:

Suppose that for some j, on_{j} = F, cnt_{j} = bv_{5}(0), done_{i} = F for all i ≤ j, and

length(recv(8 − b, not1(flg_{j}), 10, V_{j})) = 8 − b,

where bits_{j} = bv_{3}(b). Then for some m > j, done_{i} = F for all i < m, done_{m} = T , and

reg_{m} = push(recv(8 − b, not1(flg_{j}), 10, V_{j}), reg_{j}).

The proposition will then follow from the case j = 0.

First note that according to our assumption, recv(8 − b, not1(flg_{j}), 10, V_{j}) ≠ NIL, and hence, scan(not1(flg_{j}), V_{j}) = V_{k} for some k, j ≤ k < n − 10. Thus, v_{i} = not1(flg_{j}) for i = j + 1, …, k, and v_{k+1} = flg_{j}. From the definition of recv, we have recv(8 − b, not1(flg_{j}), 10, V_{j}) = cons(xor2(flg_{j}, v_{k+11}), recv(7 − k, v_{k+11}, 10, V_{k+11})),

and hence,

length(recv(7 − b, v_{k+11}, 10, V_{k+11})) = 7 − b.

By Proposition 5.11, Σ_{i} = Σ_{j} for i = j, …, k, and

Σ_{k+1} = ((T bv_{5}(0)) flg_{j} bits_{j} reg_{j} F).

By Proposition 5.12(c), for i = 0, …, 9,

Σ_{k+1+i} = ((T bv_{5}(i)) flg_{j} bits_{j} reg_{j} F).

The proof is by induction on 7 − b. Consider first the base case, b = 7. By Proposition 5.12(a),

Σ_{k+11} = ((F bv_{5}(0)) not1(v_{k+11}) bv_{3}(0) shift(xor2(flg_{j}, v_{k+11}), reg_{j}) T ).

Here, the result holds for m = k + 11, since

push(recv(8 − b, not1(flg_{j}), 10, V_{j}), reg_{j}) = push((xor2(flg_{j}, v_{k+11})), reg_{j})
= shift(xor2(flg_{j}, v_{k+11}), reg_{j}).

Now suppose that b < 7, and assume that the claim holds with b replaced with b+1. By Proposition 5.12(a),

Σ_{k+11} = ((F bv_{5}(0)) not1(v_{k+11}) bv_{3}(b + 1) shift(xor2(flg_{j}, v_{k+11}), reg_{j}) F).

We may conclude that for some m > k + 11, done_{i} = F for all i < m, done_{m} = T , and

reg_{m} = push(recv(7 − b, v_{k+11}, 10, V_{k+11}), shift(xor2(flg_{j}, v_{k+11}), reg_{j}))
= push(cons(xor2(flg_{j}, v_{k+11}), recv(7 − b, v_{k+11}, 10, V_{k+11})), reg_{j})
= push(recv(8 − b, not1(flg_{j}), 10, V_{j}), reg_{j}). □

5.7 The Main Theorem

Finally, we present our main result concerning the circuit bpm. We assume that the two clock input waveforms are admissible pulses for sndr and rcvr, respectively, with periods that conform to the constraints imposed by Moore’s theorem, and that the other inputs are well-behaved with respect to the clocks, as required by Theorem 3.1. We also assume that the SEND input has the value T on exactly one cycle, during which an 8-bit message is read from the other data inputs. This message is then encoded and transmitted by sndr, and received, decoded, and output by rcvr. As stated in the theorem, the completion of this process is signalled by the output DONE: when its value first becomes T , the other outputs display the decoded message.

Theorem 5.2 Let p_{in} = (w_{CLKS}w_{RSTS}w_{CLKR}w_{RSTR}w_{SEND}w_{0} … w_{7}) be an input packet for bpm, where

(a) (CLKS w_{RSTS} w_{SEND} w_{0} … w_{7}) is an admissible n_{s}-cycle input packet for sndr based at b_{s} with value matrix V_{s} = (V_{SEND} V_{I0} … V_{I7}) and period π_{s};

(b) w_{CLKR} is an admissible (n_{r} + 2)-cycle pulse for rcvr based at b_{r} with high h > 7000, low ℓ > 7000 + setup(SIN, rcvr), and period π_{r} = h + ℓ;

(c) w_{RSTR} is an admissible (n_{r} + 1)-cycle reset waveform for rcvr based at b_{r} with period π_{r}.

Assume 17π_{r} ≤ 18π_{s} ≤ 19π_{r}. Suppose that for some m_{s}, 1 ≤ m_{s} ≤ n_{s} − 144,

nth(j, V_{SEND}) = \{ \begin{matrix}T & if j = m_{s} \\ F & if j ≠ m_{s}, 1 ≤ j ≤ n_{s}; \end{matrix}

For i = 0, …, 7, let d_{i} = nth(m_{s}, V_{Ii}). Let t_{r} = b_{r} + π_{r}. Assume that b_{s} + 2π_{s} ≤ t_{r} ≤ b_{s} + (m_{s} + 2)π_{s} and b_{s} + (n_{s} + 2)π_{s} ≤ t_{r} + n_{r}π_{r}.

Let p_{out} = outp(bpm, sim(bpm, p_{in}, t_{f})), where t_{f} ≥ t_{r} + n_{r}π_{r}. Then p_{out} is a stable n_{r}-cycle packet based at t_{r} + π_{r} with value matrix V_{r} and period π_{r}, for some V_{r} = (V_{DONE} V_{O0} … V_{O7}). For some m_{r}, 1 ≤ m_{r} ≤ n_{r},

nth(j, V_{DONE}) = \{ \begin{matrix}T & if j = m_{r} \\ F & if j ≠ m_{r}, 1 ≤ j ≤ n_{r}, \end{matrix}

and for i = 0, …, 7, nth(m_{r}, V_{Oi}) = d_{i}.

Proof: We may assume, without loss of generality, that n_{s} = m_{s} + 144. For j = 0, …, n_{s}, let sv_{j} = sv(j, SOUT, V_{s}, sndr). By Proposition 5.9,

(sv_{1} … sv_{n_{s}}) = send((d_{7} … d_{0}), m_{s}, 5, 13, 0).

Since sv_{0} = T , we have sv_{j} = T for all j ≤ m_{s}.

Fix j so that b_{s} + jπ_{s} ≤ t_{r} < b_{s} + (j + 1)π_{s} and let t_{s} = b_{s} + jπ_{s}. Then 2 ≤ j ≤ m_{s} + 2, and hence sv_{j−2} = T . Let

S = (sv_{j−1} … sv_{n_{s}}) = send((d_{7} … d_{0}), m_{s} − j + 2, 5, 13, 0)

and let w_{LOUT} be the waveform for LOUT determined by sim(bpm, p, t_{f}). By Theorem 4.1, (w_{CLKR} w_{RSTR} w_{LOUT}) is an admissible input packet for rcvr based at b_{r} with value matrix (A) and period π_{r}, where A = asynch(U, t_{s}, t_{r}, π_{s}, π_{r}, oracle) for some bit vector oracle.

Let V_{r} = (V_{DONE} V_{O0} … V_{O7}), where

V_{DONE} = (sv(1, DONE, (A), rcvr) … sv(n_{r}, DONE, (A), rcvr))

and for i = 0, …, 7,

V_{Oi} = (sv(1, Oi, (A), rcvr) … sv(n_{r}, Oi, (A), rcvr)).

By Theorem 3.1, p_{out} is a stable n_{r}-cycle packet based at b_{r} + π_{r} + π_{r} = t_{r} + π_{r} with value matrix V_{r} and period π_{r}.

According to Moore’s Theorem, recv(8, T , 10, A) = (d_{7} … d_{0}). But then, by Proposition 5.13, there exists m_{r} such that 1 ≤ m_{r} ≤ n_{r},

nth(j, V_{DONE}) = \{ \begin{matrix}T & if j = m_{r} \\ F & if j ≠ m_{r}, 1 ≤ j ≤ n_{r}, \end{matrix}

and

(nth(m_{r}, V_{O7}) … nth(m_{r}, V_{O0})) = (d_{7} … d_{0}).

Thus, for i = 0, …, 7, nth(m_{r}, V_{Oi}) = d_{i}. □

References

[1] Boyer, R. S. and Moore, J S., A Computational Logic Handbook, Academic Press, Boston, 1988.

[2] Institute of Electrical and Electronic Engineers, Draft Standard VHDL Language Reference Manual, 1993.

[3] Kaufmann, M., A Translator from an HDL of David Russinoff to VHDL, Internal Note 278, Computational Logic, Inc., July 1993.

[4] Moore, J S., “A Formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol”, Formal Aspects of Computing 6, no. 1 (1994):60-91.

[5] Roden, M. S., Digital Communication Systems Design, Prentice-Hall, 1988.

[6] Russinoff, D. M., A Formalization of a Subset of VHDL, Technical Report 98, Computational Logic, Inc., April, 1994.

[7] Taub, H. and Schilling, D., Digital Integrated Electronics, McGraw-Hill, New York, 1977.