Automatic design verification

Details Automatic design verification Automatic design verification

1993-06-02

1995-11-07

Trans, Vincent N.

Boots, shoes, and leggings

364578, G06F 1750

Patent

active

054652162

ABSTRACT:
Methods and apparatus for formal verification. In one embodiment, values within a full model for formal verification are parameterized so that the parameters may be defined in order to perform verification on a reduced model. The number of states may then be reduced to allow formal verification on portions of a logic model of complex circuits such as microprocessors using present formal verification techniques. Preprocessor directives are used for multiple and conditional hardware description language generation for representation of a logic model of an integrated circuit, such as a microprocessor. Signals may also be freed from their associated circuitry, and placed into a non-deterministic state. Signals may also be set to a deterministic, designer-specified value. Associated circuitry may then be removed from the logic model for verification of a reduced model. Circuitry specified as "blocks" may also be entirely removed from the model, and all associated circuitry used as inputs to the removed blocks and associated signals may also be removed. Any of these are performed using pre-processor directives. A reduced logic model of a full logic model may then be generated which is used for formal verification.

REFERENCES:
patent: 4922432 (1990-05-01), Kobayashi et al.
patent: 5146583 (1992-09-01), Matsunaka et al.
patent: 5163016 (1992-11-01), Har' El et al.
patent: 5247468 (1993-09-01), Henrichs et al.
patent: 5278769 (1994-01-01), Bair et al.
patent: 5282146 (1994-01-01), Aihara et al.
patent: 5359537 (1994-10-01), Saucier et al.
E. M. Clarke, J. R. Burch, O. Grumberg, D. E. Long and K. L. McMillan; Automatic verification of sequential circuit designs; pp. 105-120 of notes from conference entitled; Mechanized Reasoning and Hardware Design, Published by Prentice Hall, Hemel Hempstead, UK 1992.
E. M. Clarke, D. E. Long and K. L. McMillan; Compositional Model Checking; pp. 353-362 of notes from conference entitled: Proceedings. Fourth Annual Symposium on Logic in Computer Science, Published by IEEE Comput. Soc. Press, Washington, DC 1989.
Z. Har'El and R. P. Kurshan; Software For Analysis of Coordination; pp. 382-385 of notes from conference entitled: Proceedings of International Conference on Systems, Science and Engineering, Published by Int. Acad. Publishers, Beijing, China 1988.
J. R. Burch, E. M. Clarke, and K. L. McMillan; Symbolic Model Checking: 10.sup.20 States and Beyond; pp. 142-170 of Journal: vol. 98, Information and Computation, No. 2, Published by Academic Press, USA 1992.
P. J. Brumfitt; MetaMorph-a formal methods toolkit with application to the design of digital hardware; pp. 437-473 of Journal: vol. 2, Journal of Functional Programming, pt. 4, Published by Cambridge Univ. Press, UK Oct. 1992.
Bill Brykczynski, David A. Wheeler; An Annotated Bibliography on Software Inspections; pp. 81-88 of vol. 18, SIGSOFT-Software Engineering Notes, No. 1, Published by ACM SIGSOFT, USA Jan. 1993.
E. M. Clarke, D. E. Long and K. L. McMillan; A Language for Compositional Specification and Verification of Finite State Hardware Controllers; pp. 281-295 of Journal: Computer Hardware Description Languages and their Applications, Published by Elsevier Science Publishers V. V. (North-Holland) 1990.
R. P. Kurshan, Member, IEEE; and K. L. McMillan; Analysis of Digital Circuits Through Symbolic Recuction; pp. 1356-1371 of Journal: vol. 10, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, No. 11, Published in USA Nov. 1991.
Janaki Akella and Kenneth McMillan: Synthesizing Converters between Finite State Protocols; pp. 410-413 of notes from conference entitled: International Conference on Computer Design: VLSI in Computers and Processors, Published in USA 1991.
B. Billard; Improving Verification Tools; pp. 248-256 of Journal: vol. 12, Journal of Electrical and Electronics Engineering, No. 3, Published in Australia Sep. 1992.

Affiliated with

Also associated with

Rating

Automatic design verification does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Automatic design verification, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Automatic design verification will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-200844