
Verification of the ISE implementation is done using a mixture of
directed testing and formal methods.

\subsection{Formal Verification Flow}

The formal flow uses Yosys and Boolector as a model checker to ensure that
for any sequence of inputs, the implementation behaves correctly with
respect to the implementation.

\subsubsection{Relevent Files}

These are the files and directories relevent to the formal flow:

\begin{itemize}
\item {\tt \$REPO\_HOME/flow/yosys/} - 
    Makefiles and synthesis scripts for turning the Verilog testbench
    and design into an SMT2 representation.
\item {\tt \$REPO\_HOME/rtl/coprocessor/} - 
    The RTL design files.
\item {\tt \$REPO\_HOME/verif/formal/} - 
    The set of property contexts used to express assertions about valid
    design behaviour. Note the contents of {\tt fml\_common.vh}, which
    defines many of the macros used across the formal environment.
\item {\tt \$REPO\_HOME/verif/tb/} - 
    Contains the top-level formal testbench {\tt tb\_formal.vh}.
\item {\tt \$XC\_WORK/smt2/} - 
    Contains the generated SMT2 files, along with logs of SMT2 file
    generation, proof progress/results and any failure traces as VCD
    files.
\end{itemize}

The formal flow also depends on the {\em generate} RTL code for the
instruction decoder.
This exists as {\tt \$XC\_WORK/ise\_decode.v} and is generated by
the {\tt rtl\_decoder} Makefile target.

\subsubsection{Flow Architecture}

\begin{figure}[h]
\centering
\includegraphics[width=0.7\textwidth]{image/formal-flow.pdf}
\caption{Information flow graph for the formal verfication flow. Rectangles
represent files, ellipses are programs / transformations on those files,
diamonds are proof outcomes.}
\label{fig:formal-flow}
\end{figure}

The high-level sequence of actions in the formal flow are shown in figure
\ref{fig:formal-flow}.

\begin{enumerate}
\item All hand-coded RTL, generated RTL, testbench code and actual
    formal assertions are gathered and fed into \yosys.
\item The \yosys tool transforms the Verilog source code into an SMT2
    representation suitable for ingestion by the formal tool we will use
    to actually do the proofs.
    The script \yosys uses to do this is found in
    {\tt \$REPO\_HOME/flow/yosys/write-smt-tb.ys}.
\item The SMT2 output is generated on a per-property-context basis.
    Each file in
    {\tt \$REPO\_HOME/verif/formal/}
    contains a single property context.
    Hence, each file here will have a corresponding {\tt .smt2}
    file generated by \yosys and placed in
    {\tt \$XC\_WORK/smt2/}.
    A property context is a logical grouping of information and assertions
    corresponding to some single feature of the design.
    Most property contexts correspond to a single instruction.
\item Each SMT2 file is then fed into the solver engine.
    This will produce either a bounded proof, or a counter example trace
    showing how the design can reach an invalid state with respect to
    one or more of the assertions.
\item The final result is a set of N reports (1 per property context)
    detailing either the failing assertion(s) and corresponding traces,
    or a pass result.
\item All proofs are run with a 10 hour automatic timeout.
    Proofs which timeout without finding a counter example are treated
    as a "qualified pass".
\end{enumerate}

All checks are run for atleast 10 cycles worth of design operation after
a reset.
This is enough time to observe one execution of every instruction (with
some important caveats detailed later) and check that they generate the
correct result.
It would be better if deeper proofs could be achieved, but the timeframe of
the project does not allow for more.
Some proofs run for specific cycle counts in order to cover the design
behaviour.
These custom proof depths are specified in 
{\tt \$REPO\_HOME/flow/yosys/proof-depths.mk}.

\subsubsection{Testbench Architecture}

The testbench is written completely in Verilog 2005 to match the RTL.
The architecture of the testbench is shown in Figure
\ref{fig:formal-tb-arch}.

\begin{figure}[h]
\centering
\includegraphics[width=0.7\textwidth]{image/formal-testbench.pdf}
\caption{Architecture of the formal testbench showing the DUV instantiation,
transaction capture and alignment logic, environmnet properties and
the property context with assertions.}
\label{fig:formal-tb-arch}
\end{figure}

The top level testbench ({\tt \$REPO\_HOME/verif/tb/tb\_formal.v}) contains
the following objects:

\begin{itemize}
\item The DUV instantiation.
\item Environment properties.
    These constrain the primary inputs driven by the formal engine so that
    they are a fair representation of the wider DUV operating environment.
