A Formalization of a Subset of VHDL

David M. Russinoff

Technical Report 98 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 that admits a semantics-preserving translation to a subset of VHDL. The language is based on the VHDL model of event-driven simulation and includes behavioral and structural circuit descriptions, the basic VHDL propagation delay mechanisms, and both zero and nonzero delays. It has 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. We prove a number of basic properties of the simulator, which we apply to the analysis of gate-level designs of a one-bit adder and a d-flip-flop.

1 Introduction

The VHSIC Hardware Description Language [2] (VHDL) has gained wide acceptance as a tool for hardware design and simulation. However, the limitations of simulation as a method of design validation are well known. A formal verification system based on VHDL would therefore have clear practical value. Naturally, a prerequisite for any such system is a precise understanding of VHDL semantics. Unfortunately, VHDL was not intended for formal analysis; it is not surprising that its semantics are complicated and obscure.

The objective of this paper is a rigorous exposition of a core subset of VHDL that is small enough to admit a clear and simple semantic definition, but extensive enough to provide realistic descriptions of interesting circuits. Thus, we avoid complicated language constructs and focus on the VHDL models of time, signal behavior, propagation delay, and event-driven simulation.

Since we are not concerned with syntactic issues, our language definition is based on an abstract syntax that is more amenable to direct formal analysis than that described in [2]. The correspondence between the two is given by a translator from our language to VHDL, which is described elsewhere [3]. Here, we concentrate on a mathematical treatment of the abstract language. This begins in Section 3, where we present the notions of time and waveform, on which the semantics of the language are based. We also define two waveform transformations that embody the main propagation delay modes of VHDL, transport and inertial, and derive their fundamental properties.

In Section 4, we describe the form and execution of behavioral modules, which are used to model gates and also to specify abstractly the behavior of circuits. Section 5 discusses structural modules, which provide hierarchical descriptions of circuits in terms of connections among their components. For the purpose of illustration, we exhibit the actual VHDL code generated by the translator for modules of both types.

The semantics of the language are given by an interpreter function, sim, which produces a list of waveforms that represent the output generated by a module in response to a given list of input waveforms. The definition of sim is presented in Section 6, along with a number of basic results pertaining to its behavior. Finally, as applications of these results, we derive behavioral specifications of several modules. Our proof methodology may be seen as a precise formulation of the informal reasoning that is commonly employed by hardware engineers in the analysis of circuits [5].

One consequence of our commitment to adhere to the VHDL standard is a faithful implementation of the “delta delay” mechanism, which provides for the simulation of zero-delay devices. We note, however, that our exposition could be shortened significantly if we were to require all delays to be positive. In particular, the definitions of time, structural module, and sim are greatly complicated by the delta delay feature.

The design of our language is based on S-expressions, the data objects of LISP, which are defined in Section 2. This choice 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 shall 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. At the time of this writing, significant progress has been made toward this objective; its completion remains a goal of our research.

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 actually 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 formal semantics for VHDL itself, these empirical observations provide the most convincing evidence possible.

2 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 INFINITY. We define a generalized number to be an atom that is either INFINITY or an element of N. Both the order relation and the addition operation on N are extended to the set of generalized numbers in the natural manner: for any n ∈ N, n < INFINITY and n + INFINITY =

INFINITY + n = INFINITY.

A list is an S-expression that is either the literal atom 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; and the ternary functions and3, or3, nand3, nor3, xor3. 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}).

3 Waveforms

Let T be the quotient set determined by the equivalence relation on N ∪ N×N that identifies each n ∈ N with the pair (n, 0) ∈ N × N. An element of T is called a time object. Thus, any element of N or N×N denotes a unique time object, with the understanding that for n ∈ N, n and (n, 0) denote the same object.

