Solidify: Static Functional Verification for HDL Design and verification engineers Averant

Introduction

Solidify, from Averant Inc., is an interactive, easy-to-use static functional verification tool. Solidify offers a new approach to functional verification based upon formal methods. You describe things your design should always do, or things that your design should never do by writing a specification in fragments called Properties. Flow Summary

Having loaded your design and the required Properties into Solidify, the tool will then consider every possible legal combination of inputs to your design to see whether the property holds true for all possible input vector sequences. The result of this is that Solidify will either confirm your design works and can never fail, or alternatively, provide an example of your design failing.

Solidify does not require either a vector set or a test bench to exercise the design and therefore there are no simulations to run. The other advantage is that testbenches are generally written to exercise the behaviour of the design in its expected mode of operation. In reality the input to a block often deviates from the designers initial expectations, and the design is then in untested territory.

Because Property Checkers consider all possible combinations of inputs to the design all possible modes of operation are tested, and hence corner case bugs the designer may not have thought to test for are quickly exposed.

Assertions

Many companies already use assertions within their designs using languages such as OVL, OVA, SVA and PSL. Solidify can take these assertions and formally prove that they will always be false for all legal input vectors. Simulations can only prove that your design works for the vectors you have chosen to apply.

Autochecks

Solidify includes a library of standard design checks that can be run automatically on any design. These include checks for reset, tri-states, lock-up , constant bits, unreachable code, and multi cycle path violations. There is also a stand-alone version which performs AutoChecks called SolidAC.

Static Coverage Analysis

Solidify provides design coverage analysis to assure that each signal in a block has been "covered" by one or more Properties. The goal of verification is to prove that a design behaves exactly as expected and that it has no unexpected behaviours. If sets of properties completely "cover" a design, then any change in observable functional behaviour should cause at least one property to fail.

Additional Plugins

Solidify also has a number of additional plugins available, including SolidPC. This allows an automated verification of AMBA bus interfaces to be performed.

Further Reading

Solidify Brochure  
Technology Backgrounder An easy read for people new to the technology
Cisco's experience with property checking This paper won Best Paper at Design Con 2000
ARM's paper on X analysis in Verilog designs An advanced paper that was voted best technical paper by the committee at SNUG 2003

Evaluation Request

To see how Solidify can help you improve the quality of your designs, fill in the evaluation request form or contact us directly.

^ back to top