Abstract
This paper enables symbolic ternary 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 distinct symbolic memory locations accessed. The behavioral model provides a conservative approximation of the replaced memory array, while allowing the address and control inputs of the memory to accept symbolic ternary values. Memory state is represented by a list of entries encoding the sequence of updates of symbolic addresses with symbolic data. The list interacts with the rest of the circuit by means of a software interface developed as part of the symbolic simulation engine. This memory model was incorporated into our verification tool based on Symbolic Trajectory Evaluation. Experimental results show that the new model significantly outperforms the transistor level memory model when verifying a simple pipelined data path.
This research was supported in part by the SRC under contract 97-DC-068.
Chapter PDF
Keywords
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
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.
R. E. Bryant, “Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams,” ACM Computing Serveys, Vol. 24, No. 3 (September 1992), pp. 293–318.
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.
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.
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.
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.
A. Jain, “Formal Hardware Verification by Symbolic Trajectory Evaluation,” Ph.D. thesis, Department of Electrical and Computer Engineering, Carnegie Mellon University, August 1997.
M. Pandey, “Formal Verification of Memory Arrays,” Ph.D. thesis, School of Computer Science, Carnegie Mellon University, May 1997.
M. Pandey, and R. E. Bryant, “Exploiting Symmetry When Verifying Transistor-Level Circuits by Symbolic Trajectory Evaluation,” CAV '97, O. Grumberg, ed., LNCS 1254, Springer-Verlag, June 1997, pp. 244–255.
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.
M. Velev, R. E. Bryant, and A. Jain, “Efficient Modeling of Memory Arrays in Symbolic Simulation,”2 CAV '97, O. Grumberg, ed., LNCS 1254, Springer-Verlag, June 1997, pp. 388–399.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Velev, M.N., Bryant, R.E. (1998). Efficient modeling of memory arrays in symbolic ternary simulation. In: Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998. Lecture Notes in Computer Science, vol 1384. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054169
Download citation
DOI: https://doi.org/10.1007/BFb0054169
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64356-2
Online ISBN: 978-3-540-69753-4
eBook Packages: Springer Book Archive