Debugging VHDL designs using model-based reasoning

The application of formal methods in software engineering and hardware desi gn has become an important field of research. It aims at minimizing time to market and reduce the overall development costs. While formal verification , e.g. model-checking, is widely used, methods for helping programmers or e ngineers in locating and fixing faults within a hardware design or software are rarely available. In this paper we describe part of the advanced diagn osis and measurement selection capabilities of the model-based diagnosis to ol VHDLDIAG designed for (semi)automatically locating bugs in VHDL programs . VHDL is an Ada-like and widely used hardware description language. VHDL p rograms are converted into logical descriptions which are then used by a di agnosis engine for detecting the parts of the program responsible for an ob served misbehavior. The results of diagnosis, i.e, the malfunctioning progr am fragments, are mapped back to the program code. Because of the logical d escription used VHDLDIAG can be applied to a wide range of programs from sm all to very large ones with up to thousands of MBytes of source code. This paper presents techniques which use multiple versions of a design in diagno sis, as well as the measurement selection process used in VHDLDIAG. Formal definitions and performance results using real-world VHDL programs are give n. (C) 2000 Published by Elsevier Science Ltd.