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 simulationbased 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 qualitydriven BMC flow, that have been introduced in [1]. 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.