Efficient modeling of memory arrays in symbolic simulation

  • Miroslav Velev
  • Randal E. Bryant
  • Alok Jain
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


This paper enables symbolic simulation of systems with large embedded memories. Each memory array is replaced with a behavioral model, where the number of symbolic variables used to characterize the initial state of the memory is proportional to the number of memory accesses. The memory state is represented by a list containing entries of the form 〈c, a, d〉, where c is a Boolean expression denoting the set of conditions for which the entry is defined, a is an address expression denoting a memory location, and d is a data expression denoting the contents of this location. Address and data expressions are represented as vectors of Boolean expressions. The list interacts with the rest of the circuit by means of a software interface developed as part of the symbolic simulation engine. The interface monitors the control lines of the memory array and translates read and write conditions into accesses to the list. This memory model was also incorporated into the Symbolic Trajectory Evaluation technique for formal verification. Experimental results show that the new model significantly outperforms the transistor level memory model when verifying a simple pipelined data path.


Memory Location Memory State Register File Boolean Expression Read 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.


  1. [1]
    D. L. Beatty, R. E. Bryant, and C.-J. H. Seger, “Synchronous Circuit Verification by Symbolic Simulation: An Illustration,” Sixth MIT Conference on Advanced Research in VLSI, 1990, pp. 98–112.Google Scholar
  2. [2]
    R. E. Bryant, D. E. Beatty, and C.-J. H. Seger, “Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation,” 28th Design Automation Conference, June, 1991, pp. 297–402.Google Scholar
  3. [3]
    J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill, “Sequential Circuit Verification Using Symbolic Model Checking,” 27th Design Automation Conference, June, 1990, pp. 46–51.Google Scholar
  4. [4]
    J. R. Burch, E. M. Clarke, and D. E. Long, “Representing Circuits More Efficiently in Symbolic Model Checking,” 28th Design Automation Conference, June, 1991, pp. 403–407.Google Scholar
  5. [5]
    J. R. Burch, and D. L. Dill, “Automated Verification of Pipelined Microprocessor Control,” CAV '94, D. L. Dill, ed., LNCS 818, Springer-Verlag, June, 1994, pp. 68–80.Google Scholar
  6. [6]
    E. M. Clarke, O. Grumberg, and D. E. Long, “Model Checking and Abstraction,” 19th Annual ACM Symposium on Principles of Programming Languages, 1992, pp. 343–354.Google Scholar
  7. [7]
    M. Pandey, and R. E. Bryant, “Exploiting Symmetry When Verifying Transistor-Level Circuits by Symbolic Trajectory Evaluation,” CAV '97, June, 1997.Google Scholar
  8. [8]
    C.-J. H. Seger, and R. E. Bryant, “Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories,” Formal Methods in System Design, Vol. 6, No. 2 (March, 1995), pp. 147–190.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Miroslav Velev
    • 1
  • Randal E. Bryant
    • 2
  • Alok Jain
    • 3
  1. 1.Department of Electrical and Computer EngineeringCarnegie Mellon UniversityPittsburgh
  2. 2.School of Computer ScienceCarnegie Mellon UniversityPittsburgh
  3. 3.Department of Electrical and Computer EngineeringCarnegie Mellon UniversityPittsburgh

Personalised recommendations