Sam comments on abstract

Author: cowardsa

paper.tex

@@ -273,7 +273,7 @@
 \begin{abstract}
 % An abstract should consist of six main sentences:
 %  1. Introduction. In one sentence, what’s the topic?
-Datapath circuits are the core computational units of the digital designs;
+Datapath circuits are the core computational units of \sam[the]{} digital designs;
 being the most timing-critical part of the design, they are aggressively optimized.
 %  2. State the problem you tackle.
 These aggresive optimizations, such as application of compression trees, make datapath circuits hard to verify.
@@ -287,23 +287,23 @@
 Our insight is that these methods attempt to tackle the verification problem at the wrong stage.
 They are all post-synthesis, where the structure of the circuit optimization has already been lost.
 Instead, we propose a pre-synthesis approach, where we build a formally verified
-synthesis pipeline built on the interactive theorem proving.
+synthesis pipeline built on \sam[the]{} interactive theorem proving.
 This eliminates the need for an expensive post-synthesis verification,
 instead leveraging the ability to implement correct-by-construction algorithms in a theorem prover.
 %  5. In one sentence, how did you go about doing the research that follows from your big idea.
 For this approach, we phrase circuit synthesis as a bit-heap compression problem.
-We formalize bit heap data structure and its operations in the Lean theorem prover,
+We formalize \sam{the} bit heap data structure and its operations in the Lean theorem prover,
 synthesize compression trees with this data structure,
-and prove the correctness of these optimizations and the datapath synthesis as a whole.
+and prove the correctness of these optimizations and \sam[the]{} datapath synthesis as a whole.
 % Has real numbers
 Furthermore, our framework produces circuits that are consumed by the CIRCT framework, 
 that when applied to real world circuit designs, are \SynthesisSpeedupGeomean{} faster
-in synthesis plus verification time on state-of-the-art verificiation tools,
+in synthesis plus verification time \sam[on]{grammar feels off} state-of-the-art verificiation tools,
 while only being \PerformanceSlowdownGeomean{} slower than the state of the art synthesis.
 %  6. As a single sentence, what’s the key impact of your research?
 This demonstrates that our approach provides orders of magnitude speedup on verification,
-while not sacrificing performance. 
-Overall, our approach lays down the foundations for fast, performant datapath circuit synthesis.
+while not \sam[sacrificing performance]{Runtime performance yes - circuit quality which feels like a measure of perf for a synthesis tool - I would not claim.}. 
+Overall, our approach lays down the foundations for fast, performant datapath circuit synthesis.\sam{Surely the focus is correct/verified not fast and performant - what does performant mean here - before it meant runtime now it means circuit quality?}
 % (http://www.easterbrook.ca/steve/2010/01/how-to-write-a-scientific-abstract-in-six-easy-steps/)
 
 \end{abstract}