龍芯2號功能部件半形式化驗證方法的研究與實現(xiàn).pdf

1、隨著集成電路設計技術的發(fā)展，芯片的設計越來越復雜。如何保證設計的功能正確，這是驗證工程師所面臨的一個嚴峻問題。由于集成電路規(guī)模增大，采用傳統(tǒng)仿真(Simulation)驗證方法進行功能驗證的復雜度呈指數級增長，而完全形式化(Formal)的方法目前難以處理百萬門以上的復雜設計，這使得集成電路設計能力和驗證能力之間的差距越來越大。為了縮短這個差距，將仿真與形式化相結合的半形式化(Semi-Formal)驗證方法成為目前國內外科研機構以及E

2、DA廠商研究的熱點。本文所做的工作也主要是在這方面的一些嘗試。 龍芯2號是我國自主研發(fā)的高性能通用處理器，其設計十分復雜。為了對它進行充分的驗證，我們也希望從可以半形式化的角度進行。為此，我們在結合CadenceSMV和NuSMV兩個形式化驗證工具的基礎上實現(xiàn)了一個半形式化的驗證原型系統(tǒng)。該半形式化驗證系統(tǒng)核心包括設計模型化、驗證規(guī)范描述、形式分析算法、初始狀態(tài)選擇四個方面。首先，將需要驗證的設計模型化為Kripke結構，并以S

3、MV語言形式在計算機中表示。其次，驗證規(guī)范通過可計算樹邏輯(CTL)或線性時態(tài)邏輯公式(LTL)表示出來。然后采用了基于SAT-BMC的模型檢驗方法作為半形式化驗證系統(tǒng)的形式化分析引擎。最后在初始狀態(tài)遷移方面可以采用仿真的方法，也可以直接初始化。 本文還根據IEEE-754標準，完成了一個部分功能的基準乘加部分部件描述。在此基礎上，對龍芯2號的重要功能部件——浮點乘加部件(FMAF)完成了初步的驗證。此外，還通過插入錯誤的方法，