Establishing PCI compliance using formal verification: a case study
- 19 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 373-377
- https://doi.org/10.1109/pccc.1995.472466
Abstract
This paper presents a case study in the practical application of formal verification. Specifically, we describe our experience in applying the formal verification technique of symbolic model checking to the verification of PCI bus bridges. During the last 2 years, we have used symbolic model checking to verify more than 12 hardware designs, including a number of PCI bus bridges. This use of formal verification has led to the better understanding of formal verification capabilities and the establishment of formal verification techniques as a standard verification tool in the Haifa Design Group at IBM's Haifa Research Laboratory. More than 5 PCI bus bridge designs have been verified using formal verification, including a design in which formal verification was used to do all checks at the unit level. A PCI bus bridge design that was verified with formal verification was announced as an IBM product and became available to customers after a single tape-out.Keywords
This publication has 5 references indexed in Scilit:
- Methodology and system for practical formal verification of reactive hardwarePublished by Springer Nature ,1994
- Symbolic Model CheckingPublished by Springer Nature ,1993
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- Automatic verification of finite state concurrent system using temporal logic specificationsPublished by Association for Computing Machinery (ACM) ,1983
- Program proving: CoroutinesActa Informatica, 1973