Advertisement

Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation

  • Manish Pandey
  • Randal E. Bryant
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)

Abstract

In this paper we describe the use of symmetry for verification of transistor-level circuits by symbolic trajectory evaluation. We show that exploiting symmetry can allow one to verify systems several orders of magnitude larger than otherwise possible. We classify symmetries in circuits as structural symmetries, arising from similarities in circuit structure, data symmetries, arising from similarities in the handling of data values, and mixed structural-data symmetries. We use graph isomorphism testing and symbolic simulation to verify the symmetries in the original circuit. Using conservative approximations, we partition a circuit to expose the symmetries in its components, and construct reduced system models which can be verified efficiently. We have verified Static Random Access Memory circuits with up to 1.5 Million transistors.

Keywords

Excitation Function Structural Symmetry Formal Verification Static Random Access Memory Temporal Formula 
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.

References

  1. 1.
    S. Aggarwal, R. P. Kurshan, and K. Sabnani. A calculus for protocol specification and validation. In Protocol Specification, Testing and Verification, volume 3, 1983.Google Scholar
  2. 2.
    Derek L. Beatty and Randal E. Bryant. Fast incremental circuit analysis using extracted hierarchy. In 25th ACM/IEEE Design Automation Conference, pages 495–500, June 1988.Google Scholar
  3. 3.
    Randal E. Bryant. Boolean analysis of MOS circuits. IEEE Transactions on Computer-Aided Design, CAD-6(4):634–649, July 1987.Google Scholar
  4. 4.
    Randal E. Bryant. Formal verification of memory circuits by switch-level simulation. IEEE Transactions on Computer-Aided Design, CAD-10(1):94–102, January 1991.Google Scholar
  5. 5.
    Randal E. Bryant and Carl-Johan H. Seger. Formal verification of digital circuits using symbolic ternary system models. In Robert P. Kurshan, editor, Computer Aided Verification, pages 121–146, 1990.Google Scholar
  6. 6.
    Edmund M. Clarke, Robert Enders, Thomas Filkorn, and Somesh Jha. Exploiting symmetry in temporal logic model checking. Formal Methods in System Design, 9:77–104, 1996.Google Scholar
  7. 7.
    E. Allen Emerson and A. Prasad Sistla. Symmetry and model checking. Formal Methods in System Design, 9:105–131, 1996.Google Scholar
  8. 8.
    C. Norris Ip and David L. Dill. Better verification through symmetry. Formal Methods in System Design, 9:41–75, 1996.Google Scholar
  9. 9.
    Manish Pandey, Richard Raimi, Derek L. Beatty, and Randal E. Bryant. Formal verification of PowerPC(TM) arrays using symbolic trajectory evaluation. In 33rd ACM/IEEE Design Automation Conference, pages 649–654, June 1996.Google Scholar
  10. 10.
    Carl-Johan H. Seger and Randal E. Bryant. Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design, 6:147–189, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Manish Pandey
    • 1
  • Randal E. Bryant
    • 1
  1. 1.School of Computer ScienceCarnegie Mellon UniversityPittsburghUSA

Personalised recommendations