Formal verification for SystemC/C++ designs

As the use of SystemC/C++ has expanded, a number of use-cases have emerged in recent years. These include the use of SystemC/C++ to build abstract algorithmic design code that can be used as an input for high-level synthesis (HLS) tools, for virtual platform models for early software test, to develop configurable intellectual property (IP) blocks, and many others.

HLS, which transforms “mostly untimed” abstract SystemC/C++ design representations to fully timed register-transfer-level (RTL) design blocks, is in use at many large semiconductor and electronics-systems companies. HLS tools are particularly popular as a method to rapidly generate design components with varying microarchitectures while supporting the optimization of algorithm-processing datapaths rapidly and effectively. Their use on control logic, as well as components with more detailed timing in general, is also becoming more widespread.

The verification of SystemC/C++ designs is largely performed by compiling the design representation. This is often performed by a standard software compiler, such as the GNU Compiler Collection (GCC). The resulting code is generally debugged in a similar fashion to software designs. The Open SystemC International (OSCI) SystemC C++ class library, now standardized as IEEE 1666-2011, introduced capability that provides a more RTL-simulation-like user experience, but there are still many issues that make the verification of SystemC code a complex, arduous task, including debug, runtime performance, and test complexity. The availability of formal techniques at this level has been sparse.

A common SystemC/C++ HLS flow makes use of algorithmic descriptions often using only C or C++ code. These descriptions are tested to ensure that the algorithm itself operates correctly. The SystemC class library functions are applied to provide minimal hardware detail, such as basic timing, reset functionality, and so on, as required by the HLS tools. The synthesis tool produces RTL code, which is then applied to a more traditional design refinement flow and verification process.

The verification of the design is split between the SystemC and RTL levels. Engineers would prefer to verify and debug the original SystemC designs and only check for functional equivalence post-synthesis, similar to traditional RTL development processes. However, the lack of effective SystemC/C++ design verification environments has driven engineers to more traditional HDL verification.

As engineers raise the abstraction level of their design approaches, it becomes more natural to also raise the level of the verification. At the pre-HLS algorithmic level, verifying the design directly against its specification with less concern for coding detail is a requirement. Functional specifications may be represented easily with assertions and, as such, the use of formal techniques, which allow assertions to be rigorously tested against the design, is a natural choice. New, control-intensive algorithms, now being coded in SystemC, are particularly hard to verify using just simulation.

We have developed an assertion-based formal methodology that allows for a broad range of formal techniques to be applied to design components coded in C++ or SystemC with varying levels of timing and code abstraction.

We propose utilizing in a push-button manner, a range of automated structural, safety, and activation checks that can be applied to designs without the manual creation of assertions. This is particularly useful for sign-off of the design code prior to high-level synthesis. We also propose applying formal techniques on SystemC/C++ design code to eliminate bugs earlier in the design process. Many issues may escape simulation or high-level synthesis. These issues include unintended behavior due to issues with specific data types, such as for fixed-point arithmetic, as well as concurrency-related issues such as race condition evaluation. Utilizing a formal approach for pre-synthesis sign-off can save a great deal of time and resources. An intuitive GUI debugger can help user to find a root cause of the issue as soon as possible.

Formal methodology

The fully automated functionality of the formal methodology for verifying SystemC/C++ designs was used on a design from MaxLinear. Fully functional assertion-based formal verification allowed comprehensive assertions to be tested against SystemC/C++ design code. The assertions were writing using the simple C assert statements, for full SystemVerilog Assertions (SVA) with all the temporal, concurrent constructs included. A unique capability of the technology used is the ability to leverage temporal assertions on SystemC/C++ designs.

Multiple proof engines that leverage a range of standard and proprietary algorithms were used to provide in-depth code analysis. This method, coupled with rapid and high-capacity operation, consistently exhibits a high degree of convergence compared to other solutions. Utilizing a proper debug environment provided a clear path to quickly track down issues with the design and tests.

The automated technology was used on SystemC/C++ hardware design code to eliminate bugs early in the design process. A full range of automated checks were utilized to provide in-depth static analysis of design code. This technique helped to eliminate the need to manually write assertions. The design-inspection technology looked 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 structural analysis including classic mismatches between simulation and synthesis operation were readily available.

