Interoperable Application-Specific Solutions For Formal Verification

Rather than deploying a general-purpose tool suite, many design teams need more targeted solutions to use throughout the design flow.

popularity

Historically, formal verification technology has been licensed as a compre- hensive suite of tools that can be used to address a broad range of formal verification applications and problems. Such deployment required a wide range of in-depth skills on the user’s part before the technology could be leveraged by not only first time users, but also experienced ones. New users were often overwhelmed by the comprehensive nature of the technology and the steep learning curve, while experienced users wishing to deploy a narrow application scope across the organization were impeded by the all-in-one approach.

Early-stage users generally prefer to adopt and deploy new design and verifi- cation methods using a low-risk, step-by-step approach, which also allows them to accumulate skills and expertise incrementally. Experienced formal users are more likely to utilize focused capabilities to tackle specific issues and applications within design and verification, but must do so across an organi- zation rather than on an individual basis. In both cases, users traditionally had to license an entire tool suite in order to access only a subset of its capability. Consequently, the all-in-one approach did not and does not provide for efficient deployment for either type of user.

To read more, click here.



  • We definitely see this trend in tools that analyze the designers intent for specific problem areas such as clock-domain crossing (CDC) verification, x-propagation and reset verification, and automatic RTL analysis for dead code, and bad FSMs, etc.. Many engineers are using formal engines in their analysis tools without having to write properties. Because the problem area is specific, only those parts of the design that are of concern get analyzed. This provides the throughput and accuracy designers are looking for. I expect to see the number of specific analysis tools that employ formal to keep growing.