摘要 一個大的記憶體一般是由多個完全相同的記憶體區塊 (block) 所組成，如此可以降低存取時間和功率。個別記憶體區塊電路的驗證可以有效率地用符號軌跡評估 (symbolic trajectory evaluation，STE) 的方法來驗證。然而，如果一個單一系統由多個記憶體區塊所組成，符號軌跡評估的方法無法有經濟效益地驗證它。這篇論文提出記憶體在區塊層級的接線驗證演算法，利用由下而上的驗證法，驗證一個大記憶體的時間可以被大量地減少。這個意思是指一個記憶體區塊先被完整地驗證，然後只剩下一個大記憶體中記憶體區塊間的接線需要被驗證。以信號錯置瑕疵 (signal misplaced faults，SMFs) 為基礎，我們針對單埠 (single-port) 記憶體及針對多埠 (multiple-port) 記憶體分別提出了三個驗證演算法。對於一個由 2^n x m 位元小記憶體組成的 2^t x s 位元大記憶體，針對單埠記憶體三個演算法的複雜度是 (2n+s+2m+2^t-n-1)x2^t-n，而針對多埠記憶體三個演算法的複雜度是Pw^2xPx(n+sx2^t-n)+Px2^2(t-n) ，其中 t 和 n 是位址寬度而 s 和 m 是資料寬度，Pw 是可以執行寫入運算的埠的數目，P 是所有埠的數目。在位址埠、資料輸入埠、和資料輸出埠上，演算法可以驗證到100%的的埠和埠之間 (inter-port) 和同一個埠之內 (intra-port) 的信號錯置瑕疵。而且演算法可以指定其參數而自動化的產生。 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.
