Patent US5513122A successfully refreshed from Google Patents.
US5513122A
Expired / Lapsed
US
⏱️ 0.0 years remaining
Method and apparatus for determining the reachable states in a hybrid model state machine
Assignee: Bell Semiconductor LLC
•
Filing: 1994-06-06
•
Granted: 1996-04-30
•
Expires: 2014-06-06
Abstract
Abstract The present invention provides a method and apparatus for more efficiently validating high-level specifications of sequential digital systems, and in particular, those represented by hybrid models. According to the present invention, the high-level representation of a system is converted into a direct sum EFSM. An operator or a data file then provides an initial configuration or set of initial configurations of states and variable values. The method of the present invention then determines the set of configuration reachable from the initial configuration through symbolic execution of the direct sum EFSM. By representing the transitional relations of the machine as the and-product of Boolean expressions and arithmetic expressions, each class of expressions may be processed separately. When complete, the symbolic execution produces a cover of the set of reachable states. The results may then be reviewed to determine if the given specification produces unexpected or incompatible results.
Inventors
- 👤 Kwang-Ting Cheng
- 👤 Anjur S. Krishnakumar
Bibliographic Details
Application Number
—
Jurisdiction
US
Data Source
google_patents
Last Synchronized
2026-11-09 05:26
CPC Classifications
G; G06; G06F; G06F30/00; G06F30/30; G06F30/32; G06F30/33; G06F30/3323
Claims Analysis
Total Claims: 25
Claim 1
Independent Claim
157 words
A method of validating a high-level specification of a sequential circuit design, 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.
Claim 2
Independent Claim
157 words
A method of validating a high-level specification of a sequential circuit design, 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.
Claim 3
Dependent Claim
35 words
The method of claim 1 further comprising the step of: g) applying a predetermined set of criteria to the set of reachable configurations, said application producing a signal indicating whether the high-level specification is valid.
Claim 4
Dependent Claim
55 words
The method of claim 1 wherein the extended finite state machine further comprises at least one non-direct sum hybrid enabling function corresponding to at least one outgoing edge of the extended finite state machine, and the step b) further comprises the step of converting the at least one hybrid enabling function into direct sum form.
Claim 5
Dependent Claim
35 words
The method of claim 3 wherein the step of converting at least one hybrid enabling function into direct sum form further comprises expanding the non-direct sum hybrid enabling function into two direct sum enabling functions.
Claim 6
Dependent Claim
35 words
The method of claim 1 wherein at least one outgoing edge of the extended finite state machine has one or more enabling functions and at least one outgoing edge has one or more update functions.
Claim 7
Dependent Claim
43 words
The method of claim 5 wherein the plurality of vertices of the derived graph comprise a set of mutually orthogonal functions that are derived from the one or more enabling functions of at least one outgoing edge of the extended finite state machine.
Claim 8
Dependent Claim
31 words
The method of claim 1 wherein the symbolic execution of the derived graph employs set manipulation operations, the set manipulation operations including Boolean set manipulation operations and arithmetic set manipulation operations.
Claim 9
Dependent Claim
32 words
The method of claim 1 wherein the symbolic execution of the derived graph employs set manipulation operations, the set manipulation operations including the manipulation of binary decision diagrams and algebraic polyhedral regions.
Claim 10
Independent Claim
133 words
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.
Claim 11
Independent Claim
133 words
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.
Claim 12
Dependent Claim
28 words
The method of claim 9 further comprising the step of generating a derived graph of the EFSM prior employing symbolic execution to determine the set of reachable states.
Claim 13
Dependent Claim
26 words
The method of claim 9 wherein step b) further comprises the step of expanding the non-direct sum hybrid enabling functions into two direct sum enabling functions.
Claim 14
Dependent Claim
23 words
The method of claim 9 wherein said method is applied to an EFSM representation of a high-level specification of a sequential circuit design.
Claim 15
Dependent Claim
23 words
The method of claim 9 wherein said method is applied to an EFSM representation of a high-level specification of a communications protocol specification.
Claim 16
Independent Claim
114 words
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.
Claim 17
Independent Claim
114 words
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.
Claim 18
Dependent Claim
12 words
The apparatus of claim 14 wherein the interactive means comprises a keyboard.
Claim 19
Dependent Claim
15 words
The apparatus of claim 14 wherein the results communicating means comprises a visual display device.
Claim 20
Dependent Claim
14 words
The apparatus of claim 14 wherein the results communicating means comprises a printing device.
Claim 21
Independent Claim
112 words
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.
Claim 22
Independent Claim
112 words
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.
Claim 23
Independent Claim
157 words
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.
Claim 24
Independent Claim
157 words
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.
Claim 25
Dependent Claim
35 words
The method of claim 19 further comprising the step of: g) applying a predetermined set of criteria to the set of reachable configurations, said application producing a signal indicating whether the high-level specification is valid.
References Cited (Backward Citations)
US4694411A
Cited
US5005136A
Cited
US5140538A
Cited
US5038307A
Cited
US5163016A
Cited
US5331568A
Cited
US5394347A
Cited
USPTO Annuity & Maintenance Windows
| Annuity Stage | Window Opens | Payment Deadline | Surcharge Period Until | Estimated Fee | Status |
|---|---|---|---|---|---|
| 3.5 Years (Year 4) | 1999-04-30 | 1999-10-30 | 2000-04-30 | $2000.00 | Window Closed / Lapsed |
| 7.5 Years (Year 8) | 2003-04-30 | 2003-10-30 | 2004-04-30 | $3760.00 | Window Closed / Lapsed |
| 11.5 Years (Year 12) | 2007-04-30 | 2007-10-30 | 2008-04-30 | $7700.00 | Window Closed / Lapsed |