Method and system for reducing state space variables prior to symbolic model checking

Abstract

A computer-implemented method for systematically eliminating redundant circuit elements in a state machine of a model having sequential circuit elements possessing one of a fixed number of possible states, typically “0” and “1”. Initially, the sequential circuit elements are sorted into groups whose state is determinate i.e. equal to “0” or “1”. The state of each circuit element whose state is determinate is stored in memory and its next state is calculated and compared with its preceding state. Each circuit element whose successive states are different is moved to the group of indeterminate circuit elements, and the cycle is repeated in respect of all remaining determinate circuit elements until no further circuit elements are moved. Each of the remaining determinate circuit elements is then replaced by a constant equal to its corresponding state i.e. “0” or “1”. Finally, any circuit elements whose output is connected to one or more of the replaced circuit elements and to no other circuit elements is eliminated from the model.

What is claimed is:  
     
       1. A computer-implemented method for systematically eliminating redundant circuit elements in a state machine of a model having sequential circuit elements possessing one of a fixed number of possible state thereby reducing model complexity and rendering the state machine of the model solvable by a computer in a short calculation time than would be possible for the state machine including the redundant circuit elements, said method comprising the steps of: 
       (a) sorting the sequential circuit elements into groups having an initial state which is determinate i.e. equal to a known one of said fixed number of possible states or which is indeterminate,  
       (b) storing the state of each circuit element whose is determinate,  
       (c) for each circuit element whose state is determinate, calculating its next state,  
       (d) moving each circuit element in (c) whose next state is different to the state thereof stored in (b) to the group of indeterminate circuit elements,  
       (e) repeating steps (b) to (d) in respect of all remaining determinate circuit elements until no further circuit elements are moved in step (d),  
       (f) replacing each of the remaining determinate circuit elements by a constant equal to its corresponding state, and  
       (g) eliminating any circuit elements whose respective output is connected to one or more of the circuit elements replaced in (f) and to no other circuit elements.  
     
     
       2. The method according to claim  1 , wherein the circuit elements are logic circuits having two possible logic states “0” and “1”. 
     
     
       3. A system for systematically eliminating redundant circuit elements in a state machine of a model having sequential circuit elements possessing one of a fixed number of possible states thereby reducing model complexity and rendering the state machine of the model solvable by a computer in a shorter calculation time than would be possible for the state machine including the redundant circuit elements, said system comprising: 
       (a) a memory for storing the state machine of the model, and  
       (b) a processing unit coupled to the memory for removing redundancy from the model;  
       (c) the processing unit including:  
       (i) a sorter for sorting the sequential circuit elements into groups having an initial state which is determinate i.e. equal to a known one of said fixed number of possible states or which is indeterminate,  
       (ii) a storage unit storing in the memory the state of each circuit element whose state is determinate,  
       (iii) a computer unit for calculating the next state of each circuit element whose state is determinate,  
       (iv) a comparator unit for comparing successive states of each circuit element and for removing any circuit element from the deteminate group whose successive states are different,  
       (v) a substitution unit for replacing each of the remaining determinate circuit elements by a constant equal to its corresponding state, and  
       (vi) an elimination unit for eliminating any circuit elements whose respective output is connected to one or more of the circuit elements replaced in (v) and to no other circuit elements.