Title :
Bug identification of a real chip design by symbolic model checking
Author :
Chen, B. ; Yamazaki, M. ; Fujita, M.
Author_Institution :
Fujitsu Digital Technol. Ltd., Yokohama, Japan
fDate :
28 Feb-3 Mar 1994
Abstract :
We show how we have successfully identified the bug of a real chip by using formal verification techniques. Since excessive number of simulation cycles are necessary to debug the chip design, formal verification techniques, specifically CTL symbolic model checking, were adopted to identify the bug. We demonstrate several approaches including abstraction, which make it possible to apply symbolic model checking methods. The methods and ideas reported here are general enough for diagnosing other real chips
Keywords :
VLSI; circuit CAD; digital integrated circuits; finite state machines; formal verification; logic CAD; logic testing; CTL symbolic model checking; FSM; abstraction; bug identification; digital VLSI chips; formal verification techniques; real chip design; symbolic model checking; Buffer storage; Chip scale packaging; Circuit simulation; Communication switching; Debugging; Formal verification; Logic; Switches; Testing; Writing;
Conference_Titel :
European Design and Test Conference, 1994. EDAC, The European Conference on Design Automation. ETC European Test Conference. EUROASIC, The European Event in ASIC Design, Proceedings.
Conference_Location :
Paris
Print_ISBN :
0-8186-5410-4
DOI :
10.1109/EDTC.1994.326886