T is ordered according to the lexicographic order on N×N, which is consistent with the natural ordering of N: for time objects t_{1} = (m_{1}, k_{1}) and t_{2} = (m_{2}, k_{2}), t_{1} ≤ t_{2} iff m_{1} ≤ m_{2} and either m_{1} < m_{2} or k_{1} ≤ k_{2}. Thus the minimum element of T is the time object that is denoted alternatively as 0 or (0, 0). For t_{1}, t_{2} ∈ T, the interval {t ∈ T : 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) ∈ T. 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 ∈ T, 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. During the course of a simulation, these waveforms are updated at various times. 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, as described below.

Whenever a new event e is to be scheduled for a signal, time(e) is computed from the current time t_{0} = (m, k) and a delay d ∈ N that is associated with the signal, by means of an addition operation from T×N to T, defined as follows:

(m, k) ⊕ d = \{ \begin{matrix}(m + d, 0) & if d ≠ 0 \\ (m, k + 1) & if d = 0. \end{matrix}

The possibility of zero-delay devices, as provided by VHDL, is the sole reason for our ordered-pair model of time. The above definition of addition suggests the following interpretation for the components of a time object: the global component represents the number of time units, which we arbitrarily take to be picoseconds, that have elapsed since the start of a simulation; the delta component represents the number of successive zero-delay events that have been scheduled during the current time unit.

Thus, regardless of delay, when a new event e = (v, t_{v}) is scheduled on a waveform w at time t_{0}, we have t_{0} < t_{v}. The scheduling 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).

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 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 3.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 3.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}).

4 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 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.

Transport mode is often used to model wires along which pulses of arbitrarily small duration are propagated to the delayed signal. For the purpose of illustration, the following primitive module m is defined to have one output of each propagation mode:

(BEHAV (A B) (C D)
  ((NAND2 A B) (NOT1 A))
  (2000 5000)
  (INERTIAL TRANSPORT))

The VHDL code generated by Kaufmann’s translator for m is displayed in Figure 1(a). Note that our time units are interpreted by the translator as picoseconds, and hence the delays are expressed as 2 and 5 nanoseconds. Note also that there is no mention of inertial delay in the translation, since this is the VHDL default mode.

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

ENTITY adder2 IS
PORT (a,b,c: IN BIT; l,h: OUT BIT)
END adder1;
ARCHITECTURE adder2 OF adder2 IS
ENTITY m IS                                 COMPONENT nand
PORT(a,b: IN BIT; c,d: OUT BIT)              PORT(a,b: IN BIT; l,h: OUT BIT);
END m;                                      END COMPONENT;
SIGNAL t1,t2,t3,t4,t5,t6,t7: BIT;
ARCHITECTURE m OF m IS                    BEGIN
BEGIN                                       I1: nand PORT MAP (a,b,t1);
c <= a NAND b AFTER 2 NS;                 I2: nand PORT MAP (a,t1,t2);
d <= TRANSPORT NOT a AFTER 5 NS;          I3: nand PORT MAP (b,t1,t3);
END m;                                      I4: nand PORT MAP (t2,t3,t4);
I5: nand PORT MAP (c,t4,t5);
I6: nand PORT MAP (c,t5,t7);
I7: nand PORT MAP (t5,t4,t6);
I8: nand PORT MAP (t5,t1,h);
I9: nand PORT MAP (t7,t6,l);

(a)

(b)

Figure 1: VHDL Code

(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. 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 4.1 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 3.1(b) and 3.2:

Lemma 4.2 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 4.3 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}).

5 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.

One additional constraint must be imposed on structural modules: in order to ensure that any simulation (as defined in the next section) of a module terminates, our structures are required to be free of zero-delay cyclic paths. Several preliminary definitions will be needed in order to make this notion precise.

We shall define a computable function that measures the (possibly infinite) maximum length of any path of signals within a structure along which the total delay is 0. The definition will be based on an auxiliary function, δ(M, s, E, L), the arguments of which are to be understood as follows:

(1) M may be either the top-level structure or one of its components at any level of the hierarchy;

