Liveness vs Safety – A Practical Viewpoint
- 746 Downloads
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.
KeywordsSafety Property Formal Verification Practical Viewpoint Liveness Property Forward Progress
Unable to display preview. Download preview PDF.
- 1.Lamport, L.: Proving the Correctness of Multiprocess Programs. IEEE Transactions on Software Engineering SE-3(2) (March 1977)Google Scholar
- 2.Liveness Manifestoes. In: Beyond Safety International Workshop, Schloss Ringberg, Germany (April 2004), http://cs.nyu.edu/acsys/brond-safety/
- 3.Biere, A., Artho, C., Schuppan, V.: Liveness Checking as Safety Checking. Electronic Notes in Theoretical Computer Science 66(2) (2002)Google Scholar
- 4.Shreedar, M., Varghese, G.: Efficient Fair Queing using Deficit Round Robin. IEEE/ACM Trans. Networking 4(3) (June 1996)Google Scholar
- 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.Incisive Formal Verifier User Guide, Cadence Design SystemsGoogle Scholar
- 7.IEEE Standard for System Verilog – Unified Hardware Design, Specification and Verfication Language, IEEE Standards Board (November 2005)Google Scholar
- 8.Bryant, R.E.: Graph Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35(8) (1986)Google Scholar
- 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.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.Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: Proc. FMCAD (2007)Google Scholar