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

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

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

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