diff options
Diffstat (limited to 'proof.tex')
| -rw-r--r-- | proof.tex | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -93,7 +93,7 @@ Finally, to prove the backward simulation given the forward simulation, it has t The Verilog semantics that are used are deterministic, as the order of operation of all the constructs is defined. -\subsection{Coq Mechanisation} +%\subsection{Coq Mechanisation} \JW{Would be nice to include a few high-level metrics here. How many person-years of effort was the proof (very roughly)? How many lines of Coq? How many files, how many lemmas? How long does it take for the Coq proof to execute?} @@ -118,7 +118,7 @@ x \div 2^y = The \compcert{} semantics for the \texttt{Oshrximm} instruction express it's operation exactly as shown in the equation above, even though in hardware the computation that would be performed would be different. In \vericert{}, if the same operation would be implemented using Verilog operators, it is not guaranteed to be optimised correctly by the synthesis tools that convert the Verilog into a circuit. To guarantee an output that does not include divides, we therefore have to express it in Verilog using shifts, and then prove that this representation is equivalent to the divide representation used in the \compcert{} semantics. This proof discovered quite a few bugs in our initial implementation of optimisations, which rounded to $-\infty$ instead of 0. -\subsection{Coq Mechanisation} +%\subsection{Coq Mechanisation} %%% Local Variables: %%% mode: latex |