Remove unnecessary \MP comment from introduction

1 files changed, 1 insertions, 2 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index 7f5f57c..0efccb9 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -90,8 +90,7 @@ escapeinside=||,
 \begin{abstract}
   High-level synthesis (HLS) is playing an ever-increasing role in hardware design, but concerns have been raised about its reliability. Seeking to address these concerns, Herklotz et al. have recently developed an HLS compiler, called \vericert{}, that has been mechanically proven (using the Coq proof assistant) to output Verilog designs that are behaviourally equivalent to the input C program. Unfortunately, \vericert{}'s output cannot compete performance-wise with that of established HLS tools such as LegUp. A major reason for this is \vericert{}'s complete lack of support for resource sharing. 
   
-  In this paper, we present \vericertfun: \vericert{} extended with function-level resource sharing. Where original \vericert{} creates one block of hardware per function \emph{call}, %\MP{Is this an over-simplification? We don't really generate a `block of hardware' for function calls}
-  \vericertfun{} creates one block of hardware per function \emph{definition}. The enabling innovation is to extend \vericert{}'s intermediate language HTL with the ability to represent \emph{multiple} state machines, and then to add support for function calls that transfer control between these state machines. We are working to extend \vericert{}'s formal correctness proof to cover the translation from C source into this extended HTL language, and thence on to Verilog.
+  In this paper, we present \vericertfun: \vericert{} extended with function-level resource sharing. Where original \vericert{} creates one block of hardware per function \emph{call},   \vericertfun{} creates one block of hardware per function \emph{definition}. The enabling innovation is to extend \vericert{}'s intermediate language HTL with the ability to represent \emph{multiple} state machines, and then to add support for function calls that transfer control between these state machines. We are working to extend \vericert{}'s formal correctness proof to cover the translation from C source into this extended HTL language, and thence on to Verilog.
   
 We have benchmarked \vericertfun's performance on the PolyBench/C suite, and our results show the generated hardware having a resource usage of 61\% of \vericert{}'s on average and 46\% in the best case, for only a 3\% average decrease in max frequency and 1\% average increase in cycle count.
 \end{abstract}