Formal Verification of Digital Systems
Author: 
G. SwamyAuthors Info & Claims
Abstract
A formal verifier is an automated decision procedure that can prove or disprove a set of statements in some logical system of reasoning. Problems informal verification have been posed and studied in a variety of disciplines for many years. However the last ten years have produced significant advances in both the theory and practical art of building formal verifiers. Various formal proof techniques available today include language containment, model checking, equivalence checking, symbolic simulation and theorem proving. In this tutorial, we will be restricting ourselves to the formal finite state machine based techniques: language containment, model checking and equivalence checking. A brief introduction to the technologies that underly these techniques will be presented as well. The tutorial will conclude with some examples of how formal methods can be employed in the verification of hardware systems.
References
[1]
S. B. Akers. Binary Decision Diagrams. IEEE Trans. Comput., C-37:509-516, June 1978.
[2]
A. Aziz, S. Tasiran, and R. K. Brayton. A Communication Complexity Based Approach to BDD Variable Ordering for systems of Interacting Finite State Machines. In Workshop Notes of the Intl. Workshop on Logic Synthesis, Tahoe City, CA, May 1993.
[3]
D. Brand. Verification of Large Synthesized Designs. In Proc. Intl. Conf. on Computer-Aided Design, pages 534- 537, Nov. 1993.
[4]
R. K. Brayton et al. VIS: A System for Verification and Synthesis. In Proc. of the Conf. on Computer-Aided Verification, pages 428-432, 1996.
[5]
M. A. Breuer and A. D. Friedman. Diagnosis and Reliable Design of Digital Systems. Computer Science Press, 1976.
[6]
R. Bryant. Graph-based Algorithms for Boolean Function Manipulation. IEEE Trans. Comput., C-35:677-691, Aug. 1986.
[7]
R. E. Bryant, D. L. Beatty, and C.-J. H. Seger. Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation. In Proc. of the Design Automation Conf., pages 397- 402, June 1991.
[8]
J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Symbolic Model Checking: 1020 States and Beyond. Information and Computation, 98(2): 142-170, 1992.
[9]
H. Cho, S.-w. Jeong, F. Somenzi, and C. Pixley. Synchronizing Sequences and Symbolic Traversal Techniques in Test Generation. Journal of Electronic Testing: Theory and Applications, 4(12):19-31, 1993.
[10]
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. Prog. Lang. Syst., 8(2):244-263, 1986.
[11]
O. Coudert and J. C. Madre. A Unified Framework for the Formal Verification of Sequential Circuits. In Proc. Intl. Conf. on Computer-Aided Design, pages 126-129, Nov. 1990.
[12]
D. Dill. The Murphy Verification System. In Proc. of the Conf. on Computer-Aided Verification, pages 390-393, 1996.
[13]
E. Clarke and O. Grumberg and K. McMillan and X. Zhao. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proc. of the Design Automation Conf., pages 454-459, June 1995.
[14]
E. A. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Formal Models and Semantics, volume B of Handbook of Theoretical Computer Science, pages 996- 1072. Elsevier Science, 1990.
[15]
E. A. Emerson and C. L. Lei. Modalities for Model Checking: Branching Time Strikes Back. In Proc. ACM Symposium on Principles of Programming Languages, pages 84-96, 1985.
[16]
Z. Har'El and R. P. Kurshan. Software for Analytical Development of Communication Protocols. AT&T Technical Journal, pages 45-59, Jan. 1990.
[17]
G. Holzmann and D. Pe1ed. The State of Spin. In Proc. of the Conf. on Computer-Aided Verification, pages 385-389, 1996.
[18]
J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979.
[19]
R. P. Kurshan. Automata-Theoretic Verification of Coordinating Processes. Princeton University Press, 1993.
[20]
W. Lee, A. Pardo, J. Jang, G. Hachtel, and F. Somenzi. Tearing Based Automatic Abstraction for CTL Model Checking. In Proc. Intl. Conf. on Computer-Aided Design, page To appear, 1996.
[21]
S. Malik, A. R. Wang, R. K. Brayton, and A. Sangiovanni-Vincentelli. Logic Verification using Binary Decision Diagrams in a Logic Synthesis Environment. In Proc. Intl. Conf. on Computer-Aided Design, pages 6-9, Nov. 1988.
[22]
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
[23]
C. Mead and L. Conway. Introduction to VLSI systems. Addison-Wesley, 1980.
[24]
R. Brayton et al. HSIS: A BDD-Based Environment for Formal Verification. In Proc. of the Design Automation Conf., pages 454-459, June 1994.
[25]
R. K. Ranjan, A. Aziz, R. K. Brayton, B. Plessier, and C. Pixley. Efficient formal design verification data structure and algorithms. Technical Report UCB/ERL M94/100, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, Oct. 1994.
[26]
R. Rudell. Dynamic Variable Ordering for Binary Decision Diagrams. In Proc. Intl. Conf. on Computer-Aided Design, pages42-47, Nov. 1993.
[27]
The VIS Group. VIS: Verification Interacting with Synthesis. http://www-cad.eecs.berkeley.edu/Respep/Research/vis.
[28]
The VIS Group. VIS: A System for Verification and Synthesis. Technical Report UCB/ERL M95/104, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, 1995.
[29]
W. Thomas. Automata on Infinite Objects. In J. van Leeuwen, editor, Formal Models and Semantics, volume B of Handbook of Theoretical Computer Science, pages 133-191. Elsevier Science, 1990.
[30]
H. Touati, R. K. Brayton, and R. P. Kurshan. Checking Language Containment using BDDs. In Proc. of Intl. Workshop on Formal Methods in VLSI Design, Miami, FL, Jan. 1990.
[31]
H. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. Implicit State Enumeration of Finite State Machines using BDD's. In Proc. Intl. Conf. on Computer-Aided Design, pages 130-133, Nov. 1990.
[32]
J. van Leeuwen, editor. Handbook of Theoretical Computer Science, volume B. Elsevier Science, 1990.
[33]
M. Y. Vardi and P. L. Wolper. An Automata-Theoretic Approach to Program Verification. In Proc. IEEE Symposium on Logic in Computer Science, pages 332-334, 1986.
Index Terms
- Formal Verification of Digital Systems
Recommendations
Formal verification in hardware design: a survey
In recent years, formal methods have emerged as an alternative approach to ensuring the quality and correctness of hardware designs, overcoming some of the limitations of traditional validation techniques such as simulation and testing.
There are two ...
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Survey on Formal Verification Methods for Digital IC
ICICSE '09: Proceedings of the 2009 Fourth International Conference on Internet Computing for Science and EngineeringThis paper presents a survey of the state-of-art of formal verification technique. The expression models for formal verification are introduced and analyzed. The characteristics of each model are expounded. Moreover, the typical model checking ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 1997
ISBN:0818677554
Copyright © Copyright (c) 1997 Institute of Electrical and Electronics Engineers, Inc. All rights reserved.
Publisher
IEEE Computer Society
United States
Publication History
Published: 04 January 1997
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 20 Nov 2024