(2) s is a signal of M;

(3) E = (e_{1} … e_{n}) is a list of generalized numbers corresponding to O(M). For each i, e_{i} is intended to represent the maximum length of any path that starts at the i^{th} output and leads out of M. Such a list is called an environment for M;

(4) L is a list of signals of M, each of which is known to lie on some infinite path.

Under these assumptions, we may think of δ = δ(M, s, E, L) as the maximum length of a path starting at s. It is computed recursively as follows:

(1) If s is a member of L, then δ = INFINITY. Otherwise:

(2) Let Δ_{1} = max{e_{i} : s = s_{i}}, where O(M) = (s_{1} … s_{n}). (If this set is empty, then Δ_{1} = 0.)

(3) Suppose M is behavioral. Let D(M) = (d_{1} … d_{n}). If s is an input of M and some d_{i} > 0, then let Δ_{2} = 1 + max{e_{i} : d_{i} = 0}; otherwise, Δ_{2} = 0.

(4) Suppose M is structural with S(M) = (μ_{1} … μ_{k}). For each i, 1 ≤ i ≤ k, let nth(i, LI(M)) = (a_{i1} … a_{im_{i}}), nth(i, LO(M)) = (b_{i1} … b_{in_{i}}), I(μ_{i}) = (α_{i1} … α_{im_{i}}), and let E_{i} be the environment (ϵ_{i1} … ϵ_{in_{i}}) for μ_{i}, where for 1 ≤ k ≤ n_{i}, ϵ_{ik} = δ(M, b_{ik}, E, cons(s, L)). Let δ_{ij} = δ(μ_{i}, α_{ij}, E_{i}, NIL) for i = 1, …, k and j = 1, …, m_{i}. Let Δ_{2} = max{δ_{ij} : s = a_{ij}}.

(5) δ = max(Δ_{1}, Δ_{2}).

The function Δ is defined by by Δ(M, s, E) = δ(M, s, E, NIL). Next, we define the relative δ-depth of a module M with respect to an environment E to be the number ρ computed as follows:

(1) Let D_{0} be the maximum value of Δ(M, s, E) over all signals s of M. If M is behavioral, then ρ = D_{0}. Otherwise:

(2) Let M be structural with S(M) = (μ_{1} … μ_{k}). For 1 ≤ i ≤ k, let nth(i, LO(M)) = (b_{i1} … b_{in_{i}}) and let D_{i} be the relative δ-depth of μ_{i} with respect to the environment (Δ(M, b_{i1}, E) … Δ(M, b_{in_{i}}, E)). Then ρ = max(D_{0}, D_{1}, …, D_{k}).

Finally, we define the δ-depth of M to be its relative δ-depth with respect to the environment (0 … 0). This represents the length of the longest 0-delay path through M. If it is not INFINITY, we shall say that M is δ-acyclic. All structural modules in our language are required to have this property.

Although we have gone to considerable effort to formalize the VHDL “delta delay” mechanism, the examples in which we are interested exhibit only positive delays. 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)))

The VHDL code for adder2 is shown in Figure 1(b), and a circuit diagram appears in Figure 2(b). Later, we shall compare the behaviors of adder1 and adder2.

Of course, a signal path may be cyclic, provided that some signal in the path is associated with a positive delay. This is an important feature of our language, as it allows the modeling of state-holding devices. Figure 2(a) shows a clocked d-flip-flop, which is modeled by the structural module dff:

(STRUCT
 (CLK D)
 (Q QN)
 (nand2 nand2 nand3 nand2 nand2 nand2)
 ((B2 B1) (A1 CLK) (B1 CLK B2) (A2 D) (B1 QN) (Q A2))
 ((A1) (B1) (A2) (B2) (Q) (QN) (A2)))

The submodules include five 2-input nand gates and a 3-input nand gate nand3, which is similarly defined with an inertial delay of 2000.

We shall define the semantics of structural modules by means of a function step, based on the exec function of Section 4. Note that the notions of input and output packets may be naturally applied to any module. For a structural module

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

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 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 4.1:

Lemma 5.1 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 4.2 may be generalized as follows:

Lemma 5.2 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}).

6 Simulation

Let p and B be an input packet and a bundle for a module M. For any t ∈ T, we define t_{next}(t, p, B, M) to be the minimum element of the set of all t′ ∈ T 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.

It is not obvious that this is a valid recursive definition, i.e., that it is satisfied by a unique function. This may be established by exhibiting some measure of the arguments that decreases with each recursive call. More precisely, it suffices to define a function meas such that under the assumptions imposed on the arguments of run,

meas(M, p, step(M, p, B, t_{next}), t_{next}, t_{f}) ≺ meas(M, p, B, t_{0}, t_{f})

with respect to some well-founded order “≺”. (In fact, this is the requirement for admissibility of Nqthm function definitions.)

We may construct an appropriate measure based on a function ϕ(M, p, B) that computes an upper bound on the delta component of any time object that occurs in any waveform during the course of a simulation. For each signal s of M or any module occurring in M, this function computes the sum of (a) the length of the longest 0-delay path through M starting at s and (b) the largest delta component that occurs in the waveform of p or B that corresponds to s. ϕ(M, p, B) is the maximum of these sums. (We omit the actual recursive definition of ϕ, which parallels that of δ-depth.)

Now, if t_{0} = (m_{i}, k_{i}) and t_{f} = (m_{f}, k_{f}), then we define

meas(M, p, B, t_{0}, t_{f}) = (m_{f} − m_{i}, ϕ(M, p, B) − k_{i}).

It may be shown that with respect to the lexicographic order “≺” on N×N, this function satisfies the property stated above. Note that its definition, and hence that of run, ultimately depends on the assumption that M is δ-acyclic.

The function meas provides an induction scheme for deriving properties of run. The following, for example, is proved by induction as an immediate consequence of Lemma 5.2:

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

The next lemma, similarly proved by induction, provides for the decomposition of a simulation interval:

Lemma 6.2 If p and B are an input packet and a bundle for a module M, and t_{0} ≤ t′ ≤ t_{f}, then run(M, p, B, t_{0}, t_{f}) = run(M, p, run(M, p, B, t_{0}, t′), t′, t_{f}).

Another property of run that is important in the analysis of circuit behavior is the following basic result, which describes the behavior of a structural module in terms of that of its components. It is interesting that its proof requires the two properties of step that are stated in Lemmas 5.1 and 5.2, namely that module execution is neither predictive (with respect to input) nor retroactive (with respect to output).

Lemma 6.3 Let p and A = (α_{1} … α_{k}) be an input packet and a bundle for a structural module M with S(M) = (μ_{1} … μ_{k}). Let t_{0}, t_{1} ∈ T and B = (β_{1} … β_{k}) = run(M, p, A, , t_{0}, t_{1}). Then β_{i} = run(μ_{i}, b_{i}, α_{i}, t_{0}, t_{1}), where b_{i} = inp(i, M, p, B), i = 1, …, k.

Proof: Let A′ = (α′_{1} … α′_{k}) = step(M, p, A, t′), where t′ = t_{next}(t_{0}, p, A, M). Then by definition of step, α′_{i} = step(μ_{i}, a_{i}, α_{i}, t′), where a_{i} = inp(i, M, p, A), and by definition of run, B = run(M, p, A′, t′, t_{1}). By induction, we may assume that β_{i} = run(μ_{i}, b_{i}, α′_{i}, t′, t_{1}). It follows from Lemmas 5.2 and 6.1 that hist(A, t′) = hist(B, t′). Consequently, hist(a_{i}, t′) = hist(b_{i}, t′). By Lemma 5.1, α′_{i} = step(μ_{i}, b_{i}, α_{i}, t′). Thus, we have

β_{i} = run(μ_{i}, b_{i}, step(μ_{i}, b_{i}, α_{i}, t′), t′, t_{1}) = run(μ_{i}, b_{i}, α_{i}, t_{0}, t_{1}).□

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)))).

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).

We note the following restatements of Lemmas 6.2 and 6.3:

Lemma 6.4 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}).

Lemma 6.5 Let p be an input packet for a structural module M with S(M) = (μ_{1} … μ_{k}). Let t ∈ T 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.

Figure 3: Simulation of m

As a simple example, a simulation of the primitive module m is illustrated in Figure 3. The waveforms corresponding to the inputs A and B are

w_{A} = ((T , 60000) (F, 21000) (T , 20000) (F, 10000) (T , 0))

and

w_{B} = ((T , 70000) (F, 30000) (T , 0)),

respectively. These are shown along with the waveforms

w_{C} = (((F, 72000) (T , 12000) (F, 0)))

and

w_{D} = ((F, 65000) (T , 26000) (F, 25000) (T , 15000) (F, 0))

of the output sim(m, (w_{A}w_{B}), 80000) = (w_{C} w_{D}).

This example exhibits a fundamental difference between transport and inertial delay: an input pulse of duration less than the delay, as occurs in w_{A}, is not reflected in an inertial output.

All of the simulation results that we report herein were produced by the Nqthm implementation of sim and have been matched with the output of the corresponding Vantage simulations of the VHDL translations of these modules. One further observation is warranted, however, in support of the claim that our language definition adheres to the VHDL standard [2]. There is an apparent discrepancy between the definition of sim and the standard: in our language, each output waveform of a behavioral module is updated whenever there is a change in any input value. In VHDL, on the other hand, in the absence of any instruction to the contrary (i.e., an explicit “sensitivity list”), a signal’s waveform is updated only in response to changes in those inputs on which the signal is functionally dependent.

Consider, for example, the output D of the module m. The VHDL code corresponding to this signal (Figure 1) is executed only in response to events of the input waveform w_{A}. However, according to our definitions of exec and step, its waveform is also updated whenever the value of B changes, e.g., at time 30000 in our example.

Nonetheless, as illustrated in Figure 3, the behavior of this output signal is completely independent from that of B, in accordance with the VHDL standard. In order to understand this, consider the waveform w that represents this signal before the execution of m at time 21000. The updated waveform after this execution is w′ = transport(w, T , 26000). Although w′ is further updated when the value of B changes at 30000, the value of (NOT1 A) remains T , and hence, by Lemma 3.2, the resulting waveform is transport(w′, T , 35000) = w′.

The above argument is based on the simple observation that at the time of any change in input during a simulation of a behavioral module, the output packet is the result of executing the module at that time. In fact, an interesting property of our simulator is that this holds true even when there is no input change, i.e, regardless of whether the execution actually occurs:

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

Proof: Let B_{0} = exec(M, p, B_{0}, t_{0}) and B_{1} = run(M, p, B_{0}, t_{0}, t_{1}). It is easily shown by induction and Lemma 4.3 that B_{1} = exec(M, p, B_{1}, t_{1}). The lemma is an instance of this result, with t_{0} = t, B_{0} = init(M, p), t_{1} = t, and B_{1} = B. □

7 Analysis of Circuit Behavior

We make use of Lemma 6.6 in the proof of the following useful characterization of behavioral modules:

Lemma 7.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}). According to Lemma 6.6, p_{1} = exec(M, p, p_{1}, t_{1}). It follows from Lemma 3.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 6.4 upon substituting p_{1} and t_{1} for p′ and t′.

Figure 4: Simulation of adder1 and adder2

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 3.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 3.1(c), and on [t′′ + d, t_{2} + d) by Lemma 3.1(a). □

