The Secret To Good Comedy And SystemC Code Verification… Timing!

The High-Level Synthesis (HLS) of algorithmic code, usually written in SystemC, is steadily gaining ground. However, the verification of this code is still a somewhat mixed-up, ad-hoc process. The situation is improving as new techniques are applied, but it is clear that in-the-trenches evaluation of these solutions on real projects is more important right now than grand visions missing substance!

SystemC is built upon C++, with the idea of adding Hardware Description Language (HDL)-like features into the software base. Much like teaching an old dog new tricks, there are some difficulties, given the C++ software origins. C++ has no concept of an “X” or unknown state, leading to initialization bugs that are hard to track. It offers no convenient <= non-blocking assignments to avoid painful race conditions.  Many common software programming language constructs can be hard to relate to hardware –– such as pointers to an array –– causing unexpected behavior.

An emerging method to track down these issues is to use an automated Formal App specifically tuned to handle SystemC designs, and tied into the HLS tools and their associated functional libraries. OneSpin announced such a tool a year ago and has been working with a few customers and partners ever since. The focus is to nail down the key issues that otherwise cause the painful experience of debugging post-synthesis register transfer level (RTL) code and then translating the results back up to the original abstract SystemC files.

Formal verification is good at targeting these types of code issues given the nature in which it inspects the entire state-space of a design over a number of clock cycles. Furthermore, new capabilities specific to algorithmic HLS code, such as number precision analysis, have proven useful. A number of these issues have surfaced as companies work cooperatively with partners in this area. It is clear that a powerful formal tool that can handle full, temporal (i.e. with timing) SystemVerilog Assertions, even if they are somewhat hidden in an automated app, is essential to solve these problems.

But this is tough technology. It’s hard enough to produce a viable formal tool that can reliably execute temporal assertions on RTL code. Imagine translating this into the less rigorous SystemC domain. The benefits are huge, however, as long as the formal tool can fully exploit apps driven by temporal assertions such as SystemVerilog.

What is this timing issue? Some HLS users might point out that, at least for one class of algorithmic designs, one of the major functions of the synthesis process is to insert appropriate registers into the largely untimed design, and that the original design has limited timed functionality. This is becoming less common. We are seeing more control logic and data transport systems coded in SystemC, and the marrying of control with mathematical algorithms pre-synthesis.

Indeed ensuring that the math is correct in these designs requires multistage pipeline verification, and the fact that a verification tool can accomplish this allows for more of the components around the central pipeline to be coded in SystemC. This enables a holistic approach to the design of these components. The advancement in tools leads to more design work at the SystemC level, in turn driving tool capability in a virtuous circle.

Untimed C Asserts were designed for software verification. For hardware, timed, temporal assertions are key and SystemVerilog is the answer. Beware the static verification tools that promise quick fixes to one or two SystemC problems. If their timing is off, then so is their verification!