Advertisement

Liveness vs Safety – A Practical Viewpoint

  • B. A. Krishna
  • Jonathan Michelson
  • Vigyan Singhal
  • Alok Jain
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7261)

Abstract

Within the formal verification community, choosing between liveness and safety approaches has long been a subject of debate. This paper applies both approaches to a common design in the networking industry, a Deficit Weighted Round Robin (DWRR) arbiter. It then presents the tradeoffs we encountered while applying both approaches and also describes how we overcame state space explosion. We also describe two real post-silicon design bugs that we found, which were missed by all simulation methods.

Keywords

Safety Property Formal Verification Practical Viewpoint Liveness Property Forward Progress 
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.
    Lamport, L.: Proving the Correctness of Multiprocess Programs. IEEE Transactions on Software Engineering SE-3(2) (March 1977)Google Scholar
  2. 2.
    Liveness Manifestoes. In: Beyond Safety International Workshop, Schloss Ringberg, Germany (April 2004), http://cs.nyu.edu/acsys/brond-safety/
  3. 3.
    Biere, A., Artho, C., Schuppan, V.: Liveness Checking as Safety Checking. Electronic Notes in Theoretical Computer Science 66(2) (2002)Google Scholar
  4. 4.
    Shreedar, M., Varghese, G.: Efficient Fair Queing using Deficit Round Robin. IEEE/ACM Trans. Networking 4(3) (June 1996)Google Scholar
  5. 5.
    Manna, Z., Pnueli, A.: Adequate proof principles for invariance and liveness properties of concurrent programs. Science of Computer Programming 4(3) (December 1984)Google Scholar
  6. 6.
    Incisive Formal Verifier User Guide, Cadence Design SystemsGoogle Scholar
  7. 7.
    IEEE Standard for System Verilog – Unified Hardware Design, Specification and Verfication Language, IEEE Standards Board (November 2005)Google Scholar
  8. 8.
    Bryant, R.E.: Graph Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35(8) (1986)Google Scholar
  9. 9.
    Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, M.: Chaff: Engineering an Efficient SAT solver. In: Proceedings of the 38th Design Automaton Conference (2001)Google Scholar
  10. 10.
    Emerson, E.A., Lei, C.L.: Efficient Model Checking in Fragments of the Proposition Mu-Calculus. In: Proceedings of the 1st Symposium on Logic in Computer Science (1986)Google Scholar
  11. 11.
    Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: Proc. FMCAD (2007)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • B. A. Krishna
    • 1
  • Jonathan Michelson
    • 2
  • Vigyan Singhal
    • 3
  • Alok Jain
    • 4
  1. 1.Chelsio CommunicationsIndia
  2. 2.NVIDIAUSA
  3. 3.Oski TechnologyUSA
  4. 4.Cadence Design SystemsUSA

Personalised recommendations