Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation

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.