\documentclass{article}
\usepackage{acl2,latexsym,pifont,amsmath,amstext,amssymb,amsfonts}

\begin{document}

\title{Verification of Pipeline Circuits}

\date{September 1, 2000}

\author{Matt Kaufmann\\David M.~Russinoff}

\maketitle

\newtheorem{theorem}{Theorem}
\newtheorem{definition}{Definition}[section]
\newtheorem{lemma}{Lemma}[section]
\newtheorem{corollary}[lemma]{Corollary}

\newcommand{\tm}{$^{[tm]}$}

\begin{abstract}
The use of pipelines is an important technique in contemporary hardware design,
particularly at the level of register-transfer logic (RTL).  Earlier formal
analysis (e.g., \cite{mult}) using the ACL2 theorem prover showed correctness
of pipelined floating-point RTL.  This paper extends that work by considering a
notion of a {\it conditional pipeline}, essentially the result of sharing
hardware among several distinct pipelines.  We have employed a {\it pipeline
tool}, written in ACL2 but completely unverified, to find a pipeline-related
bug in an industrial hardware design, which has since been corrected.  We then
enhanced this tool to generate lemmas that we have used to prove properties of
the corrected design.  This paper presents a theoretical basis for this tool
and describes its design and operation at an abstract level, showing how it
fits into the correctness proof.  This work may be viewed, from a high-level
perspective, as encouragement for formal verifiers to prove properties of the
actual RTL-level models, rather than stopping with their various abstractions.
\end{abstract}

\section{Introduction}\label{intro}

Practical algorithms for even the most elementary floating-point
operations are sufficiently complex that their hardware
implementations may require at least several cycles to execute.  In order
to maximize throughput, such operations may be pipelined by partitioning
them into simpler computations that can be performed independently,
each within a single cycle. Verifying that an algorithm is implemented
correctly by a pipeline circuit requires demonstrating the absence of
any resource conflicts that might result in interference between
pipeline stages.  Once this is done, the circuit may be modeled at a
more abstract level without reference to time, i.e., it may be
treated as combinational, which greatly simplifies its analysis.

In an earlier paper~\cite{mult}, we formalized the notion of a
pipelined circuit and described a verification methodology that
involves establishing the behavioral equivalence between a pipeline
and a derived combinational circuit, which allows theorems about the
latter to be transferred to the former.  The theorems are mechanically
checked with ACL2, supported by a library of lemmas pertaining to bit
vectors and floating-point arithmetic~\cite{fplib}.  This methodology
has been applied successfully in proving the correctness of a number
of floating-point instructions of the AMD Athlon$^{\rm TM}$
processor\footnote{AMD, the AMD logo and combinations thereof, 3DNow!,
and AMD Athlon are trademarks of Advanced Micro Devices, Inc.}  with
ACL2.

In general, however, pipelined circuits do not strictly conform to the
simple definition presented in~\cite{mult}, which requires that a
unique pipeline depth be associated with each signal.  On the
contrary, it is not uncommon for a single floating-point module to
perform several operations of different latencies that involve similar
computations, and may therefore be optimized through the sharing of
circuitry.  With respect to each operation, the module behaves as a
simple pipeline subject to certain constraints.  A given signal may be
of different depths with respect to different pipelines.

An example of such a complex pipeline is a version of the AMD Athlon
processor floating-point adder that performs several addition and
subtraction operations, each of latency 4, along with a variety of
floating-point comparisons of latencies 2 and 3.  The module is known
as the {\it merged adder} because it is the result of modifying an
earlier version by implementing additional instructions, including the
{\it 3DNow!}$^{\rm TM}$ instruction set, designed by AMD to support
3-dimensional graphics.  The purpose of this paper is to extend our
simple pipeline methodology to a larger class of circuits that
includes the merged adder.

The circuitry with which we are concerned (indeed the entire AMD
Athlon processor) is designed in a simple register-transfer logic
(RTL) language, which is defined in~\cite{mult}.  Our approach is
based on an automatic translator from this language to the logic of
ACL2, also described in~\cite{mult}.  We begin in
Sections~\ref{circuit-descriptions} and~\ref{trans} by reviewing both
the RTL language and the translator, including extensions to the
latter that have been implemented for our present purpose.  In
Section~\ref{pipes} we develop a theory based on a notion of {\it
conditional pipeline} and identify a context in which several distinct
conditional pipelines within a circuit may be modeled by means of the
same combinational circuit.  In Section~\ref{correctness}, we present
a scheme, based on this theory, using the merged adder as an
illustration, by which ACL2 theorems pertaining to the pipelines can
be derived from corresponding theorems about the combinational
circuit.  Section~\ref{pipeline-tool} describes a tool, written in
ACL2, that analyzes pipelines and facilitates the ACL2 proofs of these
theorems.  This tool discovered a flaw in the pipeline structure of
the merged adder: a number of signals were being accessed one cycle
before their values were valid.  The problem was easily corrected,
before the design was committed to silicon.

\section{Circuit Descriptions}\label{circuit-descriptions}

Each signal $s$ of a circuit description ${\cal D}$ in our RTL
language is defined by a statement of one of three forms,
\begin{equation}\label{input}
\texttt{input}\;\;s[n:0];
\end{equation}
\begin{equation}\label{wire}
s[n:0]\mbox{\texttt{~= }}E;
\end{equation}
or
\begin{equation}\label{reg}
s[n:0]\mbox{\texttt{~<=~}}E;
\end{equation}
and $s$ is thereby identified as an {\it input}, a {\it wire}, or a
{\it register}, respectively.  The {\it size} of $s$, which will be
denoted as $\lambda(s)$, is defined to be $n+1$, where $n \in {\mathbb
N}$.  In the case of a wire or a register, $E$ is an expression
constructed from signals of ${\cal D}$ and standard logical
connectives, called the {\it expression for s}.  Any signal (input,
wire, or register) may also appear in a declaration of the form
\begin{equation}
\texttt{output}\;\;s[n:0];
\end{equation}
and is thus identified as an {\it output} of ${\cal D}$.

Let $S({\cal D})$ denote the set of signals of ${\cal D}$, and let
$I({\cal D})$, $O({\cal D})$, $W({\cal D})$, and $R({\cal D})$ denote
the subsets consisting of its inputs, outputs, wires, and registers,
respectively.  Note that $S({\cal D})$ is the disjoint union of
$I({\cal D})$, $W({\cal D})$, and $R({\cal D})$.

Let $s, s' \in S({\cal D})$ and let $E$ be the expression for $s$.  Then $s'$
is a {\it combinational supporter} of $s$ iff $s \in W({\cal D})$ and either
$s'$ occurs in $E$ or $s'$ is a combinational supporter of some wire occurring
in $E$.  It is a syntactic requirement of the language that no wire is a
combinational supporter of itself.  We derive a weaker notion of support by
dropping the requirement that $s$ be a wire: $s'$ is a {\it supporter} of $s$
iff either $s'$ occurs in $E$ or $s'$ is a supporter of some signal occurring
in $E$.  A circuit ${\cal D}$ is {\it acyclic} if no signal of ${\cal D}$
supports itself.  In this paper, we shall consider only acyclic
circuits.\footnote{In the actual RTL, a register is sometimes assigned
conditionally, i.e., it can hold its previous value when this value is
irrelevant.  Our translation replaces this irrelevant value with 0 in order to
produce a strictly acyclic circuit.}

A valuation for ${\cal D}$ is a partial function $v$ from $S({\cal D})$ to
${\mathbb N}$ such that for each $s \in dom(v)$, $v(s)$ is a bit
vector of length $\lambda(s)$.  If a valuation $v$ is defined on all
signals that occur in an expression $E$, then $v(E)$ is defined in
the natural way, e.g., $v({\tt x}\;\verb!&!\;{\tt y}) = v({\tt x})
\;\verb!&!\; v({\tt y})$, and in this case, if $E$ is the expression
for a signal $s$, then $v(E)$ is always a bit vector of length
$\lambda(s)$.  If the domain of $v$ is $I({\cal D})$ or $R({\cal D})$,
then $v$ is called an {\it input valuation} or a {\it register state},
respectively.  Given an input valuation ${\cal I}$ and a register
state ${\cal R}$, there exists a unique valuation with domain $S({\cal
D})$, which we shall denote as ${\cal V}_{{\cal D},{\cal I},{\cal
R}}$, that extends both ${\cal I}$ and ${\cal R}$ and such that ${\cal
V}_{{\cal D},{\cal I},{\cal R}}(s) = {\cal V}_{{\cal D},{\cal I},{\cal
R}}(E)$ whenever $s$ is a wire and $E$ is the expression for $s$.

