Operational checks for standard coding problems
A broad range of bugs may be introduced into design blocks either by coding accidents or a misunderstanding of expected Verilog or VHDL semantic operation. Some coding problems can be identified through the use of linting and structural analysis, however, many issues can only be exposed by analyzing the sequential operation of a design. This can be achieved by simulation; however, it requires the creation of tests and is therefore applied late in the process, almost certainly leading to a large expenditure of debug resources to repair.
OneSpin’s Safety Checks App automatically detects a wide range of coding issues, without the need to provide test vectors, exhaustively examining every possible scenario.
Why formal is more productive
Using formal technology, it is possible to check that code safely executes in a more exhaustive manner than other techniques, as this approach will examine all code operational scenarios. This is a more extensive check than that possible by linting tools, as those simply examines code syntax for possible errors, but it still does not require the significant overhead of simulation stimulus creation or execution. Furthermore, the formal approach is more likely to detect actual errors rather than warnings, avoiding the linting problem of log file “noise.” Unlike simulation, it will complete an exhaustive check of the code without the requirement for the stimulus to examine every possible scenario.
The OneSpin Safety Checks App is designed to provide these checks in a fully automated, push button fashion, allowing designers to quickly verify their code early in the development process, in a low overhead, “agile” fashion. It provides the most comprehensive, automated and effective way to exhaustively prove the correct behavior of RTL code verified for a broad range of common problems.
How it works
The VHDL and Verilog / SystemVerilog standards allow for a range of coding issues that can lead to bugs. The app automatically synthesizes safety checks based on the source code and common potential error schemes. The generated checks exhaustively track down coding problems based, not just on syntax, but sequential code operation as they are exhaustively and sequentially checked using the OneSpin formal platform. In case the checks pass, no such problem can occur in the design.
In case of a failing check, the app reports a violation, and generates a short simulation trace for debugging that reveal the source of the problem. The generated trace starts with an active reset and leads to the violation, demonstrating the presence of an RTL issue. Failing checks can intuitively be analyzed in the OneSpin’s integrated debugging environment. Color coding, active code annotation, active driver and load tracing, and dynamic synchronization between source code and waveform viewers, enable users to quickly identify the root cause of the issue and fix the RTL.
Example for Undefined Design Behavior
For example, consider an array with n elements, accessed through an index that can potentially have values beyond the [0, n - 1] range, e.g. a 6-element array indexed by a 3-bit signal. In the case of VHDL the standard prescribes that a simulator must generate a Fatal Design Error (FDE) and stop running if during a simulation the array is indexed out of its bounds. Of course, this requires stimulus to be executed to allow its discovery during RTL simulation. In the case of Verilog, the standard prescribes the generation of X states in this scenario, requiring the problem to be stimulated and the cause of the X state propagated to testbench checks. In both cases a synthesized netlist will have an undefined behavior that does not match the RTL simulation semantics, which can lead to the issue being hidden at the netlist level. This issue is easy to accidently create, and can be hard to detect during simulation, or will often be buried as one of many “out-of-bound access” warnings in a linting log file.
The Safety Checks App will inspect any array access. Much like a simulator, it will analyze actual code behavior to understand if the scenario will arise during real operation. Unlike the simulation approach, the formal app will consider ALL possible operational sequences automatically without the need to provide stimulus. If the design is capable of an out of bounds access, the error will be flagged, the code driver creating that mechanism will be highlighted, and a simulation trace leading to this situation will be shown in the debugger.
Example for a Synthesis / Simulation Mismatch
Another classic scenario that could produce a Simulation-Synthesis Mismatch (SSM) is the misuse, in Verilog, of full-case and parallel-case pragmas. These pragmas instruct the synthesis tool that certain logic optimizations can be safely made in order to improve area and timing. However, they have no effect on the RTL simulation semantics and if the designer has made a mistake, for example using the parallel-case pragma in a case statement with branches that are not mutually exclusive, the behavior of the synthesized netlist will potentially not match the RTL semantics.
SystemVerilog has introduced two keywords, ‘unique’ and ‘priority’, to mitigate this problem. The use of the keyword ‘unique’ is equivalent to using both the parallel-case and full-case pragmas. The use of the keyword ‘priority’ is similar to using the full-case pragma. The advantage is that the standard prescribes that a simulator must issue a warning if a scenario is hit where the case statement does not respect the unique or priority semantics. This will help in flagging a problem but of course the scenario must be uncovered by the simulation stimulus.
The Safety Checks App will synthesize safety checks whenever this style of case statement is used, for both the SystemVerilog key words and the Synopsys Design Compiler pragmas. It will then exhaustively check formally that the design cannot reach an unsafe situation where the optimization assumptions specified above are violated. It thus formally proves that no simulation synthesis mismatches can occur.