Article from Verification Horizons February 2023
Jumpstart Your Formal Verification with a Little Help
by Senior Member Technical Staff, Doug Smith
An advantage of using formal verification is how quickly a formal environment can be created with a few simple properties that immediately start finding design issues. However, not all design behaviors are easily modeled using SystemVerilog's property syntax, resulting in complex or numerous properties, or behaviors that require more than just SVA. That is where helper code comes to the rescue. Helper code can significantly reduce the complexity of properties as well as be used to constrain formal analysis. Likewise, formal analysis may need to reduce the complexity of the problem and state space, which helper code can also help. So where are some places to use helper code and when?
This article looks at how helper code can be used to simplify our properties, model formal abstractions, constrain formal inputs, and aid formal analysis.
Article Downloads
You can download the article using the following link and also the associated code. In exchange, we will ask you to enter some personal details. To read about how we use your details, click here. On the registration form, you will be asked whether you want us to send you further information concerning other Doulos products and services.
Downloads: Jumpstart Your Formal Verification with a Little Help »
