Linking high-level synthesis with formal verification
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.
Figure 1 A typical C++/SystemC HLS flow
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.
Due to this issue, much of the verification performed on SystemC designs is executed at the HDL level on the synthesized code, allowing a more traditional design refinement flow and verification process. However, the level of indirection introduced with this flow renders it complex in the extreme.
As engineers raise the abstraction level of their designs, it becomes more natural to raise the level of the verification experience. Pre-HLS algorithmic blocks tend to reflect the original specification more closely, with none of the circuit-level detail. As such, it is more natural to use the specification to produce abstract verification tests, with less concern for coding detail. Functional specifications at this level may be represented more naturally using assertions and, as such, the use of formal techniques becomes a natural choice for the exhaustive processing of those assertions.
Multiple opportunities exist for formal verification to address these requirements, as shown in Figure 2. A broad range of formal verification techniques may be applied to design components coded in C, C++ or SystemC with varying levels of timing and code abstraction. This allows bugs to be eliminated earlier in the design process to save engineering hours downstream, especially when the design process starts at the microarchitecture abstraction level.
Figure 2 The use of formal verification within an HLS design flow
Formal techniques can be helpful at higher levels of abstraction in a variety of ways. Automated formal apps may have some specific uses at the SystemC level –– testing for bit accuracy and overflow in a fixed point, arithmetic implementation, for example. Full property checking allows for specification elements to be transcribed into assertions and played against the algorithmic block. If the same assertions can be applied at the RTL level with the appropriate allowance made for timing insertion, then a certain level of equivalency checking is possible between pre- and post-synthesized code.
Let’s examine some of these possibilities.
A description of the use of formal verification around HLS would not be complete without a mention of Equivalence Checking (EC). EC would be a useful function to be applied at this level in a similar manner to its application in RTL-to-gate comparison testing. However, any EC tool to operate at this level must be able to cope with the sequential nature of the HLS tool optimizations as they insert timing registers and more into the code. It must be able to cope with high-level transformations leveraged into such components as multipliers and other complex RTL blocks. This is possible with some modern EC tools, although it is way beyond the possibilities of a standard RTL EC process. Solutions may emerge in the future.
A fair amount of the functionality contained in the formal verification tool today most often used for RTL verification can be leveraged on C-Based hardware design code. It provides a range of automated checks, using the formal engines to provide in-depth static analysis of design code without the need to manually write assertions. This design inspection technology goes further than linting tools and looks for potential bugs by analyzing operational scenarios based on the code construction. Safety checks, such as out-of-bounds access on an array or state-machine deadlock, activation checks and raw structural analysis, including classic mismatches between simulation and synthesis operation, are available.
Numeric application
In working with a number of users, we have discovered an application for formal technology at this level –– the analysis of the width of fixed-point number systems. In many algorithmic SystemC code blocks, a fixed number definition is used that sets a number of bits for the integer and fractional parts of a number. This bit width is varied throughout the design datapath to match the various arithmetic functions and the accuracy required of the algorithms being processed. If the number of bits at any one point in the design is too small, overflow might occur. If it is too large, circuit elements and, therefore, power consumption will be wasted.
To get this right using simulation, a complex and large stimulus set would have to be generated that tests the various arithmetic functions together, and it would be easy to get this wrong. An exhaustive simulation with all possible numbers is often impractical.
This is an ideal application for a formal solution, which can look at the entire design and accurately predict in which direction the bit usage will fall, without any requirement for stimulus and lengthy test runs. An assertion may be automatically generated by an arithmetic app based on the design, which is set to check specifically for an overflow condition, i.e. a hypothetical overflow bit being set by the arithmetic operation driving that register.
The formal tool can then analyze every possible state on the inputs to the arithmetic function and check that this bit will never be set. Similarly, an assertion that checks the Most Significant Bit (MSB) of a register for usage will indicate wasted bits if the MSB never becomes a 1. This technique can be applied on a combination of arithmetic functions and registers to evaluate an entire algorithmic implementation, ensuring optimal bit usage. This is now a typical app provided by OneSpin.
Assertion language choices
HLS verification can involve a choice of assertion languages. Both simple ANSI C Boolean assertions, even within a timed state machine, and full temporal SystemVerilog Assertions (SVA) can be used with C-Based designs. The use of SVA with SystemC might seem an odd choice but actually it makes a lot of sense when looking at the design flow.
This assertion description flexibility allows existing assertions for other designs to be reused or leveraged as templates, reducing the learning overhead associated with a new format. It also enables a consistent pre- and post-synthesis flow where the same assertions, if written with the flow in mind, can be reused on C-Based golden models and their Verilog or VHDL synthesized derivatives. In addition, Verification Intellectual Property (VIP) assertion sets created for Verilog environments ––a bus protocol verifier, as an example ––can be reused on C-based code.
By allowing full property checking at this level, and being able to use full temporal SystemVerilog assertions, users get closer to the initial specification and create functional specification elements that might be played against the design code, timed or untimed. This allows for a greater degree of functional testing, which on some of these algorithmic blocks, is effective for solving complex issues prior to timing insertion.
SystemC is alive and healthy in this HLS based application, and this will drive more effective verification methods. It could be argued that formal verification comes into its own at this level, with the abstraction of code blocks improving capacity characteristics, and the functional specification nature of assertions proving a greater fit with higher level code. Watch for more formal usage at this level in the future.
About the author
Dave Kelf heads OneSpin’s marketing efforts and services as vice president of marketing. Previously, he was president and CEO of Sigmatix, Inc. He worked in sales and marketing at Cadence Design Systems, and was responsible for the Verilog and VHDL verification product line. As vice president of marketing at Co-Design Automation and then Synopsys, Kelf oversaw the successful introduction and growth of the SystemVerilog language, before running marketing for Novas Software, which became Springsoft (now Synopsys). He holds a Master of Science degree in Microelectronics and an MBA from Boston University.
OneSpin
San Jose, CA and Munich, Germany
