Property Analysis and Design Understanding in a Quality-Driven Bounded Model Checking Flow

In the design process of digital systems, functional verification is a major issue. Generally, formal methods like bounded model checking (BMC) offer the highest quality of the verification results, especially when used in combination with techniques that check if a set of properties forms a complete specification of a design. However, in contrast to simulation-based methods, like random testing, formal verification requires a detailed knowledge of the design implementation. Formalizing a specification as a set of properties is a tedious and time consuming process. In this paper, we show the application of techniques to aid the verification engineer in writing properties in a quality-driven BMC flow. The first method can be used to remove redundant assumptions from properties and to separate different scenarios. The second technique, here called inverse property checking, takes an expected behavior of a design and automatically generates valid properties that can be checked for conformance with a specification. Both techniques can serve to reduce the number of iterations to obtain full coverage, when integrated with the verification flow. The benefits of the techniques are demonstrated with a memory management unit.