Efficient Modeling of MemoryArrays in Symbolic Simulation

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 vari-ables used to characterize the initial state of the memory is proportional to the number of mem-ory 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 con-tents 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 devel-oped 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 veri-fication. Experimental results show that the new model significantly outperforms the transistor level memory model when verifying a simple pipelined data path