| dc.description.abstract | Abstract
A large memory is typically designed with multiple identical memory blocks for reducing access time and power. The circuit verification of individual memory blocks can be effectively handled by the Symbolic Trajectory Evaluation (STE) approach. However, if multiple memory blocks are integrated into a single system, the STE approach cannot verify it economically. This thesis introduces algorithms for verifying block-level connectivity of memories. The verification time of a large memory can be reduced a lot by using bottom-up verification scheme. It means that a memory block is first verified thoroughly, and then only the interconnection between memory blocks of the large memory needs to be verified. In this thesis, we propose three algorithms for single-port RAMs and three algorithms for multiple-port RAMs based on signal misplaced faults (SMFs). The complexity of the three algorithms for single-port RAMs is(2n+s+2m+2^t-n-1)x2^t-n for a 2^t x s bit large memory composed of 2^n x m bit small memories, where t , n and s , m are the address width and data width, respectively. The complexity of the three algorithms for multiple-port RAMs is Pw^2xPx(n+sx2^t-n)+Px2^2(t-n) , where Pw is the number of read-write ports and write-only ports and P is the total number of ports. And the algorithms can verify 100% of the inter-port and intra-port signal misplaced faults of the address, data input, and data output ports. The algorithms can be generated automatically by indicating the parameters s , t , m , and n. | en_US |