On combining formal and informal verification

  • Jun Yuan
  • Jian Shen
  • Jacob Abraham
  • Adnan Aziz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


We propose algorithms which combine simulation with symbolic methods for the verification of invariants. The motivation is two-fold. First, there are designs which are too complex to be formally verified using symbolic methods; however the use of symbolic techniques in conjunction with traditional simulation results in better “coverage” relative to the computational resources used. Additionally, even on designs which can be symbolically verified, the use of a hybrid methodology often detects the presence of bugs faster than either formal verification or simulation.


Boolean Function Binary Decision Diagram Reachability Analysis Cycle Simulation Symbolic Model 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. 1.
    P. Ashar and S. Malik. Fast Functional Simulation Using Branching Programs. In Proc. Intl. Conf. on Computer-Aided Design, November 1995.Google Scholar
  2. 2.
    R. K. Brayton, G. D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G. Swamy, and T. Villa. VIS: A system for Verification and Synthesis. In Proc. of the Computer Aided Verification Conf., July 1996.Google Scholar
  3. 3.
    R. Bryant. Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35:677–691, August 1986.Google Scholar
  4. 4.
    B. Chen, M. Yamazaki, and M. Fujita. Bug Identification of a Real Chip Design by Symbolic Model Checking. In Proc. European Conf. on Design Automation, pages 132–136, March 1994.Google Scholar
  5. 5.
    H. Cho, G. D. Hachtel, E. Macii, M. Poncino, and F. Somenzi. A Structural Approach to State Space Decomposition for Approximate Reachability Analysis. In Proc. Intl. Conf. on Computer Design, October 1994.Google Scholar
  6. 6.
    W.J. Culler. Implementing Safety Critical Systems: The VIPER microprocessor. Kluwer Academic Publishment, 1987.Google Scholar
  7. 7.
    Richard C. Ho, C. Han Yang, Mark A. Horowitz, and David L. Dill. Architectural Validation for Processors. In Proceedings of the International Symposium on Computer Architecture, June 1995.Google Scholar
  8. 8.
    Y. Hoskote, D. Moundanos, and J. Abraham. Automatic Extraction of the Control Flow Machine and Application to Evaluating Coverage of Verification Vectors. In Proc. Intl. Conf. on Computer Design, Austin, TX, October 1995.Google Scholar
  9. 9.
    B. Lin and R. Newton. Implicit Manipulation of Equivalence Classes Using Binary Decision Diagrams. In Proc. Intl. Conf. on Computer Design, Cambridge, MA, October 1991.Google Scholar
  10. 10.
    P. McGeer, K. McMillan, A. Saldanha, A. Sangiovanni-Vincentelli, and P. Scaglia. Fast Discrete Function Evaluation. In Proc. Intl. Conf. on Computer-Aided Design, November 1995.Google Scholar
  11. 11.
    Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.Google Scholar
  12. 12.
    R. Ranjan, J. Sanghavi, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. High Performance BDD Package Based on Exploiting Memory Hierarchy. In Proc. of the Design Automation Conf., Las Vegas, NV, June 1996.Google Scholar
  13. 13.
    K. Ravi and F. Somenzi. High Density Reachability Analysis. In Proc. Intl. Conf. on Computer-Aided Design, Santa Clara, CA, November 1995.Google Scholar
  14. 14.
    Vigyan Singhal. Design Replacements for Sequential Circuits. PhD thesis, University of California Berkeley, Electronics Research Laboratory, College of Engineering, University of California, Berkeley, CA 94720, 1996.Google Scholar
  15. 15.
    K. Thompson. Retrograde analysis of certain endgames. ICCA Journal, 9(3):131–139, 1986.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Jun Yuan
    • 1
  • Jian Shen
    • 2
  • Jacob Abraham
    • 2
  • Adnan Aziz
    • 2
  1. 1.Motorola Inc.Austin
  2. 2.ECE Dept.Univ. of TexasAustin

Personalised recommendations