Announcing Jasper C2RTL App: Formal for Algorithmic Designs

Today is the first day of the Jasper User Group (unofficially known as JUG to attendees). All being well, Ziyad should be on stage (well, on the video stream) opening the meeting and he will introduce the Jasper C2RTL App.

You can read my preview of the meeting in my post a couple of weeks ago, Jasper User Group Preview. I obviously wasn't inspired to come up with a catchy title that day!

Jasper C2RTL App

You can probably make an educated guess at what the C2RTL App does. It formally verifies that very general C and C++ designs match the RTL implementation. A lot of algorithmic silicon blocks are first worked on by the architect(s) at the C level since it is fast and can be used to validate design features such as performance before undertaking more detailed design. Typically algorithmic designs are trading off latency, throughput, and other aspects such as estimated power. The new C2RTL App is targeted at hand-crafted datapath designs with all the complexity that they can involve.

The C2RTL App supports the latest ANSI C++ standards and common math libraries. The innovative compilation technology was co-developed with Oxford University in the UK. This development has created a new class of formal engines optimized for checking RTL datapath implementations versus their C/C++ algorithmic specifications, with up to 100X performance improvement compared to existing general-purpose formal engines.

As you can see from the above diagram, at the high level the app does what you would expect, reads in the algorithmic spec in C or C++, reads in the RTL implementation in SystemVerilog, and some mapping information. It then proves that the two are equivalent, or, if not, details where there are issues. It has a rich feature set including handling pipelines, pipeline stalls, feedback loops, bit twiddling, floating-point, SystemC datatypes, and more. Technically, the C++ front-end supports ANSI C++ 98, 03, 11, 14, and 17. Everything is integrated with the Jasper Formal Verification Platform so that you can switch apps with the same look and feel.

And also the same debugger. The Jasper Visualize debug has been extended to C/C++ so that it is straightforward to directly compare RTL datapath implementation with the C/C++ specification to speed debug and to dive deep into any issues brought to light.

• RTL-like waveform debug for C++ code
  • “Why” tracing in C++
  • Driver/load tracing
  • Value annotation in source
• Specialized source debug for C/C++
• Powerful Visualize features integrated
  • What-if analysis
  • Quiet trace
  • Freeze

Summary

Learn More

See the Jasper C2RTL product page.

Sign up for Sunday Brunch, the weekly Breakfast Bytes email.