Title :
Finding good counter-examples to aid design verification
Author :
Fey, Gorschwin ; Dreschler, R.
Author_Institution :
Inst. of Comput. Sci., Bremen Univ., Germany
Abstract :
Today up to 80% of the design costs for integrated circuits are due to verification. Verification tools guarantee completeness if equivalence of two designs or a property for a design is proven. In the other case, usually only one counter-example is produced. Then debugging has to be carried out to locate the design error. This paper investigates, how debugging can benefit from using more than one counter-example generated by the verification tool. The problem of finding useful counter-examples is theoretically analyzed and proven to be difficult. Heuristics are introduced and their quality is underlined by experimental results. Guidelines how to generate counter-examples are extracted from one of these heuristics.
Keywords :
formal verification; integrated circuit design; logic design; systems analysis; counter-example; debugging; design cost; design equivalence; design error location; design verification aid; integrated circuit design; verification tool; Boolean functions; Circuits; Computer science; Costs; Data structures; Debugging; Error correction; Formal verification; Guidelines; Testing;
Conference_Titel :
Formal Methods and Models for Co-Design, 2003. MEMOCODE '03. Proceedings. First ACM and IEEE International Conference on
Conference_Location :
Mont Saint Michel, France
Print_ISBN :
0-7695-1923-7
DOI :
10.1109/MEMCOD.2003.1210088
