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.