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

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

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

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