Update on Overleaf.

1 files changed, 7 insertions, 2 deletions

diff --git a/limitations.tex b/limitations.tex
index e64d427..c653a23 100644
--- a/limitations.tex
+++ b/limitations.tex
@@ -1,10 +1,15 @@
 \section{Limitations}
 
-There are various limitations in \vericert{} compared to other HLS tools due to the fact that the main focus was to formally verify the translation from 3AC to Verilog.
+There are various limitations in \vericert{} compared to other HLS tools due to the fact that our main focus was on formally verifying the translation from 3AC to Verilog. \JW{In this section, we outline the current limitations of our tool and suggest how they can be overcome in future work.}
 
 \paragraph{Lack of instruction-level parallelism}
 
-The main limitation of \vericert{} is that it does not perform scheduling of instructions into the same state, meaning that instructions cannot be executed in parallel.  However, the design of the intermediate languages in \vericert{} take this optimisation into account and are designed to support scheduling.  HTL is already an intermediate language which represents an FSMD which can have any number of statements in each state, and the semantics of HTL and Verilog allow for parallel assignments to registers.  To simplify the proof of the scheduling algorithm, and to minimise the changes necessary for the current translation from 3AC to HTL, a new language must be introduced, called 3ACPar, \JW{I think this is getting too far into the details of how to add scheduling, and risks stealing the thunder of our next submission. I think the basic point to make is: Vericert is currently all sequential, that's pretty bad, but it's not a fundamental limitation. So it's good to point out that HTL is a very general language -- anything that can be put into an always-block in Verilog can be put into an HTL state -- but I wouldn't go into details about new languages like 3ACPar here.} which would be equivalent to 3AC but instead of consisting of a map from program counter to instruction, it would consist of a map from program counter to list of instructions, which can all be executed in parallel.  A new proof for the scheduling algorithm would have to be written for the translation from 3AC to 3ACPar, for which a verified translation validation approach might be appropriate, however, the translation form 3ACPar to HTL would not change conceptually, except for the fact that multiple instructions can now be translated into the same state.  This small difference means that most of the proof can be reused without any changes, as the translation of instructions was the main body of the proof and did not change.
+The main limitation of \vericert{} is that it does not perform instruction scheduling, meaning that instructions cannot be gathered into the same state and executed in parallel.  However, the design of the intermediate languages in \vericert{} take this optimisation into account and are designed to support scheduling in the future. For instance, our HTL language allows arbitrary Verilog to appear in each state of the FSMD, including parallel assignments to registers. 
+
+Our plan for adding scheduling support involves adding a new intermediate language after 3AC, tentatively called 3ACPar. This would be similar to 3AC but rather than mapping program counters to instructions, it would map program counters to \emph{lists} of instructions that can all be executed in parallel. The translation from 3AC to 3ACPar would be performed by a scheduling algorithm. Following \cite{tristan08_formal_verif_trans_valid} and \citet{six+20}, we expect to use verified translation validation to check that the output of the scheduling algorithm is correct (rather than verify the scheduling algorithm itself).
+
+
+To simplify the proof of the scheduling algorithm, and to minimise the changes necessary for the current translation from 3AC to HTL, a new language must be introduced, called 3ACPar, \JW{I think this is getting too far into the details of how to add scheduling, and risks stealing the thunder of our next submission. I think the basic point to make is: Vericert is currently all sequential, that's pretty bad, but it's not a fundamental limitation. So it's good to point out that HTL is a very general language -- anything that can be put into an always-block in Verilog can be put into an HTL state -- but I wouldn't go into details about new languages like 3ACPar here.} which would be equivalent to 3AC but instead of consisting of a map from program counter to instruction, it would consist of a map from program counter to list of instructions, which can all be executed in parallel.  A new proof for the scheduling algorithm would have to be written for the translation from 3AC to 3ACPar, for which a verified translation validation approach might be appropriate, however, the translation form 3ACPar to HTL would not change conceptually, except for the fact that multiple instructions can now be translated into the same state.  This small difference means that most of the proof can be reused without any changes, as the translation of instructions was the main body of the proof and did not change.
 
 \paragraph{Lack of pipelined division}
 In a similar vein, the introduction of pipelined operators, especially for division, can alleviate many of the timing issues shown in the \polybench{} benchmarks with divisions included in Section~\ref{sec:evaluation}.  These operators can execute different stages of the operation in parallel, and therefore run long operations in parallel while sharing the same hardware.  In HTL, operations like this can be represented in a similar fashion to the load and store instructions to the RAM, by using wires to communicate with an abstract computation block modelled in HTL and later replaced by a hardware implementation.  However, 3ACPar would have to be modified to also describe such instructions so that these can be placed optimally using the external scheduling algorithm.