A verification method and apparatus of the hardware in the software context of the hardware, and a verification method and apparatus R of the software in the hardware context of the software.

摘要

The method and apparatus of the present invention using static partial order reduction and symbol verification enable the design of a system that includes both hardware and software to be verified. The system is appropriately specified as a hardware-centric language and a software-centric language, and properties are verified one at a time. Each property is identified as it is hardware-centric or software-centric. Hardware-centric features that contain little software do not use static partial order reduction. Software-centric and hardware-centric features with a substantial amount of software use static subsequence scaling. With partial order reduction, the software-centric language specification is converted to a synchronous format and combined with a hardware-centric specification. The combined specification is applied to symbol verification such as COSPAN, and the result is displayed.