Description and Reasoning of VLSI circuit in temporal logic

This paper presents a method for describing and reasoning about the behavior of VLSI circuits within the framework of Extended Temporal Logic. For a reasoning method, an “ω-graph approach” is proposed which is useful in verifying the validity of a design. Not only verification but also other reasoning about circuit properties, such as unknown signal identification, can be treated in a unified way by this ω-graph approach. This approach has been studied as a basis of an expert system for the authors’ VLSI CAD system.