Verifying hardware in its software context

ABSTRACT

We describe a method for verifying hardware whose correct behavior depends upon its software interface. It is presumed that the hardware is presented as a synchronous RTL model whereas the software is presented as an asynchronous abstraction. Our methodology incorporates partial order reduction on the software side, and localization reduction, to deal with the computational complexity of the verification. The partial order reduction is implemented as a constraint on the transition relation of a synchronous transformation of the software model. The reduced transformed model then may be verified using a verification algorithm whose scope is purely synchronous models, without modification. Thus, independent of the interface verification problem, this gives a general method for combining partial order reduction with symbolic model-checking.

REFERENCES

• 1: Rajeev Alur , Robert K. Brayton , Thomas A. Henzinger , Shaz Qadeer , Sriram K. Rajamani, Partial-Order Reduction in Symbolic State Space Exploration, Proceedings of the 9th International Conference on Computer Aided Verification, p.340-351, June 22-25, 1997
• 2: O. Basbu~o~lu, K. inan, Compiling SDL into the finite state specification language COSPAN. Proceedings of the Tenth International Symposium on Computer and Information Scienees(ISCIS X), Kusadasl, Turkey, 1995.
• 3: Patrice Godefroid , Pierre Wolper, A partial approach to model checking, Papers presented at the IEEE symposium on Logic in computer science, p.305-326, May 1994, Amsterdam, The Netherlands
• 4: R. H. Hardin, Z. Har'E1, R. P. Kurshan, COSPAN, Conference on Computer Aided Verification (CA V 96), LNCS 1102, Springer-Verlag, (1996) pp 423- 427.
• 5: Z. Har'E1, R. P. Kurshan, Software for Analytical Development of Communication Protocols, AT&T Tech. J. 69 (1) (1990), pp 45- 59.
• 6: Gerard J. Holzmann , Doron Peled, An improvement in formal verification, Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, p.197-211, January 1995
• 7: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 8: R. P. Kurshan, Formal verification in a commercial setting, Proceedings of the 34th annual conference on Design automation, p.258-262, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266089]
• 9: Robert P. Kurshan , Michael Merritt , Ariel Orda , Sonia R. Sachs, Modelling Asynchrony with a Synchronous Model, Proceedings of the 7th International Conference on Computer Aided Verification, p.339-352, July 03-05, 1995
• 10: V. Levin, E. Bounimova, O. Basbu~;o~;lu and K. Inan, A Verifiable Software/Hardware Codesign Using SDL and COSPAN, Proceedings of the COST 2~7 International Workshop on Applied Formal Methods In System Design, Maribor, Slovenia, 1996, pp 6-16.
• 11: D. Peled. Combining partial order reductions with on-the-fly model-checking. Formal Methods in System Design 8 (1996), pp 39-64.
• 12: Functional Specification and Description Language (SDL), CCITT Blue Book, Recommendation Z. 100, Geneva, 1992.
• 13: Antti Valmari, Stubborn sets for reduced state generation, Proceedings on Advances in Petri nets 1990, p.491-515, March 1991

INDEX TERMS

Primary Classification:
  J. Computer Applications

Additional Classification:
  C. Computer Systems Organization
  C.0 GENERAL
      Subjects: Hardware/software interfaces
  C.2 COMPUTER-COMMUNICATION NETWORKS

  D. Software
  D.3 PROGRAMMING LANGUAGES

General Terms:
Algorithms, Design, Languages, Performance, Theory, Verification

Keywords:
verification, formal verification, model-checking, partial order reduction, localization reduction, co-verification, co-design, stepwise refinement