Techniques for effectively applying model checking to design projects

This paper describes some techniques for applying model checking to actual design projects. Because of the rapid growth of digital systems, logic veri fication will be a main problem in the design flow. Although simulation-bas ed verification has been adopted, it is widely accepted that the evolutiona ry progress of simulation techniques will not provide a solution to the ver ification crisis. We have been conducting research on formal verification, especially on model checking. We have developed some advanced techniques th at should work effectively on actual designs and have applied our tool "BIN GO" to some design projects. This paper compares model checking with simula tion-based verification. It also describes how to use model checking techni ques complementally with simulation.