Update on Overleaf.

1 files changed, 3 insertions, 1 deletions

diff --git a/evaluation.tex b/evaluation.tex
index 4d4eb32..056aa18 100644
--- a/evaluation.tex
+++ b/evaluation.tex
@@ -101,7 +101,9 @@ It is notable that even without \vericert{} performing many optimisations, a few
 %We are very encouraged by these data points. 
 As we improve \vericert{} by incorporating further  optimisations, this gap should reduce whilst preserving our correctness guarantees.
 
-Cycle count is one factor in calculating execution latency. The other factor is the clock frequency, which tells us how fast a cycle executes. Figure~\ref{fig:comparison_time} compares the execution times of \vericert{} and \legup{}. On average, \vericert{} designs are about $10\times$ slower than \legup{} designs. As mentioned earlier, we modify the Polybench programs to utilise C-based divides and modulos. We had to avoid using the built-in Verilog divides and modulos, since Quartus interprets them as single-cycle operations. This interpretation affects clock frequency drastically. On average, when using the built-in Verilog approach, \vericert{}'s clock frequency was 21MHz, compared to \legup{}'s clock frequency of 247MHz. By moving to the C-based approach, our average clock frequency is now 112MHz. Hence, we reduce the frequency gap from approximately $12\times$ to $2\times$. This gap still exists because \legup{} uses various optimisation tactics and Intel-specific IPs, which requires further engineering effort and testing from our side. 
+Cycle count is one factor in calculating execution times; the other is the clock frequency, which determines the duration of each of these cycles. Figure~\ref{fig:comparison_time} compares the execution times of \vericert{} and \legup{}. Across the original Polybench/C benchmarks, we see that \vericert{} designs are about $60\times$ slower than \legup{} designs. This more dramatic 
+
+As mentioned earlier, we modify the Polybench programs to utilise C-based divides and modulos. We had to avoid using the built-in Verilog divides and modulos, since Quartus interprets them as single-cycle operations. This interpretation affects clock frequency drastically. On average, when using the built-in Verilog approach, \vericert{}'s clock frequency was 21MHz, compared to \legup{}'s clock frequency of 247MHz. By moving to the C-based approach, our average clock frequency is now 112MHz. Hence, we reduce the frequency gap from approximately $12\times$ to $2\times$. This gap still exists because \legup{} uses various optimisation tactics and Intel-specific IPs, which requires further engineering effort and testing from our side. 
 
 % 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.