Verifying Transaction Ordering Properties in Unbounded Bus Networks through Combined Deductive/Algorithmic Methods

  • Michael Jones
  • Ganesh Gopalakrishnan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)


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.


Model Check Inference Rule Operational Semantic Reachable State Execution Trace 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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
  2. AL91.
    Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, May 1991.Google Scholar
  3. 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
  4. 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
  5. Cor96.
    Francisco Corella. Proposal to fix ordering problem in PCI 2.1, 1996. Accessed April 2000.
  6. 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
  7. DDP99.
    Satyaki Das, David L. Dill, and Seungjoon Park. Eperience with predicate abstruction. In Halbwachs and Peled [HP99].Google Scholar
  8. 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
  9. 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
  10. Jon00.
    Michael Jones. PCI transaction ordering case study., 2000.
  11. 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
  12. 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
  13. MHJG00.
    Abdel Mokkedem, Ravi Hosabettu, Michael D. Jones, and Ganesh Gopalakrishnan. Formalization and proof of a solution to the PCI 2.1 bus transaction ordering problem. Formal Methods in Systems Design, 16(1):93–119, January 2000.CrossRefGoogle Scholar
  14. PCI95. PCISIG. PCI Special Interest Group–PCI Local Bus Speci.cation, Revision 2.1, June 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Michael Jones
    • 1
  • Ganesh Gopalakrishnan
    • 1
  1. 1.University of UtahSalt Lake City

Personalised recommendations