Boots – shoes – and leggings
Patent
1994-06-06
1996-04-30
Teska, Kevin J.
Boots, shoes, and leggings
364488, 364578, 395500, G05B 19045, G06F 1126
Patent
active
055131220
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.
REFERENCES:
patent: 4694411 (1987-09-01), Burrows
patent: 5005136 (1991-04-01), Van Berkel et al.
patent: 5038307 (1991-08-01), Krishnakumar et al.
patent: 5140538 (1992-08-01), Bass et al.
patent: 5163016 (1992-11-01), Har'El et al.
patent: 5331568 (1994-07-01), Pixley
patent: 5394347 (1995-02-01), Kita et al.
Alur, R., et al., "An Implementation of Three Algorithms for Timing Verification Based on Automata Emptiness," Proceedings of the Real-Time Systems Symposium, Phoenix, Arizona, Dec. 2-4, 1992, pp. 157-166.
Burch, J. R., et al., "Sequential Circuit Verification Using Symbolic Model Checking," 27th ACM/IEEE Design Automation Conference, Orlando, Florida, Jun. 24-28, 1990, pp. 46-51.
Cheng, K.-T., Krishnakumar, A. S., "Automatic Functional Test Generation Using The Extended Finite State Machine Model," Proceedings of the 30th Design Automation Conference, Dallas, Texas, Jun. 14-18, 1993, pp. 86-91.
Cho, H., et al., "ATPG Aspects of FSM Verification," Digest of Technical Papers, IEEE International Conference on Computer-Aided Design, Santa Clara, CA, Nov. 11-15, 1990, pp. 134-137.
Coudert, O., and Madre, J. C., "A Unified Framework for the Formal Verification of Sequential Circuits," IEEE International Conference on Computer-Aided Design, Santa Clara, CA, Nov. 11-15, 1990, pp. 126-129.
Coudert, O., et al., "Verification of Synchronous Sequential Machines Based on Symbolic Execution," Lecture Notes in Computer Science, Automatic Verification Methods for Finite State Systems, Proc. of Intern. Workshop, Grenoble, France, Jun. 12-14, 1989, pp. 365-373.
Devadas, S., et al., "Design Verification and Reachability Analysis Using Algebraic Manipulation," Proc. of IEEE Inter. Conference on Computer Design: VLSI in Computers & Processors, Cambridge, MA, Oct. 14-16, 1991, pp. 250-258.
Dill, D. L., "Timing Assumptions and Verification of Finite-State Concurrent Systems," Lecture Notes in Computer Science, Automatic Verification Methods for Finite State Systems, Proc. on International Workshop, Grenoble, France, Jun. 12-14, 1989, pp. 197-212.
Hopcroft, J., and Pansiot, J.-J., "On the Reachability Problem for 5-Dimensional Vector Addition Systems," Theoretical Computer Science, No. 8, 1979, pp. 135-159.
Touati, H. J., et al., "Implicit State Enumeration of Finite State Machines Using BDD's," Digest of Technical Papers, IEEE Intern. Conf. on Computer-Aided Design, Santa Clara, CA, Nov. 11-15, 1990, pp. 130-133.
Cheng Kwang-Ting
Krishnakumar Anjur S.
AT&T Corp.
Frejd Russell W.
Teska Kevin J.
LandOfFree
Method and apparatus for determining the reachable states in a h does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Method and apparatus for determining the reachable states in a h, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and apparatus for determining the reachable states in a h will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-634055