diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-11-18 13:56:57 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-18 13:57:08 +0000 |
| commit | a72d9e55c66d3d44b8a6c31e0941773600bd0fe5 (patch) | |
| tree | 983dadf26e3f4a342fee5ad41e48aea0601ce69f /proof.tex | |
| parent | 082f071640621153c46d7bd60a5f1ed1a8f276d1 (diff) | |
| download | oopsla21_fvhls-a72d9e55c66d3d44b8a6c31e0941773600bd0fe5.tar.gz oopsla21_fvhls-a72d9e55c66d3d44b8a6c31e0941773600bd0fe5.zip | |
Finish statistics about proof
Diffstat (limited to 'proof.tex')
| -rw-r--r-- | proof.tex | 16 |
1 files changed, 8 insertions, 8 deletions
@@ -111,15 +111,15 @@ The Verilog semantics that are used are deterministic, as the order of operation \toprule & \textbf{Coq Code} & \textbf{OCaml Code} & \textbf{Specifi\-cations} & \textbf{Theorems \& Proofs} & \textbf{Total}\\ \midrule - {\footnotesize Data structures and libraries} & 274 & - & - & 654 & 928\\ - {\footnotesize Integer, values} & 2 & 8 & 10 & &\\ - {\footnotesize HTL semantics} & 1048 & 8093 & 9141 & &\\ - {\footnotesize HTL generation} & 2 & 8 & 10 & &\\ - {\footnotesize Verilog semantics} & 2 & 8 & 10 & &\\ - {\footnotesize Verilog generation} & 2 & 8 & 10 & &\\ - {\footnotesize Top-level driver, pretty printers} & & & & &\\ + {\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 \\ \midrule - \textbf{Total} & & & & &\\ + \textbf{Total} & 1184 & 747 & 1007 & 5526 & 8464 \\ \bottomrule \end{tabular} \caption{Statistics about the proof.} |