Patent Document ID: 10007746
Application ID: 15292292
Patent Flag: 1

Claim One:
1. A method for generalized next-state-directed constrained random simulation comprising: obtaining an initial state s 1 for a finite state machine (FSM) that models a design of an electronic circuit of a device under test, the initial state assigning values to each register of the device under test, by providing an initial state function relating to the FSM to a satisfiability problem (SAT) solver to obtain register values that satisfy the initial state function; generalizing the initial state by randomly selecting a first Boolean random circuit from a set of Boolean circuits that are satisfied by the initial state; unrolling the FSM, wherein at a kth step (k>1) of steps of the unrolling, the unrolling includes finding a state s k for which the following formula is satisfiable: I ⁡ ( s 1 ) ⋀ ⁢ ⩓ i = 1 k - 1 ⁢ [ R i ⁡ ( s i ) ⋀ Tr ⁡ ( s i , s i + 1 ) ] ⋀ Q ⁡ ( s k ) where I(s 1 ) is an initial state function, R i is the first Boolean random circuit, T r is a Boolean transition function indicating the existence of a transition from state s j to state s j+1 , and Q is a second Boolean random circuit that is satisfied by state s k ; and generalizing using a third Boolean random circuit R k chosen at random from the set of Boolean circuits that are satisfied by state s k .