Data processing: structural design – modeling – simulation – and em – Simulating electronic device or electrical system – Circuit simulation
Patent
1998-02-26
2000-10-31
Teska, Kevin J.
Data processing: structural design, modeling, simulation, and em
Simulating electronic device or electrical system
Circuit simulation
703 2, 703 27, 716 4, G06F 1750
Patent
active
061416339
ABSTRACT:
A verification apparatus which verifies whether or not a finite state machine indicating the operation of a synchronous sequential machine satisfies the property indicating the functional specification repeats the image computation in the M and the computation of a set product by q starting with the state set p when the finite state machine M, the subset q of the state of the M, and the subset p of the q are given; and checks the relation of the state set of the computation process. As a result, it can be determined, starting with a certain state in the p, whether or not a state transition path which eternally does not exceed the q exists.
REFERENCES:
patent: 5680332 (1997-10-01), Raimi et al.
T. Nakata, et al., "Improving Quality of Simulation-Based Verification Using State Enumeration"; Fujitsu Scientific & Tech. Journal, No. 2, pp. 135-142.
J. Burch, et al., "Symbolic Model Checking Sequential Circuit Verification", IEEE Transation on Computer-Aided Design of Integrated Circuits & Systems, No. 4, pp. 401-424.
H. Iwashita, et al., "CTL Model Checking Based on Forward State Traversal", IEEE, pp. 82-87.
Hyunwoo Cho, et al, "Alogrithms for Approximate FSM Traversal Based on State Space Decomposition", Design of Integrated Circuits and Systems, vol. 15, No. 12, pp. 1465-1478.
H. Iwashita, et al., "Forward Model Checking Techniques Oriented to Buggy Designs", IEEE, pp. 400-404.
H. Iwashita, et al.; "Automatic Test Program Generation For Pipelined Processors"; In Proceedings of the International Conference on Computer-Aided Design 1994; pp. 580-583.
K. Ravi, et al.; "High-Density Teachability Analysis"; In Proceedings of the International Conference on Computer-Aided Design 1995; pp. 154-158.
J.R. Burch, et al.; "Sequential Circuit Verification Using Symbolic Model Checking"; Proc. 27.sup.th DAC 1990; pp. 45-51.
H. Iwashita, et al.; "CLT Model Checking Based On Forward State Traversal"; IEEE/ACM International Conference on Computer-Aided Design 1996; pp. 882-87.
E.M. Clarke, et al.; "Efficient Generation of Countexamples And Witnesses In Symbolic Model Checking"; 32.sup.nd ACM/IEEE Design Automation Conference 1995; pp. 1-6.
Randal E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation", Transactions On Computers, vol. C-35, No. 8, Aug. 1996, pp. 677-691.
E. M. Clarke et al., "Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications", ACM Transactions on Programming Languages and Systems, vol. 8, No. 2, Apr. 1986 pp. 244-263.
Fujita et al., "Example of application to actual design of formal verification method", 1994, pp. 719-725.
Fujita et al., "Application of BDD to CAD", 1993, pp. 610-611.
Hiraishi et al., "Formal Verification Method Based on Logical Function Process", 1994, pp. 710-718.
Minato, "BDD Process Technology Through Computer", 1993, pp. 593-599.
Ishiura, "Whats BDD?", 1993, pp. 585-592.
Kimura, "Formal Timing Verification", 1994, pp. 726-735.
Yosinori Watanabe et al., "Applications of Binary Decision Diagrams", May 1993, pp. 600-608.
Iwashita Hiroaki
Nakata Tsuneo
Broda Samuel
Fujitsu Limited
Teska Kevin J.
LandOfFree
Logical device verification method and apparatus does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Logical device verification method and apparatus, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Logical device verification method and apparatus will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2064551