Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1145/1403375.1403506 | Proceedings of the conference on Design, automation and test in Europe |
Keywords | Field | DocType |
design automation,formal verification,trusted computing,logic design,formal specifications,productivity,reconfigurable hardware,computer science,property checking,embedded systems,hardware,signal generators,fpga | Logic synthesis,Model checking,Computer science,Correctness,Field-programmable gate array,Formal specification,Electronic design automation,Computer hardware,Computer engineering,Reconfigurable computing,Formal verification | Conference |
ISSN | Citations | PageRank |
1530-1591 | 24 | 1.43 |
References | Authors | |
4 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Frank Rogin | 1 | 44 | 4.05 |
| Thomas Klotz | 2 | 41 | 6.50 |
| Görschwin Fey | 3 | 238 | 31.41 |
| Rolf Drechsler | 4 | 3707 | 351.36 |
| Steffen Rülke | 5 | 52 | 7.40 |