The semantics of circuit descriptions are based on an underlying
notion of {\it clock cycle}.  Let ${\cal I}_{0},{\cal I}_{1},\ldots$
be a sequence of input valuations and let ${\cal R}_{0}$ be a register
state for ${\cal D}$.  We think of each ${\cal I}_{k}$ as representing
the values of the input signals of ${\cal D}$ on the $k^{th}$ cycle of
an execution, and ${\cal R}_0$ as an initial set of register values.
Register states for successive cycles are computed as
\[{\cal R}_{k+1} = next_{\cal D}({\cal I}_{k},{\cal R}_{k}),\]
where the function $next_{\cal D}$ is defined as follows: Given an
input valuation ${\cal I}$ and a register state ${\cal R}$,
$next_{\cal D}({\cal I},{\cal R})$ is the register state ${\cal R}'$,
where for each $s \in R({\cal D})$, if $E$ is the expression for $s$,
then
\[{\cal R}'(s) = {\cal V}_{{\cal D},{\cal I},{\cal R}}(E).\]

If $R({\cal D})$ is empty, then ${\cal D}$ is {\it combinational};
otherwise, ${\cal D}$ is {\it sequential}.  In the combinational case,
the semantics of ${\cal D}$ are considerably simpler: the value of
each signal on cycle $k$ is determined by the input valuation ${\cal
I}_k$, and thus we may write ${\cal V}_{{\cal D},{\cal I}}$
unambiguously.  Naturally, it is in general easier to characterize the
behavior of combinational circuits than sequential circuits.

For any acyclic circuit ${\cal D}$, the result of replacing each
register assignment~(3) of ${\cal D}$ by the corresponding wire
assignment~(2) is a combinational circuit, which we shall denote as
$\tilde{\cal D}$.  In Section~\ref{pipes}, we shall examine a class of
acyclic circuits ${\cal D}$ for which we can establish a relation
between ${\cal D}$ and $\tilde{\cal D}$ that allows us to derive
properties of ${\cal D}$ from corresponding properties of $\tilde{\cal
D}$.  Since we hope to support our proofs with the ACL2 prover, we
shall first describe our scheme for modeling circuits in the ACL2
language.


\section{Translation to ACL2}\label{trans}

The RTL-ACL2 translator analyzes the input declarations and
assignments of a circuit description ${\cal D}$, classifies each
signal as an input, a wire, or a register, and determines its size
$\lambda(s)$.  If a signal $s$ is a wire or a register, then the
expression for $s$ is translated into an ACL2 term
whose free variables are the signals occurring in the
expression.  This requires a translation of each RTL construct into
some ACL2 function.  For example, the term derived from the wire
definition

\begin{verbatim}
M4_mantissa_ols_high[22:0] = 
  {M4_sum71_co[68:47], 
   M4_sum71_co[46] & ~(~M4_sum71_co[45] &
                       ~M4_sticky_ols_high & M4_RN_sel)};
\end{verbatim}
is
\begin{verbatim}
(cat (bits m4_sum71_co 68 47)
     (logand (bitn m4_sum71_co 46)
             (comp1 (logand (logand (comp1 (bitn m4_sum71_co 45) 
                                           1)
                                    (comp1 m4_sticky_ols_high
                                           1))
                            m4_rn_sel)
                    1))
     1)).
\end{verbatim}
Here, {\tt logand} is the LISP primitive for logical (bitwise) ``and'', and
{\tt cat}, {\tt comp1}, {\tt bitn}, and {\tt bits} are defined functions that
perform concatenation, bitwise complementation, bit extraction, and bit
slicing, respectively (see~\cite{mult}).

Next, the translator generates a unary function corresponding to each
signal, the argument of which represents a cycle number.  For $s \in
I({\cal D})$, the function that represents $s$ is undefined,
constrained only to have the required length $\lambda(s)$.  Let
$I({\cal D}) = \{q_1,\ldots,q_N\}.$  Then the following single {\tt
encapsulate} form is generated:\medskip

\begin{acl2}
(encapsulate (($q_1$ (n) t) $\ldots$ ($q_N$ (n) t))
  (local (defun $q_1$ (n) (declare (ignore n)) 0))
  (defthm bvecp-$q_1$
     (bvecp ($q_1$ n) $\lambda(q_1)$)
     :rule-classes :rewrite $\ldots$)
  ...
  (local (defun $q_N$ (n) (declare (ignore n)) 0))
  (defthm bvecp-$q_N$
     (bvecp ($q_N$ n) $\lambda(q_N)$)
     :rule-classes :rewrite $\ldots$)).
\end{acl2}\noindent
The functions corresponding to wires and registers are then defined in terms
of the input functions.  For each wire $s$, the following definition is
generated, in which we write {\tt (f $a_1 \ldots a_j$)} to denote the form
derived from the expression for $s$:\medskip

\begin{acl2}
(defun $s$ (n) 
  (f ($a_1$ n) $\ldots$ ($a_j$ n))).
\end{acl2}\noindent
If $s$ is a register, then the value of $s$ on cycle $n$ is determined
by the values of $a_1,\ldots,a_j$ on cycle $n-1$.  In order to avoid
any assumptions about the value of $s$ on cycle $0$, we make use of an
undefined function {\tt unknown}, which is constrained to return a bit
vector of a specified length.  The following definition is
generated:\medskip

