It could happen to any of us: your plane is stricken by mechanical failure and is forced on a desert island. Your only hope of rescue is to verify the RTL for a solar powered drone that will fly to the nearest civilization with your message. All you have for your EDA usage is a solar powered Linux laptop, your DUT's RTL, some planning & management tools, and formal & CDC apps -- no simulation!
The questions before you include:
- How do you translate verification requirements into a machine-readable verification plan and related coverage goals?
- How do I create the corresponding "formal testbench"?
- Are there any formal apps that can expedite or expand the scope my verification?
- The drone's FPGA design will call for multiple asynchronous clocks – will this be a problem?
- Is my drone's RTL sensitive to any logic faults, and how can I verify that the internal safety mechanism handles them to avoid a catastrophic failure?
- How can I be confident that my verification is complete, and it is safe to launch the drone?
In this tutorial you will learn how to:
- Map your verification requirements to a human and machine readable verification plan
- Select & run automated formal apps to expedite your verification effort without writing any SVA code
- Setup a formal testbench and related verification methodology efficient property checking and analysis. This includes how to translate your requirements into SVA assertions, constraints, and "covers" that will be optimized for formal analysis. Not all formal runs get a complete proof on the first pass, so we will also share methodologies for dealing with "inconclusives" and how to leverage "bounded proofs" to meet your verification objectives even if a formal proof isn't obtained.
- Use formal-based CDC analysis to make sure none of the inter-clock domain signals go metastable
- Use formal to check your drone's sensitivity to logic faults so it will endure its trip to civilization
- Close the verification loop by electronically mapping all your progress back to your original plan
Save yourselves and view to this tutorial!
