\section{Formal verification: `bread and butter' method}
\label{sec-verf}

In this section, we
describe the formal verification
of \Tamarack\ when operating in fully synchronous mode.
Verifying \Tamarack\ in this mode
is relatively simple because each programming level operation is
implemented by a fixed sequence (or finite set of fixed sequences)
of microinstructions.
The considerably more difficult task of verifying
\Tamarack\ for fully asynchronous
mode is outlined later in Section~\ref{sec-asyn}.

\subsection{Phase level}
\label{sec-verfphase}

As explained earlier in Section~\ref{sec-phase},
the phase level operation of \Tamarack\ is described in terms
of elementary operations performed by register-transfer level components.
The interpretation of a microinstruction at the phase level during
a single clock cycle results in a sequence of events which includes:

\begin{center}
\begin{itemize}
\item Fetch the current microinstruction.
\item Compute the address of the next microinstruction.
\item Read data onto the system bus.
\item Evaluate operations performed by functional elements.
\item Update storage elements such as memory, registers and flipflops.
\end{itemize}
\end{center}

Verifying the operation of the microprocessor at this level
is a matter of deriving the cumulative effect of these elementary operations
for each of the sixteen microinstructions.
We show that the cumulative effect of these operations satisfies the
intended effect of each microinstruction.

To illustrate this process,
we outline the steps taken to establish
that microinstruction~0, i.e., the microinstruction at
location~0 in the microcode,
is correctly interpreted at the phase level.
The intended effect of \mbox{microinstruction 0},

\begin{quote}
\verb"MicroCode 0 = ((`rpc`,`wmar`,`none`), waitidle, jireq, (1,2))"
\end{quote}

\noindent
is to transfer
the contents of the program counter
\verb"pc" to the memory address register \verb"mar"
and update the microcode program counter \verb"mpc"
according to conditions given in the flow graph of Figure~\ref{fig-flow}.
Furthermore, the execution of this microinstruction must leave the
internal state of the memory \verb"mem" and the contents of the
program counter \verb"pc", accumulator \verb"acc", return address
register \verb"rtn" and interrupt acknowledge flag \verb"iack" unchanged.
The effect of this microinstruction on the remaining components of the
internal state,
namely, the \verb"arg" and \verb"buf" registers,
is unimportant and can be ignored.
Finally,
the memory data output bus \verb"dataout"
must be set to its default value and the memory control flags,
\verb"wmem" and \verb"dreq", must be set to \verb"F".



These requirements are formally expressed in the goal term
of the following call to the ML function \verb"set_goal".
This is the first step in an interactive proof
to formally derive this
goal\footnote{
The term `goal' has technical meaning in the \HOL\ system
(as a ML type abbreviation) but
we use it more generally to mean a \mbox{yet-to-be-proven} theorem.}
as a theorem using the
\HOL\ sub-goal package.

\newpage % PBHACK

