Formal verification of deadlock property

Abstract

A verification system determines proof of the absence of a deadlock condition or other data-transport property in a multi-system SoC using helper assertions derived from a transaction definition. The verification system receives the circuit design information along with a transaction definition for one or more ports of the SoC. Once specified, the transaction definition is instantiated into the full system or subsystem RTL, generating an expanded RTL and a deadlock property. Data flow through the RTL is analyzed to extract helper assertions describing how the data flowed through the RTL. Helper assertions are automatically extracted to aid in the verification of the absence of a deadlock condition. Using the helper assertions, the formal engine applies one or more techniques to formally analyze the circuit design to prove the absence of a deadlock condition.