Debugging Missing Assumptions in a Formal Verification Environment

Abstract—In the past decade, formal tools have increased functional verification efficiency by searching for corner-case bugs using mathematical reasoning. At the same time, this prac-tice has introduced new challenges when failures are detected. Once a counter-example is returned by a formal tool, the user typically does not know if the failure is caused by a design bug, an incorrectly written assertion, or a missing assumption. This paper introduces a novel methodology to automatically debug missing assumptions. We first present an algorithm to automati-cally generate missing input constraints given a failing counter-example. The algorithm is then extended to provide higher quality assumptions using multiple failing counter-examples. A function is extracted from these counter-examples that encodes the input combinations that cause the assertion to fail. This function is later used to generate a list of fixed cycle assumptions that prevent failures similar to the generated counter-examples. These filtered assumptions can then be used as hints for the actual missing assumption. Further, if a missing assumption is not the cause of the failure, the method offers the additional benefit that the counter-examples it generates can be utilized to debug the RTL and/or the assertion. Preliminary experimental results show that the generated properties provide a strong intuition as to what input constraints may be missing. I