Add reviews

1 files changed, 67 insertions, 0 deletions

diff --git a/review.md b/review.md
new file mode 100644
index 0000000..c863082
--- /dev/null
+++ b/review.md
@@ -0,0 +1,67 @@
+# FCCM'22 Response
+
+We're very grateful to the reviewers for their encouraging words about our work, and their thoughtful and detailed comments.
+
+## Review 1
+
+> Does Vericert-Fun require pragmas to indicate sharing?
+
+No, this is entirely automated -- all functions that can be shared are shared. It will be straightforward to add pragmas that give the programmer control over which functions are shared, because having proved that sharing is correct in general, we can share as little or as much as we like without affecting correctness.
+
+> Function block sharing in FPGAs sometimes increases area due to the need for multiplexer insertion. How big are the shared functions represented in Figure 6 compared to multiplexers?
+
+As a consequence of Vericert-Fun not supporting the sharing of functions that contain call instructions, it is the case that whenever there are multiple calls to the same function, those calls must come from the same always-block. This means that we don't need explicit multiplexers in the generated Verilog. (Vivado will most likely insert multiplexers during synthesis to implement those always-blocks correctly, but the impact of this is not something we can measure directly.)
+
+## Review 2
+
+> The limited 20% cost saving is surprising.
+
+This is a consequence of our current prototype implementation only being able to share _some_ functions; i.e., those that do not contain loads, stores, or calls. Once we add support for more sharing, we expect the cost saving to increase accordingly.
+
+> The baseline should include a soft-core processor running code to show the HLS outcome advantageous across cost and performance.
+
+We agree that it is worthwhile in general to show that HLS produces better results than running code on a softcore processor, but we're not sure that this baseline would be the right one for this piece of work, given that we're not proposing a _new_ HLS tool, but rather, investigating how to make an _existing_ HLS tool produce smaller designs. We think the relevant baselines are: (1) the original verified HLS tool without any area-minimising optimisations, and (2) a state-of-the-art (but unverified) HLS tool with area-minimising optimisations.
+
+## Review 3
+
+> Its research value seems limited since function sharing is already implemented in most existing HLS tools.
+
+We agree that function sharing is already a well understood optimisation. Rather, we think that the research value of our work is in how to implement function sharing in a manner that is amenable to formal verification, how to carry out that formal verification, and what the costs and benefits of doing so are.
+
+> It would be great to discuss how scalable the approach is. For example, by increasing the CFGs, how well can it support many functions?
+
+This is a very good suggestion, thank you. When we revise and extend this work into a full-length paper, we would like to include an experiment where we evaluate Vericert-Fun on an artificial benchmark containing programs with N function calls, and measure how the compilation time and the quality of the generated hardware scale with N.
+
+## Review 4
+
+> Does Vericert-Fun provide pragmas to guide resource-sharing?
+
+It provides command-line arguments to choose between full inlining and resource sharing. Finer control over the resource-sharing would not be terribly useful currently because relatively few functions can be shared. Adding pragmas is straightforward implementation work, requiring no changes to the proofs -- that's because once we have proved that sharing is correct in general, then whether or not resource sharing is applied to a particular function does not affect correctness.
+
+> Providing more details about how HTL was extended.
+
+Yes, the short page limit meant we had to be very terse when it came to describing our extensions to the HTL language and describing the details of our proof. We intend to expand on these aspects of our project when we revise the manuscript into a full-length paper.
+
+> A wider category of functions should be treated as local state machines rather than being inlined.
+
+Currently, due to limitations of the proof, relatively few functions can be shared, so there is not much scope for evaluating Vericert-Fun on a larger category of programs. However, it should be possible to design artificial benchmarks, as Reviewer 3 suggests, for testing the compilation of programs that have more functions and function calls.
+
+> Are any directives given to Bambu?
+
+No directives were inserted into the code, but Bambu was run using the `--experimental-setup=BAMBU-AREA` flag, which tries to optimise for area.
+
+> How do you measure the area of the generated design?
+
+To compare the area of the generated designs, we used the number of slices from the utilization report that Vivado generates.
+
+> Could you provide an evaluation on the negative effect caused by the incomplete proof?
+
+The impact of the incomplete proof is simply that we cannot yet guarantee the correctness of our implementation. Technically, we guarantee precisely nothing until the proof is 100% complete; in practice, the iterative process of developing the proof and the implementation in tandem leads to a tool that we suspect is already likely to have fewer bugs than a tool that has not been subjected to any correctness proof.
+
+> It would be clearer if the effect of the stack were described.
+
+The layout and implementation of the stack did not change from the original Vericert, so we elided these details because of the page limit. More details about the stack can be found in Herklotz et al.'s OOPSLA 2021 paper, reference 12.
+
+> Are nested functions supported?
+
+Nested function calls are supported insofar as they are inlined at each call site, as they will contain call instructions.  Only functions that are at the innermost level of nesting can be shared. So, for instance, if main() calls f() and g(), and f() and g() both call h(), then f() and g() will be inlined into main() and h() will be shared.