\begintt
set_goal (
  [],
  "Val3_CASES_ASM (rep:^rep_ty) \(\wedge\)
   Val4Word4_ASM rep \(\wedge\)
   TamarackImp rep (
     datain,dack,idle,ireq,mpc,mar,pc,
     acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr)
   ==>
   \(\forall\)t.
    (((val4 rep) o mpc) t = 0)
    ==>
    (((val4 rep) o mpc) (t+1) =
       ((\(\neg\)((idle t) \(\vee\) \(\neg\)(dack t))) => 0 |
        ((ireq t) \(\wedge\) \(\neg\)(iack t)) => 1 | 2)) \(\wedge\)
    (mar (t+1) = pc t) \(\wedge\)
    (pc (t+1) = pc t) \(\wedge\)
    (acc (t+1) = acc t) \(\wedge\)
    (rtn (t+1) = rtn t) \(\wedge\)
    (iack (t+1) = iack t) \(\wedge\)
    (dataout t = ((wordn rep) 0)) \(\wedge\)
    (wmem t = F) \(\wedge\)
    (dreq t = F)");;
\endtt

A sequence of interactions with the sub-goal package eventually
results in the generation of this goal as a theorem.
To illustrate the strategy which underlies this sequence of interactions
and more generally,
how formal proof can be used to symbolically execute hardware,
we describe a condensed view of the proof procedure
given in:

\begin{quote}
\verb"hol/Training/studies/microprocessor/proof/example2.ml"
\end{quote}

The reader may wish to examine this \HOL\ source file for details
of the actual interactions used to generate this proof
since we only describe the proof procedure in terms
of intermediate results generated by the \HOL\ system
in response to these interactions.

We begin by expanding the above goal with the definitions
for \verb"TamarackImp", \verb"CntlUnit" and \verb"DataPath".
We then apply standard goal reduction techniques
to strip antecedents from the goal
and break them up into a number of assumptions which are put into
the assumption list.
The result is shown below where each assumption appears as a
term between a matching pair of brackets \verb"[" and \verb"]".
Most of these assumptions correspond to primitive components
of the internal architecture with internal connections
(hidden in the specification by existential quantification)
now exposed as free variables in the assumption list.

\begintt
OK..
"(val4 rep(mpc(t + 1)) =
  ((\(\neg\)(idle t \(\vee\) \(\neg\)dack t)) => 0 | ((ireq t \(\wedge\) \(\neg\)iack t) => 1 | 2))) \(\wedge\)
 (mar(t + 1) = pc t) \(\wedge\)
 (pc(t + 1) = pc t) \(\wedge\)
 (acc(t + 1) = acc t) \(\wedge\)
 (rtn(t + 1) = rtn t) \(\wedge\)
 (iack(t + 1) = iack t) \(\wedge\)
 (dataout t = wordn rep 0) \(\wedge\)
 (wmem t = F) \(\wedge\)
 (dreq t = F)"
    [ "Val3_CASES_ASM rep" ]
    [ "Val4Word4_ASM rep" ]
    [ "NextMPC 
       rep
       (f0,f1,f2,f3,dack,idle,ireq,iack,zeroflag,opc,addr1,addr2,mpc,
        next)" ]
    [ "MPC(next,mpc)" ]
    [ "ROM rep(mpc,rom)" ]
    [ "DecodeROM(rom,f0,f1,f2,f3,addr1,addr2,cntls)" ]
    [ "DecodeCntls
       (cntls,wmem,rmem,wmar,wpc,rpc,wacc,racc,wir,rir,wrtn,rrtn,warg,
        alu0,alu1,rbuf)" ]
    [ "BusOkay(rmem,rpc,racc,rir,rrtn,rbuf,busokay)" ]
    [ "Interface rep(busokay,wmem,rmem,bus,datain,dataout)" ]
    [ "OR(wmem,rmem,dreq)" ]
    [ "Register(busokay,wmar,gnd,bus,bus,mar)" ]
    [ "AddrField rep(mar,addr)" ]
    [ "Register(busokay,wpc,rpc,bus,bus,pc)" ]
    [ "Register(busokay,wacc,racc,bus,bus,acc)" ]
    [ "TestZero rep(acc,zeroflag)" ]
    [ "Register(busokay,wir,rir,bus,bus,ir)" ]
    [ "OpcField rep(ir,opc)" ]
    [ "Register(busokay,wrtn,rrtn,bus,bus,rtn)" ]
    [ "JKFF(wrtn,rrtn,iack)" ]
    [ "Register(busokay,warg,gnd,bus,bus,arg)" ]
    [ "ALU rep(alu0,alu1,arg,bus,alu)" ]
    [ "Register(busokay,pwr,rbuf,alu,bus,buf)" ]
    [ "PWR pwr" ]
    [ "GND gnd" ]
    [ "val4 rep(mpc t) = 0" ]

() : void
\endtt

After this initial bit of backward proof,
forward inference steps are achieved by repeated use of resolution
tactics.
Theorems generated by resolution in this manner are logical consequences of
the assumptions already in the assumption list.
These theorems contribute various facts which incremently advance the
state of the symbolic execution.
As theorems are generated,
they are added to the current list of assumptions and may be used
by subsequent resolution steps to generate more theorems.

Since this part of the proof
is only concerned with generating new theorems for
the assumption list,
we just show what gets added onto the end of the assumption list
after each main step.
We begin by using
the definition of \verb"ROM"
to generate the following equation for the current output of the ROM.

\begin{quote}
\verb"rom t = CompileMicroCode rep(MicroCode 0)"
\end{quote}

Instead of adding this equation directly to the assumption list,
we use the microcode specification \verb"MicroCode" and
definitions for the micro-assembler functions
given in Section~\ref{sec-microcode}
to transform it into an equation
which gives the assembled form of microinstruction~0.

\begintt
OK..
    \(\ldots\)
    [ "rom t =
       (F,F,T,F,T,F,F,F,F,F,F,F,F,F,F),(T,F),(T,F),word4 rep 1,
       word4 rep 2" ]

() : void
\endtt

The definition of \verb"DecodeROM" is then used to separate the ROM output
into datapath control bits, \verb"cntls",
next address logic control bits,
\verb"f0", \verb"f1", \verb"f2" and \verb"f3", and
microcode addresses, \verb"addr1" and \verb"addr2".

\begintt
OK..
    \(\ldots\)
    [ "cntls t = F,F,T,F,T,F,F,F,F,F,F,F,F,F,F" ]
    [ "f0 t = T" ]
    [ "f1 t = F" ]
    [ "f2 t = T" ]
    [ "f3 t = F" ]
    [ "addr1 t = word4 rep 1" ]
    [ "addr2 t = word4 rep 2" ]

() : void
\endtt

The next address logic control bits and microcode addresses
extracted from the current output of the ROM
are used to derive an expression for the output of the next address
logic.
This expression is obtained from the definition of \verb"NextState".
The value of this expression depends
on external inputs,
\verb"idle", \verb"dack", and \verb"ireq",
and the current value
of the interrupt acknowledge flag \verb"iack".

\begintt
OK..
    \(\ldots\)
    [ "next t =
       ((\(\neg\)(idle t \(\vee\) \(\neg\)dack t)) => 
        mpc t | 
        ((ireq t \(\wedge\) \(\neg\)iack t) => word4 rep 1 | word4 rep 2))" ]

() : void
\endtt

At the end of the clock cycle,
the value computed by the next address logic is loaded into
the microcode program counter \verb"mpc".
The definition of \verb"MPC" is used to establish this fact.

\begintt
OK..
    \(\ldots\)
    [ "mpc(t + 1) =
       ((\(\neg\)(idle t \(\vee\) \(\neg\)dack t)) => 
        mpc t | 
        ((ireq t \(\wedge\) \(\neg\)iack t) => word4 rep 1 | word4 rep 2))" ]

() : void
\endtt


Meanwhile,
the datapath is performing actions specified by the datapath control bits.
To derive the result of these actions,
we start with the definition of \verb"DecodeCntls" to separate
the bundle of control bits into individual control signals.

\newpage % PBHACK


\begintt
OK..
   \(\ldots\)
    [ "wmem t = F" ]
    [ "rmem t = F" ]
    [ "wmar t = T" ]
    [ "wpc t = F" ]
    [ "rpc t = T" ]
    [ "wacc t = F" ]
    [ "racc t = F" ]
    [ "wir t = F" ]
    [ "rir t = F" ]
    [ "wrtn t = F" ]
    [ "rrtn t = F" ]
    [ "warg t = F" ]
    [ "alu0 t = F" ]
    [ "alu1 t = F" ]
    [ "rbuf t = F" ]

() : void
\endtt

The definitions of \verb"PWR" and \verb"GND" yield
equations for the voltage sources \verb"pwr" and \verb"gnd".
These two signals are used to permanently enable or disable various
functions in the datapath.

\begintt
OK..
   \(\ldots\)
    [ "pwr t = T" ]
    [ "gnd t = F" ]

() : void
\endtt

All of the `read' signals are equal to \verb"F" except for \verb"rpc"
satisfying the condition that only one bus device can attempt to read
a value onto the system bus.
The definition of \verb"BusOkay" is used to establish
that the virtual signal \verb"busokay" is equal to \verb"T"
indicating that this condition is satisfied.

\begintt
OK..
   \(\ldots\)
    [ "busokay t = T" ]

() : void
\endtt

Using these values for \verb"rpc" and \verb"busokay",
the definition of \verb"Register" yields an equation
for the value of the system bus.

\begintt
OK..
   \(\ldots\)
    [ "bus t = pc t" ]

() : void
\endtt

Hence, the contents of the program counter \verb"pc" are
successfully read onto the bus.
The data transfer is completed by writing the value of the bus into
the memory address register \verb"mar".
The contents of other registers in the datapath (ignoring \verb"buf")
and the value of the interrupt acknowledge flag \verb"iack"
remain unchanged.
These facts can be established
from the above equations for the control signals and the
definitions of \verb"Register" and \verb"JKFF".

\begintt
OK..
   \(\ldots\)
    [ "mar(t + 1) = pc t" ]
    [ "pc(t + 1) = pc t" ]
    [ "acc(t + 1) = acc t" ]
    [ "ir(t + 1) = ir t" ]
    [ "rtn(t + 1) = rtn t" ]
    [ "arg(t + 1) = arg t" ]
    [ "buf(t + 1) = alu t" ]
    [ "iack(t + 1) = iack t" ]

() : void
\endtt

Finally, the control signals cause certain values to be generated
as external outputs.  The definitions of \verb"OR" and \verb"Interface"
yield the following equations for \verb"dreq" and \verb"dataout"
(an equation for \verb"wmem" has already appeared in a previous step).

\begintt
OK..
   \(\ldots\)
    [ "dreq t = F" ]
    [ "dataout t = wordn rep 0" ]

() : void
\endtt

This completes the symbolic execution part of the proof:
the results of symbolic execution are used to solve
all the remaining goals of the backward proof.
At the beginning of the symbolic execution part of the proof,
the top level goal was:

\begintt
"(val4 rep(mpc(t + 1)) =
  ((\(\neg\)(idle t \(\vee\) \(\neg\)dack t)) => 0 | ((ireq t \(\wedge\) \(\neg\)iack t) => 1 | 2))) \(\wedge\)
 (mar(t + 1) = pc t) \(\wedge\)
 (pc(t + 1) = pc t) \(\wedge\)
 (acc(t + 1) = acc t) \(\wedge\)
 (rtn(t + 1) = rtn t) \(\wedge\)
 (iack(t + 1) = iack t) \(\wedge\)
 (dataout t = wordn rep 0) \(\wedge\)
 (wmem t = F) \(\wedge\)
 (dreq t = F)"
\endtt

But by the end of symbolic execution,
most of the conjuncts in this goal have already been solved
as a side-effect of various manipulations of the goal stack
(e.g., uses of \verb"ASM_REWRITE_TAC").
The original goal has been reduced to:

\begintt
"val4 
 rep
 ((\(\neg\)(idle t \(\vee\) \(\neg\)dack t)) => 
  mpc t | 
  ((ireq t \(\wedge\) \(\neg\)iack t) => word4 rep 1 | word4 rep 2)) =
 ((\(\neg\)(idle t \(\vee\) \(\neg\)dack t)) => 0 | ((ireq t \(\wedge\) \(\neg\)iack t) => 1 | 2))"
\endtt



This reduced goal is easily solved by case analysis on Boolean terms
and using the assumption expressed by \verb"Val4Word4_ASM".

\newpage % PBHACK

\begintt
OK..
goal proved

\( \ldots additional output deleted here \ldots \)

|- Val3_CASES_ASM rep \(\wedge\)
   Val4Word4_ASM rep \(\wedge\)
   TamarackImp 
   rep
   (datain,dack,idle,ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,dataout,
    wmem,dreq,addr) ==>
   (\(\forall\)t.
     (((val4 rep) o mpc)t = 0) ==>
     (((val4 rep) o mpc)(t + 1) =
      ((\(\neg\)(idle t \(\vee\) \(\neg\)dack t)) => 0 | ((ireq t \(\wedge\) \(\neg\)iack t) => 1 | 2))) \(\wedge\)
     (mar(t + 1) = pc t) \(\wedge\)
     (pc(t + 1) = pc t) \(\wedge\)
     (acc(t + 1) = acc t) \(\wedge\)
     (rtn(t + 1) = rtn t) \(\wedge\)
     (iack(t + 1) = iack t) \(\wedge\)
     (dataout t = wordn rep 0) \(\wedge\)
     (wmem t = F) \(\wedge\)
     (dreq t = F))

Previous subproof:
goal proved
() : void
\endtt

A similar pattern of reasoning is used to derive correctness results for the
remaining fifteen microinstructions
(these results are given in Appendix~\ref{apx-phase}).
Each of these theorems shows that the microinstruction
satisfies a set of equations for the next state of the microprocessor
at time~\verb"t+1" in terms of its state at time~\verb"t".
Each theorem expresses the minimal (or close to minimal) set of results
needed at higher proof levels;
irrelevent details (such as the effect of
microinstruction~0 on \verb"arg" and \verb"buf") are ignored.

These sixteen correctness results collectively
capture the informal description conveyed by
the flow graph in Figure~\ref{fig-flow} and corresponding
datapath actions described in Figure~\ref{fig-map}.

\subsection{Microprogramming level}
\label{sec-verfmicro}

The second main step of the verification procedure is
to examine the interpretation of programming level operations
by sequences of microinstructions.
Here we consider the operation of the microprocessor
in fully synchronous mode where each programming level operation
is implemented by a fixed sequence of microinstructions, or in the
case of a \verb"JZR" instruction,
by one of two possible sequences.
Symbolic execution of these microinstruction sequences
is used to show that their cumulative effect
satisfies the semantics of the instruction
set formally defined in Section~\ref{sec-formsem}.
Symbolic execution of microinstructions is also used to show that
hardware interrupts are correctedly implemented.

A behavioural model for external memory was not needed to verify
the phase level operation of the microinstruction since
correctness results at that level are simply concerned with
sampling and generating inputs and outputs on pins of the microchip.
However, a behavioural model for external memory is needed to verify
the microprogramming level.
Whereas the terms \verb"fetch" and \verb"store"
did not appear the correctness results for the phase level,
they do appear in
correctness results for the microprogramming level.

The predicate \verb"SynSystem" is defined below to specify
a system consisting of the \Tamarack\ microchip interfaced to
a fully synchronous memory device.
The specification of the memory device was given earlier in
Section~\ref{sec-formmem}
by the definition of \verb"SynMemory".
The internal architecture is made to operate in fully synchronous mode
by wiring the two pins \verb"dack" and \verb"idle" to \verb"T", i.e.,
the output of a voltage source.

\begintt
let SynSystem = new_definition (
  `SynSystem`,
  "SynSystem (rep:^rep_ty)
    (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) =
    \(\exists\)datain pwr dataout wmem dreq addr.
      TamarackImp rep (
        datain,pwr,pwr,ireq,mpc,mar,pc,
        acc,ir,rtn,arg,buf,iack,dataout,wmem,dreq,addr) \(\wedge\)
      SynMemory rep (wmem,addr,dataout,mem,datain) \(\wedge\)
      PWR pwr");;
\endtt

Each programming level operation is interpreted by a non-empty,
fixed sequence of microinstructions (or pair of possible sequences
in the case of the JZR instruction).
It is convenient to define the function \verb"MicroCycles"
which specifies the length of sequence about to be executed
given the current state of the microprocessor
(assuming that the microprocessor is operating in fully synchronous mode).

\begintt
let MicroCycles = new_definition (
  `MicroCycles`,
  "MicroCycles (rep:^rep_ty) (ireq,mem,pc,acc,rtn:*wordn,iack) =
    (ireq \(\wedge\) \(\neg\)iack) => 3 |
    let opcval = OpcVal rep (mem,pc) in
    ((opcval = 0) => (((iszero rep) acc) => 5 | 6) |
     (opcval = 1) => 4 |
     (opcval = 2) => 8 |
     (opcval = 3) => 8 |
     (opcval = 4) => 6 |
     (opcval = 5) => 6 |
     (opcval = 6) => 4 |
                     5)");;
\endtt

\verb"MicroCycles"
provides the basis for relating behaviour models of \Tamarack\
expressed in terms of different granularities of time.
\footnote{
The function \verb"MicroCycles" is similar in purpose to the
function \mbox{\footnotesize \verb"NUMBER\_OF\_STEPS"}
in the \mbox{\footnotesize VIPER} proof and the oracle function
in the verification of \mbox{\footnotesize FM8501}
(except that the \mbox{\footnotesize FM8501} oracle
also takes account of handshaking delays).}
Later in Section~\ref{sec-temp},
we describe a more general way of relating
different granularities of time that does not involve
\verb"MicroCycles".

To reason about the implementation of particular programming level
operation at the microprogramming level,
we assume that the value of the microcode program counter \verb"mpc" is
equal to zero at time \verb"t", that is, the beginning of the
instruction cycle.
The results of symbolic execution are used to determine the
state of the microprocessor and memory
at the end of the instruction cycle denoted as time \verb"t+m" where
\verb"m" is the value returned by \verb"MicroCycles".
Correctness results are obtained by showing that the state of
system at the end of the interpretation sequence
is consistent with the definition of \verb"NextState".
To eventually get rid of the assumption about the value of
the microcode program counter \verb"mpc" at the beginning of the cycle,
we must also show that its value returns to zero at the end of the cycle.

These requirements could be translated directly into
an individual statement of correctness for each programming level
operation.
But all of these correctness statements would be nearly identical
except for minor (textual)
distinctions such as the opcode value of the current
instruction in each case.
We can avoid a great deal of redundant text by defining a predicate
\verb"SynCorrectness1" which is a generalized form of
correctness statement.  It is parameterized by the variables,

\begin{quote}
\begin{tabular}{ll}
\verb"ircond"& - interrupt condition\\
\verb"opcval"& - opcode value\\
\verb"iszerocond"& - result of \verb"testzero" operation
\end{tabular}
\end{quote}

\noindent
which distinguish one programming level operation from another.

\begintt
let SynCorrectness1 = new_definition (
  `SynCorrectness1`,
  "SynCorrectness1 (rep:^rep_ty) (ircond,opcval,iszerocond) =
    \(\forall\)ireq mpc mar pc acc ir rtn arg buf iack mem.
      Val3_CASES_ASM (rep:^rep_ty) \(\wedge\)
      Val4Word4_ASM rep \(\wedge\)
      SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)
      ==>
      \(\forall\)t:time.
        (((val4 rep) o mpc) t = 0) \(\wedge\)
        ((ireq t \(\wedge\) \(\neg\)(iack t)) = ircond) \(\wedge\)
        (OpcVal rep (mem t,pc t) = opcval) \(\wedge\)
        ((iszero rep) (acc t) = iszerocond)
        ==>
        let m = MicroCycles rep (ireq t,mem t,pc t,acc t,rtn t,iack t) in
        ((((val4 rep) o mpc) (t+m) = 0) \(\wedge\)
         ((mem (t+m),pc (t+m),acc (t+m),rtn (t+m),iack (t+m)) =
          NextState rep (ireq t,mem t,pc t,acc t,rtn t,iack t)))");;
\endtt

To illustrate details of this verification step,
we consider the sequence of microinstructions for an ADD instruction.
As shown earlier in Section~\ref{sec-micro},
the ADD instruction is interpreted in fully synchronous mode
by the sequence of
microinstructions stored in the microcode ROM at the following
locations.

\begin{quote}
0, 2, 3, 6, 13, 15, 11 and 12
\end{quote}

The ADD instruction case is specified by the assumption that
the opcode of the current instruction is the ADD instruction opcode
and that a hardware interrupt is not about to be processed in this cycle.
Since the result of the \verb"testzero" operation are not relevant in
this case, the value for \verb"iszerocond"
is given by a variable \verb"b".
The desired correctness result is expressed by the goal term in
the following call to \verb"set_goal".

\begintt
set_goal ([],"\(\forall\)b. SynCorrectness1 (rep:^rep_ty) (F,ADD_OPC,b)");;
\endtt

The style of interaction with the \HOL\ system described earlier
for verifying the phase level is also used here
to verify the microprogramming level.
The steps shown below are based (more or less)
on the proof procedure given in:

\begin{quote}
\verb"hol/Training/studies/microprocessor/proof/example3.ml"
\end{quote}

We begin with a little backward proof to expand the
correctness condition expressed by \verb"SynCorrectness1"
and move the expanded result
into the assumption list.
Definitions for \verb"MicroCycles" and \verb"NextState"
along with some arithmetic facts are
then used to simplify the goal for the ADD instruction case.

\begintt
OK..
"let m = 8
 in
  ((((val4 rep) o mpc)(t + m) = 0) \(\wedge\)
   (mem(t + m),pc(t + m),acc(t + m),rtn(t + m),iack(t + m) =
    ADD_SEM rep(mem t,pc t,acc t,rtn t,iack t)))"
    [ "Val3_CASES_ASM rep" ]
    [ "Val4Word4_ASM rep" ]
    [ "TamarackImp 
       rep
       (datain,pwr,pwr,ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,dataout,
        wmem,dreq,addr)" ]
    [ "SynMemory rep(wmem,addr,dataout,mem,datain)" ]
    [ "\(\forall\)t. pwr t = T" ]
    [ "((val4 rep) o mpc)t = 0" ]
    [ "ireq t \(\wedge\) \(\neg\)iack t = F" ]
    [ "val3 rep(opcode rep(fetch rep(mem t,address rep(pc t)))) = 2" ]
    [ "iszero rep(acc t) = b" ]

() : void
\endtt

After this initial bit of backward proof,
we begin the symbolic execution of the microcode for
the ADD instruction.
The symbolic execution begins with the value of the microcode program
counter \verb"mpc" equal to zero.
We use correctness results for microinstruction~0
(obtained earlier from the verification of the phase level)
to derive the state of the machine
at time \verb"t+1".

\begintt
OK..
    \(\ldots\)
    [ "iack(t + 1) = iack t" ]
    [ "rtn(t + 1) = rtn t" ]
    [ "acc(t + 1) = acc t" ]
    [ "pc(t + 1) = pc t" ]
    [ "mar(t + 1) = pc t" ]
    [ "mem(t + 1) = mem t" ]
    [ "((val4 rep) o mpc)(t + 1) = 2" ]

() : void
\endtt

As we have assumed that the microprocessor is operating in fully
synchronous mode and that an interrupt request is not
about to be processed in this cycle,
we can show that the value of the
microcode program counter \verb"mpc" becomes equal to two
at time \verb"t+1".
To advance the state of the symbolic execution to time \verb"t+2",
we use the correctness results for microinstruction~2
and the behavioural model of external memory to obtain:

\begintt
OK..
    \(\ldots\)
    [ "iack(t + 2) = iack t" ]
    [ "rtn(t + 2) = rtn t" ]
    [ "ir(t + 2) = fetch rep(mem t,address rep(pc t))" ]
    [ "acc(t + 2) = acc t" ]
    [ "pc(t + 2) = pc t" ]
    [ "mar(t + 2) = pc t" ]
    [ "mem(t + 2) = mem t" ]
    [ "((val4 rep) o mpc)(t + 2) = 3" ]

() : void
\endtt

By time \verb"t+2",
the instruction addressed by the program counter \verb"pc" has been
read from memory and loaded into the instruction register \verb"ir".
The opcode field of the instruction register now contains the
opcode for the current instruction which, in the case of ADD,
has the value two.
Correctness results for microinstruction~2 show that
the address of the next microinstruction is obtained
by adding four to the value of the opcode;
hence, the address of the next microinstruction is six.

\begintt
OK..
    \(\ldots\)
    [ "iack(t + 3) = iack t" ]
    [ "rtn(t + 3) = rtn t" ]
    [ "ir(t + 3) = fetch rep(mem t,address rep(pc t))" ]
    [ "acc(t + 3) = acc t" ]
    [ "pc(t + 3) = pc t" ]
    [ "mar(t + 3) = fetch rep(mem t,address rep(pc t))" ]
    [ "mem(t + 3) = mem t" ]
    [ "((val4 rep) o mpc)(t + 3) = 6" ]

() : void
\endtt

This sequence continues with the symbolic execution of
microinstruction at locations 6, 13, 15, 11 and 12.
New assumptions added to the assumption list
for each step are shown below.

\begintt
OK..
    \(\ldots\)
    [ "iack(t + 4) = iack t" ]
    [ "arg(t + 4) = acc t" ]
    [ "rtn(t + 4) = rtn t" ]
    [ "acc(t + 4) = acc t" ]
    [ "pc(t + 4) = pc t" ]
    [ "mar(t + 4) = fetch rep(mem t,address rep(pc t))" ]
    [ "mem(t + 4) = mem t" ]
    [ "((val4 rep) o mpc)(t + 4) = 13" ]

() : void
\endtt

\begintt
OK..
    \(\ldots\)
    [ "iack(t + 5) = iack t" ]
    [ "buf(t + 5) =
       add 
       rep
       (acc t,
        fetch rep(mem t,address rep(fetch rep(mem t,address rep(pc t)))))" ]
    [ "arg(t + 5) = acc t" ]
    [ "rtn(t + 5) = rtn t" ]
    [ "acc(t + 5) = acc t" ]
    [ "pc(t + 5) = pc t" ]
    [ "mar(t + 5) = fetch rep(mem t,address rep(pc t))" ]
    [ "mem(t + 5) = mem t" ]
    [ "((val4 rep) o mpc)(t + 5) = 15" ]

() : void
\endtt

\begintt
OK..
    \(\ldots\)
    [ "iack(t + 6) = iack t" ]
    [ "rtn(t + 6) = rtn t" ]
    [ "acc(t + 6) =
       add 
       rep
       (acc t,
        fetch rep(mem t,address rep(fetch rep(mem t,address rep(pc t)))))" ]
    [ "pc(t + 6) = pc t" ]
    [ "mem(t + 6) = mem t" ]
    [ "((val4 rep) o mpc)(t + 6) = 11" ]

() : void
\endtt

\begintt
OK..
    \(\ldots\)
    [ "iack(t + 7) = iack t" ]
    [ "buf(t + 7) = inc rep(pc t)" ]
    [ "rtn(t + 7) = rtn t" ]
    [ "acc(t + 7) =
       add 
       rep
       (acc t,
        fetch rep(mem t,address rep(fetch rep(mem t,address rep(pc t)))))" ]
    [ "mem(t + 7) = mem t" ]
    [ "((val4 rep) o mpc)(t + 7) = 12" ]

() : void
\endtt

\begintt
OK..
    \(\ldots\)
    [ "iack(t + 8) = iack t" ]
    [ "rtn(t + 8) = rtn t" ]
    [ "acc(t + 8) =
       add 
       rep
       (acc t,
        fetch rep(mem t,address rep(fetch rep(mem t,address rep(pc t)))))" ]
    [ "pc(t + 8) = inc rep(pc t)" ]
    [ "mem(t + 8) = mem t" ]
    [ "((val4 rep) o mpc)(t + 8) = 0" ]

() : void
\endtt

Eventually we obtain
a set of equations for the state of the system at the
end of this particular execution sequence,
that is, at time \verb"t+8".
These equations describe the net effect of executing
the microinstruction sequence which implements an ADD instruction.
The backward proof is easily completed by showing that these
equations are consistent with the definition of \verb"ADD_SEM".

\begintt
OK..
goal proved

\( \ldots additional output deleted here \ldots \)

|- \(\forall\)b. SynCorrectness1 rep(F,ADD_OPC,b)

Previous subproof:
goal proved
() : void
\endtt

There are nine further cases to consider:
one case for the JZR instruction when the value of the accumulator
is zero; another case for JZR instruction when the accumulator is
non-zero;
one case for each of the six remaining instructions;
and finally, a case for the processing of a hardware interrupt.
Correctness results for these nine further cases are expressed
by the following theorems:

\begintt
|- \(\forall\)b. SynCorrectness1 rep(F,JZR_OPC,T)

|- \(\forall\)b. SynCorrectness1 rep(F,JZR_OPC,F)

|- \(\forall\)b. SynCorrectness1 rep(F,JMP_OPC,b)

|- \(\forall\)b. SynCorrectness1 rep(F,SUB_OPC,b)

|- \(\forall\)b. SynCorrectness1 rep(F,LDA_OPC,b)

|- \(\forall\)b. SynCorrectness1 rep(F,STA_OPC,b)

|- \(\forall\)b. SynCorrectness1 rep(F,RFI_OPC,b)

|- \(\forall\)b. SynCorrectness1 rep(F,NOP_OPC,b)

|- \(\forall\)n b. SynCorrectness1 rep(T,n,b)
\endtt

The penultimate step in verifying the microprogramming level is to combine
the above correctness results for individual programming level operations
into a single theorem.
The theorem shown below is obtained by case analysis on the
three parameters of \verb"SynCorrectness1".
Since \verb"ircond" and \verb"iszerocond" are Boolean variables,
case analysis on these variables yields a finite number of cases
to consider in the analysis.
The variable \verb"opcval", a natural number, also yields
a finite number of cases: either it is equal to one of the
eight opcode values, i.e., \mbox{\verb"opcval" $<$ 8},
or it is not a valid opcode value,
i.e., \mbox{8 $\leq$ \verb"opcval"}, in which case the theorem
is vacuously true because of the condition expressed by
\verb"Val3_CASES_ASM".

\begintt
|- \(\forall\)b1 n b2. SynCorrectness1 rep(b1,n,b2)
\endtt

The predicate \verb"SynCorrectness1" is useful
as a parameterized correctness condition when the correctness
of programming level operations are considered individually.
But when these individual correctness results
are combined in the above theorem,
the parameterized variables of \verb"SynCorrectness1"
no longer have a useful role.
The final step in verifying the microprogramming level
is to eliminate this overhead to obtain the following theorem.

\begintt
|- Val3_CASES_ASM rep \(\wedge\)
   Val4Word4_ASM rep \(\wedge\)
   SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)
   ==>
   \(\forall\)t.
     (((val4 rep) o mpc) t = 0)
     ==>
     let m = MicroCycles rep (ireq t,mem t,pc t,acc t,rtn t,iack t) in
      ((((val4 rep) o mpc) (t+m) = 0) \(\wedge\)
       ((mem (t+m),pc (t+m),acc (t+m),rtn (t+m),iack (t+m)) =
        NextState rep (ireq t,mem t,pc t,acc t,rtn t,iack t)))
\endtt

Although we extend our correctness proof with one more step
to obtain the top level statement of correctness,
the above theorem can stand alone as a substantial result
about the correctness of the \Tamarack\ design.
For all possible instruction cycles,
we have shown that the net effect of the instruction cycle
corresponds to the state change specified by \verb"NextState"
and that \verb"MicroCycles" correctly specifies the length
of each instruction cycle.

\subsection{Completing the proof}
\label{sec-verfconcl}

As mentioned earlier in Section~\ref{sec-formsem},
the programming level operation and internal architecture
are formally specified at different granularities of time.
A formal relationship needs to be established between
these two granularities of discrete time in order to complete
the verification of \Tamarack\
(operating in fully synchronous mode).

The chief source of difficulty in
the formal definition of this timing relationship
is that a unit of
discrete time at the {\it abstract} programming level time scale
does not correspond to a constant number of clock cycles on the
{\it concrete} microprogramming level time scale.
If every programming level
operation was implemented by the same number of microinstructions,
then the relationship between the two time scales could be expressed
by a very simple arithmetic equation.
However, this is not the case for our implementation of the microprocessor.
For instance, the ADD instruction is implemented by a sequence of
eight microinstructions as shown in Figure~\ref{fig-add}
whereas the JMP instruction is implemented by
a sequence of four microinstructions as shown in Figure~\ref{fig-jmp}.

\begin{figure}
\begin{center}
\input{fig-add}

\caption{ADD Instruction Cycle Timing.}
\label{fig-add}
\end{center}
\end{figure}

\begin{figure}
\begin{center}
\input{fig-jmp}

\caption{JMP Instruction Cycle Timing.}
\label{fig-jmp}
\end{center}
\end{figure}

Instead,
we define a primitive recursive function \verb"TimeOfCycle" which
computes the concrete time of every abstract time point
using \verb"MicroCycles" to determine the number of microinstructions
executed between adjacent points on the abstract time scale.
\footnote{
The definition of \verb"TimeOfCycle" is actually just
a `wrapper' for the definition of \verb"CURRIED\_TimeOfCycle";
this is a consequence of pragmatic restrictions imposed
by the \HOL\ system on the
format of parameter lists in primitive recursive definitions.}
To compute the concrete time of \verb"u+1",
we recursively compute the concrete time of \verb"u"
and then add the number given by \verb"MicroCycles" for
the length of the next microinstruction sequence
to be executed.
As with the definition of \verb"TamarackBeh" in
Section~\ref{sec-formsem},
we emphasize the distinction between abstract and concrete time
by using the variable \verb"u" for abstract time and the
variable \verb"t" for concrete time.

\begintt
let CURRIED_TimeOfCycle = new_prim_rec_definition (
  `CURRIED_TimeOfCycle`,
  "(CURRIED_TimeOfCycle (rep:^rep_ty) ireq mem pc acc rtn iack 0 = 0) \(\wedge\)
   (CURRIED_TimeOfCycle rep ireq mem pc acc rtn iack (SUC u) =
    let t = CURRIED_TimeOfCycle rep ireq mem pc acc rtn iack u in
    (t + (MicroCycles rep (ireq t,mem t,pc t,acc t,rtn t,iack t))))");;

let TimeOfCycle = new_definition (
  `TimeOfCycle`,
  "TimeOfCycle (rep:^rep_ty) (ireq,mem,pc,acc,rtn,iack) =
    CURRIED_TimeOfCycle u rep ireq mem pc acc rtn iack u");;
\endtt

The function denoted by,

\begin{quote}
\verb"TimeOfCycle (rep:^rep_ty) (ireq,mem,pc,acc,rtn,iack)"
\end{quote}

\noindent
is the desired mapping from abstract time to concrete time
represented by the downward arrows in Figures~\ref{fig-add}
and~\ref{fig-jmp}.
For instance, in the ADD microinstruction sequence where \verb"t" is
the concrete time of \verb"u",
the next point on the abstract time scale \verb"u+1",
is mapped to \verb"t+8" on the concrete time scale.
In the JMP microinstruction sequence, \verb"u+1"
is mapped to \verb"t+4".

Using this specification of the relationship between
abstract and concrete time scales,
we can derive
correctness results expressed in terms of the abstract time scale
from results already obtained which are expressed in terms
of the concrete time scale.
In particular, we want to show that
from one abstract time point to the next,
the microprocessor executes a single programming level instruction.

We first need to show that every point on the abstract
time scale corresponds to the start of a microinstruction sequence.
It is sufficient to show that every abstract time point maps to
a concrete time when the microcode program counter is zero since
every microinstruction sequence begins at this location.
It is necessary to assume that the microcode program counter
initially has the value zero; that is, time begins when the microcode
program counter is reset.
The following theorem can be proved by mathematical induction on \verb"u".

\begintt
|- Val3_CASES_ASM (rep:^rep_ty) \(\wedge\)
   Val4Word4_ASM rep \(\wedge\)
   SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) \(\wedge\)
   (((val4 rep) o mpc) 0 = 0)
   ==>
   let f = TimeOfCycle rep (ireq,mem,pc,acc,rtn,iack) in
   \(\forall\)u. ((val4 rep) o mpc) (f u) = 0");;
\endtt

Once we have shown that every point on the abstract time scale
corresponds to the beginning of an instruction cycle,
it is a relatively simple matter to complete the last step in
this version of the correctness proof for \Tamarack.
The top-level correctness theorem is expressed by the
goal term in the following call to \verb"set_goal".

\begintt
set_goal (
  [],
  "Val3_CASES_ASM (rep:^rep_ty) \(\wedge\)
   Val4Word4_ASM rep \(\wedge\)
   SynSystem rep (ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) \(\wedge\)
   (((val4 rep) o mpc) 0 = 0)
   ==>
   let f = TimeOfCycle rep (ireq,mem,pc,acc,rtn,iack) in
   TamarackBeh rep (ireq o f,mem o f,pc o f,acc o f,rtn o f,iack o f)");;
\endtt

We begin the backward proof for this theorem
by just expanding the goal with the definition of \verb"TamarackBeh".
We can see from the result of this step that
the proof is simply a matter
of combining correctness results for the microprogramming level
with facts derived the definition of \verb"TimeOfCycle".
In a nutshell, we must show that
the externally visible state of the microprocessor at time \verb"u+1"
is determined by the function \verb"NextState" from its state
at time \verb"u".

\begintt
OK..
"Val3_CASES_ASM rep \(\wedge\)
 Val4Word4_ASM rep \(\wedge\)
 SynSystem rep(ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) \(\wedge\)
 (((val4 rep) o mpc)0 = 0) ==>
 let f = TimeOfCycle rep(ireq,mem,pc,acc,rtn,iack)
 in
  (\(\forall\)u.
    (mem o f)(u + 1),(pc o f)(u + 1),(acc o f)(u + 1),(rtn o f)(u + 1),
    (iack o f)(u + 1) =
    NextState 
    rep
    ((ireq o f)u,(mem o f)u,(pc o f)u,(acc o f)u,(rtn o f)u,(iack o f)u))"

() : void
\endtt

Next, we use
standard \HOL\ techniques to
further expand the goal and move antecedents
into the assumption list.
However, the use of standard goal reduction techniques alone would
result in a goal with some cumbersome sub-terms.
These particular sub-terms are unnecessary and
it is helpful (as a technique for managing proof complexity) to replace
them with simple variables, namely,
\verb"t" and \verb"m".
These variables are introduced by means of the following two theorems
(which are trivial facts of logic).

\begintt
|- \(\exists\)t. TimeOfCycle rep(ireq,mem,pc,acc,rtn,iack)u = t

|- \(\exists\)m. MicroCycles rep(ireq t,mem t,pc t,acc t,rtn t,iack t) = m
\endtt

After these simplifications, the new goal is:

\begintt
OK..
"mem(t + m),pc(t + m),acc(t + m),rtn(t + m),iack(t + m) =
 NextState rep(ireq t,mem t,pc t,acc t,rtn t,iack t)"
    [ "Val3_CASES_ASM rep" ]
    [ "Val4Word4_ASM rep" ]
    [ "SynSystem rep(ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem)" ]
    [ "((val4 rep) o mpc)0 = 0" ]
    [ "TimeOfCycle rep(ireq,mem,pc,acc,rtn,iack)u = t" ]
    [ "MicroCycles rep(ireq t,mem t,pc t,acc t,rtn t,iack t) = m" ]

() : void
\endtt

We have already shown that every point on the abstract time scale
corresponds to the beginning of an instruction cycle.
In particular, we know that the
value of the microcode program counter \verb"mpc"
at time \verb"t" is \verb"0".

\begintt
OK..
\(\ldots\)
    [ "((val4 rep) o mpc)t = 0" ]

() : void
\endtt

We have also shown (in Section~\ref{sec-verfmicro})
that the externally visible state
of the microprocessor at the end of the instruction cycle is
related to its initial state at the beginning of the instruction cycle
by the function \verb"NextState".
This fact
is used to solve the current goal
and complete the final step in this version of the correctness proof
for \Tamarack.

\begintt
OK..

\( \ldots additional output deleted here \ldots \)

goal proved
|- Val3_CASES_ASM rep \(\wedge\)
   Val4Word4_ASM rep \(\wedge\)
   SynSystem rep(ireq,mpc,mar,pc,acc,ir,rtn,arg,buf,iack,mem) \(\wedge\)
   (((val4 rep) o mpc)0 = 0) ==>
   let f = TimeOfCycle rep(ireq,mem,pc,acc,rtn,iack)
   in
    TamarackBeh rep(ireq o f,mem o f,pc o f,acc o f,rtn o f,iack o f)

Previous subproof:
goal proved
() : void
\endtt

This theorem
relates the design of the internal architecture given by the
definition of \verb"TamarackImp" to its behavioural specification
given by the predicate \verb"TamarackBeh".
In particular, we show that the constraints imposed by
\verb"TamarackImp" on the register-transfer level signals
of the internal architecture satisfy the constraints imposed by
\verb"TamarackBeh" on the corresponding programming level signals.