Method and apparatus for determining the reachable states in a hybrid model state machine

A method of determining the set of reachable configurations in an EFSM, the EFSM being partially defined by a set of enabling functions, at least one of the set of enabling functions being a non-direct sum hybrid enabling function dependent on at least one Boolean variable and at least one arithmetic variable, the method comprising:

• a) selecting a non-direct sum enabling function from the set of enabling functions;
• b) converting the non-direct sum hybrid enabling function into an and-product of a Boolean variable expression and an arithmetic variable expression;
• c) repeating steps a and b for all non-direct sum hybrid enabling functions in the set of enabling functions;
• d) obtaining a set of initial configurations;
• and
• e) employing symbolic execution to determine the set of configurations reachable from the set of initial configurations.

An apparatus for validating a high-level specification of a sequential circuit design, the high-level specification including both arithmetic variables and Boolean variables, the apparatus comprising:

• a) storage means for storing a high-level specification of a sequential circuit design;
• b) an interactive means for receiving input from a human operator;
• c) a computer processor connected to the storage means and further connected to the interactive means, said computer processor operable to generate a direct sum EFSM from the high-level specification and further operable to symbolically execute the direct sum EFSM;
• and
• d) means connected to the computer processor for communicating the results of the symbolic execution of the direct sum EFSM to a human operator.

An apparatus for validating a high-level specification of a sequential circuit design, the high-level specification including at least one arithmetic variable and at least one boolean variable, the apparatus comprising:

• a) an external memory device for the storage of the high level specifications;
• b) a keyboard for receiving input from a human operator;
• c) a computer processor connected to the external memory device and the keyboard, said computer processor operable to generate a direct sum EFSM from the high-level specification and further operable to execute symbolically the direct sum EFSM;
• and
• d) a video display for displaying the results of the symbolic execution of the direct sum EFSM to a human operator.

A method of validating a high-level specification of a communications protocol specification, the high-level specification including both arithmetic variables and Boolean variables, the method comprising:

• a) generating an extended finite state machine from the high-level specification, said extended finite state machine comprising at least one state connected to one or more outgoing edges, each outgoing edge terminating in one of the at least one states;
• b) converting the extended finite state machine into a direct sum extended finite state machine;
• c) generating a derived graph of the direct sum machine, said derived graph comprising a plurality of vertices connected by at least one edge;
• d) obtaining an initial configuration;
• e) effecting symbolic execution of the derived sum machine using the initial configuration, said symbolic execution providing a set of configurations reachable from the initial configuration;
• and
• f) providing the set of reachable configurations to a means for communicating said set of reachable configurations to a human operator.