diff options
Diffstat (limited to 'chapters/hls.tex')
| -rw-r--r-- | chapters/hls.tex | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/chapters/hls.tex b/chapters/hls.tex index dcdf2b2..1a5374c 100644 --- a/chapters/hls.tex +++ b/chapters/hls.tex @@ -1317,6 +1317,29 @@ $B_1$ and $B_2$ must be the same. \subsection[coq-mechanisation]{Coq Mechanisation} +\startnotmode[nolmtx] +\startplacetable[reference={tab:proof-statistics},title={Statistics about the numbers of lines of + code in the proof and implementation of Vericert.}] + \starttabulate[|l|r|r|r|r|r|] + \FL + \NC \NS[1][c] {\bf Coq code} \NS[1][c] {\bf Spec} \NC {\bf Total} \NC \NR + \ML + \NC Data structures and libraries \NC 280 \NC --- \NC --- \NC 500 \NC 780 \NC \NR + \NC Integers and values \NC 98 \NC --- \NC 15 \NC 968 \NC 1081 \NC \NR + \NC HTL semantics \NC 50 \NC --- \NC 181 \NC 65 \NC 296 \NC \NR + \NC HTL generation \NC 590 \NC --- \NC 66 \NC 3069 \NC 3725 \NC \NR + \NC RAM generation \NC 253 \NC --- \NC --- \NC 2793 \NC 3046 \NC \NR + \NC Verilog semantics \NC 78 \NC --- \NC 431 \NC 235 \NC 744 \NC \NR + \NC Verilog generation \NC 104 \NC --- \NC --- \NC 486 \NC 590 \NC \NR + \NC Top-level driver, pretty printers \NC 318 \NC 775 \NC --- \NC 189 \NC 1282 \NC \NR + \LL + \NC {\bf Total} \NC 1721 \NC 775 \NC 693 \NC 8355 \NC 11544 \NC \NR + \BL + \stoptabulate +\stopplacetable +\stopnotmode + +\startmode[nolmtx] \startplacetable[reference={tab:proof-statistics},title={Statistics about the numbers of lines of code in the proof and implementation of Vericert.}] \starttabulate[|l|r|r|r|r|r|] @@ -1336,6 +1359,7 @@ $B_1$ and $B_2$ must be the same. \HL \stoptabulate \stopplacetable +\stopmode The lines of code for the implementation and proof of can be found in \in{Table}[tab:proof-statistics]. Overall, it took about 1.5 person-years to build -- about three |