Hazard—Freedom Checking in Speed—Independent Systems

  • Husnu Yenigun
  • Vladimir Levin
  • Doron Peled
  • Peter A. Beerel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


We describe two approaches to use the model checking tool COSPAN to check the hazard freedom in speed—independent circuits. First, we propose a straight forward approach to implement a speed—independent circuit in S/R. Second, we propose a reduction technique over the first approach by restricting the original system with certain constraints. This reduction is implemented on the top of COSPAN which also applies its own reductions, including symbolic representation (BDD).


Model Check Selection Variable Boolean Function Independent System Reachable State 
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. 1.
    J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan and D. L. Dill, Symbolic model checking for sequential circuit verification, IEEE Transactions on CAD, Vol. 13, No.4, April 1994, pp. 401–424.Google Scholar
  2. 2.
    K. L. McMillan, A technique of state space search based on unfolding, Formal Methods in System Design, Vol. 6, pp. 45–65, 1995.zbMATHCrossRefGoogle Scholar
  3. 3.
    P. A. Beerel, J. R. Burch and T. H.-Y. Meng, Checking Combinational Equivalence of Speed-Independent Circuits, in Formal Methods on System Design, May 1998.Google Scholar
  4. 4.
    D. L. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, ACM Distinguished Dissertations, 1989.Google Scholar
  5. 5.
    R. P. Kurshan, Computer-aided verification of coordinating processes, Princeton University Press, Princeton, New Jersey, 1994.Google Scholar
  6. 6.
    D. Peled, Combining partial order reductions with on the fly model checking, 6th CAV, June 1994.Google Scholar
  7. 7.
    A. Valmari, A stubborn attack on state space explosion, 2nd CAV, 1990, pp. 25–42.Google Scholar
  8. 8.
    R. P. Kurshan, V. Levin, M. Minea, D. Peled and H. Yenigun, Static Partial Order Reduction, TACAS, 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Husnu Yenigun
    • 1
  • Vladimir Levin
    • 1
  • Doron Peled
    • 1
  • Peter A. Beerel
    • 2
  1. 1.Bell LaboratoriesMurray HillUSA
  2. 2.2 University of Southern CaliforniaLos AngelesUSA

Personalised recommendations