diff options
| -rw-r--r-- | proof.tex | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -118,6 +118,8 @@ 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} + %%% Local Variables: %%% mode: latex %%% TeX-master: "main" |