Verifying data intensive state transition machines related application

摘要

A method, system, and computer program product for verification of a state transition machine (STM) are provided in the illustrative embodiments. The STM representing the operation of a circuit configured to perform a computation is received. A segment of the STM is selected from a set of segments of the STM. A set of properties of the segment is determined. The set of properties is translated into a hardware description to form a translation. The segment is verified by verifying whether all relationships between a pre-condition and a post condition in the translation hold true for any set of inputs and any initial state of a hardware design under test. A verification result for the segment is generated. Verification results for each segment in the set of segments are combined to generate a verification result for the STM.

主权项

1. A computer implemented method for verifying a state transition machine (STM), the method comprising:
receiving the STM, the STM representing the operation of a circuit configured to perform a computation; selecting a segment of the STM from a set of segments of the STM; determining a set of properties of the segment; translating the set of properties into a hardware description to form a translation such that when a property holds according to the hardware description, a circuit corresponding to the hardware description outputs a predetermined value, and when the property does not hold according to the hardware description, the circuit outputs a second predetermined value; verifying, using a processor and a memory, the segment by verifying whether all relationships between a pre-condition and a post condition in the translation hold true for any set of inputs and any initial state of a hardware design under test; generating a verification result for the segment; and combining verification results for each segment in the set of segments to generate a verification result for the STM.