Patent ID: 7454324
Filing Date: 2008-11-18
Classification: G06F

Abstract:
1. A method of formal analysis of a description of a device, the method being implemented in a programmed computer, the method comprising: simulating the description of the device to verify functionality of the device; determining a set of states that occur during the simulation of the device based on the description, wherein the set of states can be used as initial states in a formal analysis; determining a predetermined criterion for the description, the criterion designed to select states in the set of states to reduce states generated by the simulation that are to be used as initial states in a formal analysis of the description of the device; automatically selecting a subset of states from the set of states generated during the simulation using the predetermined criterion, wherein selection of the subset of states using the criterion is configured to optimize a subset of defects that can be possibly found using the subset of states in the formal analysis out of a total number of defects that can be found using every state in the set of states in the formal analysis, wherein automatically selecting comprises: performing formal analysis of the description of the device to determine defects of the description of the device, the formal analysis using the subset of states as the initial states instead of using all of the set of states as initial states; and storing a result of the formal analysis.