單元級晶片驗證最佳化

Abstract

晶片驗證在晶片設計流程中扮演一個不可或缺的角色，拜半導體產業的技術與晶片設計的計密程度，驗證的工作變成是一個龐大問題與挑戰，通常晶片驗證工程師使用一種證明相同的方式下來驗證片，驗證由晶片設計師所設計出來的晶片與驗證工程師所設計出來的程式是否相同是一個非常大的挑戰，由於晶片設計師所使用的語言是低階的硬體描述語言，驗證工程師所使用的為高階的程式語言，所以唯一的克服方法為將兩種設計轉換成一種最低階的表示方式，將驗證工程師的設計轉換成低階的表示方式後在與原工程師所設計的硬體比較，通常我會將兩種設計轉換成低階的表示方式後，將他們合併在一起，去比較他們兩者之間的輸出是否相等，我們可以使用SAT引擎去解決相等的問題。 在本篇論文中我們將討論從高階的表示法轉換成低階的表示法之中的關係，與效能上的問題，不同的結構與不同的表示方式將導致有不同的效能，目的是找出最佳的結構以利於在提升驗證上面的速度。

IC verification plays an important role in the design flow and becomes a difficult work with the rising complexity of modern IC designs. Among all methods, equivalence checking is a commonly adopted approaching in IC verification. However, checking the equivalence of a system-level model and RTL design is a major challenge, since the system-level model is written in high level statement, while RTL model is written in the low level description, the challenges can only be overcome with a combination of bit-level and word-level reasoning techniques. For the system-level model, it’s need to translate to the word-level or bit-level representation and check the functionally of both RTL model and system-level model. Another equivalence checking approach, it’s usually combined those RTL model and system-level model in the word-level or bit level representation into a circuit. We use the SAT engine to solve the equivalence problem. In this disquisition, we had discussed the relationship between the system-level model and bit-level representation, and difference architecture of the bit-level implementation cause different performance.