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

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.