Abstract
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.
This research was supported in part by the SRC under contract 96-DC-068.
Chapter PDF
Similar content being viewed by others
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, 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.
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.
M. Pandey, and R. E. Bryant, “Exploiting Symmetry When Verifying Transistor-Level Circuits by Symbolic Trajectory Evaluation,” CAV '97, June, 1997.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Velev, M., Bryant, R.E., Jain, A. (1997). Efficient modeling of memory arrays in symbolic simulation. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_38
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_38
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive