Sequential ATPG techniques for Model Checking

摘要

This paper studies the application of sequential ATPG (Automatic Test-Pattern Generation) techniques to the problem of model checking. It first introduces the problems of verification and model checking for sequential circuits and discusses limitations of existing formal techniques that address these problems. It then introduces sequential ATPG techniques and studies their application to the model checking problem. Techniques are discussed for mapping the problem of model checking to the sequential ATPG problem and results are shown to demonstrate that the method has potential to scale up to large, industrial-strength, hardware designs for which traditional model checking techniques fail.