Some questions about the paper

[xfzhou01]

Dear authors,

I read your work "Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition" published in FMCAD, which is a very impressive work and and I am very interested in it. I may have some questions about the experiment part of your work.

1. For the open-sourced AES example in this repo, it seems that it is represented in high-level C design, how to verify whether the accelerator generated by HLS still meets the Strong FC and dFC?
2. For the design in Verilog, it’s hard to insert the annotations to split them into sub-accelerators, especially for the designs generated from HLS (it’s hardly readable to human programmers and hard to decompose the design according to Definition 10, 11).

3. About the dSAC verification, how do you get the Spec function from different kinds of representations?

   It would be very appreciated if you could take a look at my questions above. So sorry for bothering you.

Best Wishes, Xiaofeng ZHOU

[saranyuc3]

Hi Xiaofeng,

Thank you for your interest in our project and feel free to ask more questions if the following answers still don't make sense.

1. Here we assume that the HLS tool algorithm is correct. One might argue that the HLS pragmas/new experimental HLS tool may lead to bugs in the RTL. For that we need to synthesize the A-QED function wrapper along with the sub-accelerator and run it at the RTL level. Regarding this flow, please check out: https://github.com/upscale-project/aqed-dac2020-results/tree/master/AES_abstracted.
2. This is exactly why we target designs in the HLS flow. We piggyback on the fact that HLS designers would insert pragmas around code blocks that can be synthesized to parallel operations. The batch mode blocks that we target are a subset of these blocks. So, we don't have to spend extra time identifying these blocks for verification purpose. We will lose this advantage at the RTL level even for human readable hand-written code not just machine generated RTL. We are currently working on creating a RTL level scalability technique for our framework so please stay tuned.
3. To perform the dSAC verification we need to check for just one operation in the batch mode block instead of writing the spec function for the entire batch block. Having said that, we still need to know some spec for each sub-accelerator which might reduce the productivity benefits of A-QED^2 as we decompose to finer granularity. However, the bugs targeted by dSAC are pretty well understood in industry and there are well-known techniques to catch such bugs. These bugs don't require a special sequence to get triggered and can be checked by running just one input from reset state. Even simulation has been found to be a good candidate to catch SAC bugs.

[xfzhou01]

Dear Saranyu,

Thank you very much for your timely reply! I have understood these points. I may have another small question, in Table I, why benchmarks including keypair, gsm, HLSCNN, FlexNLP, Dataflow and Opticalflow are not listed, is it affected by the batch size of sub-accelerators?

Best Wishes, Xiaofeng ZHOU

[saranyuc3]

Hi, thanks for your query. For sub-accelerators with batch size of one, strong FC (intra-batch FC check requires at least a batch size of two) will catch bugs like initialization and Out-of-Bound bugs which can also be caught by running off-the-shelf checkers like Frama-c and Infer so we didn't run FC for sub-accelerators with batch size of one. Let me know.

[xfzhou01]

Hi Saranyu, so sorry to bother you again, I am recently collecting some benchmarks for conducting model checking on HLS designs, if possible, could you provide the source code of grayscale[32|64|128] and mean[32|64|128]? Thank you so much ~

[saranyuc3]

Hi Xiaofeng,

Can you share your email id? I'll email them to you directly.

[xfzhou01]

Hi Saranyu, thank you so much for your timely response. My email address is [xzhoubu@connect.ust.hk]. Thanks ^^