Patent ID: 6654715
Filing Date: 2003-11-25
Classification: G06F

Abstract:
A method of verifying a logical device, comprising:(a) converting a set of synchronous transition sequences of finite or infinite length having a target property of a finite state machine which is a model of a logical device to be verified into a directed graph labelled by a transition relation function, and storing configuration information about the directed graph in first memory; (b) storing in a second memory a set of states belonging to each node of the directed graph; (c) reading from the second memory a set of states belonging to each node on a starting side of the directed graph, referring to the configuration information of the directed graph stored in the first memory, selecting branches to be processed in a mapping operation and then performing the mapping operation corresponding to the branches on the set of the read states; (d) adding a mapping operation result to a set of states belonging to each node on an ending side of the branches, and storing results in the second memory; and (e) repeating said steps (c) and (d), and verifying whether or not the logical device to be verified satisfies the target property by determining whether or not the set of synchronous transition sequences indicated by the directed graph based on the set of states stored in the second memory actually has elements.