A higher level hardware design verification

A novel approach to formal verification of computer hardware designs at a higher level of representation than the register-transfer level is presented. In this verification method, the specification of a digital system is defined as the input/output behavior of the external systems that communicate with the target system. The specification description called a cospecification and the implementation description called an FBL (functional block level) description are transformed into a hardware model representation and composed by connecting their related ports in the hardware model. Whether the design is correct or not is verified by producing state transitions of the composite system. This verification method requires only input/output relations between the cospecification description and the FBL description. This feature makes it suitable for verification of a higher-level design in which implementation details may not be explicit