diff options
author | John Wickerson <j.wickerson@imperial.ac.uk> | 2020-11-18 16:45:04 +0000 |
---|---|---|
committer | overleaf <overleaf@localhost> | 2020-11-18 16:45:24 +0000 |
commit | 7a269041d29e22d6a16c582a0a3758e5efb70c37 (patch) | |
tree | 9129d4888c6b70d866c421d0700f40ecf08c225e /proof.tex | |
parent | 11b2a38aec9323ad4bc69ff7505e7f24f6833b39 (diff) | |
download | oopsla21_fvhls-7a269041d29e22d6a16c582a0a3758e5efb70c37.tar.gz oopsla21_fvhls-7a269041d29e22d6a16c582a0a3758e5efb70c37.zip |
Update on Overleaf.
Diffstat (limited to 'proof.tex')
-rw-r--r-- | proof.tex | 18 |
1 files changed, 9 insertions, 9 deletions
@@ -104,17 +104,17 @@ The Verilog semantics that are used are deterministic, as the order of operation \begin{table*} \centering - \begin{tabular}{p{4cm}p{1cm}p{1cm}p{1cm}p{1.5cm}p{1cm}} + \begin{tabular}{llllll} \toprule - & \textbf{Coq Code} & \textbf{OCaml Code} & \textbf{Specifi\-cations} & \textbf{Theorems \& Proofs} & \textbf{Total}\\ + & \textbf{Coq code} & \textbf{OCaml code} & \textbf{Specifications} & \textbf{Theorems \& Proofs} & \textbf{Total}\\ \midrule - {\footnotesize Data structures and libraries} & 274 & - & - & 654 & 928 \\ - {\footnotesize Integers and values} & 98 & - & 15 & 744 & 857 \\ - {\footnotesize HTL semantics} & - & - & 174 & - & 174 \\ - {\footnotesize HTL generation} & 655 & - & 79 & 3349 & 4083 \\ - {\footnotesize Verilog semantics} & - & - & 739 & 174 & 913 \\ - {\footnotesize Verilog generation} & 68 & - & - & 396 & 464 \\ - {\footnotesize Top-level driver, pretty printers} & 89 & 747 & - & 209 & 1045 \\ + {Data structures and libraries} & 274 & - & - & 654 & 928 \\ + {Integers and values} & 98 & - & 15 & 744 & 857 \\ + {HTL semantics} & - & - & 174 & - & 174 \\ + {HTL generation} & 655 & - & 79 & 3349 & 4083 \\ + {Verilog semantics} & - & - & 739 & 174 & 913 \\ + {Verilog generation} & 68 & - & - & 396 & 464 \\ + {Top-level driver, pretty printers} & 89 & 747 & - & 209 & 1045 \\ \midrule \textbf{Total} & 1184 & 747 & 1007 & 5526 & 8464 \\ \bottomrule |