Patent Document ID: 7900173
Application ID: 12345473
Patent Flag: 1

Claim One:
1. A method of bounded model checking to verify a design of a finite state machine comprising: unfolding a transition relation that represents combinational logic behavior of the finite state machine as a circuit graph, into a first sequence of concatenated transition relations representing combinational logic behavior of the finite state machine in a sequence of time frames; determining that at least two vertices in the circuit graph are functional equivalents in a time frame of the first sequence; merging the at least two functionally equivalent vertices in a time frame subsequent to the time frame in which they are functional equivalents so as to produce a simplified transition relation circuit graph; unfolding the transition relation into a second sequence of concatenated transition relations that includes the simplified transition relation circuit graph in the same time frame position of the second sequence that it occurs in the first sequence; providing initial state information to a first transition relation of the second sequence of concatenated transition relations; and performing, using a computer, a satisfiability check for a property to be verified using output state values reached by at least one transition relation of the second sequence in response to the initial state information.