In Figure 4, we illustrate Lemma 7.1 with a simulation of the behavioral module adder1. We also compare the result of this simulation with the corresponding output of the combinational structure adder2. Note, for example, that the first 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. The behavior of adder2 is somewhat more complicated, although for stable inputs, the two modules eventually produce the same values.

It is possible, however, to establish behavioral specifications of combinational (i.e., acyclic) structures, such as adder2, that are similar to (although somewhat weaker than) Lemma 7.1. The derivation of these specifications is straightforward, involving successive applications of Lemma 7.1 to the signals along the various paths that connect inputs to outputs.

Proposition 7.1 Let p = (w_{A}w_{B}w_{C}) be an input packet for adder2, let t_{1}, t_{2}, t_{f} ∈ T, and let sim(adder2, p, t_{f}) = ((w_{T1}) (w_{T2}) (w_{T3}) (w_{T4}) (w_{T5}) (w_{T6}) (w_{T7}) (w_{H}) (w_{L})). Let t_{1} ⊕ 12000 ≤ t_{2} ≤ t_{f}. Suppose that for all t ∈ [t_{1}, t_{2}), ŵ_{A}(t) = v_{A}, ŵ_{B}(t) = v_{B}, and ŵ_{C}(t) = v_{C}. Then for all t ∈ [t_{1} ⊕ 12000, t_{2} ⊕ 4000), ŵ_{L}(t) = xor3(v_{A}, v_{B}, v_{C}); for all t ∈ [t_{1} ⊕ 10000, t_{2} ⊕ 4000), ŵ_{H}(t) = or2(and2(v_{A}, or2(v_{B}, v_{C})), and2(v_{B}, v_{C})).

Proof: We shall concentrate on w_{L}; the analysis of w_{H} is similar. We may assume t_{1} ⊕ 8000 ≤ t_{2}. Applying Lemma 6.5 with i = 1, we have (w_{T1}) = sim(nand2, (w_{A} w_{B}), t_{f}). By Lemma 7.1, for t ∈ [t_{1} ⊕ 2000, t_{2} ⊕ 2000), ŵ_{T1}(t) = nand2(v_{A}, v_{B}). We abbreviate this value as v_{T1}. Similar applications of the same two lemmas yield the following:

ŵ_{T2}(t) = nand2(v_{A}, v_{T1}) = v_{T2} for t ∈ [t_{1} ⊕ 4000, t_{2} ⊕ 2000);; ŵ_{T3}(t) = nand2(v_{T1}, v_{B}) = v_{T3} for t ∈ [t_{1} ⊕ 4000, t_{2} ⊕ 2000); ŵ_{T4}(t) = nand2(v_{T2}, v_{T3}) = v_{T4} for t ∈ [t_{1} ⊕ 6000, t_{2} ⊕ 4000); ŵ_{T5}(t) = nand2(v_{T4}, v_{C}) = v_{T5} for t ∈ [t_{1} ⊕ 8000, t_{2} ⊕ 2000); ŵ_{T6}(t) = nand2(v_{T4}, v_{T5}) = v_{T6} for t ∈ [t_{1} ⊕ 10000, t_{2} ⊕ 4000); ŵ_{T7}(t) = nand2(v_{T5}, v_{C}) = v_{T7} for t ∈ [t_{1} ⊕ 10000, t_{2} ⊕ 2000); ŵ_{L}(t) = nand2(v_{T6}, v_{T7}) for t ∈ [t_{1} ⊕ 12000, t_{2} ⊕ 4000).

Expansion of the abbreviations v_{T1}, …, v_{T7} yields an expression for nand2(v_{T6}, v_{T7}) that may be shown to be tautologically equivalent to xor3(v_{A}, v_{B}, v_{C}). □

