Property refinement techniques for enhancing coverage of formal property verification

Abstract

Coverage metrics for formal property verification (FPV) are gaining in significance as most chip design companies are adopting formal methods within a predominantly simulation based validation flow. Researchers have observed that typical correctness properties exhibit a low amount of coverage since they check for the absence of invalid runs, rather than the existence of valid runs. In this paper, we show that feedback from FPV can be effectively used to refine an existing specification to obtain better coverage. We propose an interactive methodology for specification refinement, and present formal methods for implementing this methodology.