\begin{acl2}
(defun $s$ (n)
  (if (zp n)
      (unknown '$s$ $\lambda(s)$)
    (f ($a_1$ (1- n)) $\ldots$ ($a_j$ (1- n))))).
\end{acl2}
\indent In the general case, these functions form a mutually recursive clique.
In order for the definitions to be admitted by ACL2, a well-founded measure
must be supplied explicitly.  To this end, the translator computes the number
$\chi(s)$ of combinational supporters of each signal $s$ ($\chi(s) = 0$ unless
$s$ is a wire), and inserts the following declaration in the definition for
$s$:\medskip

\begin{acl2}
(declare (xargs :measure (cons (1+ n) $\chi(s)$))).
\end{acl2}\noindent
The prover is then able to establish their admissibility
automatically.

The library lemmas that we plan to apply to these functions generally
depend on the length $\lambda(s)$ of the bit vector {\tt (s n)}.
Therefore, the translator has been programmed to generate, in addition
to the {\tt bvecp-}$q_i$ lemmas, the following for each wire or
register $s$:\medskip

\begin{acl2}
(defthm bvecp-$s$
  (bvecp ($s$ n) $\lambda(s)$)
  :rule-classes :rewrite $\ldots$)
\end{acl2}\noindent
(An auxiliary file contains lemmas that guarantee that these 
lemmas are proved automatically.)

The translator behaves differently if the user declares the circuit
${\cal D}$ to be acyclic.  In this case, once the claim of acyclicity
is verified, the signal definitions are ordered so that no signal
precedes any of its supporters.  Since there is no mutual recursion,
the measure declarations may be omitted.  More significantly, in
addition to the primary model described above, two alternative models
of the combinational circuit $\tilde{\cal D}$ are constructed.

The first of these two is intended for execution.  We define a second
function corresponding to each wire $s$ of $\tilde{\cal D}$ (i.e.,
each wire or register of ${\cal D}$).  This function belongs to a
separate package, named \verb!"+"!; all functions previously mentioned
belong to the \verb!"ACL2"! package.  Its arguments correspond to the
signals that occur in the expression for $s$:\medskip

\begin{acl2}
(defun +::s ($a_1 \ldots a_j$)
  (f $a_1 \ldots a_j$)).
\end{acl2}
\indent One other function is included in this model of $\tilde{\cal D}$.  Let
$W(\tilde{\cal D}) = \{s_1,\ldots,s_L\}$, ordered so that no signal precedes
any of its supporters, and for $i = 1,\ldots,L$, let $a_{i1},\ldots,a_{ij_i}$
be the arguments of \verb!+::!$s_i$.  Suppose that we are interested in
observing the behavior of some set of signals $\{r_1,\ldots,r_\ell\}$.  Then we
may program the translator to generate this definition:\medskip

\begin{acl2}
(defun execute (var $q_1 \ldots q_N$)
  (let* (($s_1$ (+::$s_1$ $a_{11} \ldots a_{1j_1}$))
         ($s_2$ (+::$s_2$ $a_{21} \ldots a_{2j_2}$))
          ...
         ($s_N$ (+::$s_L$ $a_{N1} \ldots a_{Nj_N}$)))
    (case var
      ($r_1$ $r_1$)
      ($r_2$ $r_2$)
      ...
      ($r_\ell$ $r_\ell$).
\end{acl2}\noindent
The arguments of {\tt execute} are the input signals $q_1,\ldots,q_N$
and one additional argument, {\tt var}, which ranges over the signals
of interest.  It is clear from the definition that the function simply
computes the value of each signal in succession and returns the value
of the selected signal.

For the other model of $\tilde{\cal D}$, yet another function is
generated for each signal, in a package named \verb!"*"!.  These
functions have no arguments; their values represent the values of the
corresponding signals that are determined by an unspecified set of
input values.  The inputs are again introduced by an {\tt encapsulate}
form that constrains their values only to be bit vectors of the
appropriate lengths:\medskip

\begin{acl2}
(encapsulate ((*::$q_1$ () t) $\ldots$ (*::$q_N$ () t))
  (local (defun *::$q_1$ () 0))
  (defthm bvecp\verb!*!$q_1$
     (bvecp (*::$q_1$) $\lambda(q_1)$)
     :rule-classes $\ldots$)
  ...
  (local (defun *::$q_N$ () 0))
  (defthm bvecp\verb!*!$q_N$
     (bvecp (*::$q_N$) $\lambda(q_N)$)
     :rule-classes $\ldots$)).
\end{acl2}\noindent
The other signal values are then defined in terms of these:\medskip

\begin{acl2}
(defun $*::s$ () (f (*::$a_1$) $\ldots$ (*::$a_j$))).
\end{acl2}
\indent As in the \verb!"ACL2"! model, we also have the following for each
$s$:\medskip

\begin{acl2}
(defthm bvecp-*-$s$
  (bvecp (*::$s$) $\lambda(s)$)
  :rule-classes :rewrite $\ldots$)
\end{acl2}\noindent
Whenever the \verb!"*"! or \verb!"ACL2"! model is included in a proof
session, these lemmas are loaded along with the signal
definitions. The definitions are then all disabled, to be enabled
individually as required.

Of the two alternative models of $\tilde{\cal D}$, the \verb!"+"!
model has the advantage of being executable while the \verb!"*"! model
(for reasons discussed in~\cite{mult}) is more amenable to formal
analysis.  It is not difficult to show, for any acyclic circuit ${\cal
D}$, that the two are equivalent.  First, we first prove the following
rewrite rule for each signal $s_i$, $1 \leq i \leq L$:\medskip

\begin{acl2}
(equal (+::$s_i$ (*::$a_{i1}$) $\ldots$ (*::$a_{ij_i}$))
       (*::$s_i$)).
\end{acl2}\noindent
(These lemmas may be generated and proved automatically.)
Then, with all of the functions \verb!*::!$s_i$ and \verb!+::!$s_i$
disabled (and the function {\tt execute} enabled), the following
equivalence is readily proved, for each of the signals
$r_1,\ldots,r_\ell$:\medskip

\begin{acl2}
(equal (*::$r_i$) (execute '$r_i$ (*::$q_1$) $\ldots$ (*::$q_N$))).
\end{acl2}
\indent Ultimately, however, we are interested in the behavior of the
primary \verb!"ACL2"! model of ${\cal D}$.  The other two are useful
only insofar as we are able to relate them to the \verb!"ACL2"! model.
Of course, if ${\cal D}$ happens to be a combinational circuit, i.e.,
${\cal D} = \tilde{\cal D}$, then equivalence is trivial---the
following theorem may be proved, for each signal $s_i$ of ${\cal D}$,
simply by enabling and disabling definitions as appropriate:\medskip

\begin{acl2}
(implies (and (equal ($q_1$ n) (*::$q_1$))
              (equal ($q_2$ n) (*::$q_2$))
              ...
              (equal ($q_N$ n) (*::$q_N$)))
         (equal ($s_i$ n) (*::$s_i$))).
\end{acl2}\noindent
Of course, the circuits with which we are concerned are
generally not combinational.  However, in the next section, we shall
describe a class of pipeline circuits for which we can prove lemmas
similar to the above, providing a means for ``lifting'' results
pertaining to the \verb!"*"! model to the \verb!"ACL2"! model.  For
these circuits, we are thus free to focus on the combinational circuit
$\tilde{\cal D}$, using the \verb!"+"! model for testing and
concentrating our proof effort on the simpler \verb!"*"! model.


\section{Pipelines}\label{pipes}

Let $\delta : S({\cal D}) \rightarrow {\mathbb N}$.  We shall say
that ${\cal D}$ is a {\it pipeline with depth function} $\delta$ if
\begin{enumerate}

\item[(1)] for all $s \in W({\cal D})$, $\delta(s') = \delta(s)$ for
each signal $s'$ occurring in the expression for $s$, and

\item[(2)] for all $s \in R({\cal D})$, $\delta(s) > 0$ and $\delta(s') = \delta(s)-1$ for
each signal $s'$ occurring in the expression for $s$.
\end{enumerate}

Obviously, any combinational circuit is a pipeline with constant depth
function $\delta(s) = 0$.  For a nontrivial example of a sequential
pipeline, the reader is referred to the floating-point multiplier
presented in~\cite{mult}.

It is clear that any pipeline is acyclic.  It is also easy to show
that a pipeline ${\cal D}$ is related to the derived combinational
circuit $\tilde{\cal D}$ as stated in the following theorem.

\begin{theorem}\label{comb}
Let ${\cal D}$ be a pipeline with depth function $\delta$.  Let
$\{{\cal I}_0,{\cal I}_1,\ldots\}$ be a sequence of input valuations
and let ${\cal R}_0$ be a register state for ${\cal D}$.  For all
$k \in {\mathbb N}$, let ${\cal R}_{k+1} = next_{\cal D}({\cal I}_k,{\cal
R}_k)$.  Let ${\cal I}$ be the input valuation defined by ${\cal I}(s)
= {\cal I}_{\delta(s)}(s)$ for each input $s$.  Then for any signal
$s$ of ${\cal D}$,
\[{\cal V}_{{\cal D},{\cal I}_{\delta(s)},{\cal R}_{\delta(s)}}(s) = 
{\cal V}_{\tilde{\cal D},{\cal I}}(s).\]
\end{theorem}
In fact, we shall prove a generalization of Theorem~\ref{comb},
concerning a larger class of circuits that behave as pipelines under
certain constraints.

A {\it constraint set} for ${\cal D}$ is defined to be a set of
triples ${\cal A} \subset S \times {\mathbb N} \times {\mathbb N}$
such that if $(s,c,d), (s',c',d') \in {\cal A}$ and $s = s'$, then $c
= c'$.  The {\it domain} of a constraint set ${\cal A}$ is
\[dom({\cal A}) = \{s \in S({\cal D}) : (s,c,d) \in {\cal A} \mbox{ for some $c$ and $d$}\}.\]
We shall say that an expression $E$ is {\it forced} to the value $u$
at depth $d$ under ${\cal A}$ if $v(E) = u$ for every valuation $v$
that satisfies $v(s) = c$ for all $(s,c,d) \in {\cal A}$.  Note that a
given expression cannot be forced to different values at different
depths.  Given a set $P$ of signals, $E$ is {\it determined} by $P$ at
depth $d$ under ${\cal A}$ if $v(E) = v'(E)$ for any two valuations
$v$ and $v'$ such that

\begin{itemize}

\item[(a)] $v(s) = v'(s)$ for all $s \in P$, and

\item[(b)] $v(s) = v'(s) = c$ for all $(s,c,d) \in {\cal A}$.

\end{itemize}

A sequence of input valuations $\{{\cal I}_0,{\cal I}_1,{\cal
I}_2,\ldots\}$ {\it satisfies} a constraint set ${\cal A}$ if for any
register state ${\cal R}_0$, and for all $(s,c,d) \in {\cal A}$,
${\cal V}_{{\cal D},{\cal I}_d,{\cal R}_d}(s) = c$, where $R_{k+1} =
next_{\cal D}({\cal I}_k,{\cal R}_k)$ for $k \in {\mathbb N}$.  

The {\it closure} $\bar{\cal A}$ of ${\cal A}$ is recursively defined
as follows: $(s,c,d) \in \bar{\cal A}$ iff

\begin{itemize}

\item[(a)] $(s,c,d) \in {\cal A}$, or

\item[(b)] $s \in W$ and the expression for $s$ is forced to $c$ at
depth $d$ under $\bar{\cal A}$, or

\item[(c)] $s \in R$, $d > 0$,  and the expression for $s$ is forced to $c$ at
depth $d-1$ under~$\bar{\cal A}$.

\end{itemize}
It is clear that any sequence of input valuations that satisfies
${\cal A}$ must also satisfy~$\bar{\cal A}$.

We are ready to consider a generalized notion of pipeline, which involves
selecting a relevant subset $P$ of the signals of ${\cal D}$ according to a set
${\cal A}$ of constraints.  Let ${\cal A}$ be a constraint set for ${\cal D}$,
let $P \subset S({\cal D})$ such that $P \cap dom({\cal A}) = \emptyset$, and
let $\delta : P \rightarrow {\mathbb N}$.  Then ${\cal D}$ is a {\it
conditional pipeline under ${\cal A}$ with pipeline signals $P$ and depth
function} $\delta$ if for all $d \in {\mathbb N}$,

\begin{itemize}

\item[(a)] for every $s \in W({\cal D}) \cap P$, if $\delta(s) = d$,
then the expression for $s$ is determined by $P \cap \delta^{-1}(d)$
at depth $d$ under $\bar{\cal A}$; and

\item[(b)] for every $s \in R({\cal D}) \cap P$, if $\delta(s) = d$,
then $d > 0$ and the expression for $s$ is determined by $P \cap
\delta^{-1}(d-1)$ at depth $d-1$ under $\bar{\cal A}$.

\end{itemize}

The circuit that originally motivated this definition is the merged
adder mentioned in Section~\ref{intro}.  The operations performed by
this circuit include those of the original AMD Athlon processor
floating-point adder, to which we shall refer as {\it FPA}, as well as
the 3DNow! instruction extensions, which we shall call {\it F3A}.
Each of these sets contains operations of latencies 2, 3, and 4.
Thus, the full set of operations is partitioned into six subsets.  For
each of these subsets, the circuit may be viewed as a conditional
pipeline with corresponding pipeline signals and constraints.

Correct behavior of the merged adder requires that two operations are
never initiated on the same cycle, and that two operations of
different latencies are never scheduled to terminate on the same
cycle.  An FPA or F3A operation is initiated by setting the control
input {\tt EPC\verb!_!FPA\verb!_!EN0\verb!_!11} or {\tt
EPC\verb!_!F3A\verb!_!EN0\verb!_!11}, respectively, and encoding the
operation in the opcode input, {\tt
EPC\verb!_!EX1\verb!_!FPOpcode0\verb!_!11}.  Operands are represented
by the signals {\tt PIPE0\verb!_!FSRC1\verb!_!11} and {\tt
PIPE0\verb!_!FSRC2\verb!_!11}.  There is an additional control input,
{\tt EPC\verb!_!FPA\verb!_!WB0\verb!_!14}, which simply echoes {\tt
EPC\verb!_!FPA\verb!_!EN0\verb!_!11} after a 3-cycle delay.

Thus, for example, in order for a long (4-cycle) F3A operation to be
initiated at cycle $n$ and to execute correctly, the following
predicate must hold:

\begin{verbatim}
(defun f3a-long-op-assumptions (n)
 (and
      ;n is a positive integer:

      (not (zp n))

      ;;f3a 4-cycle op is initiated at n:

      (equal (epc_f3a_en0_11 n) 1)
      (f3a-long-op (epc_ex1_fpopcode0_11 n))
      (admissible-operand-p (pipe0_fsrc1_11 n))
      (admissible-operand-p (pipe0_fsrc2_11 n))
      
      ;;no fpa op is initiated at n:  
     
      (equal (epc_fpa_en0_11 n) 0)
      (equal (epc_fpa_wb0_14 (+ 3 n)) 0)
       
      ;;no 3-cycle op is initiated at n+1: 
      
      (or (equal (epc_f3a_en0_11 (+ 1 n)) 0)
          (not (f3a-mid-op (epc_ex1_fpopcode0_11 (+ 1 n)))))       
      (or (equal (epc_fpa_en0_11 (+ 1 n)) 0)
          (not (fpa-mid-op (epc_ex1_fpopcode0_11 (+ 1 n)))))
       
      ;;no 2-cycle op is initiated at n+2:
       
      (or (equal (epc_f3a_en0_11 (+ 2 n)) 0)
          (not (f3a-short-op (epc_ex1_fpopcode0_11 (+ 2 n)))))         
      (or (equal (epc_fpa_en0_11 (+ 2 n)) 0)
          (not (fpa-short-op (epc_ex1_fpopcode0_11 (+ 2 n))))))).
\end{verbatim}
This definition states not only that the operation is initiated
correctly, but also that no other operation interferes with its
execution.  This latter point is made rigorous by showing that the
circuit may be described as a conditional pipeline; we do so by
expressing the appropriate constraints.

The condition that no FPA operation is initiated at cycle $n$ is
obviously ensured by two constraints:

\begin{verbatim}
(EPC_FPA_EN0_11,0,0)
(EPC_FPA_WB0_14,0,3).
\end{verbatim}
The other constraints are less obvious, but for each relevant class of
operations, there happens to be a signal that is set whenever an
operation from that class is initiated.  For example, there are three
2-cycle F3A operations that return the minimum of two operands.  Their
opcodes are represented by the constants {\tt F3MIN}, {\tt F3MINPS},
and {\tt F3MINSS}, and thus they correspond to the signal
\verb!F3A_min_11!:

\begin{verbatim}
F3A_min_11 = EPC_F3A_EN0_11 &
             (EPC_EX1_FPOpcode0_11[11:0] == `F3MIN |
              EPC_EX1_FPOpcode0_11[11:0] == `FPKMINPS | 
              EPC_EX1_FPOpcode0_11[11:0] == `FPKMINSS).
\end{verbatim}
Clearly, the condition that none of these operations is initiated at
either cycle $n$ or cycle $n+2$ is represented by these two
constraints:

\begin{verbatim}
(F3A_min_11,0,0)
(F3A_min_11,0,2).
\end{verbatim}
Altogether, 37 constraints are required in the formulation of this
conditional pipeline.

The pipeline signals naturally include the operands and opcode, which
are assigned depth 0.  There are five other pipeline inputs---four
exception masks and one that controls rounding---which are received
one cycle later and therefore have depth 1.  There are seven outputs of
interest---the result of the operation and six exception flags---all
of which have depth 4.  Thus, correctness of the pipeline is described
by the following implication, in which the conclusion expresses some
relation among the pipeline inputs and outputs:

\begin{verbatim}
(defthm correctness-of-f3a-long-ops
  (implies (f3a-long-op-assumptions n)
           (f3a-long-op-result (pipe0_fsrc1_11 n)
                               (pipe0_fsrc2_11 n)
                               (epc_ex1_fpopcode0_11 n)
                               (rq_speccwrc_13 (+ 1 n))
                               (rq_speccwom_13 (+ 1 n))
                               (rq_speccwum_13 (+ 1 n))
                               (rq_speccwdm_13 (+ 1 n))
                               (rq_speccwim_13 (+ 1 n))
                               (pipe0_fres_fpa_15 (+ 4 n))
                               (ex_faultnormalize0_fpa (+ 4 n))
                               (ex_invalidxcp0 (+ 4 n))
                               (ex_denormxcp0 (+ 4 n))
                               (ex_inexactresult0 (+ 4 n))
                               (ex_numoverflow0 (+ 4 n))
                               (ex_tinyresult0 (+ 4 n))))).
\end{verbatim}

Of course, the other pipelines of the circuit have different
constraint sets and depth functions, although pipeline signals are
shared.  For the 3-cycle (resp., 2-cycle) operations, the operands and
opcode are pipeline signals of depth 1 (resp., depth 2) while the
outputs still have depth 4.

A natural approach to proving theorems about conditional pipelines,
such as the one above, would be to derive an actual pipeline ${\cal
D}'$ from a given conditional pipeline ${\cal D}$ such that the
signals of ${\cal D}'$ coincide with the pipeline signals of ${\cal
D}$, and such that the behaviors of these signals can be shown to be
equivalent for input sequences that satisfy the constraints of ${\cal
D}$.  This would allow us to derive properties of ${\cal D}$ by
examining the combinational circuit $\tilde{{\cal D}'}$ and applying
Theorem~\ref{comb}.  This approach, however, is not quite suitable for
our needs.

The real purpose of a conditional pipeline, as illustrated by the
merged adder, is to perform several operations that have different
latencies but involve similar computations that may be executed on the
same hardware.  Thus, a single circuit is designed as an embodiment of
several distinct conditional pipelines that perform different
functions, each with its own sets of constraints and pipeline signals.
Just as circuitry is shared by these pipelines, we would like to be
able to prove theorems about this circuitry that could be shared in
our analysis of the various pipeline behaviors.  Thus, rather than
construct and prove separate theorems about a different combinational
circuit for each of several conditional pipelines that are comprised
by a circuit ${\cal D}$, we would prefer to focus our proof efforts on
the single combinational circuit $\tilde{\cal D}$.  This requires that
we find a way to lift results pertaining to $\tilde{\cal D}$ to
results about ${\cal D}$, which motivates the following theorem.

\begin{theorem}\label{pipe}
Let ${\cal D}$ be a conditional pipeline under ${\cal A}$ with
pipeline signals $P$ and depth function $\delta$.  Let $\{{\cal
I}_0,{\cal I}_1,\ldots\}$ be a sequence of input valuations that
satisfies ${\cal A}$, and let ${\cal I}$ be an input valuation such
that

\begin{itemize}

\item[(a)] for all $s \in I({\cal D}) \cap P$, ${\cal I}(s) = {\cal I}_{\delta(s)}(s)$, and

\item[(b)] for all $(s,c,d) \in {\cal A}$, ${\cal V}_{\tilde{\cal D},{\cal I}}(s) = c$.

\end{itemize}
Let ${\cal R}_0$ be a register state, and let ${\cal R}_{k+1} =
next_{\cal D}({\cal I}_k,{\cal R}_k)$ for $k \in {\mathbb N}$.  Then
for all $s \in P$, ${\cal V}_{{\cal D},{\cal I}_{\delta(s)},{\cal
R}_{\delta(s)}}(s) = {\cal V}_{\tilde{\cal D},{\cal I}}(s)$.
\end{theorem}

Proof: First, we claim that for all $(s,c,d) \in \bar{\cal A}$, ${\cal
V}_{\tilde{\cal D},{\cal I}}(s) = c$.  More generally: if expression
$E$ is forced to the value $c$ at depth $d$ under $\bar{\cal A}$, then
${\cal V}_{\tilde{\cal D},{\cal I}}(s) = c$.  But this is easy to show
by induction on the appropriate lexicographic order, considering first
$d$ and then the sum of the numbers of supporters of signals occurring
in $E$, by using hypothesis (b) and the definition of $\bar{\cal A}$.

The conclusion of the theorem is derived using a similar induction
scheme, based on $d$ and then the number of supporters of $s$.  In the
base case, $s \in I({\cal D})$ and using hypothesis (a), we have
\[{\cal V}_{{\cal D},{\cal I}_{\delta(s)},{\cal R}_{\delta(s)}}(s)
= {\cal I}_{\delta(s)}(s)
= {\cal I}(s)
= {\cal V}_{\tilde{\cal D},{\cal I}}(s).\]
For the inductive case, let $E$ be the expression for $s$ and let
\[d = \left\{\begin{array}{ll}
         \delta(s) & \mbox{if $s \in W({\cal D})$}\\
         \delta(s)-1 & \mbox{if $s \in R({\cal D})$}. \end{array} \right. \]
By the inductive hypothesis, for all $s' \in P$ occurring in $E$ with $\delta(s') = d$,
\[{\cal V}_{{\cal D},{\cal I}_d,{\cal R}_d}(s') = {\cal V}_{\tilde{\cal D},{\cal I}}(s').\]
Now suppose that $(s',c,d) \in \bar{\cal A}$.
Since $\{{\cal I}_0,{\cal I}_1,\ldots\}$ satisfies $\bar{\cal A}$, 
${\cal V}_{{\cal D},{\cal I}_d,{\cal R}_d}(s') = c$.  As we have already noted, 
${\cal V}_{\tilde{\cal D},{\cal I}}(s') = c$ as well.  Thus, since $E$ is determined
by $P \cap \delta^{-1}(d)$ under $\bar{\cal A}$ at depth $d$, and since we have
just shown that valuations ${\cal V}_{{\cal D},{\cal I}_d,{\cal R}_d}$ and ${\cal
V}_{\tilde{\cal D},{\cal I}}$ satisfy the criteria for $v$ and $v'$ in the
definition of {\it determined},
\[{\cal V}_{{\cal D},{\cal I}_{\delta(s)},{\cal R}_{\delta(s)}}(s)
= {\cal V}_{{\cal D},{\cal I}_d,{\cal R}_d}(E)
= {\cal V}_{\tilde{\cal D},{\cal I}}(E) = {\cal V}_{\tilde{\cal D},{\cal I}}(s). \Box\]


\section{Correctness of Pipelines}\label{correctness}

Theorem~\ref{pipe} above is the theoretical basis for our scheme for
deriving ACL2 theorems pertaining to a conditional pipeline ${\cal D}$
from corresponding theorems about $\tilde{\cal D}$, which we describe
in this section.

Suppose that ${\cal D}$ is a conditional pipeline under a
constraint set ${\cal A}$ with pipeline signals $P$ and depth function $\delta$, where
\[{\cal A} = \{(s_1,c_1,d_1),\ldots,(s_A,c_A,d_A)\}.\]
Again let
\[I({\cal D}) = \{q_1,\ldots,q_N\},\]
and assume that
\[I({\cal D}) \cap P = \{q_1,\ldots,q_k\},\]
and that the set of all signals in $I({\cal D})$ that belong to
$dom({\cal A})$ is
\[\{q_{k+1},\ldots,q_m\},\]
where $1 \leq k \leq m \leq N$.  Also, let
\[O({\cal D}) \cap P = \{r_1,\ldots,r_\ell\}.\]
As a matter of convenience, assume that $\delta$ has been extended to
the inputs $q_{k+1},\ldots,q_m$ by defining $\delta(q_i)$ in each case
to be a depth at which $q_i$ is constrained by ${\cal A}$, i.e.,
$\delta(q_i) = d_j$, where $(s_j,c_j,d_j) \in {\cal A}$ and $s_j =
q_i$.  Note that there may be several possible choices of $j$, but the
selection is of no consequence.

We are interested in deriving properties of ${\cal D}$ of the
form\medskip

\begin{acl2}
(implies (assumptions n)
         (result ($q_1$ (+ $\delta(q_1)$ n)) $\ldots$ ($q_k$ (+ $\delta(q_k)$ n))
                 ($r_1$ (+ $\delta(r_1)$ n)) $\ldots$ ($r_\ell\;$ (+ $\delta(r_\ell)$ n))))
\end{acl2}\noindent
such as the theorem {\tt correctness-of-f3a-long-ops} of the preceding section.
In general, {\tt (assumptions n)} is a predicate constructed from
applications of the input functions of the form {\tt ($q_i$ (+ $j$
n))}, where $1\leq i \leq m$ and $j \geq 0$.

Note that the input functions $q_1,\ldots,q_N$ represent a sequence of
input valuations $\{{\cal I}_0,{\cal I}_1,\ldots\}$ for ${\cal D}$,
given by
\[{\cal I}_i(q_j) = \verb!(!q_j \verb!(+ ! i \verb! n))!.\]
Similarly, the corresponding constant functions in the \verb!"*"! package
represent an input valuation ${\cal I}$ for $\tilde{\cal D}$, defined by
\[{\cal I}(q_j) = \verb!(*::!q_j\verb!)!.\]
In order to establish the relevance of Theorem~\ref{pipe} in this context, we
must be able to ensure that the sequence $\{{\cal I}_0,{\cal I}_1,\ldots\}$
satisfies ${\cal A}$.  Thus, we assume that
we have proved the following lemma with the ACL2 prover:\medskip

\begin{acl2}
(defthm constraint-lemma-1
  (implies (assumptions n)
           (and (equal ($s_1$ (+ $d_1$ n)) $c_1$)
                (equal ($s_2$ (+ $d_2$ n)) $c_2$)
                ...
                (equal ($s_A$ (+ $d_A$ n)) $c_A$)))).
\end{acl2}\noindent
We further must be able to ensure that the valuation ${\cal I}$
satisfies the conditions~(a) and~(b) of the theorem.  To this end,
we introduce the following macro.\medskip

\begin{acl2}
(defmacro bindings (n)
  `(and (equal (*::$q_1$) ($q_1$ (+ $\delta(q_1)$ ,n)))
        (equal (*::$q_2$) ($q_2$ (+ $\delta(q_2)$ ,n)))
        ...
        (equal (*::$q_{m}$) ($q_{m}$ (+ $\delta(q_{m})$ ,n))))).
\end{acl2}\noindent
Now assume that we are also able to prove the following.\medskip

\begin{acl2}
(defthm constraint-lemma-2
  (implies (and (assumptions n) (bindings n))
           (and (equal (*::$s_1$) $c_1$)
                (equal (*::$s_2$) $c_2$)
                ...
                (equal (*::$s_A$) $c_A$)))).
\end{acl2}\noindent
Then all of the hypotheses of Theorem~\ref{pipe} must hold, given {\tt
(assumptions n)} and {\tt (bindings n)}.  It follows that we should be
able to prove this lemma:\medskip

\begin{acl2}
(defthm pipeline-lemma
  (implies (and (assumptions n) (bindings n))
           (and (equal ($r_1$ (+ $\delta(r_1)$ n)) (*::$r_1$))
                (equal ($r_2$ (+ $\delta(r_2)$ n)) (*::$r_2$))
                ...
                (equal ($r_\ell$ (+ $\delta(r_\ell)$ n)) (*::$r_\ell$))))).
\end{acl2}\noindent
Before considering the proof of this lemma or its implications, let us examine
{\tt constraint-lemma-1} and {\tt constraint-lemma-2} in the context of the
merged adder.  As illustrated by this example, if the constraint set ${\cal A}$
has been judiciously constructed, then the proofs of both of these lemmas
should be trivial.  For example, the conjunct of {\tt constraint-lemma-1}
corresponding to the constraint \verb!(F3A_min_11,0,2)! is
\begin{verbatim}
(equal (f3a_min_11 (+ 2 n)) 0),
\end{verbatim}
where
\begin{verbatim}
(defun f3a_min_11 (n)
 (logand (epc_f3a_en0_11 n)
         (logior (log= (epc_ex1_fpopcode0_11 n) 1492)
                 (logior (log= (epc_ex1_fpopcode0_11 n) 2050)
                         (log= (epc_ex1_fpopcode0_11 n) 2114)))))
\end{verbatim}
is the definition generated for this signal.
On the other hand, the definition of {\tt assumptions} includes the
conjunct
\begin{verbatim}
(or (equal (epc_f3a_en0_11 (+ 2 n)) 0)
    (not (f3a-short-op (epc_ex1_fpopcode0_11 (+ 2 n))))),
\end{verbatim}
where {\tt f3a-short-op} is defined by\medskip

\begin{acl2}
(defun f3a-short-op (op)
  (member op '($\ldots$ 1492 2050 2114 $\ldots$))).
\end{acl2}\noindent
Thus, when the definitions are expanded, the term {\tt (equal (f3a\_min\_11 (+ 2
n)) 0)} is immediately rewritten to {\tt T} under the hypothesis {\tt
(assumptions n)}.

Similarly, the corresponding conjunct of {\tt constraint-lemma-2} is
\begin{verbatim}
(equal (*::f3a_min_11) 0).
\end{verbatim}
The macro {\tt bindings} in this case is given by
\begin{verbatim}
(defmacro bindings (n)
  `(and (equal (*::pipe0_fsrc1_11)
               (pipe0_fsrc1_11 ,n))
        (equal (*::pipe0_fsrc2_11)
               (pipe0_fsrc2_11 ,n))
        (equal (*::epc_ex1_fpopcode0_11)
               (epc_ex1_fpopcode0_11 ,n))
        (equal (*::rq_speccwrc_13)
               (rq_speccwrc_13 (+ 1 ,n)))
        ...
        (equal (*::epc_fpa_en0_11)
               (epc_fpa_en0_11 ,n))
        (equal (*::epc_fpa_wb0_14)
               (epc_fpa_wb0_14 (+ 3 ,n))))).
\end{verbatim}
Note that this macro binds the pipeline inputs (at depths 0 and 1) as
well as the constrained inputs (at depths 0 and 3).  In this case,
{\tt assumptions} is taken to be the predicate {\tt
f3a-long-op-assumptions} defined earlier.  Thus, the hypothesis {\tt
(and (assumptions n) (bindings n))} implies

\begin{verbatim}
(f3a-long-op (*::epc_ex1_fpopcode0_11)),
\end{verbatim}
which in turn can be shown to imply

\begin{verbatim}
(equal (*::f3a_min_11) 0).
\end{verbatim}

As noted above, once we have established both {\tt constraint-lemma-1} and {\tt
constraint-}{\tt lemma-2}, Theorem~\ref{pipe} guarantees the truth of {\tt
pipeline-lemma}.  However, we would like to derive {\tt pipeline-lemma}
formally as a theorem of ACL2.  Suppose for the moment that this has been
accomplished. It remains for us to show how {\tt pipeline-lemma} can be used to
derive our stated goal from some analogous theorem pertaining to the \verb!"*"!
functions.

Suppose that for some predicate {\tt spec} we are able to prove
the following two lemmas:\medskip

\begin{acl2}
(defthm spec-lemma-1
  (implies (assumptions n)
           (spec ($q_1$ (+ $\delta(q_1)$ n)) $\ldots$ ($q_{m}$ (+ $\delta(q_{m})$ n))
\end{acl2}

\begin{acl2}
(defthm spec-lemma-2
  (implies (spec (*::$q_1$) $\ldots$ (*::$q_m$))
           (result (*::$q_1$) $\ldots$ (*::$q_k$) (*::$r_1$) $\ldots$ (*::$r_\ell$)))).
\end{acl2}\noindent
In our example, {\tt spec-lemma-1} and {\tt spec-lemma-2} were proved for the following predicate:

\begin{verbatim}
(defun spec (pipe0_fsrc1_11 ... epc_fpa_wb0_14)
  (and (equal epc_f3a_en0_11 1)
       (f3a-long-op epc_ex1_fpopcode0_11)
       (admissible-operand-p pipe0_fsrc1_11)
       (admissible-operand-p pipe0_fsrc2_11)
       (equal epc_fpa_en0_11 0)
       (equal epc_fpa_wb0_14 0))).
\end{verbatim}

The next lemma can then be proved automatically by applying the rewrite
rules {\tt pipeline-lemma} and {\tt spec-lemma-2}:\medskip

\begin{acl2}
(defthm lemma-to-be-instantiated
  (implies (and (assumptions n)
                (bindings n)
                (spec (*::$q_1$) $\ldots$ (*::$q_m$)))
           (result (*::$q_1$) $\ldots$ (*::$q_k$)
                   ($r_1$ (+ $\delta(r_1)$ n)) $\ldots$ ($r_\ell\;$ (+ $\delta(r_\ell)$ n))))).
\end{acl2}
\indent The desired theorem may now be derived by functional instantiation:\medskip

\begin{acl2}
(defthm correctness-of-pipeline
  (implies (assumptions n)
           (result ($q_1$ (+ $\delta(q_1)$ n)) $\ldots$ ($q_k$ (+ $\delta(q_k)$ n))
                   ($r_1$ (+ $\delta(r_1)$ n)) $\ldots$ ($r_\ell\;$ (+ $\delta(q_\ell)$ n))))
  :hints 
  (("Goal" :use ((:functional-instance lemma-to-be-instantiated
                   (*::$q_1$ (lambda () ($q_1$ (+ $\delta(q_1)$ n))))
                   (*::$q_2$ (lambda () ($q_2$ (+ $\delta(q_2)$ n))))
                   ...
                   (*::$q_m$ (lambda () ($q_m$ (+ $\delta(q_m)$ n)) ))))))).
\end{acl2}\noindent
In order to use the indicated functional instance of 
{\tt lemma-to-be-instantiated}, the prover is obligated to establish
the corresponding instances of the constraints on the \verb!*::!$q_i$,
namely the lemmas \verb!bvecp*!$q_i$, for $i = 1,\ldots,m$.  This
amounts to proving the subgoals
\[\verb!(bvecp (!q_i \verb!(+ !\delta(q_i)\verb! n)))!.\]
But these are simply instances of the corresponding rewrite rules
\verb!bvecp-!$q_i$.  Thus, we have the functional instance\medskip

\begin{acl2}
(implies (and (assumptions n)
              (and (equal ($q_1$ (+ $\delta(q_1)$ ,n)) ($q_1$ (+ $\delta(q_1)$ ,n)))
                   (equal ($q_2$ (+ $\delta(q_2)$ ,n)) ($q_2$ (+ $\delta(q_2)$ ,n)))
                   ...
                   (equal ($q_{m}$ (+ $\delta(q_{m})$ ,n)) ($q_{m}$ (+ $\delta(q_{m})$ ,n)))))
              (spec ($q_1$ (+ $\delta(q_1)$ n)) $\ldots$ ($q_m$ (+ $\delta(q_m)$ n))))
         (result ($q_1$ (+ $\delta(q_1)$ n)) $\ldots$ ($q_k$ (+ $\delta(q_k)$ n))
                 ($r_1$ (+ $\delta(r_1)$ n)) $\ldots$ ($r_\ell\;$ (+ $\delta(q_\ell)$ n))))),
\end{acl2}\noindent
which is automatically rewritten to the desired term by applying {\tt spec-lemma-1}.
Note that it is critical that {\tt bindings} was defined as a macro
rather than a function, in order for the functional instance of {\tt
(bindings n)} to be a conjunction of trivial equalities as included
above.

We are left with the task of proving {\tt pipeline-lemma}, which is
precisely the function of our pipeline tool, as described in the next
section.


\section{The Pipeline Tool}\label{pipeline-tool}

Retaining the notation of Section~\ref{correctness}, suppose we have a
predicate {\tt assumptions} pertaining to the signals of ${\cal D}$
for which we can prove both {\tt constraint-}{\tt lemma}{\tt
-1} and {\tt constraint-}{\tt lemma-2}.  Assume that we are also able
to prove the following:

\begin{verbatim}
(defthm n-positive-lemma
  (implies (assumptions n)
           (not (zp n))))
\end{verbatim}
The goal of our pipeline tool is to generate a file of events
culminating in {\tt pipeline-}{\tt lemma}, which may then be used to
establish the correctness of ${\cal D}$ by the procedure described in
Section~\ref{correctness}.

The tool is based on a simple recursive rewriting procedure.  This
procedure requires the computation of the {\it size} $\lambda(t)$ of a
term $t$ that is generated by the translator, as a generalization of
the {\it size} of a signal.  For example,
\begin{center}
$\lambda${\tt (bits} $x$ $i$ $j${\tt )} $= i-j+1$,
\end{center}
\begin{center}
$\lambda${\tt (comp1} $x$ $n${\tt )} $= n$,
\end{center}
and if $\lambda(x) = \lambda(y) = k$, then
\begin{center}
$\lambda${\tt (logior} $x$ $y${\tt )} $=$ $\lambda${\tt (logand} $x$ $y${\tt )} $= k$.
\end{center}

Now, a term is rewritten in the context of a constraint set ${\cal
C}$, relative to a given depth $d \in {\mathbb N}$, as follows.  (If
no case below applies, then the term is returned
unchanged.)\label{prewrite}
\begin{enumerate}

\item[(1)] If the term is a signal $s$ and there exists $(s,c,d)
\in {\cal C}$, then the constant $c$ is returned.

\item[(2)] Otherwise, assume that the term is a function call.  Each of
its arguments is first rewritten recursively.  Then the following rules are
applied.

\item[(3)] If all of its arguments are constants, then the term is
evaluated and the result is returned.

\item[(4)] Suppose the term is {\tt (logior $x$ $y$)}.  If either $x$
or $y$ is 0, then the other argument is returned; if $x$ is the
constant $2^{\lambda(y)}-1$, then that constant is returned; if $y$ is the
constant $2^{\lambda(x)}-1$, then that constant is returned.

\item[(5)] Suppose the term is {\tt (logand $x$ $y$)}.  If either $x$
or $y$ is 0, then 0 is returned; if $x$ is the constant
$2^{\lambda(y)}-1$, then $y$ is returned; if $y$ is the constant
$2^{\lambda(x)}-1$, then $x$ is returned.

\item[(6)] Suppose the term is {\tt (if $x$ $y$ $z$)}.  If $x = {\tt
T}$, then $y$ is returned; if $x = {\tt NIL}$, then $z$ is returned;
if $y = z$, then $y$ is returned.

\end{enumerate}

The input required from the user consists of four components:

\begin{enumerate}

\item[(1)] the ordered set of signal definitions produced by the
translator, with an indication of whether each signal is an input, a
wire, or a register,

\item[(2)] the size $\lambda(s)$ of each signal $s$, 

\item[(3)] the basic constraint set ${\cal A}$, and 

\item[(4)] the depth $\delta(r_i)$ of each of the pipeline signals of
interest, $r_1,\ldots,r_\ell$.  (These are generally some of the
outputs of ${\cal D}$.)

\end{enumerate}

Three passes through the signal list are required.  On the first pass,
two sets are constructed.  The first is a set ${\cal C}$ of
constraints, generated by ${\cal A}$.  We do not guarantee that ${\cal
C} = \bar{\cal A}$, but in general, ${\cal A} \subseteq {\cal C}
\subseteq \bar{\cal A}$, and ${\cal C}$ is a sufficiently close
approximation to $\bar{\cal A}$ for our purpose.  The other is a set
${\cal T}$ of triples $(s,Q,d)$, such that

\begin{enumerate}

\item[(a)]  $s$ is a signal that does not occur in ${\cal C}$, 

\item[(b)] $d \in {\mathbb N}$, and 

\item[(c)] $Q$ is a set of supporters of $s$ such that the expression
for $s$ is determined by $Q$ at depth $d$ under ${\cal C}$ (and hence
under $\bar{\cal A}$).

\end{enumerate}
These two sets are constructed concurrently as all signals are
examined in order beginning with inputs.  ${\cal C}$ is initialized to
${\cal A}$ and ${\cal T}$ is initially empty.  For each signal $s$,
the following procedure is executed:

For each $d' \in {\mathbb N}$ for which there exists at least one
constraint $(s',c',d') \in {\cal C}$ such that $s'$ occurs in the term
that the translator produced for $s$, that term is rewritten in the
context of the current value of ${\cal C}$ relative to the depth $d'$.
Thus, we may have several rewritten terms for $s$ corresponding to
different values of $d'$.  For each of these, a single element will be
inserted into either ${\cal C}$ or ${\cal T}$.

Let $t$ be the rewritten term corresponding to $d'$ and let
\[d = \left\{\begin{array}{ll}
         d' & \mbox{if $s \in W({\cal D})$}\\
         d'+1 & \mbox{if $s \in R({\cal D})$}. \end{array} \right. \]
First suppose that $t$ is a constant.  In this case, if there already
exists some $(s,c,d'') \in {\cal C}$, with $c \neq t$, then an error
is signaled.  Otherwise, $(s,t,d)$ is added to ${\cal C}$.  On the
other hand, if $t$ is not a constant and $Q$ is the set of signals
that occur in $t$, then $(s,Q,d)$ is added to ${\cal T}$.

On the second pass, a set of pairs ${\cal P} \subset S({\cal D})
\times {\mathbb N}$ is constructed, representing the pipeline signals
$P$ and depth function $\delta$.  Initially, we set
\[{\cal P} = \{(r_1,\delta(r_1)),\ldots,(r_\ell,\delta(r_\ell))\}.\]
The signals are then examined in reverse order, beginning with outputs
and proceeding toward inputs, and processed as follows:

\begin{enumerate}

\item[(1)] If $s$ does not occur in ${\cal P}$, then no action is
taken.

\item[(2)] Assume $(s,d) \in {\cal P}$.  If $s$ occurs in ${\cal C}$,
then an error is signaled.  (Recall that our definition does not
allow a pipeline signal to be constrained.)  If there exists $(s,Q,d) \in {\cal T}$,
then consider the set of signals $Q$; if not, then consider the set of
all signals that occur in the definition of $s$.  If any signal in this
set occurs in ${\cal C}$, then an error is signaled.  Otherwise, for each
signal $s'$ in the set, the pair $(s',d')$ is added to ${\cal P}$, where
\[d' = \left\{\begin{array}{ll}
         d & \mbox{if $s \in W({\cal D})$}\\
         d-1 & \mbox{if $s \in R({\cal D})$}. \end{array} \right. \]
\end{enumerate}
In the event of successful termination of this procedure, the claim
that our circuit ${\cal D}$ is a conditional pipeline under ${\cal A}$
has been established and $P$ and $\delta$ have been derived.

Finally, on the third pass, an ACL2 event file is generated, loosely
based on the proof of Theorem~\ref{pipe}.  The first event in the file
is the definition of the macro {\tt bindings}.  This involves nothing
more than printing a line corresponding to each input signal $q_i$
that occurs either in ${\cal A}$ or in $P$, as follows:
\[\verb!(equal (*::!q_i\verb!) (!q_i\verb! (+ !\delta(q_i)\verb! ,n)))!.\]
(Recall that for $q_i \in dom({\cal A})$, $\delta(q_i)$ is selected
arbitrarily from the depths at which $q_i$ is constrained.)

This is followed by a second definition, which is immediately disabled:
\begin{verbatim}
(defun assumptions-and-bindings (n)
  (and (assumptions n)
       (bindings n)))

(in-theory (disable assumptions-and-bindings))
\end{verbatim}
The purpose of this definition is to allow us to prevent the needless
expansion of {\tt (bindings n)} when it appears in the hypothesis of a
lemma.

The rest of the file consists of lemmas that are constructed from the
sets ${\cal C}$ and $P$ as the signal list is traversed in order,
starting with inputs.  Whenever a signal $s \in dom({\cal C})$ is encountered,
two or more lemmas are generated, the precise forms of which depend on
whether $s$ is an input or not.  Suppose $s$ is an input.  Then for each
$(s,c,d) \in {\cal C}$, we have the event\medskip

\begin{acl2}
(defthm $s$-$d$-simp
  (implies (assumptions n)
           (equal ($s$ (+ $d$ n)) $c$))
  :hints (("Goal" :in-theory (enable assumptions)))).
\end{acl2}\noindent
These are followed by\medskip

\begin{acl2}
(defthm $s$-*-simp
  (implies (assumptions-and-bindings n)
           (equal (*::$s$) $c$))
  :hints 
  (("Goal" :in-theory (enable assumptions-and-bindings)))).
\end{acl2}\noindent
If $s$ is any signal other than an input, then a similar set of events
is generated, differing only in the {\tt enable} hints:\medskip

\begin{acl2}
(defthm $s$-$d$-simp
  (implies (assumptions n)
           (equal ($s$ (+ $d$ n)) $c$))
  :hints (("Goal" :in-theory (enable $s$))))
\end{acl2}\noindent
followed by\medskip

\begin{acl2}
(defthm $s$-*-simp
  (implies (assumptions-and-bindings n)
           (equal (*::$s$) $c$))
  :hints (("Goal" :in-theory (enable *::$s$)))).
\end{acl2}
\indent Whenever a signal $s \in P$ is encountered, a single lemma is
generated:\medskip

\begin{acl2}
(defthm $s$-pipe
  (implies (assumptions-and-bindings n)
           (equal (*::$s$) ($s$ (+ $\delta(s)$ n))))
  :hints (("Goal" :in-theory (enable $s$ *::$s$)))).
\end{acl2}
\indent In general, this event file may be certified with minimal guidance
from the user.  It is necessary, however, that the ACL2 environment be
initialized by loading both the \verb!"ACL2"! and \verb!"*"! models of
${\cal D}$ along with the floating-point library.  The function {\tt
(assumptions n)} must then be appropriately defined and disabled.

Once this is done, the only events in the file that may require
modification are the lemmas $s$-$d$-{\tt simp} and $s$-{\tt *-simp}
that correspond to constraints belonging to the original constraint
set ${\cal A}$.  For example, in order to prove the lemma

\begin{verbatim}
(defthm f3a_min_11-simp
  (implies (f3a-long-assumptions n)
           (equal (f3a_min_11 (+ 2 n)) 0))
  :hints (("Goal" :in-theory (enable f3a_min_11))))
\end{verbatim}
the prover must be able to show, according to the definition of {\tt
f3a\verb!_!min\verb!_!11}, that
\begin{center}
{\tt (f3a-long-assumptions n)}
\end{center}
and
\begin{center}
{\tt (not (equal (epc\_f3a\_en0\_11 (+ 2 n))) 0)}
\end{center}
together imply that {\tt (epc\_ex1\_fpopcode0\_11 (+
2 n))} is not 1492, 2050, or 2114.  But this may be accomplished
simply by extending the hint to enable the definitions of {\tt
f3a-long-assumptions} and {\tt f3a-short-op}.

All other lemmas in the file, including the $s$-$d$-{\tt simp} and
$s$-{\tt *-simp} lemmas that correspond to the constraints in the
set-theoretic difference ${\cal C} - {\cal A}$, as well as the $s${\tt
-pipe} lemmas corresponding to the pipeline signals, can be proved
automatically with no user guidance.  The reason for this is that in
processing the statements of these lemmas, once the enabled
definitions of $s$ and \verb!*::!$s$ are expanded, the resulting terms
are rewritten by ACL2 by following essentially the same procedure as
that used by the pipeline tool.

For example, suppose that the file contains a lemma\medskip

\begin{acl2}
(defthm $s$-$d$-simp
  (implies (assumptions n)
           (equal ($s$ (+ $d$ n)) $c$))
 :hints (("Goal" :in-theory (enable $s$)))).
\end{acl2}\noindent
based on a constraint $(s,d,c) \in {\cal C} - {\cal A}$.  
Let {\tt (f $a_1 \ldots a_k$)} denote the term generated by the translator for $s$.
The pipeline tool must have rewritten this term to $c$ at depth $d'$, where
\[d' = \left\{\begin{array}{ll}
         d & \mbox{if $s \in W({\cal D})$}\\
         d-1 & \mbox{if $s \in R({\cal D})$}. \end{array} \right. \]
But then the ACL2 rewriter, after expanding {\tt ($s$ (+ $d$ n))} to
\begin{center}
{\tt (f ($a_1$ (+ $d'$ n)) $\ldots$ ($a_k$ (+ $d'$ n)))}
\end{center}
(using {\tt n-positive-lemma} in the case of a register), will
likewise rewrite this term to $c$ under the hypothesis {\tt
(assumptions n)}.  In order to see this, we refer to the steps of the
pipeline tool's rewriting procedure (page~\pageref{prewrite}):

\begin{enumerate}

\item[(1)] If the tool rewrites some $a_i$ to a constant $c'$ at depth
$d'$, then $(a_i,c',d') \in {\cal C}$, and there must already be a
lemma $a_i$\verb!-!$d'$\verb!-simp!, which ACL2 will invoke to
rewrite {\tt ($a_i$ (+ $d'$ n))} to $c'$.

\item[(2)] In rewriting a function call, ACL2 first rewrites the arguments
recursively.

\item[(3)] ACL2 rewrites a function call with constant arguments simply by
evaluating it.

\item[(4)] The floating-point library includes appropriate rewrite
rules for reducing {\tt (logior} $x$ $y${\tt )}, (a)~when either
argument is 0, and (b)~when one argument is $2^k-1$ and the other is a
bit vector of length $k$.

\item[(5)] The library includes similar rules pertaining to {\tt
(logand} $x$ $y${\tt )}.

\item[(6)] The ACL2 rewriter has built-in procedures for reducing \verb!(if !$x$
\verb! !$y$\verb! !$z$\verb!)! when $x = {\tt T}$, $x = {\tt NIL}$, or
$y = z$.
\end{enumerate}
Similarly, it is clear that the accompanying lemma $s$-{\tt *-simp} is
proved by expanding \verb!(*::!$s$\verb!)!  to {\tt (f (*::$a_1$)
$\ldots$ (*::$a_k$))} and rewriting that term to $c$.

Finally, suppose the file contains an event\medskip

\begin{acl2}
(defthm $s$-pipe
  (implies (assumptions-and-bindings n)
           (equal (*::$s$) ($s$ (+ $\delta(s)$ n))))
  :hints (("Goal" :in-theory (enable $s$ *::$s$))))
\end{acl2}\noindent
corresponding to some $(s,\delta) \in {\cal P}$.  Let
{\tt (f $a_1 \ldots a_k$)} denote the term generated by the translator for
$s$.  We may assume that the pipeline tool rewrote this term, at depth
\[d' = \left\{\begin{array}{ll}
         \delta(s) & \mbox{if $s \in W({\cal D})$}\\
         \delta(s)-1 & \mbox{if $s \in R({\cal D})$}, \end{array} \right. \]
to {\tt (g $a_1 \ldots a_j$)}, where $j \leq k$ and $a_1,\ldots,a_j$
are pipeline signals.  Then the two sides of the equation in
$s$\verb!-pipe! are expanded to
\begin{center}
{\tt (f (*::$a_1$) $\ldots$ (*::$a_k$))}
\end{center}
and
\begin{center}
{\tt (f ($a_1$ (+ $d'$ n)) $\ldots$ ($a_k$ (+ $d'$ n)))},
\end{center}
respectively, which are in turn rewritten to
\begin{center}
{\tt (g (*::$a_1$) $\ldots$ (*::$a_j$))}
\end{center}
and
\begin{center}
{\tt (g ($a_1$ (+ $d'$ n)) $\ldots$ ($a_j$ (+ $d'$ n)))}.
\end{center}
The proof is completed by applying the lemmas $a_i$\verb!-pipe!,
rewriting {\tt (*::$a_i$)} to {\tt ($a_i$ (+ $d'$ n))}, for $i =
1,\ldots,j$.


\section{Conclusion}

This work grew out of an effort to verify the behavior of a
floating-point RTL module, namely the AMD Athlon processor merged
adder, using ACL2.  Our initial approach was to verify a combinational
version of this module, derived by replacing register assignments with
wire assignments.  While it might have been reasonable to stop there,
we were concerned about the possibility of interference between
coexisting pipelines that may have been abstracted away by the
reduction to a purely combinational design.

This concern led to the development of a theory of pipeline circuits,
which we applied in our analysis of the adder in order to justify the
abstraction.  We wrote a prototype tool to perform checks for correct
pipeline behavior under various sets of assumptions on the inputs
corresponding to the distinct operations performed by a module.  The
tool proved its utility by exposing a bug in the adder, which was
subsequently fixed.  This experience reinforced the importance of
preserving our goal of verifying the actual RTL, rather than a
combinational abstraction of it.  Thus, we extended the pipeline tool
to generate a sequence of ACL2 events that provide support for a
complete ACL2 proof of correctness of the original RTL.

This effort illustrates an important verification technique: the use
of unverified code to generate provable lemmas.  (Macros, of course,
have been used through ACL2's history for such purposes, but here we
are referring to the automatic generation of substantial certifiable
books.)  The automation of such lemmas proved valuable here, in
support of reasoning about bit vectors (the lemmas {\tt bvecp-}$s$,
etc., of Section~\ref{trans}) and in a critical step in deriving the
final correctness theorem (the lemma {\tt pipeline-lemma} of
Section~\ref{pipeline-tool}).  This illustration of the use of lemma
generation, along with functional instantiation and other techniques,
will, we hope, encourage other formal verification workers to reason
about actual RTL hardware models, rather than limiting their efforts
to higher-level abstractions.


\begin{thebibliography}{3}

\bibitem{div}Moore, J, Lynch, T., and Kaufmann, M., ``A Mechanically Checked Proof
of the Correctness of the Kernel of the $AMD5_{K}86$ Floating Point Division Algorithm'',
{\it IEEE Transactions on Computers}, 47:9, September, 1998. 

\bibitem{k5sqrt}Russinoff, D., ``A Mechanically Checked Proof of IEEE Compliance of the AMD-K5
Floating Point Square Root Microcode'', {\it Formal Methods in System Design} 
14:1, January 1999. See URL {\tt http://www.onr.com/user/russ/david/fsqrt.html}.

\bibitem{k7divsqrt}Russinoff, D., ``A Mechanically Checked Proof of IEEE Compliance of the AMD-K7
Floating Point Multiplication, Division, and Square Root Algorithms'', {\it Journal of
Computation and Mathematics} 1, London Math. Society, December 1998.  See URL 
{\tt http://www.onr.com/user/russ/david/k7-div-sqrt.html}.

\bibitem{mult}Russinoff, D.\ and Flatau, A., ``RTL Verification: A Floating-Point Multiplier'',
in Kaufmann, M., Manolios, P., and Moore, J, eds., {\it Computer-Aided Reasoning: ACL2 Case Studies},
Kluwer Academic Press, 2000.  See URL {\tt http://www.onr.com/user/russ/david/acl2.html}.

\bibitem{fplib}Russinoff, D., ``An ACL2 Library of Floating-Point Arithmetic'', 1999.
See URL {\tt http://www.cs.utexas.edu/users/moore/publications/others/\-fp-README.html}.

\end{thebibliography}


\end{document}
