Feature: Embedded
Figure 3: Deadlock checks in SystemC/C++ code
manipulate the same state, or value, in the same time lapse) and mismatches between sequential simulation semantics and parallel operation in hardware. Many of the issues caught by DV-Inspect are not checked by
simulation or HLS. Tese include unintended behaviour due to issues with specific data types, such as for fixed-point arithmetic, as well as concurrency-related issues such as race condition evaluation. Formal analysis provides a valuable pre-synthesis signoff to save overall development time and resources.
Sequential assertion-based SystemC/C++ verification A full assertion-based verification solution for SystemC and other SystemC/C++ designs can be applied. Accepting the majority of SystemC functions, the formal solution allows assertions to be tested against a range of code abstractions, from transaction level models (TLMs) through detailed RTL and right down to netlists, and from almost untimed to full cycle accurate representations. Both simple ANSI C assertions and fully temporal concurrent
SystemVerilog assertions (SVA) may be used with the SystemC/ C++ designs. Tis assertion description flexibility allows existing assertions for other designs to be reused or leveraged as templates, and reduces the learning overhead associated with a new format. Tis also enables 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 synthesised 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. Tis unique formal capability allows sequential assertions, which can be used to describe specification elements, expected design characteristics and fault conditions to be tested against abstract code. Tis 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-synthesised RTL code.
Formal techniques Formal techniques are well established as a key part of functional verification for hardware designs. Many designers have moved to SystemC/C++ to raise the abstraction level and take advantage of high-level synthesis. Tis approach speeds up the hardware design process but, for a corresponding reduction in verification time, the focus must be on the SystemC/C++ source code and not the post-HLS RTL design. Te OneSpin DV solution for SystemC/C++ satisfies this need, providing both automated design inspection and full assertion-based verification for high-level designs. HLS users can take full advantage of the most advanced formal verification methods.
Figure 4: Wide range of checks for SystemC/C++ code
26 June 2021
www.electronicsworld.co.uk
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
