Automatic assume guarantee analysis for assertion-based formal verification

Assertion based verification encourages the insertion of many assertions into a design. Typically, not all assertions can be proven (or falsified). The indeterminate assertions require manual analysis in order to determine design correctness -- a time-consuming and error-prone process. This paper shows how automatic assume guarantee reasoning can be used to reduce the amount of manual analysis. We present algorithms to automatically compute the assume guarantee relations between assertions. We extend circular assume guarantee reasoning to compute more proofs. And, we show how automatic assume guarantee reasoning can be used in practice to reduce the number of indeterminate assertions requiring manual analysis. We present the results of applying our algorithms to large industrial designs.