diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-04-15 10:38:53 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-04-15 10:38:53 +0100 |
| commit | 2bf1ff846a792ef3007fa1e97928697509f318f7 (patch) | |
| tree | de842907b30c337f3c20a35f36fc17ede8147fd7 /proof.tex | |
| parent | 6363b3998d65dc7a4e45cec0db9b41f69f45fb31 (diff) | |
| download | oopsla21_fvhls-2bf1ff846a792ef3007fa1e97928697509f318f7.tar.gz oopsla21_fvhls-2bf1ff846a792ef3007fa1e97928697509f318f7.zip | |
Update the table
Diffstat (limited to 'proof.tex')
| -rw-r--r-- | proof.tex | 17 |
1 files changed, 9 insertions, 8 deletions
@@ -158,15 +158,16 @@ The final lemma we need is that the Verilog we generate is deterministic. This r \toprule & \textbf{Coq code} & \multicolumn{1}{p{1cm}}{\raggedleft\textbf{OCaml code}} & \textbf{Spec} & \multicolumn{1}{p{2cm}}{\raggedleft\textbf{Theorems \& Proofs}} & \textbf{Total}\\ \midrule - {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 \\ + {Data structures and libraries} & 280 & --- & --- & 500 & 780 \\ + {Integers and values} & 98 & --- & 15 & 968 & 1081 \\ + {HTL semantics} & 50 & --- & 181 & 65 & 296 \\ + {HTL generation} & 590 & --- & 66 & 3069 & 3725 \\ + {RAM generation} & 203 & --- & --- & 2843 & 3046 \\ + {Verilog semantics} & 78 & --- & 431 & 235 & 744 \\ + {Verilog generation} & 104 & --- & --- & 486 & 590 \\ + {Top-level driver, pretty printers} & 318 & 775 & --- & 189 & 1282 \\ \midrule - \textbf{Total} & 1184 & 747 & 1007 & 5526 & 8464 \\ + \textbf{Total} & 1721 & 775 & 693 & 8355 & 11544 \\ \bottomrule \end{tabular} \caption{Statistics about the numbers of lines of code in the proof and implementation of \vericert{}.} |