Abstract
在一個共享主記憶體的多處理機系統中，快取記憶體中資料的一致性是一 個非常重要的課題。而快取記憶體資料一致性協定是用來維持所有快取記 憶體和主記憶體中資料的一致性，它的硬體設計不僅複雜而且易於出錯， 因此，驗證它的硬體設計是非常重要的。為了要找出硬體設計上的錯誤， 目前主要的方法有兩種：形式驗證法和模擬驗證法。由於形式驗證法還在 初期的研究發展階段，因此工業界仍採用模擬驗證法，而隨機測試法是模 擬驗證法中常用的一種技術。在本篇碩士論文中，我們描述在 XMP系統中 驗證快取記憶體資料一致性協定的方法，XMP 系統是一個共享主記憶體的 多處理機系統，是由工業技術研究院和英代爾公司共同研究發展的。應用 隨機測試法，在系統模擬環境中，來產生子系統之間複雜的交互作用，藉 以驗證硬體設計的正確性。我們發展了一個隨機測試器和監視器，隨機測 試器是用來產生測試向量的，而監視器則可以追蹤快取記體資料一致性協 定的運作。這個隨機測試器除了能夠自動產生測試向量外，還可以根據工 程師的需求，來產生測試向量的種類。在另一方面，我們所設計的監視器 ，具有追蹤硬體行為的能力，在系統模擬時，能夠快速找到硬體設計的問 題。從模擬結果顯示，這種驗證方式非常有用，我們可以很快發現硬體設 計的問題。 In a shared-memory multiprocessor system, cache coherency is a very important issue. A cache coherency protocol is used to maintain the consistency of data across all caches and the main memory. Its hardware implementation is complex and error-prone. Thus, the verification of its design is particularly significant. To find out the design errors, there are two major approaches found in the open literature. One is formal verification and the other is simulation-based verification. The former is still in its very early stage of development. Therefore, the latter is still industry's choice to date. The random test generation method is a kind of the simulation-based verification technique. In this thesis, we describe a strategy for verifying the cache coherency protocol in the XMP, a shared- memory multiprocessor system developed by ITRI in conjuction with Intel. Based on a random test generation approach, a system-level simulation environment is created to model the complex interactions among the subsystems. We develop a random tester for generating test cases and a transactor for checking the cache coherency protocol. The random tester allows the engineers to weigh operations for generating stimulus to access memory block without writing scripts. Adding hardware knowledge to the transactor improves the debugging capability. Simulation results show that the strategy is indeed useful. We have discovered many design errors very quickly.