Verifying Hardware at the C-level

As more people adopt high-level synthesis (HLS) they start to worry about what is the best design flow to be using. This is especially so for verification since it forms such a large part of the effort on a modern SoC. The more people rely on HLS for producing their RTL from C, the more they realize they had better do a good job of verifying the C code in the first place. Waiting until RTL is inefficient, not to mention late in the flow. Issues are hard to locate and debug and you can’t change the RTL even when you do (at least you are asking for big problems if you do). Instead you need to return to the “golden” representation which is the C, find the corresponding part of the code and then fix it there.

Better by far is to do verification at the C level. If the C is correct, then HLS should produce RTL that is correct-by-construction. Of course “trust but verify” is a good maxim for IC design otherwise we wouldn’t need DRCs after place and route. Similarly, you shouldn’t assume that just because your C is good that the RTL doesn’t need any verification at all.

Unfortunately, tools for C and SystemC verification are rudimentary compared with the tools we have for RTL (software engineering methodology has changed a lot less than IC design methodology over the last couple of decades, but that is a story for another day). RTL engineers have code coverage, functional coverage, assertion-based verification, directed random and specialized verification languages. C…not so much.

But we can borrow many of these concepts and replicate them in the C and SystemC world. By inserting assertions and properties into your C models you can start to do functional coverage on the source code and formal property checking on the C-level design. An HLS tool like Catapult can actually make sense of these assertions and propagate them through into the RTL.

Catapult, along with SLEC, allows you to do this sort of analysis now. With SLEC you can check for defects in the C/SystemC source, do property checking on assertions in your C-level code and apply formal techniques to prove whether an assertion always holds true or not. Catapult will then embed all these assertions into the RTL, automatically instantiating them as Verilog assertions that do the at the RTL level as the originals did at the C-level. It also takes C cover points and synthesizes them into Verilog so that when you run Verilog you also get functional coverage.

This hybrid approach leverages all the methodology that the RTL experts have put together, but pulling it up to do more at the C-level. After all, the better the C, the better the RTL (and the gates…and the layout).

Calypto have a couple of upcoming webinars, one for India/Europe on another topic and one for US on verification.

Dynamic/leakage power reduction in memories. Timed for Europe and India at 10am UK time, 11am central Europe, 12pm Finland and 2.30pm India. September 12th (this coming Thursday). Register here.

How to Maximize the Verification Benefit of High Level Synthesis with SystemC. 10am Pacific on October 22nd. Register here.