STARI: A case study in compositional and hierarchical timing verification

  • Serdar Taşiran
  • Robert K. Brayton
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


In [TAKB96], we investigated techniques for checking if one real-time system correctly implements another and developed theory for hierarchical proofs and assume-guarantee style reasoning. In this study, using the techniques of [TAKB96], we verify the correctness of the timing of the communication chip STARI.


Abstract Model Clock Signal Timing Verification Gate Level Refinement Check 
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.


  1. [AHV93]
    R. Alur, T.A. Henzinger, M.Y. Vardi. Parametric real-time reasoning. In Proceedings of the 25th ACM Symposium on Theory of Computing, pp. 592–601, 1993.Google Scholar
  2. [AK96]
    R. Alur and R.P. Kurshan. Timing analysis in COSPAN. In Hybrid Systems III, Lecture Notes in Computer Science. Springer-Verlag, 1996.Google Scholar
  3. [G93]
    M. R. Greenstreet STARI: A Technique for High-Bandwidth Communication. PhD thesis, Princeton University, 1993.Google Scholar
  4. [G96]
    M. R. Greenstreet STARI: Skew Tolerant Communication. Unpublished manuscript.Google Scholar
  5. [HBAB93]
    H. Hulgaard, S. M. Burns, T. Amon, and G. Borriello Practical Applications of an Efficient Time Separation of Events Algorithm In Digest of Technical Papers of the 1993 IEEE Intl. Conf. on Computer-Aided Design, November 1993.Google Scholar
  6. [LG95]
    C. Leung, M. Greenstreet A Simple Proof Checker for Timing Verification. In ACM Intl. Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, pages 294–305, November 1995.Google Scholar
  7. [MP95]
    O. Maler, A. Pnueli Timing Analysis of Asynchronous Circuits Using Timed Automata In ACM Intl. Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, pages 249–257, November 1995.Google Scholar
  8. [TAKB96]
    S. Taşiran, R. Alur, R. P. Kurshan, and R. K. Brayton Verifying Abstractions of Timed Systems. In Proc. of the 7th Intl. Conf. on Concurrency Theory, CONCUR '96, LNCS 1119, pages 546–562, Springer-Verlag, 1996.Google Scholar
  9. [W3] Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Serdar Taşiran
    • 1
  • Robert K. Brayton
    • 1
  1. 1.Department of Electrical Engineering and Computer SciencesUniversity of California at BerkeleyUSA

Personalised recommendations