[Formal] High-Level Synthesis Tools should be Proven Correct

[ymherklotz]

Authors: Yann Herklotz (@ymherklotz) and John Wickerson (@johnwickerson)
Paper PDF: https://capra.cs.cornell.edu/latte21/paper/3.pdf
Talk Recording: https://youtu.be/Olhbhq46Amc

[stephenneuendorffer]

It seems like in order to make this work, you need to prove things not only about behavior, but also about performance and the secondary constraints that HLS take as input. This seems significantly different than traditional 'certified compilers'?

[ymherklotz]

Thanks for the question, yes definitely, and it's actually something that was mention in the reviews, so we added a tiny section about that. Currently, we don't make any formal claims about performance, and we'll be as flaky as other HLS tools at the moment in that respect. But it would be really interesting to add theorems that talk about performance, which might be similar to how CompCert can prove preservation of constant-time. One could see if a similar theorem could be defined for performance.

[1] https://dl.acm.org/doi/10.1145/3371075

[sampsyo]

Generally speaking, it seems like an interesting problem take work on cost semantics from the "normal" PL world and see how they play out in HLS land. (Not that I know much work on formal verification of cost semantics and their preservation through compilation anyway!)

[rachitnigam]

A key problem with HLS-like tools is that they also have to reason about structural and timing behavior of hardware designs (implied by the software program). What kind of language-level modeling do you have to do to capture these behaviors and prove timing/structural optimizations correct?

[Arkh42]

I'm also interested in the estimation of the optimization performance and the time saved by using the proposed HLS tool.

[ymherklotz]

Thanks for the question, we have a timed intermediate language called HTL, which is basically a representation of a finite state machine with data-path. Using this, one can either add states and state transitions, but one can also express specifications of external constructs (such as RAMs or pipelined dividers) and reason about them in the proof, without have to reason about the circuit itself. Then, when translating to Verilog one can prove that the Verilog implements these specifications.

[joaobispo]

What is the HLS idiom that is supported by Vericert? Does it support pragmas similar to the ones used by Vivado tools? Should it support them? (thinking about the pipeline-related pragmas)

[ymherklotz]

Thanks for the question, currently we don't even support scheduling, so we don't really have anything which pragmas could affect. However, as we add more optimisations, that's propably the paradigm we would go for. I think there is nothing which says that a verified tool shouldn't support these and not be flexible, often you can have a proof for an arbitrary translation (using translation validation) so you can have many algorithms that can be tweaked (or changed using parameters) without having to change the proof.

[KFAFSP]

I was wondering how this formal verification can deal with systems that include asynchronicity. Specifically, I am thinking of the more involved CGRA designs that include internally-clocked FUs that are connected using handshaking. This can also become a more difficult problem once you move data towards memory, if that is not exclusively assigned to certain FUs.

[ymherklotz]

Thanks for the question, yes handshaking is something that would also be interested to look into. Currently, these could actually already be expressed using specifications for the proof, we are doing something similar for a pipelined divider. Even though we know that the divider will always take 32 clock cycles, we actually added handshaking signals to it, which makes the specification much smaller, as you only really need to take action when those signals change. However, the main problem there is to prove that your specification is correct, which will be impossible for large circuits.

It would also be interesting to look into how to formalise dynamic scheduling, which exclusively uses handshaking.

[threonorm]

Hi Yann, John, I was wondering: is the semantics of vericert deterministic or non-deterministic? In a sense, are there cases where the compiler's syntehsis engine resolves non-determinism: so the source was having non-determinsitic semantics and the compiler is proven to fix the non-determinism in a correct way

[ymherklotz]

So the final Verilog semantics is actually proven to be deterministic, but I actually think that the input semantics of the Clight input language is also deterministic, so CompCert already defines a specific order of execution for the input C code.

For example, for the Verilog side, the way we ensure deterministic execution is by executing each always-block sequentially, which is equivalent to a non-deterministic execution, assuming only nonblocking assignment is used to communicate to other blocks.