Formal and High-Level Synthesis

Formal verification has made significant inroads in RTL and gate-level verification because it provides complementary strengths to conventional dynamic verification methods; using both provides higher levels of coverage and confidence in the correctness of an implementation. I haven’t heard as much about formal use in high-level synthesis (HLS) flows so was interested to see a white paper from Renesas on how they use Catapult formal tools in this context.

First, why even use formal in such a flow? One reason is obvious. When you synthesize from one format to another, from C++ to RTL or from RTL to gates, no amount of simulation is going to prove conclusively that synthesis didn’t introduce some subtle error along the way. That’s why equivalence checking was invented, to prove that at minimum the input and output implementations are functionally equivalent at a cycle-level.

Another reason is to do some level of formal checking on the C++ itself. A couple of examples are out-of-range-accesses on arrays and uninitialized memory reads. You might catch these in C++ simulation, but you might not. Experienced programmers know that behind rarely taken branches can lurk dragons; formal is a good way to expose such problems. And the beauty of these methods is that they not only discover that a problem is possible, but they also show you how to create that problem, which should make it easier to figure out a fix.

Still, the bulk of Renesas’ usage is in equivalence checking and this starts with C++ to C++ checks. Renesas talks about image processing IP and communication IP, both natural applications for HLS. Both types of design are intrinsically complex and will evolve through multiple iterations. Equivalence checking between C++ revs can assure as completely as possible that unintended functional changes are not introduced.

This is sequential equivalence checking and will not always get to a proof of equivalence (or no-equivalence) without a little assistance. What will push a proof towards convergence in these cases is more hints (constraints) on behavior, such as bounding the range of an apparently unbound array index.

The best-known application of equivalence checking in HLS flows is in comparing the source C++ with the synthesized RTL. There’s an advantage here (I’m guessing) in having the HLS synthesizer and the SLEC equivalence checker come from the same product group. The checker knows what kinds of transformations the synthesizer can make, such as how it inserts pipeline stages, and can factor these in when looking for a complete proof.

I believe based on my reading of the Renesas white paper that they only edit the source C++, so all RTL changes are based on re-synthesis from source updates. They run equivalence checking on each RTL drop to establish either that they can get to a full proof or to find any bottlenecks to getting to proofs. This is with the goal of ensuring a full proof by the time they get to the final RTL drop.

Methods to help along full-proofs at this level are pretty familiar – help in identifying equivalence points between the two designs, along with some level of abstraction and hierarchical proving.

Renesas results are impressive in comparison with verification through extensive simulation. They show one example, for an image processor IP, in which they were able to reduce turnaround time from 260 days (simulation-based) to 4 days using equivalence checking. Of course you still want to do lots and lots of simulation (in C+) to prove functionality and performance. Catapult SLEC removes the need to worry about implementation bugs being introduced in mapping from C++ to RTL.

You can read the Renesas white paper HERE.