Monitor-Based Formal Specification of PCI
Bus protocols are hard to specify correctly, and yet it is often critical and highly beneficial that their specifications are correct, complete, and unambiguous. The informal specifications currently in use are not adequate because they are dificult to read and write, and cannot be functionally verified by automated tools. Formal specifications, promise to eliminate these problems, but in practice, the dificulty of writing them limits their widespread acceptance. This paper presents a new style of specification based on writing the interface specification as a formal monitor, which enables the formal specification to be simple to write, and even allows the description to be written in existing HDLs. Despite the simplicity, monitor specifications can be used to specify industry-grade protocols. Furthermore, they can be checked automatically for internal consistency using standard model checker tools, without any protocol implementations. They can be used without modification for several other purposes, such as formal verification and system simulation of implementations. Additionally, it is proved that specifications written in this style are receptive, guaranteeing that implementations are possible. The effectiveness of the monitor specification is demonstrated by formally specifying a large subset of the PCI 2.2 standard and finding several bugs in the standard.
KeywordsModel Check Reachable State Symbolic Model Check Linear Time Temporal Logic Speci Cation
Unable to display preview. Download preview PDF.
- 1.M. Kaufmann, A. Martin, and C. Pixley. “Design Constraints in Symbolic Model Checking” in International Conference on Computer-Aided Verification, 1998.Google Scholar
- 2.PCI Special Interest Group. PCI Local Bus Specification, Revision 2.2, December 18 1995.Google Scholar
- 3.J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. “Sequential circuit verification using symbolic model checking” in Proceedings of the 27th ACM/IEEE Design Automation Conference, 1990.Google Scholar
- 5.P. Chauhan, E. M. Clarke, Y. Lu and D. Wang. “Verifying IP-Core based System-On-Chip Designs” in Proceedings of the IEEE ASIC conference, September 1999.Google Scholar
- 6.E. M. Clarke and E.A. Emerson. “Synthesis of synchronization skeletons for branching time temporal logic” in Logic of Programs: Workshop, Yorktown Heights, NY, May 1981 Lecture Notes in Computer Science, vol. 131, Springer-Verlag. 1981.Google Scholar
- 8.A. Mokkedem, R. Hosabettu, and G. Gopalakrishnan. “Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem” in Proceedings of the Second International Conference, Formal Methods in Computer-Aided Design, 1998. Lecture Notes in Computer Science, vol. 1522, Springer-Verlag.Google Scholar
- 9.D. L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits, MIT Press, 1989.Google Scholar
- 10.G. S. Govindaraju and D. L. Dill. “Counterexample-guided Choice of Projections in Approximate Symbolic Model Checking” in Proceedings of IEEE International Conference on Computer Aided Design (ICCAD), 2000. (under review).Google Scholar
- 11.R. E. Bryant, P. Chauhan, E. M. Clarke, and A. Goel. “A Theory of Consistency for Modular Synchronous Systems” in Proceedings of the Third International Conference, Formal Methods in Computer-Aided Design, 2000. (under review).Google Scholar
- 12.E. M. Clarke, Y. Lu, H. Veith, D. Wang, and S. German. “Executable Protocol Specification in ESL” in Proceedings of the Third International Conference, Formal Methods in Computer-Aided Design, 2000. (under review).Google Scholar