Sequential Equivalence Checking by Symbolic Simulation

  • Gerd Ritter
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)


An approach for interpreted sequential verification at different levels of abstraction by symbolic simulation is proposed. The equivalence checker has been used in previous work to compare two designs at rt-level.We describe in this paper the automatic verification of gate-level results of a commercial synthesis tool against a behavioral specification at rt-level. The symbolic simulator has to cope with different numbers of control steps since the descriptions are not cycle equivalent. The state explosion problem of previous approaches relying on state traversal is avoided. The simulator uses a library of different equivalence detection techniques which are surveyed with main emphasis on the new techniques required at gate-level. Cooperation of those techniques and good debugging support are possible by notifying detected relationships at equivalence classes rather than to manipulate symbolic terms.


Boolean Function Function Symbol Equivalence Check Boolean Expression Memory Operation 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    M. D. Aagaard, R. B. Jones, and C-J. H. Seger. Combining theorem proving and trajectory evaluation in an industrial environment. In DAC’98, 1998.Google Scholar
  2. [2]
    M. D. Aagaard, R. B. Jones, and C-J. H. Seger. Formal verification using parametric representations of boolean constraints. In DAC’99, 1999.Google Scholar
  3. [3]
    P. Ashar, A. Gupta, and S. Malik. Using complete-1-distinguishability for FSM equivalence checking. In ICCAD’96, 1996.Google Scholar
  4. [4]
    C. W. Barrett, D. L. Dill, and J. R. Levitt. Validity checking for combinations of theories with equality. In FMCAD’96, volume 1166 of LNCS. Springer Verlag, 1996.Google Scholar
  5. [5]
    C. W. Barrett, D. L. Dill, and J. R. Levitt. A decision procedure for bit-vector arithmetic. In DAC’98, 1998.Google Scholar
  6. [6]
    V. Bertacco, M. Damiani, and S. Quer. Cycle-based symbolic simulation of gatelevel synchronous circuits. In DAC’99, 1999.Google Scholar
  7. [7]
    R. E. Bryant. Symbolic verification of MOS circuits. In 1985 Chapel Hill Conference on VLSI, pages 419–438. Computer Science Press, 1985.Google Scholar
  8. [8]
    R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers, C-35(8):677–691, 1986.CrossRefGoogle Scholar
  9. [9]
    J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In DAC’90, 1990.Google Scholar
  10. [10]
    M. K. Ganai, A. Aziz, and A. Kuehlmann. Enhancing simulation with BDDs and ATPG. In DAC’99, 1999.Google Scholar
  11. [11]
    S. Hazelhurst and C.-J. H. Seger. Symbolic trajectory evaluation. In Formal Hardware Verification, volume 1287 of LNCS. Springer Verlag, 1997.Google Scholar
  12. [12]
    J. L. Hennessy and D. A. Patterson. Computer architecture: a quantitative approach. Morgan Kaufman, CA, second edition, 1996.zbMATHGoogle Scholar
  13. [13]
    H. Hinrichsen, H. Eveking, and G. Ritter. Formal synthesis for pipeline design. In DMTCS+CATS’99, Auckland, 1999.Google Scholar
  14. [14]
    S. Höreth. Implementation of a multiple-domain decision diagram package. In CHARME’97, 1997.Google Scholar
  15. [15]
    S. Höreth. Hybrid graph manipulation package demo, Darmstadt, 1998.
  16. [16]
    C. N. Ip and D. L. Dill. State reduction using reversible rules. In DAC’96, 1996.Google Scholar
  17. [17]
    R. B. Jones, D. L. Dill, and J. R. Burch. Efficient validity checking for processor verification. In ICCAD’95, 1995.Google Scholar
  18. [18]
    C. Kern and M. R. Greenstreet. Formal hardware verification in hardware design: A survey. ACM Trans. on Design Automation of Electronic Systems, 4(2), 1999.Google Scholar
  19. [19]
    J. O'Leary, X. Zhao, R. Gerth, and C.-J. H. Seger. Formally verifying IEEE compilance of floating-point hardware. Intel Technology Journal, Q1, 1999.Google Scholar
  20. [20]
    M. Pandey and R. E. Bryant. Exploiting symmetry when verifying transistorlevel circuits by symbolic trajectory evaluation. IEEE Trans. on Computer-Aided Design, 18(7):918–935, 1999.CrossRefGoogle Scholar
  21. [21]
    G. Ritter, H. Eveking, and H. Hinrichsen. Formal verification of designs with complex control by symbolic simulation. In CHARME’99, volume 1703 of LNCS. Springer Verlag, 1999.Google Scholar
  22. [22]
    G. Ritter, H. Hinrichsen, and H. Eveking. Formal verification of descriptions with distinct order of memory operations. In ASIAN’99, volume 1742 of LNCS. Springer Verlag, 1999.Google Scholar
  23. [23]
    C.-J. H. Seger and R. E. Bryant. Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design, 6(2):147–190, 1995.CrossRefGoogle Scholar
  24. [24]
    T. Uehara. Proofs and synthesis are cooperative approaches for correct circuit designs. In From HDL Descriptions to Guaranteed Correct Circuit Designs. North-Holland, 1987.Google Scholar
  25. [25]
    L.-C. Wang, M. S. Abadir, and N. Krishnamurthy. Automatic generation of assertions for formal verification of PowerPCTM microprocessor arrays using symbolic trajectory evaluation. In DAC’98, 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Gerd Ritter
    • 1
  1. 1.Dept. of Electrical and Computer EngineeringDarmstadt University of TechnologyDarmstadtGermany

Personalised recommendations