Property analysis and design understanding

—Verification is a major issue in circuit and system design. Formal methods like bounded model checking (BMC) can guarantee a high quality of the verification. There are several techniques that can check if a set of formal properties forms a complete specification of a design. But, in contrast to simulationbased methods, like random testing, formal verification requires a detailed knowledge of the design implementation. Finding the correct set of properties is a tedious and time consuming process. In this paper, two techniques are presented that provide automatic support for writing properties in a quality-driven BMC flow. The first technique can be used to analyze properties in order to remove redundant assumptions and to separate different scenarios. The second technique – inverse property checking – automatically generates valid properties for a given expected behavior. The techniques are integrated with a coverage check for BMC. Using the presented techniques, the numbe...

• Type: Conference
• Year: 2009
• Where: DATE
• Authors: Ulrich Kühne, Daniel Große, Rolf Drechsler
• Keywords: DATE 2009, Formal Methods, Formal Properties, Hardware, Time Consuming Process