Note that for the hypothesis of Proposition 7.1 requires that each input maintain a constant value over a fixed interval, the length of which is the total delay along the longest path that connects the output to an input. The conclusion applies to the interval that results from shifting the lower and upper endpoints of this interval by the delays along the longest and shortest paths, respectively. In the simulation displayed in Figure 4, for example, the input is constant over the interval [20000, 40000), and hence the computed value of L is valid on the interval [32000, 44000). The generalization of this proposition to to arbitrary combinational circuits is straightforward [4].

Similar reasoning may be applied to state-holding (i.e., cyclic) circuits. An analysis of an interesting class of such circuits, based on the flip-flop dff of Section 5, may be found in [4]. Here we consider only the basic flip-flop itself.

Figure 5: Simulation of dff

The intended behavior of this device depends on the assumptions that the CLK input behaves as a regular clock pulse and that the value of the D input does not change too close to a rising edge, i.e., a time when CLK assumes the value T . Under these conditions, an output event can occur only during a short period following a rising edge. The value assumed by Q following a rising edge is the value of D at the edge, and the new value of QN is its negation.

In the sample simulation shown in Fig. 5, rising edges occur at multiples of 20 ns. During the first cycle, the behavior of Q is erratic as the circuit reaches a settled state. Over the next two cycles, Q behaves as described above. The behavior becomes erratic again during the cycle following the rising edge at 60 ns, because a change in D occurs too close to the edge.

A precise specification of dff is given by the following. Its proof is an elaboration of the informal argument found in [5]:

Proposition 7.2 Let p = (w_{CLK} w_{D}) be an input packet for dff. Assume that

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

where t_{−} ⊕ 6000 ≤ t_{+}, t_{+} ⊕ 4000 ≤ t′_{−}, and t′_{−} ⊕ 2000 ≤ t′_{+}. Assume also that

ŵ_{D}(t) = v fort ∈ [t_{d}, t_{+} ⊕ 2000),

where t_{d} ⊕ 4000 ≤ t_{+}. Let sim(dff, p, t_{f}) = ((w_{A1}) (w_{B1}) (w_{A2}) (w_{B2}) (w_{Q}) (w_{QN})), where t_{f} ≥ t′_{+}. Then ŵ_{Q}(t) = v and ŵ_{QN}(t) = not1(v) for t ∈ [t_{+} ⊕ 6000, t′_{+} ⊕ 4000).

Proof: Applying Lemmas 7.1 and 6.5, we have ŵ_{A2}(t) = ŵ_{B1}(t) = T for t ∈ [t_{−} ⊕ 2000, t_{+}⊕2000) and for t ∈ [t′_{−}⊕2000, t′_{+}⊕2000). Let t_{1} = max(t_{−}⊕2000, t_{d}). Then t_{1} ⊕ 4000 ≤ t_{+}. Applying the same two lemmas again, we have ŵ_{B2}(t) = not1(v) for t ∈ [t_{1} ⊕ 2000, t_{+} ⊕ 4000), and hence ŵ_{A1}(t) = v for t ∈ [t_{1} ⊕ 4000, t_{+} ⊕ 4000).

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

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

Thus, ŵ_{B1}(t) = T and ŵ_{A2}(t) = F for t ∈ [t_{+} ⊕ 2000, t′_{−} ⊕ 2000). It follows that ŵ_{QN}(t) = T for t ∈ [t_{+} ⊕ 4000, t′_{−} ⊕ 4000), and hence ŵ_{Q}(t) = F for t ∈ [t_{+} ⊕ 6000, t′_{−} ⊕ 6000). Let t_{3} be the least time such that t_{3} > t_{+} ⊕ 6000 and either w_{Q} or w_{QN} assumes a new value at t_{3}. By an argument similar to the above, it is easily shown that t_{3} ≥ t′_{+} ⊕ 4000. □

References

[1] Boyer, R. S. and Moore, J, 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] Russinoff, D., Specification and Verification of Gate-Level VHDL Models of Synchronous and Asynchronous Circuits, forthcoming technical report, Computational Logic, Inc.

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