Feature: Embedded


Many designers have moved to SystemC/C++ to raise the abstraction level and take advantage of high-level synthesis


is a requirement. Functional specifications may be represented easily with assertions and, as such, the use of formal techniques is a natural choice since they allow assertions to be rigorously tested against the design. New control-intensive algorithms, now being coded in SystemC, are particularly hard to verify using just simulation.


Going formal Tere is a broad range of formal techniques that can be applied to design components coded in C++ or SystemC, with varying levels of timing and code abstraction. Such solutions provide a range of automated structural, safety and activation checks to be applied to designs without having to manually create assertions – particularly useful for sign-off of the design code prior to high-level synthesis. Fully-functional assertion-based formal verification tools allow


for comprehensive assertions to be tested against SystemC/C++ design code. Tese assertions may be written using the simple C assert statements, or full SystemVerilog Assertions (SVA) with all the temporal concurrent constructs included. Te ability to leverage temporal assertions on SystemC/C++ designs is a unique capability of this technology. Multiple proof engines can leverage a range of standard and


proprietary algorithms to provide in-depth code analysis, which consistently exhibits a high degree of convergence compared to other solutions, coupled with rapid, high-capacity operation. Te platform can process a range of languages and includes capabilities for easy set-up and usage. A powerful debug environment provides a clear path to quickly track down design problems or tests. Formal techniques’ flexibility allows them to be applied to a


range of problems, and these apply equally well to SystemC/C++ designs. Tools may be used in a highly-interactive mode to quickly look at how a design is operating in a “what-if” style. Tey may form the cornerstone of a full metric-driven verification solution, and an effective validation mechanism for IP integration on SoC platforms.


Automated formal SystemC/C++ design evaluation Te full automated functionality of formal verification may also be leveraged on SystemC/C++ hardware design code. Eliminating bugs as early as possible in the design process can save many engineering hours downstream, and this is even more valuable when the design process starts at the microarchitecture abstraction level.


Figure 2: Use of SVA with a SystemC/C++ design A range of automated checks that use the full power of the


formal engines can be implemented to provide in-depth static analysis of the design code, but without having to manually write assertions. Going beyond traditional linting tools (automated checking of your source code for programmatic and stylistic errors), this design inspection technology looks for potential bugs by analysing operational scenarios based on the code construction. Safety checks such as out-of-bounds access on an array or dead


code (unreachable) or deadlock activation checks and structural analysis, including classic mismatches between simulation and synthesis operation, are all available. In addition, there are checks particularly applicable to SystemC code. For example, it is important to check which registers have been explicitly initialised: SystemC variables are automatically initialised in simulation, but HLS tools ignore these initialisations, leading to simulation- synthesis mismatches that are hard to debug. Formal techniques also check to see whether uninitialised registers, undefined operations, or multiple drivers can propagate X (unknown) values in the design. Tere 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 (the only concurrent problem that can happen when two threads


www.electronicsworld.co.uk June 2021 25


Page 1  |  Page 2  |  Page 3  |  Page 4  |  Page 5  |  Page 6  |  Page 7  |  Page 8  |  Page 9  |  Page 10  |  Page 11  |  Page 12  |  Page 13  |  Page 14  |  Page 15  |  Page 16  |  Page 17  |  Page 18  |  Page 19  |  Page 20  |  Page 21  |  Page 22  |  Page 23  |  Page 24  |  Page 25  |  Page 26  |  Page 27  |  Page 28  |  Page 29  |  Page 30  |  Page 31  |  Page 32  |  Page 33  |  Page 34  |  Page 35  |  Page 36  |  Page 37  |  Page 38  |  Page 39  |  Page 40  |  Page 41  |  Page 42  |  Page 43  |  Page 44  |  Page 45  |  Page 46