Formal Verification of HLS and Design Verification

[chsasank]

I came across this paper from OOPSLA 21 about formal verification of HLS compiler. They presented how their compiler is "mechanically verified to preserve the behaviour of its input software.". I'm new to this stuff so please excuse me if my question is a bit dumb: Does this mean you don't need to verify the design built with this HLS compiler?

[rachitnigam]

Formal verification allows you to mathematically prove some property about a program. In this case, the authors of the paper proved that the program (the HLS compiler) preserves the behavior of the C program when compiled to Verilog.

There are two tricky things about this:

1. You have define some mathematical model of your languages and somehow relate it to reality. The authors used a formal model of a subset of Verilog. Someone has to make sure that this model corresponds to reality.
2. The HLS compiler, overall, does not do any of the complex optimizations needed to generate real, performant hardware designs AFAIK. For example, the paper does not support any form of pipelining which is the key optimization in HLS compiler and uses unsynthesizable/slow models of things like divider.

The second point is largely consistent across these kinds of verification projects: it is hard to verify state of the art optimizations which means most verified compilers don't actually support them. I think this problem is worse in hardware compilers than software: you can stomach slow but correct software but why would you even bother building hardware if it was slow; just use CPU/GPU code at that point.