Semi-formal Verification of Memory Systems by Symbolic Simulation

  • Husam Abu-Haimed
  • Sergey Berezin
  • David L. Dill
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2860)


We propose a debugging method for data-path intensive systems, in particular, memory systems. The approach is based on strengthening invariants by deriving constraints on data in the design using symbolic simulation with constrained inputs. A new heuristic is introduced for finding the appropriate input constraints for the symbolic simulation. We give up soundness in order to gain more automation and efficiency, minimizing or even eliminating the required manual effort. While it is no longer possible to prove the correctness of the design, experimental results demonstrate that the technique is quite effective in finding design errors.


Model Check Memory System Main Memory Safety Property Design Error 
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.
    Abu-Haimed, H., Berezin, S., Dill, D.L.: Strengthening invariants by symbolic consistency testing. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 407–419. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  2. 2.
    Bensalem, S., Lakhnech, Y., Saidi, H.: Powerful techniques for the automatic generation of invariants. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, Springer, Heidelberg (1996)Google Scholar
  3. 3.
    Bjørner, N., Browne, A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theoretical Computer Science (1997)Google Scholar
  4. 4.
    Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, Springer, Heidelberg (1994)Google Scholar
  5. 5.
    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986)zbMATHCrossRefGoogle Scholar
  6. 6.
    Colon, M., Uribe, T.E.: Generating finite-state abstractions of reactive systems using decision procedures. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, Springer, Heidelberg (1998)CrossRefGoogle Scholar
  7. 7.
    Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. 8.
    Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)Google Scholar
  9. 9.
    Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1993)Google Scholar
  10. 10.
    Rushby, J.: Integrated formal verification: Using model checking with automated abstraction, invariant generation, and theorem proving. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, Springer, Heidelberg (1999)CrossRefGoogle Scholar
  11. 11.
    Shankar, N., Owre, S., Rushby, J.M.: PVS Tutorial. Computer Science Laboratory, SRI International, Menlo Park, CA (February 1993)Google Scholar
  12. 12.
    Stump, A., Barrett, C., Dill, D.: CVC: a Cooperating Validity Checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 500. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  13. 13.
    Su, J.X., Dill, D.L., Barrett, C.W.: Automatic generation of invariants in processor verification. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, Springer, Heidelberg (1996)CrossRefGoogle Scholar
  14. 14.
    Su, J.X., Dill, D.L., Skakkebæk, J.U.: Formally verifying data and control with weak reachability invariants. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 387–402. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  15. 15.
    Tiwari, A., Rueß, H., Saidi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 113. Springer, Heidelberg (2001)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Husam Abu-Haimed
    • 1
  • Sergey Berezin
    • 1
  • David L. Dill
    • 1
  1. 1.Stanford University 

Personalised recommendations