Push button apps for formal code analysis
What designers require for early and automated detection of implementation issues are fast and easy to set up static checks for the sequential operation of the code in an exhaustive fashion, without relying on user provided stimulus. Formal has been advocated as the solution, but getting started with formal has been seen as difficult and time consuming.
OneSpin 360 DV-Inspect Apps simplify the setup and learning to a minimum. Targeting three of the most time consuming bug finding scenarios, DV-Inspect apps are the easiest to use.
The DV-Inspect Apps Library comprises the following:
Focused formal-based structural code analysis for a low noise check of code syntax and semantics... »more
The OneSpin’s low noise Structural Analysis App is applied early in the process and quickly identifies questionable language use in otherwise syntactically correct code...
Operational checks for standard coding problems, sequentially verifying code by automatically synthesizing assertions exposing those issues... »more
OneSpin’s Safety Check App automatically detects a wide range of coding issues, without the need to provide test vectors, exhaustively examining every possible scenario...
Ensuring that code segments can be activated, using automated reachability analysis to check code regions, FSM states and transitions, as well as signal value transitions... »more
OneSpin’s Activation Checks App automatically checks for activation of particular common design functions, for example if code can be reached, transitions of finite state machines...
DV-Inspect Apps Library
Structural Analysis is focused on syntactic and semantic analysis of source code. Safety Checks exhaustively verify the absence of common sequential design operation issues and failure debugging. Activation Checks ensure that specific design functions can be executed and are not blocked by unreachability. The three apps have one thing in common, they are all fully automatic and require no assertions to be created by the user.