Verifying data intensive state transition machines related application

A computer usable program product comprising a computer usable storage medium including computer usable code for verifying a state transition machine (STM), the computer usable code comprising:

• computer usable code for receiving the STM, the STM representing the operation of a circuit configured to perform a computation;
• computer usable code for selecting a segment of the STM from a set of segments of the STM;
• computer usable code for determining a set of properties of the segment;
• computer usable code for translating the set of properties into a hardware description to form a translation;
• computer usable code for verifying 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;
• computer usable code for generating a verification result for the segment;
• and
• computer usable code for combining verification results for each segment in the set of segments to generate a verification result for the STM.

A data processing system for verifying a state transition machine (STM), the data processing system comprising:

• a storage device including a storage medium, wherein the storage device stores computer usable program code;
• and
• a processor, wherein the processor executes the computer usable program code, and wherein the computer usable program code comprises:
• computer usable code for receiving the STM, the STM representing the operation of a circuit configured to perform a computation;
• computer usable code for selecting a segment of the STM from a set of segments of the STM;
• computer usable code for determining a set of properties of the segment;
• computer usable code for translating the set of properties into a hardware description to form a translation;
• computer usable code for verifying 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;
• computer usable code for generating a verification result for the segment;
• and
• computer usable code for combining verification results for each segment in the set of segments to generate a verification result for the STM.