摘要
一個大的記憶體一般是由多個完全相同的記憶體區塊 (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.

Reference
[1] U. Schlichtmann, “Tomorrows high-quality SoCs require high-quality embedded memories today”, in Proc. Int. Symp. Quality Electronic Design, March 2002, pp. 225.
[2] T. Yamauchi, L. Hammond, and K. Olukotun, “The hierarchical multi-bank DRAM: a high-performance architecture for memory integrated with processors”, in Proc. Seventeenth Advanced Research in VLSI Conference , Sept. 1997, pp. 303 – 319.
[3] K. Itoh, K. Sasaki, and Y. Nakagome, “Trends in low-power RAM circuit technologies”, in Proc. IEEE., vol. 83 , no. 4, April 1995, pp. 524 – 543.
[4] L. Benini, L. Macchiarulo, A. Macii, and M. Poncino, “Layout-driven memory synthesis for embedded systems-on-chip”, IEEE Trans. Very Large Scale Integration (VLSI) Systems, vol. 10 , no. 2 , pp. 96 – 105, April 2002.
[5] R.-F. Huang, L.-M. Denq, C.-W. Wu, and J.-F. Li, “A testability-driven optimizer and wrapper generator for embedded memories”, in Proc. IEEE Int. Workshop on Memory Technology, Design and Testing (MTDT), July 2003, pp. 53 – 56.
[6] J. Bergeron, Writing Testbenches-Functional Verification of HDL Models, Kluwer Academic Publishers, Norwell, 2000.
[7] M. Pandey and R. E. Bryant, “Formal verification of memory arrays using symbolic trajectory evaluation”, in Proc. IEEE Int. Workshop on Memory Technology, Design and Testing (MTDT), Aug. 1997, pp. 42 – 49.
[8] G. Swamy, “Formal verification of digital systems”, in Proc. Tenth Int. VLSI Design Conference, Jan. 1997, pp. 213 – 217.
[9] G. Parthasarathy, M. K. Iyer, F. Tao, L.-C. Wang, K.-T. Cheng, and M. S. Abadir, “Combining ATPG and symbolic simulation for efficient validation of embedded array systems”, in Proc. Int. Test Conf. (ITC), Oct. 2002, pp. 203 – 212.
[10] F. Tao, L.-C. Wang, K.-T. Cheng, M. Pandy, and M. S. Abadir, ”Enhanced symbolic simulation for efficient verification of embedded array systems”, in Proc. Design Automation Conf., Jan. 2003, pp. 302 – 307.
[11] S. Napper, and D. Yang, “Equivalence checking a 256 MB SDRAM”, in Proc. IEEE Int. Workshop on Memory Technology, Design and Testing (MTDT), Aug. 2001, pp. 85 – 89.
[12] N. Krishnamurthy, A. K. Martin, M. S. Abadir, and J. A. Abraham, “Validation of PowerPCTM custom memories using symbolic simulation”, in Proc. VLSI Test Symp., April-May 2000, pp. 9 – 14.
[13] D. Karlsson, P. Eles, and Z. Peng, “Formal verification in a component-based reuse methodology”, in Int. Symp. System Synthesis, Oct. 2002, pp. 156 – 161.
[14] A. J. Hu, M. Fujita, and C. Wilson, “Formal verification of the HAL S1 System Cache Coherence Protocol”, in Proc. IEEE Int. Computer Design Conference, Oct. 1997, pp. 438 – 444.
[15] S. Taylor, C. Ramey, C. Barner, and D. Asher, “A simulation-based method for the verification of shared memory in multiprocessor systems”, in Proc. IEEE/ACM Int. Computer Aided Design Conference, Nov. 2001, pp. 10 – 17.
[16] A. Pirola, “A solution for hardware emulation of non volatile memory macrocells”, in suppl. Design Automation and Test Conf. and Exhibit., Europe, 2003, pp. 262 – 266.
[17] M. Abramovici, M. A. Breuer, and A. D. Friedman, Digital Systems Testing and Testable Design, Computer Science Press, New York, 1990.
[18] A. J. Van De Goor, I. B. S. Tlili, and S. Hamdioui, “Converting march tests for bit-oriented memories into tests for word-oriented memories”, in Proc. IEEE Int. Workshop on Memory Technology, Design and Testing (MTDT), Aug. 1998, pp. 46 – 52.
[19] C.-Y. Wang, S.-W. Tung, and J.-Y. Jou, “On automatic-verification pattern generation for SoC with port-order fault model”, IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 21, no. 4, pp. 466 – 479, April 2002.
[20] M. L. Bushnell and V. D. Agrawal, Essentials of Electronic Testing for Digital, Memory & Mixed-Signal VLSI Circuits , Kluwer Academic Publishers, 2000.
[21] J.-F. Li, “Efficient block-level connectivity verification algorithms for embedded memories”, IEICE Trans. Fundamentals of Electronics, Communications and Computer Sciences, vol. E87-A, no. 12, pp. 3185 - 3192, December 2004.
[22] M. K. Ganai, A. Gupta, and P. Ashar, “Verification of embedded memory systems using efficient memory modeling”, in Proc. Design Automation and Test,, Europe, 2005, vol. 2, pp.1096-1101.
[23] R. E. Bryant, “Formal verification of memory circuits by switch-level simulation” , IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 10, no. 1, pp. 94 – 102, Jan. 1991.
[24] S. Hangal, D. Vahia, C. Manovit, J.-Y. J. Lu, S. Narayanan, “TSOtool: a program for verifying memory systems using the memory consistency model” in Proc. 31st Annual Int. Symp. Computer Architecture, pp. 114 – 123, June 2004.