Verifying Transaction Ordering Properties in Unbounded Bus Networks through Combined Deductive/Algorithmic Methods
Previously [MHG98,MHJG00], we reported our efforts to verify the producer/consumer transaction ordering property for the PCI 2.1 protocol extended with local master IDs. Although our efforts were met with some success, we were unable to show that all execution traces of all acyclic PCI networks satisfy this transaction ordering property. In this paper, we present a veri.cation technique based on network symmetry classes along with a manually derived abstraction that allows us to show, at the bus/bridge level, that all execution traces of all acyclic PCI networks satisfy the transaction ordering property. This now completed case study (modulo the validity of the axioms used to characterized the abstraction) suggests several avenues for further work in combining model-checking (algorithmic methods) and theorem-proving (deductive methods) in judicious ways to solve infinite-state verification problems at the bus/interconnect level. It is a concrete illustration of partitioning concerns where designers can specify bus protocols in an operational semantics (rule-based) style, invent abstractions, and carry out finite-state model-checking while verification experts can establish formal properties of the abstraction.
KeywordsModel Check Inference Rule Operational Semantic Reachable State Execution Trace
Unable to display preview. Download preview PDF.
- AAB+99.P. A. Abdulla, A. Annichini, S. Bensalem, A. Bouajjani, P. Habermehl, and Y. Lakhench. Verification of infinite-state systems by combining abstraction and reachability analysis. In Halbwachs and Peled [HP99].Google Scholar
- AL91.Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, May 1991.Google Scholar
- BOG00.Karthikeyan Bhargavan, Davor Obradovic, and Carl A. Gunter. Routing information protocol in HOL/SPIN. In Theorem Provers in Higher-Order Logics 2000: TPHOLs00, August 2000.Google Scholar
- CJLW99.Edmund Clarke, Somesh Jha, Yuan Lu, and Dong Wang. Abstract BDDs: A technique for using abstraction in model checking. In Laurence Pierre and Thomas Kropf, editors, Correct Hardware Design and Verification Methods, CHARME’99, volume 1703 of Lecture Notes in Computer Science, Bad Herrenalb, Germany, September 1999. Springer-Verlag.Google Scholar
- Cor96.Francisco Corella. Proposal to fix ordering problem in PCI 2.1, 1996. Accessed April 2000. http://www.pcisig.com/reflector/thrd8.html#00706.
- CSZ97.Francisco Corella, Robert Shaw, and Cui Zhang. A formal proof of absence of deadlock for any acyclic network of PCI buses. In Computer Hardware Description Languages, CHDL’97, Toledo, Spain, April 1997.Google Scholar
- DDP99.Satyaki Das, David L. Dill, and Seungjoon Park. Eperience with predicate abstruction. In Halbwachs and Peled [HP99].Google Scholar
- HP99.Nicolas Halbwachs and Doron Peled, editors. Computer-Aided Verification, CAV’99, volume 1633 of Lecture Notes in Computer Science, Trento, Italy, July 1999. Springer-Verlag.Google Scholar
- ID96.C. Norris Ip and David L. Dill. Verifying systems with repplicated components in Murø. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV’96, volume 1102 of Lecture Notes in Computer Science, pages 147–158, New Brunswick, NJ, July/August 1996. Springer-Verlag.Google Scholar
- Jon00.Michael Jones. PCI transaction ordering case study. http://www.cs.utah.edu/~mjones/pci-pvs.html, 2000.
- KMM+97.Y. Kesten, O. Maler, M. Marcus, A Pnueli, and E. Shahar. symbolic model checking with rich assertional languages. In Orna Grumburg, editor, Computer-Aided Verification, CAV’97, volume 1254 of Lecture Notes in Computer Science, Haifa, Israel, June 1997. Springer-Verlag.Google Scholar
- MHG98.Abdel Mokkedem, Ravi Hosabettu, and Ganesh6Gopalakrishnan. Formalization and proof of a solution to the PCI 2.1 bus transaction ordering problem. In Ganesh Gopalakrishnan and Phillip Windley, editors, Formal Methods in Computer-Aided Design, FMCAD’ 98, volume 1522 of Lecture Notes in Computer Science. Springer-Verlag, November 1998.Google Scholar
- PCI95. PCISIG. PCI Special Interest Group–PCI Local Bus Speci.cation, Revision 2.1, June 1995.Google Scholar