Add the reviews

1 files changed, 85 insertions, 0 deletions

diff --git a/reviews.md b/reviews.md
new file mode 100644
index 0000000..5546faf
--- /dev/null
+++ b/reviews.md
@@ -0,0 +1,85 @@
+Review #3A
+===========================================================================
+
+Discussion-provoking potential
+------------------------------
+4. Very likely to provoke excellent discussion
+
+Paper summary
+-------------
+This paper argues that C-based HLS tools should formally verified to combat the error-prone nature of developing compilers in general, and HLS compilers specifically. The paper presents six possible objections this position and presents point-by-point rebuttals.
+
+Comments for author
+-------------------
+I think this paper will provoke discussion at the workshop.
+
+The authors do a good job of laying out possible objections to this work and rebutting (I wish conference papers came with this level of practical self-reflection.) The vision of a fully verified HLS stack is a compelling one—previous work on CompCert has already shown that verified compilers tend to be less buggy than industrial strength compilers [Yang et al. PLDI 11].
+
+However, there are two points of disagreement I have with the arguments in the paper:
+
+*People should not be designing hardware in C to begin with.*
+The authors broadly lay out two arguments:
+(1) Initial models of hardware is often written in C making it a natural starting point for hardware designs, and
+(2) C enables quick behavioral testing.
+
+(1) is increasingly becoming less true as interest in hardware design grows. For example, tools like PyMTL enable designers to build behavioral models of hardware in Python and connect them to fully synthesizable circuits to perform multi-level modeling.
+Such approaches, where hardware design languages are embedded in software languages to enable productive meta-programming and multi-level modeling, will increasingly dominate the way hardware is modeled and designed in the future. HardCaml, Chisel, and PyRTL are other examples of such tools.
+
+(2) This is true of any language chosen for the purpose of hardware synthesis—if I choose to compile Python to hardware designs, it will *also* enable quick behavioral testing. This is not an argument for why C is the right input language for verified HLS; it's an argument for why existing software languages are a good input language for HLS.
+
+*Any HLS tool that is simple enough for formal verification to be feasible won't produce sufficiently optimised designs to be useful.*
+I'm confused about the choice to not formally verify the scheduling step which is often the crucial and bug ridden part of the compiler. The system of difference constraints (SDC)-based schedulers are a reasonable start by commercial compilers use a more complicated variant called SDC-SAT [Dai et al. FPGA 18] which also attempts to minimize the resource usage and
+pipeline delays.
+To me, this is the most interesting part of the verifying an HLS compiler since even an SDC scheduler has to make heuristic decisions. Verifying the correctness of, for example, translating from the CFG to a state machine in RTL that enables the right assignments is less interesting.
+
+Regardless, I think this is a well-written position paper and will provoke discussion
+
+
+* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
+
+
+Review #3B
+===========================================================================
+
+Discussion-provoking potential
+------------------------------
+4. Very likely to provoke excellent discussion
+
+Paper summary
+-------------
+The authors argue that formal verification of HLS tools could decrease the flakyness of HLS tools.
+The paper follows a dialectical method, presenting alternatively arguments downplaying the usefulness of formal verification of HLS tools, and the author responses.
+
+Comments for author
+-------------------
+# Quality flakyness  versus functional correctness flakyness
+
+What comes to my mind when one talk about the flakyness of HLS tools is the fact that the quality of the hardware the tool output is very impredictable (mentioned in [2], for example). 
+
+I understand that this paper does not intend to address this kind of flakyness,  but I think this paper may indirectly lump together the two problems: the predictability of the quality of the output (which is not mentioned, but that spontaneously come to mind for an HLS user) and the functional correctness aspect.
+
+I guess the predictability problem can be argued to be distantly related to Objection 1, but I did not think that the paper articulated that very well, while it would have been a first order Objection in my mind. The paper deserves to be scoped a little more on that subject.
+
+#  C semantics sufficient: lack of synthesis/scheduling dependency?
+
+The bit of technical description leaking into the answer to the last Objection led me to have trouble reconciling what is presented here with some previous work I had read [1].
+
+My understanding, coming from paper [1], was that the semantics of HLS programs is actually not their direct C semantics. Instead, the HLS programs are fundamentally considered non-deterministics, even when there is no undefined behavior (in this question/concern I only consider such programs).
+
+It looked like HLS tools designer wishes the semantics to be non-deterministics to leave room for the scheduling/synthesis engine, to choose one or an other timing for the synthesized hardware.
+And as pointed out by [1], in certain case it surprisingly even leads to something akin to functional correctness error.
+
+The bottom line, is that to be able to write a correct HLS simulator (in the sense that it gives the same answer than the hardware), they can't just run the C, they need to reverse engineer the choices made by the synthesis algorithm when it targets hardware and extract those choices, and instrument the C to "replay those choices" in simulation.
+
+Hence, from their work, it seems that the cycle-accurate semantics of the program is not a property of just the program (with just the program the semantics is non-deterministic), it is a property of the program *and of the choice made by the synthesis/scheduling algorithm*.
+
+I have difficulty to reconcile this with this paper that seems to say that the semantics of your source program is just its deterministic C semantics coming from Compcert: the choices made by synthesis/scheduling seems to have disappeared from the equation.
+
+It would be helpful to get some clue about why the problems [1] face seems to have disappeared in your setup.
+
+# Most objections are generic
+
+(Objection 2, 3, 4, 5, 6) are fairly generic and not specific about hardware languages.
+Their response are also standard "why proofs  of compiler are useful".
+
+This is neither a problem nor a weakness, but I believe it could have been more explicitly pointed out that many of those concern have little to do with hardware (or if they do, or their answer do, I would have missed that).