Using Abstract Specifications to Verify PowerPC™ Custom Memories by Symbolic Trajectory Evaluation

  • Jayanta Bhadra
  • Andrew Martin
  • Jacob Abraham
  • Magdy Abadir
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)


We present a methodology in which the behavior of a switch level device is specified using abstract parameterized regular expressions. These specifications are used to generate a finite automaton representing an abstraction of the behavior of a block of memory comprised of a set of such switch level devices. The automaton, in conjunction with an Efficient Memory Model [1], [2] for the devices, forms a symbolic simulation model representing an abstraction of the array core embedded in a larger design under analysis. Using Symbolic Trajectory Evaluation, we check the equivalence between a register transfer level description and a schematic description augmented with abstract specifications for one of the custom memories embedded in the MPC7450 PowerPC processor.


Partial Order Regular Expression Complete Lattice Input String Input Symbol 
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.
    M. N. Velev, R. E. Bryant, A. Jain. Efficient “Modeling of Memory Arrays in Symbolic Simulation”. CAV, 1997, Proceedings. LNCS, Vol. 1254, Springer, 1997, pp. 388–399.Google Scholar
  2. 2.
    M. N. Velev, R. E. Bryant. “Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation”. TACAS, 1998.Google Scholar
  3. 3.
    N. Krishnamurthy, A. K. Martin, M. S. Abadir, J. A. Abraham. “Validating PowerPC Microprocessor Custom Memories” IEEE Design and Test of Computers, Vol. 17, No. 4, Oct-Dec 2000, pp. 61–76.CrossRefGoogle Scholar
  4. 4.
    L.-C. Wang, M. S. Abadir, N. Krishnamurthy. “Automatic Generation of Assertions for Formal Verification of PowerPC Microprocessor Arrays Using Symbolic Trajectory Evaluation”. 35th ACM/IEEE DAC, June, 1998.Google Scholar
  5. 5.
    R. E. Bryant. “Algorithmic Aspects of Symbolic Switch Network Analysis”. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 6(4), July 1987.Google Scholar
  6. 6.
    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–189, March, 1995.Google Scholar
  7. 7.
    J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Publishing Company, 1979, pp. 1–45.Google Scholar
  8. 8.
    R. E. Bryant. “Graph-Based Algorithms for Boolean Function Manipulation”. IEEE Transactions on Computers, 35(8), August 1986.Google Scholar
  9. 9.
    R. E. Bryant. “Verifying a Static RAM Design by Logic Simulation”, Fifth MIT Conference on Advanced Research in VLSI, 1988, pp. 335–349.Google Scholar
  10. 10.
    N. Ganguly, M. S. Abadir, M. Pandey. “PowerPC array verification methodology using formal techniques”. International Test Conference 1996, pp. 857–864.Google Scholar
  11. 11.
    M. Pandey, R. Raimi, D. L. Beatty, R. E. Bryant. “Formal Verification of PowerPC arrays using Symbolic Trajectory Evaluation”. 33rd ACM /IEEE DAC, June 1996, pp. 649–654.Google Scholar
  12. 12.
    M. Pandey, R. Raimi, R. E. Bryant, M. S. Abadir. “Formal Verification of Content Addressable Memories using Symbolic Trajectory Evaluation”. 34th ACM/IEEE DAC, June 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Jayanta Bhadra
    • 1
    • 2
  • Andrew Martin
    • 1
  • Jacob Abraham
    • 2
  • Magdy Abadir
    • 1
  1. 1.Motorola Inc.USA
  2. 2.The University of Texas at AustinUSA

Personalised recommendations