System and method for executing image computation associated with a target circuit

A method for verifying a property associated with a target circuit, composing:

• receiving information associated with a target circuit, the information identifying a property within the target circuit to be verified;
• executing one or more operations for generating a set of transition relations for performing a reachability analysis associated with the target circuit;
• partitioning an image associated with the target circuit into a plurality of leaves each representing a subset of a final image to be generated by a partitioned ordered binary decision diagram (POBDD) data structure;
• and
• computing an analysis of one or more of the leaves using a selected one or both of conjunction and quantification operations separately.

Software for verifying a property associated with a target circuit, the software being embodied in a computer readable medium and including computer code such that when executed:

• receives information associated with a target circuit, the information identifying a property within the target circuit to be verified;
• executes one or more operations for generating a set of transition relations for performing a reachability analysis associated with the target circuit;
• partitions an image associated with the target circuit into a plurality of leaves each representing a subset of a final image to be generated a partitioned ordered binary decision diagram (POBDD) data structure;
• and
• computes an analysis of one or more of the leaves using a selected one or both of conjunction and quantification operations separately.

A system for verifying a property associated with a target circuit, comprising:

• means for receiving information associated with a target circuit, the information identifying a property within the target circuit to be verified;
• means for executing one or more operations for generating a set of transition relations for performing a reachability analysis associated with the target circuit;
• means for partitioning an image associated with the target circuit into a plurality of leaves each representing a subset of a final image to be generated by a partitioned ordered binary decision diagram (POBDD) data structure;
• and
• means for computing an analysis of one or more of the leaves using a selected one or both of conjunction and quantification operations separately.