基于SOC異步FIFO的設(shè)計(jì)與形式驗(yàn)證.pdf

1、近年，隨著集成電路產(chǎn)業(yè)的快速發(fā)展，半導(dǎo)體工藝水平已經(jīng)達(dá)到亞微米水平，隨之而來(lái)的現(xiàn)狀就是芯片集成規(guī)模越來(lái)越復(fù)雜。縱觀整個(gè)芯片設(shè)計(jì)流程，從行為級(jí)HDL一直到芯片最后的投片，最復(fù)雜、最重要的環(huán)節(jié)就是驗(yàn)證。在面對(duì)更大的驗(yàn)證壓力時(shí)，傳統(tǒng)的模擬仿真驗(yàn)證已經(jīng)漸漸暴露出其局限性。形式驗(yàn)證方法作為傳統(tǒng)驗(yàn)證方法的補(bǔ)充，日益引起人們的關(guān)注。形式驗(yàn)證方法以不同的驗(yàn)證邏輯實(shí)現(xiàn)驗(yàn)證目標(biāo)，能夠克服傳統(tǒng)驗(yàn)證方法的不足，所以本文的研究重心為形式驗(yàn)證，并結(jié)合JASPER平

2、臺(tái)提出了適用性更廣的形式驗(yàn)證方法。
　　首先，本文選取SOC中常用模塊異步FIFO為驗(yàn)證對(duì)象，基于傳統(tǒng)異步FIFO設(shè)計(jì)結(jié)構(gòu)和功能實(shí)現(xiàn)邏輯，本文提出了改進(jìn)后的異步FIFO設(shè)計(jì)，與傳統(tǒng)設(shè)計(jì)相比，改進(jìn)后的設(shè)計(jì)優(yōu)勢(shì)在于運(yùn)用了新的空滿(mǎn)標(biāo)志位判斷邏輯，克服了傳統(tǒng)設(shè)計(jì)中存儲(chǔ)器深度的局限性；然后，本文分析了形式驗(yàn)證當(dāng)前的應(yīng)用局限性，研究了基于Jasper平臺(tái)形式驗(yàn)證方法的邏輯原理以及形式驗(yàn)證狀態(tài)空間的意義，并對(duì)Jasper平臺(tái)特征驗(yàn)證流程進(jìn)行了詳

3、細(xì)的說(shuō)明，同時(shí)，引入了 Jasper的特征驗(yàn)證語(yǔ)言SVA，通過(guò)舉例分析研究了SVA語(yǔ)言關(guān)于設(shè)計(jì)特性的描述細(xì)則；最后，以本文中改進(jìn)后的異步FIFO為驗(yàn)證對(duì)象，制定出特定的Jasper驗(yàn)證方案，并基于異步FIFO設(shè)計(jì)的功能劃分進(jìn)行斷言語(yǔ)句的編寫(xiě)，在驗(yàn)證結(jié)果分析中，通過(guò)特征語(yǔ)句編寫(xiě)錯(cuò)誤為例詳細(xì)討論了如何使用Jasper圖形界面進(jìn)行驗(yàn)證分析糾錯(cuò)。
　　本文形式驗(yàn)證方法的研究結(jié)果表明，基于JASPER平臺(tái)的形式驗(yàn)證方法較傳統(tǒng)模擬仿真方法，具