Apparatus, method, and storage medium for verifying logical device

Abstract

First, a graph of a set of transition sequences representing the property to be satisfied by a finite state machine which is a model of a logical device. Then, a node to be processed is selected from the graph, and one of the branches connected to the node is selected. A mapping operation is performed on a set of states of the node on the starting side of the selected branch, and the result is added to the set of states of the node on the ending side. As a result of the mapping operation, it is determined whether or not the set of states which satisfies the target property has been obtained, that is, whether or not an example of a transition sequence has been successfully detected. If it has been successfully detected, then it is assumed that there is a transition sequence, the process terminates. If it has not been successfully detected, then it is determined whether or not there is an unprocessed branch connected to the node. If yes, the above described process is repeated. If not, then it is assumed that there are no transition sequences, and the process terminates.

What is claimed is:  
     
       1. 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.  
     
     
       2. The method according to  claim 1 , wherein 
       in said step (c), one state is retrieved from the set of states belonging to the node on the starting side stored in said second memory, and the mapping operation is performed only on the state.  
     
     
       3. The method according to  claim 1 , wherein 
       in said step (c), an appropriate subset is retrieved from the set of states belonging to the node on the starting side stored in said second memory, and the mapping operation is performed only on the subset.  
     
     
       4. The method according to  claim 1 , wherein 
       said mapping operation is performed by referring to a table in which a state transition relation of the finite state machine is entered.  
     
     
       5. The method according to  claim 1 , wherein 
       said mapping operation is performed according to information generated from the state transition relation of the finite state machine described in a hardware description language.  
     
     
       6. The method according to  claim 1 , wherein 
       the determination in said step (e) is to determine whether or not there is a synchronous transition sequence circulating infinite times through a specific node of the directed graph.  
     
     
       7. The method according to  claim 1 , wherein 
       the determination in said step (e) is to determine whether or not the set of states is actually obtained as a result of the mapping operation.  
     
     
       8. An apparatus for verifying a logical device, comprising: 
       first storage means for 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 labeled by a transition relation function, and storing configuration information about the directed graph;  
       second storage means for storing a set of states belonging to each node of the directed graph;  
       mapping operation means for reading from said second storage means 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 said first storage means, 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, adding a mapping operation result to a set of states belonging to the node on an ending side of the branches, and storing results in said second storage means; and  
       determination means for repeating processes performed by said mapping operation means, 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 said second storage means actually has elements.  
     
     
       9. The apparatus according to  claim 8 , wherein 
       said mapping operation means retrieves one state from the set of states belonging to the node on the starting side stored in said second storage means, and the mapping operation is performed only on the state.  
     
     
       10. The apparatus according to  claim 8 , wherein 
       said mapping operation means retrieves an appropriate subset from the set of states belonging to the node on the starting side stored in said second storage means, and the mapping operation is performed only on the subset.  
     
     
       11. The apparatus according to  claim 8 , further comprising state transition relation storage means for storing a table in which a state transition relation of the finite state machine is entered, wherein 
       said mapping operation is performed by referring to the table stored in said state transition relation storage means.  
     
     
       12. The apparatus according to  claim 8 , wherein 
       said mapping operation is performed according to information generated from the state transition relation of the finite state machine described in a hardware description language.  
     
     
       13. The apparatus according to  claim 8 , wherein it is determined whether or not there is a synchronous transition sequence circulating infinite times through a specific node of the directed graph. 
     
     
       14. The method according to  claim 8 , wherein 
       it is determined whether or not the set of states is actually obtained as a result of the mapping operation.  
     
     
       15. A computer-readable storage medium used to direct a computer to perform a process 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.  
     
     
       16. The storage medium according to  claim 15 , wherein 
       in said step (c), one state is retrieved from the set of states belonging to the node on the starting side stored in said second memory, and the mapping operation is performed only on the state.  
     
     
       17. The storage medium according to  claim 15 , wherein 
       in said step (c), an appropriate subset is retrieved from the set of states belonging to the node on the starting side stored in said second memory, and the mapping operation is performed only on the subset.  
     
     
       18. The storage medium according to  claim 15 , wherein 
       said mapping operation is performed by referring to a table in which a state transition relation of the finite state machine is entered.  
     
     
       19. The storage medium according to  claim 15 , wherein 
       said mapping operation is performed according to information generated from the state transition relation of the finite state machine described in a hardware description language.  
     
     
       20. The storage medium according to  claim 15 , wherein 
       the determination in said step (e) is to determine whether or not there is a synchronous transition sequence circulating infinite times through a specific node of the directed graph.  
     
     
       21. The storage medium according to  claim 15 , wherein 
       the determination in said step (e) is to determine whether or not the set of states is actually obtained as a result of the mapping operation.