\documentclass{article}

\usepackage{epic,eepic,url,subfigure,pstricks,graphicx,alltt,float}
%-------------------------------------------------------------------------------
% Mathematics (from Juliano)
%-------------------------------------------------------------------------------
\newcommand{\mE}[1]{\ensuremath{\mathit{#1}}} % Math environment
\newcommand{\argm}[1]{\ensuremath{\vec{#1}}} % list of arguments or parameters
\newcommand{\VAR}[1]{\ensuremath{\mathit{#1}}} % variable
\newcommand{\OR}{\ensuremath{\vee}} % logical OR
\newcommand{\AND}{\ensuremath{\wedge}} % logical AND
\newcommand{\NOT}{\ensuremath{\neg}} % logical NOT
%\newcommand{\IF}[3]{\ensuremath{#1\, \rightarrow\, #2\, \mid\ #3}} % logical IF
\newcommand{\IF}[3]{\ensuremath{\texttt{if}~#1~\texttt{then}~#2~\texttt{else}~#3}} % logical IF
\newcommand{\TURNST}{\ensuremath{\vdash}} % turnstile
\newcommand{\IMP}{\ensuremath{\Rightarrow}} % implies
\newcommand{\FIMP}{\ensuremath{\Longrightarrow}} % implies
\newcommand{\NIMP}{\ensuremath{\not\supset}} % doesn't imply
\newcommand{\DEF}[1]{\ensuremath{\mathsf{#1}}} % definition
\newcommand{\sVAR}[2]{\ensuremath{\mE{#1}_{#2}}} % variable with subscript
\newcommand{\LAMBDA}[2]{\ensuremath{\lambda\, #1.\ #2}} % lambda abstraction
\newcommand{\COMP}[2]{\ensuremath{#1 \circ #2}} % function compositon
\newcommand{\MULT}{\ensuremath{\cdot}} % multiplication

\suppressfloats[h]

% added by MJCG
\newcommand{\TY}[1]{\ensuremath{\sl{#1}}} % type
\newcommand{\TT}[1]{\ensuremath{\texttt{#1}}} % keyword

\newcommand\bigtiny{\scriptsize}

\newcommand{\imp}{\Rightarrow}
\newcommand{\ie}{{\it i.e.}}
\newcommand{\eg}{{\it e.g.}}
\newcommand{\etc}{{\it etc}}
\newcommand{\konst}[1]{\ensuremath{\mbox{\small{\textbf{\sf{#1}}}}}}

\textwidth 14.5cm
\setlength{\hoffset}{-1.5cm} 
\setlength{\voffset}{-0.5cm} 
\textheight 21cm

\renewcommand\familydefault{\sfdefault}

\begin{document}

%\pagestyle{empty}

\begin{center}
{\LARGE\bf FAQ for Proof Producing Synthesis in HOL}\\[2.0mm]
Konrad Slind, Scott Owens, Juliano Iyoda, Mike Gordon\\[0.5mm]
[Project web page: \url{http://www.cl.cam.ac.uk/~mjcg/dev/}]
\end{center}

%\vspace{10mm}


\section{What is proof producing synthesis?}

\begin{quote}
Proof producing synthesis compiles a source specification
(see~\ref{synthSubset}) to an implementation and generates a theorem
certifying that the implementation is correct. The specification is
expressed in higher order logic.
\end{quote}


\section{What is the synthesisable subset of HOL?}\label{synthSubset}

\begin{quote}
The compiler automatically translates functions $f :
\sigma_1\times\cdots\times\sigma_m \rightarrow
\tau_1\times\cdots\times\tau_n$, where the argument ($\sigma_i$) and
result ($\tau_j$) types are words.  It can translate any tail
recursive definition of such a function as long as the sub-functions
used in the definition are in the library of primitive or previously
defined functions. Formal refinement into this subset is by
proof in the HOL4 system (\ref{highLevel}, \ref{linRec}, \ref{simpleEx}, \ref{let}, \ref{TEA}
have more discussion and examples).
\end{quote}

\section{Why not verify synthesis functions?}

\begin{quote}
Synthesis functions would need to be coded inside higher order logic
if they were to be proved correct.  This would be impractical as the
compiler uses many HOL4 system tools to automatically infer
circuits -- it would not be feasible to represent these tools (a
substantial chunk of the HOL4 theorem proving infrastructure) in higher
order logic.
\end{quote}

\section{Is proof producing synthesis really theorem-proving?}

\begin{quote}
The compiler that synthesises circuits is a derived proof rule
in the HOL4 system which is implemented by rewriting and  a variety of
custom proof strategies. It is a special purpose automatic theorem prover 
for proving correctness certifying theorems (see~\ref{certThm}).
\end{quote}

\section{Is proof producing synthesis the same as formal synthesis?}

\begin{quote}
Proof producing synthesis is a kind of formal synthesis \cite{kumar96formal} in which the synthesised
circuit is not only formally inferred from the specification, but, in addition,
a certifying theorem is produced (see~\ref{related} also).
\end{quote}

\section{Are there benefits of formal synthesis besides assurance?}\label{benefits}

\begin{quote}
Formal synthesis by theorem proving ensures that circuits are correct
by construction. Users can safely tinker with the proof scripts used
by the compiler, confident that they cannot produce incorrect
implementations. Users familiar with the underlying HOL4 theorem proving
infrastructure can easily experiment with application-specific
extensions or optimisations. An example of an optimisation is combinational inlining
(see~\ref{handshakeExplosion}). An example of an extension is \texttt{let}-expressions
(see~\ref{let}). Safe extensibility is thus a benefit.
\end{quote}

\section{Why use proof producing synthesis for crypto hardware?}\label{crypto}

\begin{quote}
Implementations of cryptographic algorithms are evaluated to a high
standard of assurance such as Common Criteria Evaluation Assurance
Level 7 (EAL7) \cite[5.9]{CC}.  Formal methods are an established technique in this
area.  Proof producing synthesis provides a new way of
certifying that cryptographic hardware implements high level
specifications.
\end{quote}

\section{Formal synthesis is an old idea, so why is it still interesting?}

\begin{quote}
In the past it has been hard to justify the high cost of formal
synthesis -- the additional confidence of correctness it produces has
not been considered worth the expense. However, we think there are
niche applications (see~\ref{crypto}) where the approach could be cost
effective, because it may make it easier to achieve required levels of
assurance. Also, we think that safe extensibility (see~\ref{benefits})
is a feature that
is worth exploring more.
\end{quote}

\section{Is proof producing synthesis automatic?}

\begin{quote}
The synthesis of clocked synchronous circuits from tail recursive
definitions of functions mapping words to words is fully automatic.
Currently users must manually refine specifications that use general
recursion schemes to tail recursive form (there is a tool in
development to automatically compile linear recursion to tail
recursion). Data refinement from functions operating on types other
than words must also be done manually.
\end{quote}

\section{What is the hardware realisation of a HOL function?}

\begin{quote}
A function $f$ defined in higher
order logic is realised by a device
\texttt{DEV$\;f$} that computes $f$ via a four-phase handshake circuit
on signals \texttt{load}, \texttt{inp}, \texttt{done} and
\texttt{out}.

\medskip

\hspace*{5mm}\input{device.eepic}

At the start of a transaction (say at
time~$t$) the device must be outputting \DEF{T} on \texttt{done} (to
indicate it is ready) and the environment must be asserting \DEF{F} on
\texttt{load}, i.e.~in a state such that a positive edge on
\texttt{load} can be generated.  A transaction is initiated by
asserting (at time $t{+}1$) the value \DEF{T} on \texttt{load},
i.e.~\texttt{load} has a positive edge at time $t{+}1$. This causes
the device to read the value, $v$ say, input on \texttt{inp} (at
time $t{+}1$) and to set \texttt{done} to \DEF{F}.  The device then
becomes insensitive to inputs until \DEF{T} is next asserted on
\texttt{done}, when the computed value $f(v)$
will be output on \texttt{out}. See~\ref{simulation} for an example.

\end{quote}


\section{What is the formal specification of a handshake device?}

\begin{quote}

The specification of the four-phase handshake protocol is represented by
the definition of the predicate \texttt{DEV}, which uses
auxiliary predicates \DEF{Posedge} and \DEF{HoldF}.
A positive edge of a signal is defined as the transition of its
value from low to high, i.e.~from \DEF{F} to \DEF{T}. 
The formula \mE{\DEF{HoldF}\ (t_1,t_2)\ s} says that a
signal \VAR{s} holds a low value \DEF{F} during a half-open interval
starting at \sVAR{t}{1} to just before \sVAR{t}{2}. The formal definitions are:

%\vspace*{-1mm}

$\begin{array}{ll}
\TURNST\ \DEF{Posedge}\ s\ t~ &      = ~ \IF{~t{=}0~}{~\DEF{F}~}{~(\NOT\hspace*{0.8mm} s(t{-}1)\ \AND\ s\ t~})\\
\TURNST\ \DEF{HoldF}\ (t_1,t_2)\ s & = ~ \forall t.\ t_1 \leq t < t_2\ \IMP\ \NOT(s\ t)
\end{array}$

%\vspace*{-1mm}

The behaviour of the handshaking device computing a function $f$ is described by the term 
$\DEF{DEV}\ f\ \VAR{(load,inp,done,out)}$ where:

$\begin{array}{l}
\TURNST\ \DEF{DEV}\ f\ \VAR{(load,inp,done,out)} = \\
~~\quad     (\forall t.\ \VAR{done}\ t\ \AND\ \DEF{Posedge}\ \VAR{load}\ (t{+}1)\ \\
\phantom{~~\quad     (\forall t.~} \IMP \\
\phantom{~~\quad     (\forall t.\ ~ } \exists t'.\ t' > t{+}1\ \AND\ \DEF{HoldF}\ (t{+}1,t')\ \VAR{done}\ \AND \\
\phantom{~~\quad     (\forall t.\ ~ \exists t'.\ }  \VAR{done}\ t'\ \AND\ (\VAR{out}\ t' = f (\VAR{inp}\ (t{+}1))))\ ~  \AND \\
~~\quad (\forall t.\ \VAR{done}\ t\ \AND\ \NOT(\DEF{Posedge}\ \VAR{load}\ (t{+}1))\ \IMP\  \VAR{done}\ (t{+}1)) ~\AND \\
~~\quad (\forall t.\ \NOT(\VAR{done}\ t)\ \IMP\ \exists t'.\ t' > t\ \AND \VAR{done}\ t')
\end{array}$

The first conjunct in the right-hand side specifies that
if the device is available and a positive
edge occurs on \VAR{load}, there exists a time \VAR{t'} in future
when \VAR{done} signals its termination and the output is produced.
The value of the output at time \VAR{t'} is the result
of applying \VAR{f} to the value of the input at time $\VAR{t}{+}1$.
The signal \VAR{done} holds the value \DEF{F} during the computation.
The second conjunct specifies the situation where no call
is made on \VAR{load} and the device simply remains idle.
Finally, the last conjunct states that if the device
is busy, it will eventually finish its computation
and become idle.

\end{quote}

\section{What is the form of a correctness certifying theorem?}\label{certThm}

\begin{quote}

Synthesising a circuit implementing $f :
\sigma_1\times\cdots\times\sigma_m \rightarrow
\tau_1\times\cdots\times\tau_n$ (see~\ref{synthSubset}) proves:


\vspace*{-3mm}

{\small\baselineskip12pt\begin{alltt}
   |- InfRise clk
       ==> CIR\(\sb{f}\)
       ==> DEV \(f\) (load at clk, {\it{inputs}} at clk, done at clk, {\it{outputs}} at clk)
\end{alltt}}

\vspace*{-3mm}

\texttt{CIR}$_f$ is a formula representing a circuit containing
variables \texttt{clk}, \texttt{load}, \texttt{inp1}, $\ldots$,
\texttt{inpm} representing inputs and variables \texttt{done},
\texttt{out1}, $\ldots$, \texttt{outn} representing outputs.  The type
of \texttt{inp$i$} matches $\sigma_i$ and the type of
\texttt{out$j$} matches $\tau_j$.
\texttt{InfRise clk} asserts that clock \texttt{clk} has infinitely many rising edges.
See~\ref{simpleEx} and \ref{TEA} for examples.
The term {\it inputs\/} stands for \texttt{inp1<>$\cdots$<>inpm} which
is the concatenation of the variables \texttt{inp1}, $\ldots$ ,
\texttt{inpm} using the word concatenation operator \texttt{<>} and
{\it outputs\/} is \texttt{out1<>$\cdots$<>outn} representing the
concatenation of the output variables. A term 
\texttt{$s$~at~clk} is the temporal projection of signal $s$
at rising edges of \texttt{clk} (see~\ref{circComponents}, \ref{compilerFlow}).
\end{quote}

\section{Are specifications using high level datatypes synthesisable?}\label{highLevel}

\begin{quote}

During synthesis the compiler generates circuits that use polymorphic
registers and combinational components (i.e.~components having inputs
and outputs of arbitrary types). However, the lower level phases
instantiate all types to words (currently represented as lists of
bits). Thus we can generate circuits with wires carrying abstract
values (e.g.~numbers), but these cannot be refined to a form that can
be input to FPGA tools.
Our intention is that users will derive Boolean level specifications
inside higher order logic using data-refinement methods. Automating
this is a possible future direction.

\end{quote}

\section{Are there tools to translate into the synthesisable subset?}\label{linRec}

\begin{quote}
There is an experimental proof producing tool called \texttt{linRec} that translates
linear recursions to tail recursions. For example it translates:\\[-6mm]
\begin{verbatim}
   FACT n = if n = 0 then 1 else Mult(n, FACT(n-1))
\end{verbatim}

\vspace*{-3mm}

\noindent to:

\vspace*{-3mm}

\newcommand\vsp{\(\vspace*{-4mm}\)}
{\begin{alltt}
   FactIter(n,acc) = if n = 0 then (n,acc) else FactIter(n-1,Mult(n,acc)))
\vsp
   Fact n = SND(FactIter (n,1))
\end{alltt}}

\end{quote}

\vspace*{-4mm}

\section{What hardware components are used in circuits?}\label{circComponents}

\begin{quote}

The compiler generates circuits built from a user-specifiable library
of combinational components, e.g.~\texttt{AND}, \texttt{OR},
\texttt{NOT}, \texttt{MUX}, \texttt{ADD} (the default library is
chosen for use with the Quartus~II FPGA software).  Synthesised
circuits may also contain constants (\texttt{CONSTANT}),
edge-triggered D-type registers with unspecified initial state
(\texttt{Dtype}) and Dtypes that power up into an initial state
storing the value \DEF{T} (\texttt{DtypeT}). Constants and the
registers are specified in higher order logic by:

\smallskip

$\begin{array}{ll}
\DEF{CONSTANT}~v~out & =~\forall t.~out(t) = v \\
\DEF{Dtype}\phantom{\DEF{T}}(clk,d,q)  & = ~\forall t.~ q(t{+}1) = \texttt{if}~\DEF{Rise}~clk~t~\texttt{then}~d~t~\texttt{else}~q~t\\
\DEF{DtypeT}(clk,d,q)                  & = ~(q~0 = \DEF{T}) ~\wedge~ \DEF{Dtype}(clk,d,q)
\end{array}$

where $\DEF{Rise}~s~t$ means signal $s$ has a rising edge starting at time $t$:\\[1mm]
$\begin{array}{l}
\DEF{Rise}~s~t~ = ~ \neg s(t) ~\wedge~ s(t{+}1)
\end{array}$

Both \texttt{Dtype} and \texttt{DtypeT} are implemented in Verilog by
instantiating a single generic register module \texttt{dtype} that is
parametised on its size and initial stored value (see~\ref{multVl}).
\end{quote}

\vspace*{-3mm}

\section{How much do you rely on untrustworthy FPGA tools?}

\begin{quote}
The `sign-off' from logic to EDA tools occurs at the clocked
synchronous RTL level (see~\ref{circComponents}). A circuit
$\texttt{CIR}_f$ (see~\ref{certThm}) is translated to Verilog using a
pretty-printer written in ML, and this Verilog is then fed to FPGA
tools (e.g.~Quartus~II).  FPGA implementations thus rely on the
Verilog pretty-printer and the subsequent industrial tools. Higher
assurance could be gained by taking the proof producing synthesis to a
lower level (e.g. to an FPGA netlist language).
\end{quote}

\section{Can users control how specifications are synthesised?}

\begin{quote}
The architecture of synthesised circuits reflects the input
specification, so can be tuned by adjusting the
higher order logic source.  For example, 
using \texttt{let}-expressions (see~\ref{let}) prevents logic blocks from
being duplicated. There are also user-settable parameters: for
example, modules can be inserted directly as combinational logic
(i.e.~without an enclosing handshake interface) if they are declared
``combinational'' (see~\ref{handshakeExplosion}, \ref{optimise}).
\end{quote}



\section{How efficient is proof producing synthesis?}

\begin{quote}
Because synthesisers invokes a theorem prover it is relatively
slow. Simple one-line examples take a few seconds on a standard
workstation, bigger examples take several minutes.
\end{quote}

\section{How fast are synthesised circuits?}

\begin{quote}
Some simple experiments comparing synthesised and hand coded circuits
suggest that performance is not too bad, but we do not have solid
evidence. However, the user has some control over the amount of
computation per clock cycle via a facility to declare functions to be
inlined as combinational logic, rather that via a handshake
(see~\ref{optimise}). We think the approach will support the creation
of optimised implementations (necessary for crypto applications), but
so far the emphasis has been on proof of concept.
\end{quote}

\section{How large are synthesised circuits?}

\begin{quote}
Some of the bigger examples we have synthesised did not at first fit
onto the FPGAs we are using.  Whole program compaction
(see~\ref{optimise}) and use of \texttt{let} (see~\ref{let}) solved
the problem for these examples, but we still worry that the circuits
are too big.
\end{quote}

\section{How does the hardware compiler work?}\label{compilerFlow}

\begin{quote}
The operation of the compiler can be decomposed into four phases.
\begin{enumerate}
\item Translate $\forall x_1\ldots x_n.~f(x_1,\ldots,x_n)=e$ to 
an equivalent equation $f={\cal{E}}$, where the
expression, ${\cal{E}}$ is built from combinators \DEF{Seq}
(compute in sequence),
\DEF{Par} (compute in parallel), \DEF{Ite} (if-then-else) and \DEF{Rec} (recursion).

\item Replace the combinators \DEF{Seq}, \DEF{Par}, \DEF{Ite} and
\DEF{Rec} with corresponding circuit constructors \DEF{SEQ},
\DEF{PAR}, \DEF{ITE} and \DEF{REC} to create a circuit term and
a theorem that this implements $\DEF{DEV}~f$.

\item Replace circuit constructors with 
cycle-level implementations
and prove a theorem that the resulting design implements $\DEF{DEV}~f$.

\item Introduce a clock and perform temporal projection~\cite{Mel93}
from cycle level 
to a clocked RTL circuit and prove a theorem that the resulting RTL
circuit implements $\DEF{DEV}~f$.

\end{enumerate}
\end{quote}

\section{What are the combinators \DEF{Seq}, \DEF{Par}, \DEF{Ite} and \DEF{Rec}?}\label{swComb}

\begin{quote}




\DEF{Seq}, \DEF{Par}, \DEF{Ite} and \DEF{Rec} are used
to build the combinatory expression ${\cal{E}}$ that is generated when translating
$\forall x_1\ldots x_n.~f(x_1,\ldots,x_n)=e$ to 
$f={\cal{E}}$. They are defined by:


~~~$\begin{array}{ll}
\DEF{Seq}~f_1~f_2     &   = \lambda x.~f_2(f_1~x)\\
\DEF{Par}~f_1~f_2     &   = \lambda x.~(f_1~x,~f_2~x)\\
\DEF{Ite}~f_1~f_2~f_3 &   = \lambda x.~ \TT{if}~f_1~x~\TT{then}~f_2~x~\TT{else}~f_3~x\\
\DEF{Rec}~f_1~f_2~f_3 &   = \lambda x.~\TT{if}~f_1~x~\TT{then}~f_2~x~\TT{else}~\DEF{Rec}~f_1~f_2~f_3~(f_3~x)\\
\end{array}
$


For example:

\vspace*{-3mm}

\begin{alltt}
\( \vdash \DEF{FactIter}(n,acc) = \)
\(     \texttt{if} n=0 \texttt{then} (n,acc) \texttt{else} \DEF{FactIter}(n-1,n{\times}acc) \)
\end{alltt}

\vspace*{-3mm}

\noindent is translated to:

\vspace*{-3mm}

{\baselineskip14pt\begin{alltt}
\( \vdash \DEF{FactIter} =                                                                        \)
\(     \DEF{Rec} (\DEF{Seq} (\DEF{Par} ({\lambda}(n,acc). n) ({\lambda}(n,acc). 0)) ({=}))        \)
\(         (\DEF{Par} ({\lambda}(n,acc). n) ({\lambda}(n,acc). acc))                              \)
\(         (\DEF{Par} (\DEF{Seq} (\DEF{Par} ({\lambda}(n,acc). n) ({\lambda}(n,acc). 1)) ({-}))   \)
\(              (\DEF{Seq} (\DEF{Par} ({\lambda}(n,acc). n) ({\lambda}(n,acc). acc)) ({\times}))) \)
\end{alltt}}

\end{quote}

\section{What components do circuit constructors use?}\label{netlist}

\begin{quote}
The circuit constructors are built using the following components,
which are represented at an unclocked cycle level of abstraction.


~~$\begin{array}{l}
\TURNST\ \DEF{AND}\ (\sVAR{in}{1},\sVAR{in}{2},\VAR{out}) ~ = 
   \forall t.\ \VAR{out}\ t = (\sVAR{in}{1}\ t\ \AND\ \sVAR{in}{2}\ t)\\
\TURNST\ \DEF{OR}\ (\sVAR{in}{1},\sVAR{in}{2},\VAR{out}) ~ =
   \forall t.\ \VAR{out}\ t = (\sVAR{in}{1}\ t\ \OR\ \sVAR{in}{2}\ t)\\
\TURNST\ \DEF{NOT}\ (\VAR{inp},\VAR{out}) ~ = 
   \forall t.\ \VAR{out}\ t = \NOT(\VAR{inp}\ t)\\
\TURNST\ \DEF{MUX} (\VAR{sw,in_1,in_2,out})~ =~
 \forall t.\ out~t =  \IF{sw~t}{in_1~t}{in_2~t}\\
\TURNST\ \DEF{COMB}\ f\ \VAR{(inp,out)} ~ = \forall t.\ \VAR{out}\ t = f (\VAR{inp}\ t)\\
\TURNST\ \DEF{DEL}\ (\VAR{inp},\VAR{out}) ~ = \forall t.\ \VAR{out} (t{+}1) = \VAR{inp}\ t\\
\TURNST\ \DEF{DELT}\ (\VAR{inp},\VAR{out}) ~ = 
    (\VAR{out}\ 0 = \DEF{T})\ \AND\ 
    \forall t.\ \VAR{out} (t{+}1) = \VAR{inp}\ t\\
\TURNST\ \DEF{DFF} (\VAR{d,sel,q})~ =~
 \forall t.\ q (t{+}1) =  \IF{\DEF{Posedge}\ \VAR{sel}\ (t{+}1)}{d (t{+}1)}{q\ t}\\
\TURNST\ \DEF{POSEDGE} (\VAR{inp},\VAR{out}) = 
    \exists c_0~ c_1.\ \DEF{DELT}(\VAR{inp},c_0) \AND
                  \DEF{NOT}(c_0, c_1) \AND \DEF{AND}(c_1,\VAR{inp},\VAR{out})\\
\end{array}$

\end{quote}



\section{What are the circuit constructors \DEF{SEQ}, \DEF{PAR}, \DEF{ITE} and \DEF{REC}?}\label{hwComb}

\begin{quote}

\DEF{SEQ}, \DEF{PAR}, \DEF{ITE} and \DEF{REC} are circuit constructors
that implement \DEF{Seq}, \DEF{Par}, \DEF{Ite} and \DEF{Rec},
respectively (see~\ref{swComb}). They construct circuits that combine
delay elements with combinational logic. The delay elements are
refined to clocked synchronous registers.

The circuit constructors are defined in higher order logic below. The components they use are defined
in~\ref{circComponents} and schematic diagrams of the implementations are in~\ref{circDiagram}.

\noindent Sequential composition of handshaking devices.
\medskip

$\begin{array}{l}
\TURNST\ \DEF{SEQ}\ f\ g\ (\VAR{load,inp,done,out}) = \\
\phantom{\TURNST\ ~~} \exists c_0~ c_1~ c_2~ c_3~ \VAR{data}.\\
\phantom{\TURNST\ ~~\exists~}                      \DEF{NOT} (c_2,c_3) \ \AND \ 
                      \DEF{OR} (c_3,\VAR{load},c_0) \ \AND \  f (c_0,\VAR{inp},c_1,\VAR{data}) \ \AND \\
\phantom{\TURNST\ ~~ \exists~} 
        g (c_1,\VAR{data},c_2,\VAR{out})\ \AND\ 
        \DEF{AND} (c_1,c_2,\VAR{done}) 
\end{array}$

\medskip
\noindent Parallel composition of handshaking devices.
\medskip

$\begin{array}{l}
\TURNST\ \DEF{PAR}\ f\ g\ (\VAR{load,inp,done,out}) = \\
\phantom{\TURNST\ ~}     \exists c_0~c_1~\VAR{start}~\sVAR{done}{1}~\sVAR{done}{2}~
                                 \sVAR{data}{1}~\sVAR{data}{2}~\sVAR{out}{1}~\sVAR{out}{2}.\\
\phantom{\TURNST\ ~~ \exists~}
       \DEF{POSEDGE} (\VAR{load},c_0)\ \AND\  
       \DEF{DEL} (\VAR{done},c_1)\ \AND \ 
       \DEF{AND} (c_0,c_1,\VAR{start})\ \AND\\
\phantom{\TURNST\ ~~ \exists~}
       f (\VAR{start},\VAR{inp},\sVAR{done}{1},\sVAR{data}{1})\ \AND \ 
       g (\VAR{start},\VAR{inp},\sVAR{done}{2},\sVAR{data}{2})\ \AND\\
\phantom{\TURNST\ ~~ \exists~}
       \DEF{DFF} (\sVAR{data}{1},\sVAR{done}{1},\sVAR{out}{1})\ \AND \  
       \DEF{DFF} (\sVAR{data}{2},\sVAR{done}{2},\sVAR{out}{2})\ \AND\\
\phantom{\TURNST\ ~~ \exists~}
       \DEF{AND} (\sVAR{done}{1},\sVAR{done}{2},done)\ \AND \ 
       (\VAR{out} = \LAMBDA{t}{(\sVAR{out}{1}\ t,\sVAR{out}{2}\ t)})
\end{array}$

\medskip
\noindent Conditional composition of handshaking devices.
\medskip

$\begin{array}{l}
\TURNST\ \DEF{ITE}\ e\ f\ g\ (\VAR{load,inp,done,out}) =\\
\phantom{\TURNST\ ~}
   \exists c_0~c_1~c_2~\VAR{start}~\VAR{start'}~\VAR{done\_e}~\VAR{data\_e}~q~ 
                          \VAR{not\_e}~\VAR{data\_f}~\VAR{data\_g}~\VAR{sel}\\
\phantom{\TURNST\ ~\exists }
                  \VAR{done\_f}~\VAR{done\_g}~
                          \VAR{start\_f}~\VAR{start\_g}.\ \\
\phantom{\TURNST\ ~\exists ~}
           \DEF{POSEDGE} (\VAR{load},c_0)\ \AND\
           \DEF{DEL} (\VAR{done},c_1)\ \AND\ \DEF{AND} (c_0,c_1,\VAR{start})\ \AND \\
\phantom{\TURNST\ ~\exists ~}
           e (\VAR{start},\VAR{inp},\VAR{done\_e},\VAR{data\_e})\ \AND\
           \DEF{POSEDGE} (\VAR{done\_e},\VAR{start'})\ \AND \\
\phantom{\TURNST\ ~\exists ~}
           \DEF{DFF} (\VAR{data\_e},\VAR{done\_e},\VAR{sel})\ \AND\
           \DEF{DFF} (\VAR{inp},\VAR{start},q)\ \AND \\
\phantom{\TURNST\ ~\exists ~}
           \DEF{AND} (\VAR{start'},\VAR{data\_e},\VAR{start\_f})\ \AND\
           \DEF{NOT} (\VAR{data\_e},\VAR{not\_e})\ \AND \\
\phantom{\TURNST\ ~\exists ~}
           \DEF{AND} (\VAR{start'},\VAR{not\_e},\VAR{start\_g})\ \AND\
           f (\VAR{start\_f},q,\VAR{done\_f},\VAR{data\_f})\ \AND\\
\phantom{\TURNST\ ~\exists ~}
           g (\VAR{start\_g},q,\VAR{done\_g},\VAR{data\_g})\ \AND\
           \DEF{MUX} (\VAR{sel},\VAR{data\_f},\VAR{data\_g},out)\ \AND \\
\phantom{\TURNST\ ~\exists ~}
           \DEF{AND} (\VAR{done\_e},\VAR{done\_f},c_2)\ \AND\
           \DEF{AND} (c_2,\VAR{done\_g},\VAR{done})
\end{array}$

\medskip
\noindent Tail recursion constructor.
\medskip


$\begin{array}{l}
\TURNST\ \DEF{REC}\ e\ f\ g\ (\VAR{load,inp,done,out}) = \\
\phantom{\TURNST\ ~}
     \exists \VAR{done\_g}~ \VAR{data\_g}~ \VAR{start\_e}~ q~ \VAR{done\_e}~ 
             \VAR{data\_e}~ \VAR{start\_f}~ \VAR{start\_g}~ \VAR{inp\_e}~ 
             \VAR{done\_f}\\
\phantom{\TURNST\ ~\exists }
             \sVAR{c}{0}~ \sVAR{c}{1}~ 
             \sVAR{c}{2}~ \sVAR{c}{3}~\sVAR{c}{4}~
             \VAR{start}~ \VAR{sel}~ \VAR{start'}~ \VAR{not\_e}. \\
\phantom{\TURNST\ ~\exists~ }
        \DEF{POSEDGE}(\VAR{load},\sVAR{c}{0})\ \AND\
        \DEF{DEL}(\VAR{done},\sVAR{c}{1})\ \AND\
        \DEF{AND}(\sVAR{c}{0},\sVAR{c}{1},\VAR{start})\ \AND \\
\phantom{\TURNST\ ~\exists~ }
        \DEF{OR}(\VAR{start,sel,start\_e})\ \AND\
        \DEF{POSEDGE}(\VAR{done\_g,sel})\ \AND \\
\phantom{\TURNST\ ~\exists~ }
        \DEF{MUX}(\VAR{sel,data\_g,inp,inp\_e})\ \AND\
           \DEF{DFF}(\VAR{inp\_e},\VAR{start\_e},q)\ \AND \\
\phantom{\TURNST\ ~\exists~ }
           e (\VAR{start\_e},\VAR{inp\_e},\VAR{done\_e},\VAR{data\_e}) \AND\
        \DEF{POSEDGE}(\VAR{done\_e,start'})\ \AND \\
\phantom{\TURNST\ ~\exists~ }
        \DEF{AND}(\VAR{start',data\_e,start\_f})\ \AND\
        \DEF{NOT}(\VAR{data\_e,not\_e})\ \AND \\
\phantom{\TURNST\ ~\exists~ }
        \DEF{AND}(\VAR{not\_e,start',start\_g})\ \AND\
           f (\VAR{start\_f},q,\VAR{done\_f},\VAR{out})\ \AND\\
\phantom{\TURNST\ ~\exists~ }
           g (\VAR{start\_g},q,\VAR{done\_g},\VAR{data\_g})\ \AND\
        \DEF{DEL}(\VAR{done\_g},\sVAR{c}{3})\ \AND\\ 
\phantom{\TURNST\ ~\exists~ }
        \DEF{AND}(\VAR{done\_g},\sVAR{c}{3},\sVAR{c}{4})\ \AND\
        \DEF{AND}(\VAR{done\_f},\VAR{done\_e},\sVAR{c}{2})\ \AND\
        \DEF{AND}(\sVAR{c}{2},\sVAR{c}{4},\VAR{done})
\end{array}$

\end{quote}

\vspace*{-3mm}

\section{How are combinational circuits represented?}\label{comb}

\begin{quote}
A function $f$ can be packaged as a handshaking device with
constructor \DEF{ATM}:



$\begin{array}{l}
\TURNST\ \DEF{ATM}\ f\ (\VAR{load,inp,done,out}) =\\
\phantom{\TURNST\ ~~}    \exists c_0~ c_1.\ \DEF{POSEDGE} (\VAR{load}, c_0) \AND 
\DEF{NOT} (c_0, \VAR{done}) \AND \\
\phantom{\TURNST\ ~~\exists c_0, c_1.\ } 
 \DEF{COMB}\ f\ (\VAR{inp},c_1) \AND \DEF{DEL} (c_1,\VAR{out})
\end{array}$



This creates a simple handshake interface that computes $f$ and
satisfies the refinement theorem: $\TURNST\ \forall f.~\DEF{ATM}\ f\
\FIMP \ \DEF{DEV}\ f$.



Formulas of the form $\DEF{COMB}~g~(inp,out)$ are compiled
into circuits built only using components in user-supplied library of predefined  circuits.
The default library  currently includes Boolean functions (e.g. $\wedge$,
$\vee$ and $\neg$), multiplexers and simple operations  on $n$-bit words (e.g.~versions
of $+$, $-$ and $<$, various shifts etc.). 
A special purpose proof rule uses a recursive algorithm to synthesise
combinational circuits. For example:

\vspace*{-2mm}

{\begin{alltt}
\( \vdash \DEF{COMB}\ ({\lambda}(m,n). (m<n, m+1))\ (inp\sb{1}\texttt{<>}inp\sb{2},out\sb{1}\texttt{<>}out\sb{2}) =              \)
\(     {\exists}v\sb{0}. \DEF{COMB}\ ({<})\ (inp\sb{1}\texttt{<>}inp\sb{2},out\sb{1}) \wedge \DEF{CONSTANT} 1 v\sb{0} \wedge \)
\(         \! \DEF{COMB}\ ({+})\ (inp\sb{1}\texttt{<>}v\sb{0},out\sb{2})                                              \)
\end{alltt}}

\vspace*{-2mm}

\noindent where \texttt{<>} is bus concatenation,
$\DEF{CONSTANT}~1~v_0$ drives $v_0$ high continuously, and
$\DEF{COMB}~{<}$ and $\DEF{COMB}~{+}$ are assumed
given components (if they were not given, then they could be
implemented explicitly, but one has to stop somewhere). 

\end{quote}


\section{How is an explosion of internal handshakes avoided?}\label{handshakeExplosion}

\begin{quote}
When processing $\DEF{Seq}~f_1~f_2$ (see \ref{introConstructors}), the compiler checks to see whether $f_1$ or $f_2$ 
are compositions of combinational functions and if so introduces \DEF{PRECEDE} or \DEF{FOLLOW} instead of \DEF{SEQ},
using the theorems:


$\begin{array}{l}
~\TURNST\
      (P\ \FIMP\ \DEF{DEV}~f_2)~\IMP~(\DEF{PRECEDE}~f_1~P\ \FIMP\ \DEF{DEV}\ (\DEF{Seq}~f_1~f_2))\\
~\TURNST\
(P\ \FIMP\ \DEF{DEV}~f_1)~\IMP~(\DEF{FOLLOW}~P~f_2\  \FIMP\ \DEF{DEV}\ (\DEF{Seq}~f_1~f_2))\\
\end{array}$


where $\DEF{PRECEDE}~f~d$ processes inputs with $f$ before sending them to $d$ and
$\DEF{FOLLOW}~d~f$ processes outputs of $d$ with
$f$. The definitions are:

\medskip

$\tt\begin{array}{l}
\DEF{PRECEDE}~f~d~(load,inp,done,out)  =
 \exists v.~ \DEF{COMB}~f~(inp,v) ~\wedge~ d(load,v,done,out)\\
 \\[-4mm]
\DEF{FOLLOW}~d~f~ (load,inp,done,out)\hspace{2mm}  =
 \exists v.~d(load,inp,done,v) ~\wedge~ \DEF{COMB}~f~(v,out)
\end{array}$

\medskip

$\DEF{SEQ}~d_1~d_2$ introduces a handshake between the executions
of $d_1$ and $d_2$, but $\DEF{PRECEDE}~f~d$ and $\DEF{FOLLOW}~d~f$
just `wire' $f$ before or after $d$ without introducing a
handshake.
\end{quote}


\section{How are the circuit constructors introduced?}\label{introConstructors}

\begin{quote}
The
following theorems enable the compiler to compositionally deduce theorems
of the form $\vdash {\it{Imp}} \Longrightarrow \DEF{DEV}~f$, where
${\it{Imp}}$ is a formula constructed using the circuit constructors.
The long arrow symbol
$\Longrightarrow$ denotes implication lifted to functions:\\
%-- i.e.~$f\Longrightarrow g~=~\forall x.~f(x)\Rightarrow g(x)$):
$f\Longrightarrow g~=~\forall 
\mbox{\it\small{load}}\;\mbox{\it\small{inp}}\;\mbox{\it\small{done}}\;\mbox{\it\small{out}}.
~f(\mbox{\it\small{load}},\mbox{\it\small{inp}},\mbox{\it\small{done}},\mbox{\it\small{out}})
\Rightarrow 
g(\mbox{\it\small{load}},\mbox{\it\small{inp}},\mbox{\it\small{done}},\mbox{\it\small{out}})$.

\smallskip

$\begin{array}{l}

~\TURNST\
(P_1\ \FIMP\ \DEF{DEV}~f_1)~\AND~(P_2 \ \FIMP\ \DEF{DEV}~f_2)\\
\phantom{~\TURNST~}
~ \IMP ~
(\DEF{SEQ}\ P_1\ P_2 \ \FIMP \ \DEF{DEV}\ (\DEF{Seq}~f_1~f_2))

\end{array}$

$\begin{array}{l}


~\TURNST\ 
(P_1 \ \FIMP\ \DEF{DEV}~f_1)~\AND~(P_2 \ \FIMP\ \DEF{DEV}~f_2)\\
\phantom{~\TURNST~}
~ \IMP ~
(\DEF{PAR}\ P_1\ P_2\ \FIMP \ \DEF{DEV}\ (\DEF{Par}~f_1~f_2))


\end{array}$

$\begin{array}{l}



~\TURNST\ 
(P_1 \ \FIMP\ \DEF{DEV}~f_1)~\AND~(P_2 \ \FIMP\ \DEF{DEV}~f_2)~\AND~(P_3 \ \FIMP\ \DEF{DEV}~f_3)\\
\phantom{~\TURNST~}
\IMP ~
(\DEF{ITE}\ P_1\ P_2\ P_3\  \FIMP \ \DEF{DEV}\ (\DEF{Ite}~f_1~f_2~f_3))

\end{array}$

$\begin{array}{l}



~\TURNST\ 
\DEF{Total}(f_1,f_2,f_3)\\
\phantom{~\TURNST~}
\IMP ~
(P_1 \ \FIMP\ \DEF{DEV}~f_1)~\AND~(P_2 \ \FIMP\ \DEF{DEV}~f_2)~\AND~(P_3 \ \FIMP\ \DEF{DEV}~f_3)\\
\phantom{~\TURNST~}
\IMP ~
(\DEF{REC}\ P_1\ P_2\ P_3 \ \FIMP \ \DEF{DEV}\ (\DEF{Rec}~f_1~f_2~f_3))

\end{array}$

\smallskip


\noindent The predicate \DEF{Total} is defined so that $\DEF{Total}(f_1,f_2,f_3)$ ensures termination.

If ${\cal{E}}$ is an expression built using \DEF{Seq}, \DEF{Par},
\DEF{Ite} and \DEF{Rec}, then by instantiating the predicate variables
$P_1$, $P_2$ and $P_3$, these theorems enable a logic formula
${\cal{F}}$ to be built from circuit constructors \DEF{SEQ},
\DEF{PAR}, \DEF{ITE} and \DEF{REC} such that $\vdash {\cal{F}} \FIMP
\DEF{DEV}~{\cal{E}}$. We have $\vdash f={\cal{E}}$ (see
\ref{compilerFlow}, phase 1), hence $\vdash {\cal{F}} \FIMP
\DEF{DEV}~f$. This is the basic idea, but see also
\ref{handshakeExplosion}, \ref{optimise}.

\end{quote}


\section{What optimisation does the compiler perform?}\label{optimise}

\begin{quote} There are currently two main optimisations used in synthesis:
reducing handshakes between implementations
of functions (see~\ref{handshakeExplosion}) and whole program
compaction.

The normal synthesis of \DEF{Seq}~$f_1~f_2$ (see~\ref{swComb}) is to
\DEF{SEQ}~$d_1~d_2$ (see~\ref{hwComb}), where the circuit combinator
\DEF{SEQ} puts a handshake between the device $d_1$ implementing
$f_1$ and the device $d_2$ implementing $f_2$. Users may declare $f_1$
to be `combinational' and then a combinational logic block $c_1$
implementing $f_1$ is synthesised and put in series before
$d_2$. Similarly $f_2$ can be declared combinational and then
combinational logic $c_2$ will be put in series after $d_1$. Only
components that can be realised using known combinational logic blocks
can be declared combinational. Using this mechanism, all the
computation from the arguments of a function to its recursive call can
be synthesised as combinational logic, so there is just a single
handshake to manage the iteration.

This optimisation is restricted to the scope
of a single function. However, before applying this method,
we can inline the function calls to produce a system
defined by a single function (the function 'main').
The whole program compaction eliminates unnecessary
handshake circuits that could have been generated
to implement the function calls.

In practise these techniques can generate long
logic paths (i.e.~slow clocks), so some pipelining
via internal handshakes can be appropriate.
\end{quote}

\section{What do the circuit constructor implementations look like?}\label{circDiagram}

%\suppressfloats

\begin{figure}[H]
   \centerline{
      \subfigure[$\DEF{POSEDGE}$]{
         \label{figPosedge}\input{posedge.eepic}\hspace*{-5mm}}
      \subfigure[$\DEF{ATM}\ f$]{
         \label{figAtom}\input{atm.eepic}\hspace*{-0.4cm}}
      \subfigure[$\DEF{SEQ}\ f\ g$]{
         \label{figSeq}\input{seq.eepic}\hspace*{-2mm}}
      \subfigure[$\DEF{PAR}\ f\ g$]{
         \label{figPar}\input{par.eepic}}}
%\end{figure}
%\begin{figure}[H]
   \centerline{
       \subfigure[$\DEF{IF}\ e\ f\ g$]{
           \label{figIf}\input{ifReduced.eepic}\hspace*{0.3cm}}
       \subfigure[$\DEF{REC}\ e\ f\ g$]{
           \label{figRec}\input{recReduced.eepic}\hspace*{0cm}}}
\end{figure}


\section{How do \texttt{let}-expressions work?}\label{let}

\begin{quote}
A \texttt{let}-expression has the form
\texttt{let~$v$~=~$e_1$~in~$e_2$} where $v$ is a ``varstruct''
(variable structure) which is either a single variable or,
recursively, a non-empty tuple of varstructs
(e.g.~\texttt{(x,(m,n),y)}).  

If $e_1$ is combinational, then a
\texttt{let}-expression is synthesised into a circuit consisting of
$e_1$ driving wires corresponding to $v$ that are inputs to the circuit
corresponding to $e_2$. 

If $e_1$ is not combinational, the \texttt{let}-expression is compiled
using:

~~$\TURNST\ \forall f_1~f_2.~(\lambda x.~\texttt{let}~v~=~f_1~x~\texttt{in}~f_2~(x,v))~=~\DEF{Seq}~(\DEF{Par}~(\lambda x.~x)~f_1)~f_2$

For example, suppose \texttt{H} and \texttt{J} are defined by:

\vspace*{-2mm}

\begin{verbatim}
 H x = x+1w
 J x = let y = H x in y + y + y
\end{verbatim}

\vspace*{-2mm}

where \texttt{1w} is the 32-bit word denoting $1$ and \texttt{+} is 32-bit addition.

If \texttt{H} is not declared combinational, then \texttt{J} compiles to:

\vspace*{-2mm}

{\bigtiny\begin{alltt}
    |- InfRise clk ==>
       (\(\exists\)v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 
          v22 v23 v24 v25 v26 v27.
          DtypeT (clk,load,v10) \(\wedge\) NOT (v10,v9) \(\wedge\) AND (v9,load,v8) \(\wedge\) Dtype (clk,done,v7) \(\wedge\) 
          AND (v8,v7,v6) \(\wedge\) DtypeT (clk,v6,v13) \(\wedge\) NOT (v13,v12) \(\wedge\) AND (v12,v6,v11) \(\wedge\) 
          NOT (v11,v5) \(\wedge\) Dtype (clk,inp,v3) \(\wedge\) DtypeT (clk,v6,v17) \(\wedge\) NOT (v17,v16) \(\wedge\)
          AND (v16,v6,v15) \(\wedge\) NOT (v15,v4) \(\wedge\) CONSTANT 1w v18 \(\wedge\) ADD32 (inp,v18,v14) \(\wedge\) 
          Dtype (clk,v14,v2) \(\wedge\) DtypeT (clk,v5,v21) \(\wedge\) NOT (v21,v20) \(\wedge\) AND (v20,v5,v19) \(\wedge\)
          MUX (v19,v3,v22,v1) \(\wedge\) Dtype (clk,v1,v22) \(\wedge\) DtypeT (clk,v4,v25) \(\wedge\) NOT (v25,v24) \(\wedge\) 
          AND (v24,v4,v23) \(\wedge\) MUX (v23,v2,v26,v0) \(\wedge\) Dtype (clk,v0,v26) \(\wedge\) AND (v5,v4,done) \(\wedge\)
          ADD32 (v0,v0,v27) \(\wedge\) ADD32 (v27,v0,out)) ==>
       DEV J (load at clk,inp at clk,done at clk,out at clk) 
\end{alltt}}

\vspace*{-2mm}

but if \texttt{H} is declared to be combinational, then \texttt{J} compiles to:

\vspace*{-2mm}
{\bigtiny\begin{alltt}
    |- InfRise clk ==>
       (\(\exists\)v0 v1 v2 v3 v4 v5 v6.
          DtypeT (clk,load,v3) \(\wedge\) NOT (v3,v2) \(\wedge\) AND (v2,load,v1) \(\wedge\) NOT (v1,done) \(\wedge\) 
          CONSTANT 1w v5 \(\wedge\) ADD32 (inp,v5,v4) \(\wedge\) ADD32 (v4,v4,v6) \(\wedge\) ADD32 (v6,v4,v0) \(\wedge\) 
          Dtype (clk,v0,out)) ==>
       DEV J (load at clk,inp at clk,done at clk,out at clk) 
\end{alltt}}
\end{quote}




\section{What is a simple example?}\label{simpleEx}

\begin{quote}
A simple example is iterative
accumulator-style multiplication on 32-bit words:

%\vspace*{-1mm}

{\begin{verbatim}
 Mult32Iter(m,n,acc) = 
  if m = 0w then (0w, n, acc) else Mult32Iter(m-1w, n, n+acc)
\end{verbatim}}

%\vspace*{-1mm}

where \texttt{0w}, \texttt{1w} are 32-bit numbers and \texttt{+},
\texttt{-} are 32-bit operations. 

This specification compiles to:

%\vspace*{-1mm}

{\bigtiny\begin{alltt}
     |- InfRise clk ==>
       (\(\exists\;\)v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 
          v24 v25 v26 v27 v28 v29 v30 v31 v32 v33 v34 v35 v36 v37 v38 v39 v40 v41 v42 v43 v44 
          v45 v46 v47 v48 v49 v50 v51 v52 v53 v54 v55 v56 v57.
           DtypeT (clk,load,v21) \(\wedge\) NOT (v21,v20) \(\wedge\) AND (v20,load,v19) \(\wedge\) Dtype (clk,done,v18) \(\wedge\) 
           AND (v19,v18,v17) \(\wedge\) OR (v17,v16,v11) \(\wedge\) DtypeT (clk,v15,v23) \(\wedge\) NOT (v23,v22) \(\wedge\) 
           AND (v22,v15,v16) \(\wedge\) MUX (v16,v14,inp1,v3) \(\wedge\) MUX (v16,v13,inp2,v2) \(\wedge\) 
           MUX (v16,v12,inp3,v1) \(\wedge\) DtypeT (clk,v11,v26) \(\wedge\) NOT (v26,v25) \(\wedge\) AND (v25,v11,v24) \(\wedge\) 
           MUX (v24,v3,v27,v10) \(\wedge\) Dtype (clk,v10,v27) \(\wedge\) DtypeT (clk,v11,v30) \(\wedge\) NOT (v30,v29) \(\wedge\)
           AND (v29,v11,v28) \(\wedge\) MUX (v28,v2,v31,v9) \(\wedge\) Dtype (clk,v9,v31) \(\wedge\) DtypeT (clk,v11,v34) \(\wedge\) 
           NOT (v34,v33) \(\wedge\) AND (v33,v11,v32) \(\wedge\) MUX (v32,v1,v35,v8) \(\wedge\) Dtype (clk,v8,v35) \(\wedge\)
           DtypeT (clk,v11,v39) \(\wedge\) NOT (v39,v38) \(\wedge\) AND (v38,v11,v37) \(\wedge\) NOT (v37,v7) \(\wedge\) 
           CONSTANT 0w v40 \(\wedge\) EQ32 (v3,v40,v36) \(\wedge\) Dtype (clk,v36,v6) \(\wedge\) DtypeT (clk,v7,v44) \(\wedge\) 
           NOT (v44,v43) \(\wedge\) AND (v43,v7,v42) \(\wedge\) AND (v42,v6,v5) \(\wedge\) NOT (v6,v41) \(\wedge\) AND (v41,v42,v4) \(\wedge\) 
           DtypeT (clk,v5,v48) \(\wedge\) NOT (v48,v47) \(\wedge\) AND (v47,v5,v46) \(\wedge\) NOT (v46,v0) \(\wedge\) 
           CONSTANT 0w v45 \(\wedge\) Dtype (clk,v45,out1) \(\wedge\) Dtype (clk,v9,out2) \(\wedge\) Dtype (clk,v8,out3) \(\wedge\) 
           DtypeT (clk,v4,v53) \(\wedge\) NOT (v53,v52) \(\wedge\) AND (v52,v4,v51) \(\wedge\) NOT (v51,v15) \(\wedge\) 
           CONSTANT 1w v54 \(\wedge\) SUB32 (v10,v54,v50) \(\wedge\) ADD32 (v9,v8,v49) \(\wedge\) Dtype (clk,v50,v14) \(\wedge\)
           Dtype (clk,v9,v13) \(\wedge\) Dtype (clk,v49,v12) \(\wedge\) Dtype (clk,v15,v56) \(\wedge\) AND (v15,v56,v55) \(\wedge\) 
           AND (v0,v7,v57) \(\wedge\) AND (v57,v55,done)) ==>
       DEV Mult32Iter (load at clk, (inp1<>inp2<>inp3) at clk, done at clk, (out1<>out2<>out3) at clk)
\end{alltt}}

See \ref{certThm} and \ref{circComponents} for  explanations and~\ref{multVl} for the
Verilog that is extracted from this circuit.
\end{quote}

\section{What is the generated Verilog like?}\label{multVl}

\vspace*{-1mm}

The iterative accumulator-style multiplication device
(see~\ref{simpleEx}) generates the following Verilog.

\vspace*{-1mm}

{\bigtiny\baselineskip6.5pt\begin{verbatim}
   module dtype (clk,d,q);
    parameter size = 31; parameter value = 1; 
    input clk; input [size:0] d; output [size:0] q; reg [size:0] q = value;
   
    always @(posedge clk) q <= d;
   
   endmodule
   
   module Mult32Iter (clk,load,inp1,inp2,inp3,done,out1,out2,out3);
    input clk,load; input [31:0] inp1; input [31:0] inp2; input [31:0] inp3;
    output done; output [31:0] out1; output [31:0] out2; output [31:0] out3;
    wire clk,done; wire [0:0] v0; wire [31:0] v1; wire [31:0] v2; wire [31:0] v3; wire [0:0] v4; 
    wire [0:0] v5; wire [0:0] v6; wire [0:0] v7; wire [31:0] v8; wire [31:0] v9; wire [31:0] v10; 
    wire [0:0] v11; wire [31:0] v12; wire [31:0] v13; wire [31:0] v14; wire [0:0] v15; 
    wire [0:0] v16; wire [0:0] v17; wire [0:0] v18; wire [0:0] v19; wire [0:0] v20; wire [0:0] v21; 
    wire [0:0] v22; wire [0:0] v23; wire [0:0] v24; wire [0:0] v25; wire [0:0] v26; wire [31:0] v27; 
    wire [0:0] v28; wire [0:0] v29; wire [0:0] v30; wire [31:0] v31; wire [0:0] v32; wire [0:0] v33;
    wire [0:0] v34; wire [31:0] v35; wire [0:0] v36; wire [0:0] v37; wire [0:0] v38; wire [0:0] v39; 
    wire [31:0] v40; wire [0:0] v41; wire [0:0] v42; wire [0:0] v43; wire [0:0] v44; wire [31:0] v45; 
    wire [0:0] v46; wire [0:0] v47; wire [0:0] v48; wire [31:0] v49; wire [31:0] v50; wire [0:0] v51;
    wire [0:0] v52; wire [0:0] v53; wire [31:0] v54; wire [0:0] v55; wire [0:0] v56; wire [0:0] v57;
   
    dtype   dtype_0 (clk,load,v21);   defparam dtype_0.size = 0;
    assign v20 = ~ v21;
    assign v19 = v20 && load;
    dtype   dtype_1 (clk,done,v18);   defparam dtype_1.size = 0;
    assign v17 = v19 && v18;
    assign v11 = v17 || v16;
    dtype   dtype_2 (clk,v15,v23);    defparam dtype_2.size = 0;
    assign v22 = ~ v23;
    assign v16 = v22 && v15;
    assign v3 = v16 ? v14 : inp1;
    assign v2 = v16 ? v13 : inp2;
    assign v1 = v16 ? v12 : inp3;
    dtype   dtype_3 (clk,v11,v26);    defparam dtype_3.size = 0;
    assign v25 = ~ v26;
    assign v24 = v25 && v11;
    assign v10 = v24 ? v3 : v27;
    dtype   dtype_4 (clk,v10,v27);    defparam dtype_4.size = 31;
    dtype   dtype_5 (clk,v11,v30);    defparam dtype_5.size = 0;
    assign v29 = ~ v30;
    assign v28 = v29 && v11;
    assign v9 = v28 ? v2 : v31;
    dtype   dtype_6 (clk,v9,v31);     defparam dtype_6.size = 31;
    dtype   dtype_7 (clk,v11,v34);    defparam dtype_7.size = 0;
    assign v33 = ~ v34;
    assign v32 = v33 && v11;
    assign v8 = v32 ? v1 : v35;
    dtype   dtype_8 (clk,v8,v35);     defparam dtype_8.size = 31;
    dtype   dtype_9 (clk,v11,v39);    defparam dtype_9.size = 0;
    assign v38 = ~ v39;
    assign v37 = v38 && v11;
    assign v7 = ~ v37;
    assign v40 = 0;
    assign v36 = v3 == v40;
    dtype   dtype_10 (clk,v36,v6);    defparam dtype_10.size = 0;
    dtype   dtype_11 (clk,v7,v44);    defparam dtype_11.size = 0;
    assign v43 = ~ v44;
    assign v42 = v43 && v7;
    assign v5 = v42 && v6;
    assign v41 = ~ v6;
    assign v4 = v41 && v42;
    dtype   dtype_12 (clk,v5,v48);    defparam dtype_12.size = 0;
    assign v47 = ~ v48;
    assign v46 = v47 && v5;
    assign v0 = ~ v46;
    assign v45 = 0;
    dtype   dtype_13 (clk,v45,out1);  defparam dtype_13.size = 31;
    dtype   dtype_14 (clk,v9,out2);   defparam dtype_14.size = 31;
    dtype   dtype_15 (clk,v8,out3);   defparam dtype_15.size = 31;
    dtype   dtype_16 (clk,v4,v53);    defparam dtype_16.size = 0;
    assign v52 = ~ v53;
    assign v51 = v52 && v4;
    assign v15 = ~ v51;
    assign v54 = 1;
    assign v50 = v10 - v54;
    assign v49 = v9 + v8;
    dtype   dtype_17 (clk,v50,v14);   defparam dtype_17.size = 31;
    dtype   dtype_18 (clk,v9,v13);    defparam dtype_18.size = 31;
    dtype   dtype_19 (clk,v49,v12);   defparam dtype_19.size = 31;
    dtype   dtype_20 (clk,v15,v56);   defparam dtype_20.size = 0;
    assign v55 = v15 && v56;
    assign v57 = v0 && v7;
    assign done = v57 && v55;
    
   endmodule
\end{verbatim}}

\begin{quote}
To conserve space, all comments and many line breaks have been removed
from the preceding Verilog.  Each Verilog statement is printed
with a comment showing the HOL source to aid visual checking (e.g.~for
Common Criteria EAL7 certification evaluators \cite[5.9]{CC}). We are
still tinkering with the Verilog: for example, experiments show
that Quartus II configures Altera FPGAs to initialise faster 
with registers as instances of a separate module (\texttt{dtype}
above) than with inlined behavioral statements
{\verb+always @(posedge clk) q <= d+}, where \texttt{q} is
initialised with declaration {\verb+reg q = 1+}.

\end{quote}

\section{What simulation tools have you used?}\label{simulation}

\begin{quote}
We currently use Icarus Verilog (\url{http://www.icarus.com}) for
simulation and then view waveforms with GTKWave
(\url{http://home.nc.rr.com/gtkwave}). These tools are both public
domain.
If we simulate the \texttt{Mult32Iter} example (see~\ref{simpleEx}) with inputs
$(5,7,0)$, then the resulting waveform is:

\hspace*{5mm}\mbox{}\vspace*{0mm}\scalebox{0.53}{\includegraphics[viewport = 0 12 600 210, clip = true]{Mult32IterWave.epsi}}\vspace*{2mm}

\noindent \texttt{load} is asserted at time 15 and \texttt{done} is \DEF{T} then, but \texttt{done} immediately drops to \DEF{F} in response
to \texttt{load} being asserted. At the same time
as \texttt{load} is asserted the values $5$, $7$ and $0$ are put on lines \texttt{inp1},
\texttt{inp2} and \texttt{inp3}, respectively. At time 135 \texttt{done} rises to \DEF{T} again,
and by then the values on \texttt{out1},
\texttt{out2} and \texttt{out3} are $0$, $7$ and $35$, respectively,
thus \texttt{Mult32Iter($5$,$7$,$0$) = ($0$,$7$,$35$)}, which is correct.

\end{quote}


\section{What is a bigger example?}\label{TEA}

% @inproceedings{TEA,
% author={David Wheeler and Roger Needham},
% title={{TEA}, a tiny encryption algorithm},
% booktitle={Fast Software Encryption: Second International Workshop},
% year=1999,publisher={Springer Verlag},series=LNCS,volume=1008,pages="363--366"}

\begin{quote}
An example drawn from cryptography is the TEA block cipher \cite{TEA}. The 
encryption algorithm is described by the following HOL definitions
(all variables are 32-bit words):

\vspace*{-2mm}

{\small\baselineskip9pt
\begin{verbatim}
   TEAEncrypt (keys,txt) = FST(Rounds (32,(txt,keys,0)))

   Rounds (n,s) = if n=0 then s else Rounds(n-1, Round s)

   Round ((y,z),(k0,k1,k2,k3),s) =
     let s' = s + DELTA in
     let t = y + ShiftXor(z,s',k0,k1)
     in
        ((t, z + ShiftXor(t,s',k2,k3)), (k0,k1,k2,k3), s')

   ShiftXor (x,s,k0,k1) = ((x << 4) + k0) # (x + s) # ((x >> 5) + k1)

   DELTA = 0x9e3779b9w
\end{verbatim}}

\vspace*{-2mm}

There is a corresponding \verb+TEADecrypt+ function (omitted). In HOL-4 
we can prove functional correctness:

\vspace*{-2mm}

{\small
\begin{alltt}
   |- \(\forall\)plaintext keys. TEADecrypt(keys,TEAEncrypt(keys,plaintext)) = plaintext
\end{alltt}}

\noindent The compiler generates the following netlist for \verb+TEAEncrypt+
and also one for \verb+TEADecrypt+:

{\bigtiny\baselineskip7.6pt
\begin{alltt}
   |- InfRise clk ==>
       (\(\exists\)v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18
        v19 v20 v21 v22 v23 v24 v25 v26 v27 v28 v29 v30 v31 v32 v33 v34 v35 
        v36 v37 v38 v39 v40 v41 v42 v43 v44 v45 v46 v47 v48 v49 v50 v51 v52 
        v53 v54 v55 v56 v57 v58 v59 v60 v61 v62 v63 v64 v65 v66 v67 v68 v69
        v70 v71 v72 v73 v74 v75 v76 v77 v78 v79 v80 v81 v82 v83 v84 v85 v86
        v87 v88 v89 v90 v91 v92 v93 v94 v95 v96 v97 v98 v99 v100 v101 v102 
        v103 v104 v105 v106 v107 v108 v109 v110 v111 v112 v113 v114 v115 v116
        v117 v118 v119 v120 v121 v122 v123 v124 v125 v126 v127 v128 v129 v130
        v131 v132 v133 v134 v135 v136 v137 v138 v139 v140 v141 v142 v143 v144
        v145 v146 v147 v148 v149 v150 v151 v152 v153 v154 v155 v156 v157 v158
        v159 v160 v161 v162 v163 v164 v165 v166 v167 v168 v169 v170 v171 v172 
        v173 v174 v175 v176 v177 v178 v179 v180 v181 v182 v183 v184 v185 v186
        v187 v188 v189 v190 v191 v192 v193 v194 v195 v196 v197 v198 v199 v200
        v201 v202 v203 v204 v205 v206 v207 v208 v209 v210 v211 v212 v213 v214
        v215 v216 v217 v218 v219 v220 v221 v222 v223 v224 v225 v226 v227 v228
        v229 v230 v231 v232 v233 v234 v235 v236 v237 v238 v239 v240 v241 v242 
        v243 v244 v245 v246 v247 v248 v249 v250 v251 v252 v253 v254 v255 v256
        v257 v258 v259 v260 v261 v262 v263 v264 v265 v266 v267 v268 v269 v270 
        v271 v272 v273 v274 v275 v276 v277 v278 v279 v280 v281 v282 v283 v284
        v285 v286 v287 v288 v289 v290 v291 v292 v293 v294 v295 v296 v297 v298
        v299 v300 v301 v302 v303 v304 v305 v306 v307 v308 v309 v310 v311 v312
        v313 v314 v315 v316 v317 v318 v319 v320 v321 v322 v323 v324 v325 v326 
        v327 v328 v329 v330 v331 v332 v333 v334 v335 v336 v337 v338 v339 v340 
        v341 v342 v343 v344 v345 v346 v347 v348 v349 v350 v351 v352 v353 v354.
          CONSTANT 32w v6 \(\land\) CONSTANT 0w v5 \(\land\) DtypeT (clk,load,v43) \(\land\) 
          NOT (v43,v42) \(\land\) AND (v42,load,v41) \(\land\) Dtype (clk,done,v40) \(\land\) 
          AND (v41,v40,v39) \(\land\) OR (v39,v38,v28) \(\land\) DtypeT (clk,v37,v45) \(\land\)
          NOT (v45,v44) \(\land\) AND (v44,v37,v38) \(\land\) MUX (v38,v36,v6,v15) \(\land\)
          MUX (v38,v35,inp2,v14) \(\land\) MUX (v38,v34,inp3,v13) \(\land\) MUX (v38,v33,inp11,v12) \(\land\) 
          MUX (v38,v32,inp12,v11) \(\land\) MUX (v38,v31,inp13,v10) \(\land\) MUX (v38,v30,inp14,v9) \(\land\)
          MUX (v38,v29,v5,v8) \(\land\) DtypeT (clk,v28,v48) \(\land\) NOT (v48,v47) \(\land\)
          AND (v47,v28,v46) \(\land\) MUX (v46,v15,v49,v27) \(\land\) Dtype (clk,v27,v49) \(\land\) 
          DtypeT (clk,v28,v52) \(\land\) NOT (v52,v51) \(\land\) AND (v51,v28,v50) \(\land\) 
          MUX (v50,v14,v53,v26) \(\land\) Dtype (clk,v26,v53) \(\land\) DtypeT (clk,v28,v56) \(\land\) 
          NOT (v56,v55) \(\land\) AND (v55,v28,v54) \(\land\) MUX (v54,v13,v57,v25) \(\land\)
          Dtype (clk,v25,v57) \(\land\) DtypeT (clk,v28,v60) \(\land\) NOT (v60,v59) \(\land\)
          AND (v59,v28,v58) \(\land\) MUX (v58,v12,v61,v24) \(\land\) Dtype (clk,v24,v61) \(\land\) 
          DtypeT (clk,v28,v64) \(\land\) NOT (v64,v63) \(\land\) AND (v63,v28,v62) \(\land\) 
          MUX (v62,v11,v65,v23) \(\land\) Dtype (clk,v23,v65) \(\land\) DtypeT (clk,v28,v68) \(\land\) 
          NOT (v68,v67) \(\land\) AND (v67,v28,v66) \(\land\) MUX (v66,v10,v69,v22) \(\land\)
          Dtype (clk,v22,v69) \(\land\) DtypeT (clk,v28,v72) \(\land\) NOT (v72,v71) \(\land\)
          AND (v71,v28,v70) \(\land\) MUX (v70,v9,v73,v21) \(\land\) Dtype (clk,v21,v73) \(\land\) 
          DtypeT (clk,v28,v76) \(\land\) NOT (v76,v75) \(\land\) AND (v75,v28,v74) \(\land\) 
          MUX (v74,v8,v77,v20) \(\land\) Dtype (clk,v20,v77) \(\land\) DtypeT (clk,v28,v81) \(\land\) 
          NOT (v81,v80) \(\land\) AND (v80,v28,v79) \(\land\) NOT (v79,v19) \(\land\) CONSTANT 0w v82 \(\land\)
          EQ32 (v15,v82,v78) \(\land\) Dtype (clk,v78,v18) \(\land\) DtypeT (clk,v19,v86) \(\land\)
          NOT (v86,v85) \(\land\) AND (v85,v19,v84) \(\land\) AND (v84,v18,v17) \(\land\) NOT (v18,v83) \(\land\) 
          AND (v83,v84,v16) \(\land\) DtypeT (clk,v17,v89) \(\land\) NOT (v89,v88) \(\land\) AND (v88,v17,v87) \(\land\) 
          NOT (v87,v7) \(\land\) Dtype (clk,v26,out1) \(\land\) Dtype (clk,v25,out2) \(\land\) Dtype (clk,v24,v4) \(\land\) 
          Dtype (clk,v23,v3) \(\land\) Dtype (clk,v22,v2) \(\land\) Dtype (clk,v21,v1) \(\land\) 
          Dtype (clk,v20,v0) \(\land\) DtypeT (clk,v16,v104) \(\land\) NOT (v104,v103) \(\land\) 
          AND (v103,v16,v102) \(\land\)  Dtype (clk,v37,v101) \(\land\) AND (v102,v101,v100) \(\land\)
          DtypeT (clk,v100,v108) \(\land\) NOT (v108,v107) \(\land\) AND (v107,v100,v106) \(\land\) 
          NOT (v106,v99) \(\land\) CONSTANT 1w v109 \(\land\) SUB32 (v27,v109,v105) \(\land\) 
          Dtype (clk,v105,v97) \(\land\) DtypeT (clk,v100,v123) \(\land\) NOT (v123,v122) \(\land\)
          AND (v122,v100,v121) \(\land\) Dtype (clk,v98,v120) \(\land\) AND (v121,v120,v119) \(\land\) 
          DtypeT (clk,v119,v132) \(\land\) NOT (v132,v131) \(\land\) AND (v131,v119,v130) \(\land\)
          Dtype (clk,v118,v129) \(\land\) AND (v130,v129,v128) \(\land\) DtypeT (clk,v128,v143) \(\land\)
          NOT (v143,v142) \(\land\) AND (v142,v128,v141) \(\land\) Dtype (clk,v127,v140) \(\land\)
          AND (v141,v140,v139) \(\land\) DtypeT (clk,v139,v146) \(\land\) NOT (v146,v145) \(\land\) 
          AND (v145,v139,v144) \(\land\) NOT (v144,v138) \(\land\) Dtype (clk,v26,v136) \(\land\) 
          CONSTANT 2654435769w v148 \(\land\) ADD32 (v20,v148,v147) \(\land\) DtypeT (clk,v139,v152) \(\land\)
          NOT (v152,v151) \(\land\) AND (v151,v139,v150) \(\land\) NOT (v150,v137) \(\land\)
          CONSTANT 4 v158 \(\land\) LSL32 (v25,v158,v157) \(\land\) ADD32 (v157,v24,v156) \(\land\) 
          ADD32 (v25,v147,v155) \(\land\) XOR32 (v156,v155,v154) \(\land\) CONSTANT 5 v160 \(\land\)
          ASR32 (v25,v160,v159) \(\land\) ADD32 (v159,v23,v153) \(\land\) XOR32 (v154,v153,v149) \(\land\)
          Dtype (clk,v149,v135) \(\land\) DtypeT (clk,v138,v163) \(\land\) NOT (v163,v162) \(\land\)
          AND (v162,v138,v161) \(\land\) MUX (v161,v136,v164,v134) \(\land\) Dtype (clk,v134,v164) \(\land\) 
          DtypeT (clk,v137,v167) \(\land\) NOT (v167,v166) \(\land\) AND (v166,v137,v165) \(\land\)
          MUX (v165,v135,v168,v133) \(\land\) Dtype (clk,v133,v168) \(\land\) AND (v138,v137,v127) \(\land\)
          ADD32 (v134,v133,v125) \(\land\) DtypeT (clk,v128,v179) \(\land\) NOT (v179,v178) \(\land\)
          AND (v178,v128,v177) \(\land\) Dtype (clk,v126,v176) \(\land\) AND (v177,v176,v175) \(\land\) 
          DtypeT (clk,v175,v182) \(\land\) NOT (v182,v181) \(\land\) AND (v181,v175,v180) \(\land\) 
          NOT (v180,v174) \(\land\) Dtype (clk,v25,v172) \(\land\) NOT (v187,v190) \(\land\) 
          OR (v190,v175,v189) \(\land\) DtypeT (clk,v189,v201) \(\land\) NOT (v201,v200) \(\land\)
          AND (v200,v189,v199) \(\land\) Dtype (clk,v188,v198) \(\land\) AND (v199,v198,v197) \(\land\) 
          DtypeT (clk,v197,v212) \(\land\) NOT (v212,v211) \(\land\) AND (v211,v197,v210) \(\land\)
          Dtype (clk,v196,v209) \(\land\) AND (v210,v209,v208) \(\land\) DtypeT (clk,v208,v215) \(\land\) 
          NOT (v215,v214) \(\land\) AND (v214,v208,v213) \(\land\) NOT (v213,v207) \(\land\) 
          Dtype (clk,v26,v205) \(\land\) CONSTANT 2654435769w v217 \(\land\) ADD32 (v20,v217,v216) \(\land\)
          DtypeT (clk,v208,v221) \(\land\) NOT (v221,v220) \(\land\) AND (v220,v208,v219) \(\land\) 
          NOT (v219,v206) \(\land\) CONSTANT 4 v227 \(\land\) LSL32 (v25,v227,v226) \(\land\) 
          ADD32 (v226,v24,v225) \(\land\) ADD32 (v25,v216,v224) \(\land\) XOR32 (v225,v224,v223) \(\land\)
          CONSTANT 5 v229 \(\land\) ASR32 (v25,v229,v228) \(\land\) ADD32 (v228,v23,v222) \(\land\) 
          XOR32 (v223,v222,v218) \(\land\) Dtype (clk,v218,v204) \(\land\) DtypeT (clk,v207,v232) \(\land\)
          NOT (v232,v231) \(\land\) AND (v231,v207,v230) \(\land\) MUX (v230,v205,v233,v203) \(\land\) 
          Dtype (clk,v203,v233) \(\land\) DtypeT (clk,v206,v236) \(\land\) NOT (v236,v235) \(\land\)
          AND (v235,v206,v234) \(\land\) MUX (v234,v204,v237,v202) \(\land\) Dtype (clk,v202,v237) \(\land\)
          AND (v207,v206,v196) \(\land\) ADD32 (v203,v202,v194) \(\land\) DtypeT (clk,v197,v241) \(\land\)
          NOT (v241,v240) \(\land\) AND (v240,v197,v239) \(\land\) NOT (v239,v195) \(\land\)
          CONSTANT 2654435769w v242 \(\land\) ADD32 (v20,v242,v238) \(\land\) Dtype (clk,v238,v193) \(\land\) 
          Dtype (clk,v22,v192) \(\land\) Dtype (clk,v21,v191) \(\land\) DtypeT (clk,v196,v245) \(\land\)
          NOT (v245,v244) \(\land\) AND (v244,v196,v243) \(\land\) MUX (v243,v194,v246,v186) \(\land\) 
          Dtype (clk,v186,v246) \(\land\) DtypeT (clk,v195,v249) \(\land\) NOT (v249,v248) \(\land\)
          AND (v248,v195,v247) \(\land\) MUX (v247,v193,v250,v185) \(\land\) Dtype (clk,v185,v250) \(\land\) 
          DtypeT (clk,v195,v253) \(\land\) NOT (v253,v252) \(\land\) AND (v252,v195,v251) \(\land\)
          MUX (v251,v192,v254,v184) \(\land\) Dtype (clk,v184,v254) \(\land\) DtypeT (clk,v195,v257) \(\land\)
          NOT (v257,v256) \(\land\) AND (v256,v195,v255) \(\land\) MUX (v255,v191,v258,v183) \(\land\)
          Dtype (clk,v183,v258) \(\land\) AND (v196,v195,v188) \(\land\) DtypeT (clk,v188,v262) \(\land\)
          NOT (v262,v261) \(\land\) AND (v261,v188,v260) \(\land\) NOT (v260,v187) \(\land\) 
          CONSTANT 4 v268 \(\land\) LSL32 (v186,v268,v267) \(\land\) ADD32 (v267,v184,v266) \(\land\) 
          ADD32 (v186,v185,v265) \(\land\) XOR32 (v266,v265,v264) \(\land\) CONSTANT 5 v270 \(\land\) 
          ASR32 (v186,v270,v269) \(\land\) ADD32 (v269,v183,v263) \(\land\) XOR32 (v264,v263,v259) \(\land\)
          Dtype (clk,v259,v171) \(\land\) AND (v188,v187,v173) \(\land\) DtypeT (clk,v174,v273) \(\land\) 
          NOT (v273,v272) \(\land\) AND (v272,v174,v271) \(\land\) MUX (v271,v172,v274,v170) \(\land\)
          Dtype (clk,v170,v274) \(\land\) DtypeT (clk,v173,v277) \(\land\) NOT (v277,v276) \(\land\) 
          AND (v276,v173,v275) \(\land\) MUX (v275,v171,v278,v169) \(\land\) Dtype (clk,v169,v278) \(\land\)
          AND (v174,v173,v126) \(\land\) ADD32 (v170,v169,v124) \(\land\) DtypeT (clk,v127,v281) \(\land\)
          NOT (v281,v280) \(\land\) AND (v280,v127,v279) \(\land\) MUX (v279,v125,v282,v116) \(\land\)
          Dtype (clk,v116,v282) \(\land\) DtypeT (clk,v126,v285) \(\land\) NOT (v285,v284) \(\land\)
          AND (v284,v126,v283) \(\land\) MUX (v283,v124,v286,v115) \(\land\) Dtype (clk,v115,v286) \(\land\)
          AND (v127,v126,v118) \(\land\) DtypeT (clk,v119,v290) \(\land\) NOT (v290,v289) \(\land\) 
          AND (v289,v119,v288) \(\land\) NOT (v288,v117) \(\land\) CONSTANT 2654435769w v291 \(\land\) 
          ADD32 (v20,v291,v287) \(\land\) Dtype (clk,v24,v114) \(\land\) Dtype (clk,v23,v113) \(\land\)
          Dtype (clk,v22,v112) \(\land\) Dtype (clk,v21,v111) \(\land\) Dtype (clk,v287,v110) \(\land\) 
          DtypeT (clk,v118,v294) \(\land\) NOT (v294,v293) \(\land\) AND (v293,v118,v292) \(\land\)
          MUX (v292,v116,v295,v96) \(\land\) Dtype (clk,v96,v295) \(\land\) DtypeT (clk,v118,v298) \(\land\) 
          NOT (v298,v297) \(\land\) AND (v297,v118,v296) \(\land\) MUX (v296,v115,v299,v95) \(\land\)
          Dtype (clk,v95,v299) \(\land\) DtypeT (clk,v117,v302) \(\land\) NOT (v302,v301) \(\land\) 
          AND (v301,v117,v300) \(\land\) MUX (v300,v114,v303,v94) \(\land\) Dtype (clk,v94,v303) \(\land\)
          DtypeT (clk,v117,v306) \(\land\) NOT (v306,v305) \(\land\) AND (v305,v117,v304) \(\land\) 
          MUX (v304,v113,v307,v93) \(\land\) Dtype (clk,v93,v307) \(\land\) DtypeT (clk,v117,v310) \(\land\)
          NOT (v310,v309) \(\land\) AND (v309,v117,v308) \(\land\) MUX (v308,v112,v311,v92) \(\land\) 
          Dtype (clk,v92,v311) \(\land\) DtypeT (clk,v117,v314) \(\land\) NOT (v314,v313) \(\land\)
          AND (v313,v117,v312) \(\land\) MUX (v312,v111,v315,v91) \(\land\) Dtype (clk,v91,v315) \(\land\) 
          DtypeT (clk,v117,v318) \(\land\) NOT (v318,v317) \(\land\) AND (v317,v117,v316) \(\land\)
          MUX (v316,v110,v319,v90) \(\land\) Dtype (clk,v90,v319) \(\land\) AND (v118,v117,v98) \(\land\) 
          DtypeT (clk,v99,v322) \(\land\) NOT (v322,v321) \(\land\) AND (v321,v99,v320) \(\land\) 
          MUX (v320,v97,v323,v36) \(\land\) Dtype (clk,v36,v323) \(\land\) DtypeT (clk,v98,v326) \(\land\)
          NOT (v326,v325) \(\land\) AND (v325,v98,v324) \(\land\) MUX (v324,v96,v327,v35) \(\land\) 
          Dtype (clk,v35,v327) \(\land\) DtypeT (clk,v98,v330) \(\land\) NOT (v330,v329) \(\land\) 
          AND (v329,v98,v328) \(\land\) MUX (v328,v95,v331,v34) \(\land\) Dtype (clk,v34,v331) \(\land\)
          DtypeT (clk,v98,v334) \(\land\) NOT (v334,v333) \(\land\) AND (v333,v98,v332) \(\land\)
          MUX (v332,v94,v335,v33) \(\land\) Dtype (clk,v33,v335) \(\land\) DtypeT (clk,v98,v338) \(\land\) 
          NOT (v338,v337) \(\land\) AND (v337,v98,v336) \(\land\) MUX (v336,v93,v339,v32) \(\land\) 
          Dtype (clk,v32,v339) \(\land\) DtypeT (clk,v98,v342) \(\land\) NOT (v342,v341) \(\land\) 
          AND (v341,v98,v340) \(\land\) MUX (v340,v92,v343,v31) \(\land\) Dtype (clk,v31,v343) \(\land\)
          DtypeT (clk,v98,v346) \(\land\) NOT (v346,v345) \(\land\) AND (v345,v98,v344) \(\land\)
          MUX (v344,v91,v347,v30) \(\land\) Dtype (clk,v30,v347) \(\land\) DtypeT (clk,v98,v350) \(\land\) 
          NOT (v350,v349) \(\land\) AND (v349,v98,v348) \(\land\) MUX (v348,v90,v351,v29) \(\land\) 
          Dtype (clk,v29,v351) \(\land\) AND (v99,v98,v37) \(\land\) Dtype (clk,v37,v353) \(\land\)
          AND (v37,v353,v352) \(\land\) AND (v7,v19,v354) \(\land\) AND (v354,v352,done)) 
      ==>
       DEV TEAEncrypt
         (load at clk,
          ((inp11 <> inp12 <> inp13 <> inp14) <> inp2 <> inp3) at clk,
          done at clk,(out1 <> out2) at clk) : thm
\end{alltt}}
\end{quote}


\section{How are HOL designs downloaded to an FPGA?}\label{download}

\begin{quote}
There are four steps to download our circuits to an FPGA.

\begin{figure}[H]
   \centerline{
      \subfigure[Proof producing synthesis.]{
         \label{figProofProducing}\input{fpga1.eepic}}
      \subfigure[Verilog compilation.]{
         \label{figCompilation}\input{fpga2.eepic}}}\vspace*{0.3cm}
   \centerline{
      \subfigure[Download the object file.]{
         \label{figDownload}\input{fpga3.eepic}}
      \subfigure[Run the circuit.]{
         \label{figRun}\input{fpga4.eepic}}}
%      \label{figFPGA}\caption{The design process.}
\end{figure}

\begin{description}
   \item[Proof Producing Synthesis.] The initial step is concerned with
        the production of the theorem: ~
        \mbox{$\TURNST\ \DEF{InfRise}\ \mE{clk} \IMP (\mE{Cir} \FIMP \DEF{Dev}\ f)$}.
   \item[Verilog compilation.] A pretty-printer translates
        the circuit \mE{Cir} into the Verilog file {\tt Cir.v}.
        No formal verification is applied to this translation as
        Verilog has no formal semantics. The primitive components
        --- operators like \DEF{AND}, \DEF{OR}, \DEF{MUX} --- are 
        mapped to Verilog modules. The file {\tt UART.v} contains a 
        Verilog implementation of an interface that connects a serial
        cable to the circuit (this interface has not being formally verified).
        Both files are sent to Quartus~II for compilation.
   \item[Download the object file.] Quartus~II translates the Verilog files
        into the object file {\tt device.sof}, which is downloaded 
        to the FPGA via the parallel cable.
   \item[Run the circuit.] HOL is connected to the serial cable 
        by a UART program previously coded in C. The circuit is 
        triggered interactively via an automatically generated 
        function defined in HOL which communicates with the UART program.
\end{description}

All the four steps can be carried out from the HOL system 
provided that the pretty-printer is able to map every 
primitive combinational operator to Verilog.
\end{quote}


\section{What are the plans for the future?}

\begin{quote}
We hope to use the compiler to generate various kinds of cryptographic
hardware.  We expect more aggressive compaction may be needed to fit
bigger examples (e.g.~AES) onto the FPGAs we are using.  

Eventually, it is hoped to provide wrapper circuitry to enable
synthesised HOL functions to be invoked from ARM code as hardware
co-processors. The FPGA board we are using (Altera Excalibur) has an
ARM processor on it.
\end{quote}


\section{Is the compiler freely available?}

\begin{quote}
The compiler is distributed with the HOL-4 system
(\url{http://hol.sourceforge.net/}) in the directory
\texttt{examples/dev}.
\end{quote}


\section{What related work is there?}\label{related}

\begin{quote}
There is considerable previous work on using functional programming to
specify and design hardware. Examples include $\mu$FP (Sheeran
\cite{Sheeran84}), Ruby (Jones \& Sheeran \cite{jones91relations,Ruby}),
Hydra (O'Donnell~\cite{OD02}), Lava (Bjesse et al~\cite{BCSS99}), DDD
(Johnson \& Bose~\cite{Johnson90}), LAMBDA (Finn et al~\cite{Fou89}),
Gropius (Blumenr\"{o}hr \cite{Blu01}), DUAL-EVAL (Brock \&
Hunt~\cite{DBLP:journals/fmsd/BrockH97}) and SAFL (Mycroft \&
Sharp~\cite{MS01a}).

Our work was initially inspired by SAFL, a hardware compiler for a
language based on a first-order subset of ML, though we use a subset
of higher order logic rather than a separate special-purpose design
specification language.  The general way we employ serial/parallel
combinators for compositional translation has similarities to
compilers for Handel (Page~\cite{page96constructing}) and
SAFL. However, many details differ in our approach: in particular, our
compiler is proof-producing.

The paper ``Formal Synthesis in Circuit Design
-- A Classification and Survey'' \cite{kumar96formal} provides an
excellent overview. In terms of the classification in that paper, our
approach is {\it formal synthesis\/} by {\it transformational derivation\/} in a
{\it general purpose calculus}.

The way we realise HOL functions by handshaking devices is
reminiscent of some self-timed design methods
\cite{hauck93asynchronous,KeesvanBerkel93}, though we produce
clocked synchronous circuits.
\end{quote}

\section*{Acknowledgements}

David Greaves gave us advice on the hardware implementation of
handshake protocols and also helped us understand the results of
simulating circuits produced by our compiler.  Simon Moore and Robert
Mullins lent us an Excalibur FPGA board on which we are running compiled hardware at Cambridge,
and they helped us with the Quartus~II design software that we are using to drive the board.
Ken Larsen used his dynlib library to write an ML version of our
original C interface to the serial port (this is used to communicate
with the Excalibur board, see~\ref{download}).

\bibliographystyle{plain}
{%\small
\bibliography{faq}
}

\end{document}


