I am a...
I want to...
Sign In/Register for Account
External Research Office
The lights in the Tunnel: Coverage Analysis for Formal Verification (August 2016)
ABSTRACT As formal verification engineers, the authors always face challenges to know the current status of test benches. Many questions need to be answered at certain stages of a project. E.g., do we need more assertions? Did you over-constrain inputs that drop an important design scenario? Are proof bounds for bounded proofs good enough to catch potential design bugs? For the properties that are fully proven, do they cover the design logic that were intended to cover? These four most-asked questions don’t have answers without extracting information from formal engines, which is not feasible for general users. However, like coverages from simulation-based verification, formal verification coverages can be defined and used as matrices to measure formal verification progress and completeness. In this paper, the authors will introduce formal verification coverage models and their usages by real-life examples. The four most-asked questions finally have reasonable and acceptable answers supported by matrices.
Oracle Labs on OTN
Want to try out some of the cool technology being built at Oracle Labs?
Email to a friend
Integrated Cloud Applications and Platform Services
Oracle RSS Feed