\item Alignment Logic.
    This consists of a set of FIFOs which capture and align corresponding
    event information so it can be fed to the property context as a single
    transaction for verification.
    Key to this is associating an input instruction with it's eventual
    output result, which might not appear until many cycles after the
    instruction was initially accepted.
    Also included is capture of memory transactions associated with a
    particular instruction.
\item Monitor ports.
    These are probes into the design which are {\em only} used for
    verification. In this testbench, they mainly consist of register file
    sample signals and random number generator sampling.
\item The current property context with the assertions to be proved.
    Each property context is implemented as a verilog module.
    Each property context has an indentical interface, defined by the
    {\tt `VTX\_CHECKER\_MODULE\_BEGIN}
    macro in
    {\tt \$REPO\_HOME/verif/formal/fml\_common.vh}.
    At the top level, we swap different property context modules in and
    out of the design by re-defining the value of the
    {\tt `FML\_CHECK\_NAME}
    macro when parsing the design with \yosys.
\end{itemize}

\noindent
Each property context then contains:

\begin{itemize}
\item The set of property inputs used by all property contexts.
    These represent the pre/post state of the design and the instruction
    which caused the state transition.
\item A number of helper logic constructs which are usually used to generate
    things like expected results/values.
\item A set of assertions which use the property inputs to express valid
    state transitions for the given instruction being checked.
\end{itemize}

\subsubsection{Formal Flow Bug List}

This section is a {\em trophy cabinet} of bugs found using the formal
verification flow.

\begin{itemize}
\item Input instruction and RS1 data not registered properly by the COP during
    stalled or multi-cycle execution.
\item Memory read data polluting other writeback data when no memory
    instruction was active due to poorly gated and/or tree.
\item Memory bus error exception raised ahead of invalid opcode exception.
\item Memory bus errors being raised when no memory instruction was active.
\item Pack width instructions not raising invalid opcode exceptions for
    invalid pack widths.
\item Raising invalid pack width exceptions for instructions with no pack
    width fields.
\item Design shift amount fields 1 bit too big resulting in different results
    only when the pack width is 1 and the operand values were in a certain
    range.
\item Rotate instruction {\em model} was incorrect if the rotate ammount was
    greater than twice the pack width.
\item Insert bitfield instruction was blanking out destination beyond the
    bitfield.
\item All memory instructions were not recording transaction history correctly.
\item A bus error in the first cycle of a memory transaction caused memory
    transactions to be missed in the formal environment, even though it
    should have been ignored iff it was the first cycle of the transaction.
\item Scatter/Gather instruction addresses were not correctly registered
    by the formal verification interface.
\item Scatter instructions set write enable but no byte enable bits.
\item {\tt mgte} Instruction gave incorrect result iff crs2==crs3.
\item {\tt msrl} and {\tt msll} didn't give a 0 result if the shift
    amount was out of bounds.
\item {\tt mmul.3} was missing the final addition writeback due to not
    storing temporaries properly.
\item {\tt pmul.l} did not mask partial sums properly and was writing
    intermediate results to the register file.
\item {\tt pclmul.*} instructions did not clear the accumulator register
    properly, meaning the results of a previous instruction poluted the
    next one.
\item We found that if the design is fed a {\em valid} instruction which
    was not then handled by one of the functional units, the design would
    deadlock.
    This was discovered by the coverage checks, rather than correctness
    assertions.
    A new check was added that asserts all accepted instructions are
    retired within 36 cycles or fewer, thus proving the absence of
    deadlocks.
\item AES instructions did not store their partial results before
    writing them back to the register file. If source registers were the
    same as the destination register, this could lead to corruption of
    results.
\end{itemize}


\subsubsection{Flow Limitations}

While we are confident that the design is robust with respect to the
specification, there are several known holes in the current formal
verification effort which were not fillable due to time constraints on
the project.

\begin{itemize}
\item The design and verification was done by a single person. This
    is considered bad practice, as that person lacks a "fresh pair
    of eyes" needed to critically analyse a design.
    This situation was impossible to avoid during the project for
    lack of person power.
\item We know that every assertion within the formal environment is
    covered during BMC, but we cannot know if our property set is
    ``complete" in the sense it covers the entire design all of the
    time.
    This would require extending our toolset, and fell outside the
    scope of the project.
\end{itemize}

\noindent
All of these represent valid and valuable areas for future work /
external contributions.
