Linking high-level synthesis with formal verification

Tech Design Forum article: David Kelf, OneSpin Solutions

High-level synthesis provides a way to explore hardware architectures to come up with the most efficient implementation for a given situation. But it has taken time for verification techniques to catch up with the idea and ensure design and architecture match.

 

The growth in the use of C++ and SystemC for describing electronic hardware components, particularly at the algorithmic level, has been one of the best-kept secrets in EDA. Although multiple SystemC applications are envisaged –– for example, abstract hardware, virtual platforms and configurable intellectual property (IP) –– the use of SystemC for modeling algorithms and then using them as the input to High Level Synthesis (HLS) tools is becoming much more common.

 

HLS transforms “mostly untimed”, abstract C-based design representations to fully timed register transfer level (RTL) design blocks, and is in use at many large semiconductor and electronic systems companies. These tools are popular as a method to rapidly generate design components that have different microarchitectures to evaluate their relative throughput, power and area performance, allowing the optimization of algorithm processing datapaths efficiently and effectively. Their use in signal processing applications in the image processing and communications sectors is becoming widespread.

 

The verification of designs expressed using SystemC has been one of the factors that has limited its growth to date. The Open SystemC International (OSCI) SystemC C++ open source class library, now controlled by the Accellera Systems Initiative, introduces functions similar to HDL-like for use in C++ design descriptions. The verification of these descriptions has largely been focused on compiling the design and class library using a compiler such as GCC and then executing the block similarly to any other software program.

 

Promise versus reality

The initial appeal of this approach, which does not require a separate simulator and allowed the use of open-source software, rapidly gave way to reality. Bringing up such a design with only compiler-level error messages to go on, debugging code blocks with limited capabilities, and putting up with performance and other issues made the solution impractical for large design components. Some simulation providers allowed for SystemC code to be executed within their environments, but this lacked many of the advantages of HDL simulation. The availability of formal techniques at this level has been almost non-existent.