Verification of hardware design for data transformation component

摘要

Methods and systems for verifying a hardware design for a main data transformation component. The main data transformation component is representable as a hierarchical set of data transformation components which includes (i) a plurality of leaf data transformation components which do not have children, and (ii) one or more parent data transformation components which each comprise one or more child data transformation components. The method includes: (a) for each of the plurality of leaf data transformation components, verifying that an instantiation of the hardware design for the leaf data transformation component generates an expected output transaction in response to each of a plurality of test input transactions; and (b) for each of the one or more parent data transformation components, formally verifying, using a format verification tool, that an instantiation of an abstracted hardware design for the parent data transformation component generates an expected output transaction m response to each of a plurality of test input transactions. The abstracted hardware design for the parent data transformation component represents each of the one or more child data transformation components of the parent data transformation component with a corresponding abstracted component that is configured to for a specific input transaction to the child data transformation component produce a specific output transaction with a causal deterministic relationship to the specific input transaction. During formal verification the formal verification tool is configured to select the specific input transaction and the specific output transaction pair to be each possible valid input transaction and valid output transaction pair for the child data transformation component.