Easy bug detection and functional verification of SystemC/C++ code prior to High-Level Synthesis
High-Level Synthesis (HLS) (aka behavioral synthesis) transforms algorithmic and potentially untimed design models often written in SystemC and C++ to fully timed Register Transfer Level (RTL) design blocks. HLS tools are particularly popular as a method to rapidly generate design components with varying microarchitectures, while optimizing algorithm processing datapaths rapidly and effectively. This provides substantial benefits in terms of flexibility and time-to-market. Consequently, HLS is now in use at many large semiconductor and electronic systems companies. However, the verification options for SystemC and C++ designs have not kept pace with the synthesis technology.
OneSpin’s SystemC/C++ Design Verification solution provides a formal verification environment allowing for easy bug detection and functional verification of SystemC/C++ code prior to high-level synthesis.
The need for a new HLS Verification Methodology
Simulation-style verification of HLS code is largely performed by compiling and debugging the design representation, linked with the Accellera OSCI SystemC Class Library, in a similar fashion to software test. Due to the limited availability of SystemC tools, much of the verification task is performed on the resulting synthesized RTL code, introducing a level of indirection that makes correcting issues at the SystemC/C++ level complex and time consuming.
The primary verification requirement is to allow thorough verification of algorithmic code prior to synthesis, in order to ensure that the abstract algorithm implementation is tested and fully optimized against the original specification, as well as avoiding long debug cycles.
In addition, artifacts of the SystemC standard, for example the lack of an unknown, or X, state, potential race conditions between threads, etc., result in further ambiguity that must be eliminated before synthesis. Specific issues related to this abstract design level may be easily tackled with the right verification methods, improving final design quality.
SystemC/C++ Formal Verification
OneSpin’s unique SystemC/C++ Design Verification solution enables a broad range of formal verification techniques to be applied to SystemC and C++ components with varying levels of timing and code abstraction.
Hardware issues, such as the detection of uninitialized value propagation, or the effects of undefined operations (e.g. array out-of-bounds) may be effectively detected using OneSpin’s automated apps at the SystemC/C++ level. A SystemC-specific automated arithmetic overflow check has been added to 360 DV-Verify, which allows for the inspection of number precision across algorithmic datapaths.
Full assertion-based formal verification is also provided that allows comprehensive, temporal SystemVerilog assertions or C-asserts to be tested against SystemC/C++ design code. This provides a rich verification capability that makes use of a common assertion mechanism that can also be applied to post synthesized HDL code.
360 DV-Verify Product Page
Quote: “In an era where developers consistently use one or more of C/C++, Perl, Tcl, Python, Verilog, and VHDL on a daily basis, it is hard to catch such trivial mistakes, more difficult still to catch functional mistakes, and extremely difficult and time consuming to uncover either after synthesis.” Xilinx/UG1197.
Quote: “Good verification practice requires that the input to High-level Synthesis (HLS) be verified first, via simulation (or some other analytical means), and then the output of HLS be verified, again via simulation or some other means.” John Sanguinetti, CTO of Forte Design Systems Inc.