Title :
Automatic verification of memory systems which service their requests out of order
Author :
Hojati, Ramin ; Mueller-Thuns, Robert ; Loewenstein, Paul ; Brayton, Robert K.
fDate :
29 Aug-1 Sep 1995
Abstract :
In a shared memory multi-processor environment, one can achieve greater performance by out-of-order servicing of memory requests. Although this results in higher performance, such systems are complicated and their design and programming requires care. Recently, there have been efforts to develop concise formal specifications of such systems. We present a general strategy, based on the language containment paradigm, to automatically verify such memory systems against their formal specifications. The size of the state space explored during the verification is dependent on the number of data values, length of buffers, number of processors, and number of memory locations. Abstraction is used to reduce the number of data values to just two, and the number of memory locations to a small number without losing any accuracy in our verification. As an example, we concentrate on SPARC´s V8 memory model, for which we have built a sample hardware description language model. Experimental results demonstrating the feasibility of our approach are presented
Keywords :
formal specification; formal verification; logic testing; memory architecture; shared memory systems; formal specifications; language containment; memory systems; multi-processor environment; shared memory; state space; Automata; Costs; Equations; Formal specifications; Hardware design languages; Out of order; Random access memory; Space exploration; State-space methods;
Conference_Titel :
Design Automation Conference, 1995. Proceedings of the ASP-DAC '95/CHDL '95/VLSI '95., IFIP International Conference on Hardware Description Languages. IFIP International Conference on Very Large Scal
Conference_Location :
Chiba
Print_ISBN :
4-930813-67-0
DOI :
10.1109/ASPDAC.1995.486379