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

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

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

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