A Specification Methodology by a Collection of Compact Properties as Applied to the Intel® Itanium™ Processor Bus Protocol
In practice, formal specifications are often considered too costly for the benefits they promise. Specifically, interface specifications such as standard bus protocol descriptions are still documented informally, and although many admit formal versions would be useful, they are dissuaded by the time and effort needed for development.
We champion a formal specification methodology that attacks this cost-value problem from two angles. First, the framework allows formal specifications to be feasible for signal-level bus protocols with minimal effort,lowering costs. And second, a specification written in this style has many different uses, other than as a precise specification document, resulting in increased value over cost. This methodology allows the specification to be easily transformed into an executable checker or an simulation environment, for example.
In an earlier paper, we demonstrated the methodology on a widely-used bus protocol. Now, we show that the generalized methodology can be applied to more advanced bus protocols, in particular, the Intel® Itanium™ Processor bus protocol. In addition, the paper outlines how writing and checking such a specification revealed interesting issues, such as deadlock and missed data phases, during the development of the protocol.
KeywordsModel Check Data Phase Trigger Condition Compact Property Core Subset
- [ABG+00]_Y. Abarbanel, I. Beer, L. Gluhovsky, S. Keidar, and Y. Wolfsthal. FoCs-Automatic Generation of Simulation Checkers from Formal Specification. In International Conference on Computer-Aided Verification, volume 1855 of Lecture Notes in Computer Science. Springer-Verlag, 2000.CrossRefGoogle Scholar
- [AS00]F. Aloul and K. Sakallah. Efficient Verification of the PCI Local Bus using Boolean Satisfiability. In International Workshop on Logic Synthesis (IWLS), 2000.Google Scholar
- [CCLW99]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
- [CE81]E.M. Clarke and E.A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs: Workshop, volume 131 of Lecture Notes in Computer Science, May 1981.Google Scholar
- [CGY+00]_E. Clarke, S. German, Y. Lu, H. Veith, and D. Wang. Executable Protocol Specification in ESL. In Proceedings of the Third International Conference of Formal Methods in Computer-Aided Design, November 2000.Google Scholar
- [Cor]Intel Corporation. Itanium Processor Bus Protocol Specification. Internal document.Google Scholar
- [GD00]Shankar G. Govindaraju and David L. Dill. Counterexample-guided choice of projections in approximate symbolic model checking. In Proceedings of International Conference on Computer-Aided Design, November 2000. San Jose, CA.Google Scholar
- [HCRP91]N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language lustre. Proceedings of the IEEE, 79(9):1305–1320, September 1991.Google Scholar
- [KMP98]M. Kaufmann, A. Martin, and C. Pixley. Design Constraints in Symbolic Model Checking. In International Conference on Computer-Aided Verification, 1998.Google Scholar
- [McM]Kenneth McMillan. http://www-cad.eecs.berkeley.edu/~kenmcmil/smv/.
- [MHG98]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, volume 1522 of Lecture Notes in Computer Science. Springer-Verlag, 1998.CrossRefGoogle Scholar
- [SDH00]Kanna Shimizu, David L. Dill, and Alan J. Hu. Monitor-Based Formal Specification of PCI. In Proceedings of the Third International Conference of Formal Methods in Computer-Aided Design, November 2000.Google Scholar
- [SIG95]PCI SIG. PCI Local Bus Specification, Revision 2.2, 12 1995.Google Scholar