Automatic Generation of Complex Properties for Hardware Designs

Property checking is a promising approach to prove the correctness of today’s complex designs. However, in practice this requires the formulation of formal properties which is a time consuming and non-trivial task. Therefore the acceptance and efficiency of formal verification techniques can be raised by an automated support for formulating design properties. In this paper we propose a new methodology to automatically generate complex properties for a given design. The tool, Dianosis, implements this methodology by analyzing a simulation trace. The extracted properties describe the abstract design behavior and are presented in a format that is easy to read and can be added to the set of properties used for formal or assertion-based verification. We provide experimental results on industrial hardware designs that show the effectiveness of Dianosis and motivate the practical use.

• Type: Conference
• Year: 2008
• Where: DATE
• Authors: Frank Rogin, Thomas Klotz, Görschwin Fey, Rolf Drechsler, Steffen Rülke
• Keywords: DATE 2008, Formal Properties, Formal Verification Techniques, Hardware, Today’s Complex Designs