Patent ID: 7155374

Claim:
A method for checking a model, which defines states of a hardware system under study and a transition relation among the states, the method comprising: providing a specification of a path to be found through the states of the hardware system under study from an initial set that comprises at least one initial state among the states of the hardware system to a target set that comprises at least one target state among the states of the hardware system, such that a specified sequence of events is to occur on the path between the at least one initial state and the at least one target state; beginning from the initial set, computing successive reachable sets comprising the states of the hardware system that are reachable from the initial set along the path, such that in the successive reachable sets the events occur in the specified sequence; determining whether an intersection exists between one of the reachable sets on the path and the target set; and when the intersection is not found to exist, producing a partial trace along the path between the at least one initial state and a termination state in which at least one of the specified events occurs.