整數乘法器之對等檢查

Abstract

隨著現今的糸統越來越複雜，證明糸統設計的正確性已成為十分重要的事。以模擬(simulation)為主的方法一般已無法完全地確認一設計的正確性。英特爾(Intel)的奔騰除法錯誤(Pentium Division Bug)及最近的820晶片組錯誤(820 Chip Set Bug)顯示了正規驗證(formal verification)方法之需求在確保系統的正確性上。對等檢查(equivalence checking)是正規驗證的一種方法，已廣泛地被使用在工業上對於確保原來的設計和修改過後的設計是等效的。據我們所知關於市面上的對等檢查之工具，它們無法處理很複雜且僅有些微結構上相似的算術電路如有不同設計架構之乘法器。因此,有一個急切需要對於有一方法能檢查兩個乘法器是否等效。 先前的研究大都集中在驗證乘法器的正確性經由使用Binary Decision Diagrams (BDDs)或word-level representations 如 Multiplicative Binary Moment Diagrams (*BMD)等。據我們所知，僅有一整數乘法器之對等檢查上的研究，是由Stanion所作的。他的方法只能驗證兩個不相似的乘法器在一相同局部乘積產生(partial product generation)下。 在這篇論文裡，我們討論了整數乘法器之對等檢查，尤其是結構不相似之乘法器。我們的方法主要是針對Hamaguchi的反向替代方法(backward substitution method)做了以下幾點改進: (1) 自動確認元件(automatic identification of compnents)以形成合適的中斷點，因而大大地改善那反向替代過程 (2) 一階層反向替代演算法(layered-backward substitution algorithm)來減少替代的次數 (3) 以Multiplicative Power Hybrid Decision Diagrams (*PHDDs)作為我們的word-level representation，而非使用在Hamaguchi方法裡的*BMDs。因為*PHDDs至少比*BMDs快五倍在表示算術電路的word-level functions上。 實驗結果顯示我們的方法能有效地檢查兩個乘法器是否等效。例如，我們的方法僅花了大約15分鐘的時間就能驗證出一64 x 64 array multiplier是否對等於一64 x 64 Wallace-tree multiplier，而Stanion的方法卻要花6個小時以上及130MB以上的記憶體。另外，我們也證明了我們的方法之複雜度(complexity)是O(n^4)， n是word的大小。實驗結果卻顯示了我們的方法之複雜度以三次方成長對於大部分的乘法器，除了bit-pair Wallce-tree multipliers 是O(n^(3.5))。

With the increase in the complexity of today systems, proving the correctness of a design has become a major concern. simulation-based methodologies are generally inadequate to validate the correctness of a design with a reasonable confidence. The Intel's Pentium Division Bug and recent 820 chip set Bug have demonstrated the need of formal verification approach to ensure the correctness of the system. Equivalence checkers, one of formal verification approach, have been widely used in the industry to ensure the equivalence of the original design and the modified(optimized) design with large structure similarity. Based on our knowledge about commercial equivalence checkers, they can not handle large complex arithmetic circuits with very little structural similarity such as multipliers with different design architecture. Thus, there is an emergence need to have an approach to check the equivalence of two multipliers. Most of previous researches focused on verifying the correctness of integer multipliers based on Binary Decision Diagrams (BDDs) or word-level representations such as Multiplicative Binary Moment Diagrams (*BMDs), etc. To our knowledge, the only research on equivalence checking of integer multipliers was done by Stanion. His approach can only verify two dissimilar multipliers with same partial product generation. In this thesis, we address on equivalence checking of integer multipliers, especially for the multipliers without structure similarity. Our approach is based on Hamaguchi's backward substitution method [19] with the following improvements: (1) automatic identification of components to form proper cut point and thus dramatically improve the backward substitution process, (2) a layered-backward substitution algorithm to reduce the number of substitutions, and (3) Multiplicative Power Hybrid Decision Diagrams(*PHDDs) as our word-level representation rather than *BMD in Hamaguchi's approach. *PHDDs is at least 5 times faster than *BMDs to represent word-level functions for arithmetic circuits. Experimental results show that our approach can effiently check the equivalence of two integer multipliers. For example, our approach takes about 15 minutes of CPU time to verify the equivalence of a 64 x 64 array multiplier versus a 64 x 64 Wallace tree multiplier, while Stanion's approach took 6 hours and used 130MBytes. We also show that the complexity of our approach is upper bounded by O(n ^4 ), where n is the word size. Our experimental results show that the complexity of our approach grows cubically O(n ^3 ) for most of the multipliers we verified, except the bit-pair Wallace-tree multiplier case (O(n^3.5 )).