It was important to check which registers were explicitly initialized. SystemC variables are automatically initialized in simulation but HLS tools typically ignore these initializations. This leads to simulation-synthesis mismatches that are hard to debug. Verification teams also checked to see whether uninitialized registers, undefined operations, or multiple drivers can propagate X (unknown) values in the design. There is no notion of unknown values in SystemC simulation, so formal analysis is needed to find propagation issues. SystemC also lacks non-blocking assignments, leading to race conditions and mismatches between sequential simulation semantics and parallel operation in hardware.

Many of the issues caught using this methodology are not checked by simulation of high-level code. These include unintended behavior due to issues with specific data types, such as for fixed-point arithmetic, as well as concurrency-related issues such as race condition evaluation.

Accepting the majority of SystemC functions, the technique allows assertions to be tested against a range of code abstractions, from transactionl-level models (TLMs) through detailed RTL and down to the netlist, and from untimed to full, cycle-accurate representations.

Both simple ANSI C assertions and those written using fully temporal, concurrent SVA may be used with the SystemC/C++ designs. This assertion-description flexibility allows existing assertions for other design to be reused or leveraged as templates and reduces 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, may be reused on SystemC/C++ golden models and their RTL-synthesized derivatives. In addition, verification intellectual property (VIP) assertion sets created for RTL environments, for example a bus protocol verifier, may be reused on SystemC/C++ code.

The methodology allows sequential assertions, which can be used to describe specification elements, expected design characteristics, and fault conditions to be tested against abstract code. This allows engineers to work at the SystemC/C++ level on their golden designs to ensure that they meet their specifications prior to synthesis. It enables a comprehensive formal solution at a level where specifications may be played against different microarchitecture options. Finally, it eliminates the indirection of debugging a SystemC/C++ design using the post-synthesized RTL code.

Methodology in practice

As noted earlier, the above methodology was put to the test with MaxLinear on a new design. The technology and methodology were used on the top-level design and not on specific modules. Implementation on the top-level was performed in order to speed-up the entire verification process and to run verification of the corresponding level of the design that will be used later in the HLS process. Another possible application is described below using sub-modules and hierarchies below, but this method requires potential input constraints to replicate the subset of the values that other sub-modules are driving.

The Quick, Lunch, Night and Weekend runs (QLNW) flow was used for performing checks. QLNW is an intuitive and easy to use procedure used to perform verification checking in the corresponding time frame (Q=15m, L=1hr, N=12hr, W=48hr). It is implemented for maximum efficiency to obtain as many as possible converged checks within the runtime available.

GUI-mode base tests were performed to filter out non-important checks and run the required checks. Additionally, some groups of the checks are filtered-out that were originally from files that were already verified.

The failed checks that were reported were then debugged using the GUI debugger. The debugger is intuitive and can display active code in the selected timeframe with the waveforms of the related signals. With the active code, the user could follow values with the driver tracing feature to find the root cause of the issues in the design code. The checks were then rerun to ensure there were no additional failed checks.

Results and future plans

Several out-of-bounds and truncated-operation issues were found using the prescribed methodology during the Quick and Lunch runs and were found to correspond to the real design bugs. The out-of-bounds failure checks were hard to spot using other techniques. The team at MaxLinear used the automated OneSpin SystemC Inspect solution to analyze the issues. If these issues were not identified on the SystemC code, it would have been difficult to find the issues with standard simulation-based techniques as simulation cannot guarantee 100% coverage and driver stimulus, whereas formal techniques can.

MaxLinear is planning to utilize these formal techniques in the pre-design phase of a future project. The team expects that doing so will dramatically cut verification and debug time and lead to more functionally correct and secure designs.

The next steps are to integrate OneSpin SystemC verification technology into other projects and to perform additional analysis and checks with the new capabilities that are available with the latest OneSpin version starting from 2021.2. The new features include process overwrite (signal written in several times in one clock period in one process consequently) and read before write (signal being read before being written).

Vlada Kalinic is a product specialist working at OneSpin, a Siemens business, and presented a tutorial based on this material at the 2021 SystemC Evolution Day workshop, colocated with the DVCon Europe conference.