基于斷言的形式化驗證與UVM的綜合應用
發(fā)布時間:2021-08-20 05:09
在整個片上系統(tǒng)的開發(fā)流程中,驗證工作發(fā)揮著非常重要的作用,其在項目中所占的時間平均已經達到55%。即使這樣,大多數(shù)芯片在投入生產前至少需要進行兩次流片,其中芯片的功能性缺陷是導致重新流片的頭號原因。伴隨著更復雜的電路功能和更快的產品上市的壓力,功能驗證已成為芯片設計開發(fā)周期的瓶頸。使用好現(xiàn)有的驗證工具,對它們的驗證特性進行深入的研究,對保證芯片功能的正確性、提高驗證效率至關重要。針對這一問題,本文從最基本的模塊驗證做起,選擇了目前芯片開發(fā)流程中用于模塊驗證的最流行的兩種驗證方法進行研究。本文以多核調試模塊為驗證案例,先后使用基于斷言的形式化驗證方法和UVM驗證方法對多核調試模塊進行驗證,并記錄下使用兩種驗證方法對多核調試模塊進行驗證時各個階段的工作量,以此來發(fā)現(xiàn)適用于兩種驗證方發(fā)的電路特點。然后根據不同的電路特點選擇合適的驗證方法進行綜合驗證。分析對比三種驗證方式用于驗證平臺建立、斷言的開發(fā)與調試、測試用例的開發(fā)與調試、覆蓋率分析的工作量,總結三種驗證方式的優(yōu)劣,并結合實際項目給出綜合使用兩種驗證方法的建議。在本文的研究過程中,形式化驗證的證明覆蓋率為93.96%,功能覆蓋率為100%...
【文章來源】:西安電子科技大學陜西省 211工程院校 教育部直屬院校
【文章頁數(shù)】:85 頁
【學位級別】:碩士
【部分圖文】:
驗證在整個項目周期中的占比[2]
第三章 基于斷言的形式化驗證證結果及覆蓋率分析的覆蓋率分為兩部分,一部分是由形式化驗證工具 rage,COI Coverage,Proof Coverage 和 Bound Cover能覆蓋組,用于統(tǒng)計功能覆蓋率。試模塊的功能相對簡單,因此并沒有對驗證的深度進可以,知道形式化驗證完畢。所以并沒有對 Bound 的結果如圖 3.2,可見總共有 3774 個狀態(tài)被驗證,其接性檢查共檢查了 966 個狀態(tài)。
驗證前定義的功能覆蓋組,用于統(tǒng)計功能覆蓋率。由于多核調試模塊的功能相對簡單,因此并沒有對驗證的深度進行限制,即跑多少個時鐘周期都可以,知道形式化驗證完畢。所以并沒有對 Bound Coverage 進行覆蓋率分析。形式化驗證的結果如圖 3.2,可見總共有 3774 個狀態(tài)被驗證,其中有 9 個狀態(tài)沒有驗證成功。連接性檢查共檢查了 966 個狀態(tài)。圖3.2形式化驗證結果9 個 未 覆 蓋 到 的 狀 態(tài) 名 稱 如 圖 3.3 , 可 見 沒 有 覆 蓋 到 的 狀 態(tài) 均 來 自mon_pulse_pulse2pulse_sync_i 模塊。
【參考文獻】:
期刊論文
[1]Jasper:形式驗證令你快人一步[J]. 梁曉歡. 電腦與電信. 2013(11)
[2]提高SoC硬件系統(tǒng)驗證效率方法的綜述(英文)[J]. 劉強,馬建國. 電子科技大學學報. 2013(02)
[3]系統(tǒng)芯片的混合驗證方法[J]. 韓俊剛. 西安郵電學院學報. 2002(01)
碩士論文
[1]基于SVA功能驗證方法的中斷延遲控制器和GPIO的驗證研究[D]. 馬恒.西安電子科技大學 2015
本文編號:3352878
【文章來源】:西安電子科技大學陜西省 211工程院校 教育部直屬院校
【文章頁數(shù)】:85 頁
【學位級別】:碩士
【部分圖文】:
驗證在整個項目周期中的占比[2]
第三章 基于斷言的形式化驗證證結果及覆蓋率分析的覆蓋率分為兩部分,一部分是由形式化驗證工具 rage,COI Coverage,Proof Coverage 和 Bound Cover能覆蓋組,用于統(tǒng)計功能覆蓋率。試模塊的功能相對簡單,因此并沒有對驗證的深度進可以,知道形式化驗證完畢。所以并沒有對 Bound 的結果如圖 3.2,可見總共有 3774 個狀態(tài)被驗證,其接性檢查共檢查了 966 個狀態(tài)。
驗證前定義的功能覆蓋組,用于統(tǒng)計功能覆蓋率。由于多核調試模塊的功能相對簡單,因此并沒有對驗證的深度進行限制,即跑多少個時鐘周期都可以,知道形式化驗證完畢。所以并沒有對 Bound Coverage 進行覆蓋率分析。形式化驗證的結果如圖 3.2,可見總共有 3774 個狀態(tài)被驗證,其中有 9 個狀態(tài)沒有驗證成功。連接性檢查共檢查了 966 個狀態(tài)。圖3.2形式化驗證結果9 個 未 覆 蓋 到 的 狀 態(tài) 名 稱 如 圖 3.3 , 可 見 沒 有 覆 蓋 到 的 狀 態(tài) 均 來 自mon_pulse_pulse2pulse_sync_i 模塊。
【參考文獻】:
期刊論文
[1]Jasper:形式驗證令你快人一步[J]. 梁曉歡. 電腦與電信. 2013(11)
[2]提高SoC硬件系統(tǒng)驗證效率方法的綜述(英文)[J]. 劉強,馬建國. 電子科技大學學報. 2013(02)
[3]系統(tǒng)芯片的混合驗證方法[J]. 韓俊剛. 西安郵電學院學報. 2002(01)
碩士論文
[1]基于SVA功能驗證方法的中斷延遲控制器和GPIO的驗證研究[D]. 馬恒.西安電子科技大學 2015
本文編號:3352878
本文鏈接:http://sikaile.net/kejilunwen/dianzigongchenglunwen/3352878.html
教材專著