diff options
Diffstat (limited to 'evaluation.tex')
| -rw-r--r-- | evaluation.tex | 44 |
1 files changed, 22 insertions, 22 deletions
diff --git a/evaluation.tex b/evaluation.tex index 17e2e36..45fcc27 100644 --- a/evaluation.tex +++ b/evaluation.tex @@ -2,31 +2,31 @@ \NR{Do we want to collect C-to-Verilog compile time?} \begin{table} -\begin{tabular}{|l|c|c|c|c|c|c|} -\hline -Benchmark & Cycles & Frequency & LUTs & Registers & BRAMs\\ -\hline\hline -adpcm & 30241 &90.05 & 7719 & 12034 & 7\\\hline -aes & 8489 & 87.83 & 24413 & 23796 & 19 \\\hline -gsm & 7190 & 119.25 & 6638 & 9201 & 3 \\\hline -mips & 7754 & 98.95 & 5049 & 4185 & 0 \\\hline -\hline -\end{tabular} -\caption{CHstone programs synthesised in LegUp 5.1} + \begin{tabular}{lcccccc} + \toprule + Benchmark & Cycles & Frequency & LUTs & Registers & BRAMs\\ + \midrule + adpcm & 30241 &90.05 & 7719 & 12034 & 7\\ + aes & 8489 & 87.83 & 24413 & 23796 & 19 \\ + gsm & 7190 & 119.25 & 6638 & 9201 & 3 \\ + mips & 7754 & 98.95 & 5049 & 4185 & 0 \\ + \bottomrule + \end{tabular} + \caption{CHstone programs synthesised in LegUp 5.1} \end{table} \begin{table} -\begin{tabular}{|l|c|c|c|c|c|c|} -\hline -Benchmark & Cycles & Frequency & LUTs & Registers & BRAMs\\ -\hline\hline -adpcm & XXX & XXX & XXX & XXX & XXX \\\hline -aes & 41958 & & & & \\\hline -gsm & 21994 & & & & \\\hline -mips & 18482 & 78.43 & 10617 & 7690 & 0 \\\hline -\hline -\end{tabular} -\caption{CHstone programs synthesised in CoqUp} + \begin{tabular}{lcccccc} + \toprule + Benchmark & Cycles & Frequency & LUTs & Registers & BRAMs\\ + \midrule + adpcm & XXX & XXX & XXX & XXX & XXX \\ + aes & 41958 & & & & \\ + gsm & 21994 & & & & \\ + mips & 18482 & 78.43 & 10617 & 7690 & 0 \\ + \bottomrule + \end{tabular} + \caption{CHstone programs synthesised in CoqUp} \end{table} The difference in cycle counts shows the degree of parallelism that LegUp's scheduling and memory system can offer. However, their Verilog generation is not guaranteed to be correct. Although the runtime LegUp outputs are tested to be correct for these programs, this does not provide any confidence on the correctness of Verilog generation of any other programs. Our Coq proof mechanisation guarantees that generated Verilog is correct for any input program that uses the subset of CompCert instructions that we have proven to be correct. |