AUTOMATED FORMAL VERIFICATION ANALYSIS OF COMPLEX HARDWARE CIRCUITS

摘要

The present invention consists in a technique, called Logic Compiler Technology, for performing an efficient fully automated formal verification analysis of complex hardware circuit descriptions. By using the Logic Compiler Technology, a formal verification tool can be implemented with the ability to support higher order logic for describing functional specifications and structural implementations of hardware circuits, and to perform an efficient fully automated validation of the circuit descriptions. The Logic Compiler Technology consists in a compilation technique embodied by a compiler (2) which translates the source description of a hardware circuit (1) into a semantically equivalent target description of it (3). The source description is expressed by using a special kind of higher-order logic, while the target description is expressed by using a special kind of many-sorted first-order logic. The target description can be elaborated by an efficient fully automated theorem prover (5), able to perform the hardware verification (6).