Advertisement

A Theory of Consistency for Modular Synchronous Systems

  • Randal E. Bryant
  • Pankaj Chauhan
  • Edmund M. Clarke
  • Amit Goel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)

Abstract

We propose a model for modular synchronous systems with combinational dependencies and define consistency using this model. We then show how to derive this model from a modular specification where individual modules are specified as Kripke Structures and give an algorithm to check the system for consistency. We have implemented this algorithm symbolically using BDDs in a tool, SpecCheck. We have used this tool to check an example bus protocol derived from an industrial specification. The counterexamples obtained for this protocol highlight the need for consistency checking.

Keywords

Model Check Observable State Linear Temporal Logic Atomic Proposition Kripke Structure 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    R. Alur and T.A. Henzinger. “Reactive modules.” In Proceedings of the 11th IEEE Symposium on Logic in Computer Science, pp. 207–218. 1996.Google Scholar
  2. 2.
    G. Berry, G. Gonthier. “The synchronous programming language Esterel: Design, semantics, implementation.” Technical Report 842, INRIA. 1988.Google Scholar
  3. 3.
    R. E. Bryant. “Graph-based algorithms for boolean function manipulation.” IEEE Transactions on Computers, C-35(8), pp. 677–691. 1986.CrossRefGoogle Scholar
  4. 4.
    P. Chauhan, E. Clarke, Y. Lu, D. Wang. “Verifying IP-Core based System-On-Chip designs.” In Proceedings of the IEEE ASIC/SOC Conference, pp. 27–31. 1999.Google Scholar
  5. 5.
    E. Clarke, O. Grumberg. H. Hamaguchi. “Another look at LTL model checking.” Formal Methods in System Design, 10, pp. 47–71. 1997.CrossRefGoogle Scholar
  6. 6.
    E. Clarke, O. Grumberg, D. Peled. Model Checking. MIT Press. 1999.Google Scholar
  7. 7.
    E. Clarke, Y. Lu, H. Veith, D. Wang, S. German. “Executable Protocol Specification in ESL.” Formal Methods in Computer-Aided Design (FMCAD’00). 2000.Google Scholar
  8. 8.
    D.L. Dill. Trace theory for automatic hierarchical verification of speed-independent circuits. ACM Distinguished Dissertations. MIT Press, 1989.Google Scholar
  9. 9.
    A. Goel, W. R. Lee. “Formal Verification of an IBM CoreConnect Processor Local Bus Arbiter Core.” 37th ACM/IEEE Design Automation Conference. 2000.Google Scholar
  10. 10.
    D. E. Long. “Model Checking, Abstraction and Compositional Reasoning.” PhD Thesis, Carnegie Mellon University, 1993.Google Scholar
  11. 11.
    Milner, Tofte, Harper, MacQueen. The Definition of Standard ML. MIT Press, 1997.Google Scholar
  12. 12.
    K. Shimizu, D. L. Dill, A. J. Hu. “Monitor-Based Formal Specification.” Formal Methods in Computer Aided Design (FMCAD’00). 2000.Google Scholar
  13. 13.
    K. F. Larsen, J. Lichtenberg. MuDDy. Version 1.7. http://www.itu.dk/research/muddy.
  14. 14.
    J. L. Nielsen. BuDDy–A Binary Decision Diagram Package. Version 1.7. http://www.itu.dk/research/buddy.
  15. 15.
    S. Romanenko, P Sestoft. Moscow ML. Version 1.44. http://www.dina.dk/~sestoft/mosml.html.

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Randal E. Bryant
    • 1
  • Pankaj Chauhan
    • 1
  • Edmund M. Clarke
    • 1
  • Amit Goel
    • 2
  1. 1.Computer Science DepartmentCarnegie Mellon UniversityPittsburghUSA
  2. 2.Electrical and Computer Engineering DepartmentCarnegie Mellon UniversityPittsburghUSA

Personalised recommendations