remove unreferenced chapter

irr/irr.tex

-\clearemptydoublepage
-\chapter{IRR: an Intermediate Representation for Reasoning}
-\label{ch:irr}
-
-This chapter motivates and discusses the methodology used for verifying hardware
-throughout this thesis.
-
-In a few words, it is about turning descriptions of hardware written in a
-high-level HDL to a lower-level, explicit form. All formal reasoning, be it
-manual or automatic, is done on terms of this generic form, which we call an IRR
-(Intermediate Representation for Reasoning).
-
-There are two main reasons why we do this. First, remember that we are working
-from within the Coq proof assistant. Large workloads such as descriptions of
-processors really put a strain on current generation proof assistants. As we
-shall see, there are some ways of getting around this issue, but none of them
-are convenient. It turns out that keeping everything explicit and staying clear
-of fancy features really does help with performance. Note that this is more of
-an engineering problem more than a fundamental issue with formal methods. The
-second reason is that such low-level, explicit forms are very close to what
-powerful proof search automation tools such as SMT solvers take as input. One of
-the main issues with formal methods is the cost that they incur. Bringing
-automation tools in is a good way to bridge the complexity gap between verified
-and unverified developments.
-
-% This chapter starts with a discussion of the performance profile of proof
-% assistants in section~\ref{sec:perf}. Section~\ref{sec:hw_verif_perf} follows
-% with a discussion of how this is relevant to the problem of processor
-% verification and compares approaches for dealing with the unique challenges of
-% this field. The approach followed throughout this thesis is presented in greater
-% detail in section~\ref{sec:irr_detail}. Finally,
-% section~\ref{sec:irr_extensions} closes this chapter by mentioning some
-% possible extensions of this approach.
-
-\section{Generalizations of IRR}
-\label{sec:irr_extensions}