A Formal Design Verification System Based on an Automated Reasoning System

In recent years, interest has grown in the possibility of developing a formal design verification approach as an alternative to standard simulation techniques for verification. Several researchers have used, or suggested the use of, artificial intelligence techniques in such a formal system. The purpose of this paper is to briefly describe the ongoing work on the development of a viable formal design verification system based on an automated reasoning system. This system, called LMA (Logic Machine Architecture), has been developed at Argonne National Laboratory. This paper describes the basic ideas underlying this formal system for verification and discusses several of the current research projects.