Property analysis and design understanding

9 years 8 months ago
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...
Ulrich Kühne, Daniel Große, Rolf Drechs
Added 20 May 2010
Updated 20 May 2010
Type Conference
Year 2009
Where DATE
Authors Ulrich Kühne, Daniel Große, Rolf Drechsler
Comments (0)