形式驗證（Formal Verification）是一種IC設計的驗證方法，它的主要思想是通過使用形式證明的方式來驗證一個設計的功能是否正確。形式驗證可以分為三大類：等價性檢查（Equivalence Checking）、形式模型檢查（Formal Model Checking）（也被稱作特性檢查）和定理證明(Theory Prover)?。

　　等價性檢查的驗證用于驗證RTL設計與門級網(wǎng)表、門級網(wǎng)表與門級網(wǎng)表是否一致。在進行掃描鏈重排、時鐘樹綜合等過程中，都可以用等價性檢查保證網(wǎng)表的一致性。等價性檢查已經(jīng)融入IC標準設計流程中。等價性檢查在檢查ECO時非常有用。例如，設計者在修改門級網(wǎng)表時，由于手誤，錯將一個或門寫成或非門，等價性檢查工具通過比較RTL設計與門級網(wǎng)表，可以很容易地發(fā)現(xiàn)這種錯誤。

　　模型檢查用時態(tài)邏輯來描述規(guī)范，通過有效的搜索方法來檢查給定的系統(tǒng)是否滿足規(guī)范。模型檢查是目前研究的熱點，但其驗證的電路規(guī)模受限制這一問題還沒有得到很好的解決。

　　定理證明把系統(tǒng)與規(guī)范都表示成數(shù)學邏輯公式，從公理出發(fā)尋求描述。定理證明驗證的電路模型不受限制，但需要使用者的人工干預和較多的背景知識。

在當前復雜的數(shù)字設計開發(fā)過程中，功能驗證十分重要。雖然硬件的復雜度仍遵循摩爾定律持續(xù)增長，但是驗證的復雜性更具挑戰(zhàn)。事實上，隨著硬件復雜性隨時間呈雙指數(shù)增長，驗證復雜性理論上也呈指數(shù)增長。驗證已被公認為是設計過程中的主要瓶頸：高達70%的設計開發(fā)時間和資源花在功能驗證上。Collett International Research認為，即使在驗證上花費如此巨大的精力和資源，功能性缺陷仍是芯片重新流片的頭號原因。

　　功能性驗證挑戰(zhàn)

　　邊際情形(corner-case)的缺陷是仿真偽像，由于以仿真為基礎(chǔ)的驗證具有非窮盡的固有特性，因此邊際情形無法被檢測到。事實上，不管你用多少時間仿真，也不管你的測試平臺和發(fā)生器有多么智能，通過仿真驗證設計意圖對于最小電路以外的所有電路來說都是不完整的。基本的仿真?zhèn)蜗窨梢员环殖扇悾焊F盡型、可控型和可觀察型，如下表1所示。

　　形式驗證是一個系統(tǒng)性的過程，將使用數(shù)學推理來驗證設計意圖(指標)在實現(xiàn)(RTL)中是否得以貫徹。形式驗證可以克服所有3種仿真挑戰(zhàn)(表1)，因為形式驗證能夠從算法上窮盡檢查所有隨時間可能變化的輸入值。換句話說，沒有必要表明如何激勵設計或創(chuàng)建多種條件來實現(xiàn)較高的可觀察性。

　　雖然從理論上講，仿真測試平臺的輸入端口針對待驗證設計(DUV)具有較高的可控性，但測試平臺對內(nèi)部點的可控性一般較差。為了使用基于仿真的方法識別設計錯誤，以下條件必須保持：

　　* 必須產(chǎn)生正確的輸入激勵，以激活(也就是敏感化)設計中某個點的缺陷

　　* 必須產(chǎn)生正確的輸入激勵，以便將源自缺陷的所有效果傳送到輸出端口

　　在使用基于仿真的驗證時，需要規(guī)劃設計中需要驗證的對象：

　　* 定義需要測試的各種輸入條件

　　* 創(chuàng)建功能性覆蓋模型(確定是否做了足夠的仿真)

　　* 搭建測試平臺(檢查器，測試樁，發(fā)生器等)

　　* 創(chuàng)建特定的直接測試

　　* 成年累月的仿真

　　現(xiàn)實中，工程師一直在反復做著這些事：運行測試、調(diào)試故障、再次仿真回歸組、觀察各種覆蓋率指標，以及調(diào)整激勵(例如操控輸入發(fā)生器)以覆蓋以前未覆蓋的設計部分。

　　這里我們討論一個彈性緩存例子(見圖1)。數(shù)據(jù)可以在時鐘域間改變，能夠根據(jù)兩個時鐘之間的相位和頻率偏移做出調(diào)整。數(shù)據(jù)必須無損地通過彈性緩存進行傳送，即使在設計允許時鐘不完全同步的情況下。在這個案例中的一個功能性缺陷例子是在時鐘有效沿對齊時由于數(shù)據(jù)的變化而出現(xiàn)的緩存溢出。這就可能要求對所有可能的輸入條件進行大量的仿真和考慮，以建模和仿真這種錯誤行為。

　　圖1：彈性緩存框圖

　　高層要求

　　許多公司已經(jīng)采用基于斷言的驗證(ABV)技術(shù)來縮短驗證時間，同時改進他們的整體驗證工作。然而，一般采用的ABV專注于局部的、在仿真中使用的RTL實現(xiàn)相關(guān)斷言。所有內(nèi)部斷言的匯聚不會表征或完整規(guī)定微架構(gòu)定義的那種模塊的端到端行為。此外，當設計實現(xiàn)改變時，這些局部性斷言不能重復使用。換句話說，通過端到端屬性(包括數(shù)據(jù)完整性和包順序)和規(guī)定模塊必需的黑箱行為，高層斷言(我們在本文中指高層要求)提供高得多的設計功能覆蓋率，并且能在各種設計實現(xiàn)和多個項目之間重復使用。更重要的是，通過形式性驗證模塊的高層要求集，可以使驗證完整性和產(chǎn)能得到顯著提高。因此，高層形式驗證無需模塊級仿真，可極大地縮短系統(tǒng)級驗證時間。讓我們詳細地看看圖2所示的高層要求。

　　圖2：要求與RTL斷言對比。

　　Y軸代表抽取層，X軸代表被某個特殊斷言或要求覆蓋的設計數(shù)量。沿Y軸越往上走，被高層要求覆蓋的設計空間就越大。證實這些高層要求具有很高價值，原因有很多：

　　1. 高層要求關(guān)系到微架構(gòu)中的要求

　　2. 高層要求關(guān)系到測試平臺中的輸出檢查器組

　　3. 高層要求覆蓋了與工程師想要寫入的數(shù)百條較低層斷言相同的設計空間

　　4. 高層要求覆蓋了由于工程師遺漏的較低層斷言的缺失而未被覆蓋的設計空間

　　最后一點我們這里舉個例子，假如設計包含一個FIFO，并且工程師忘了編寫一個斷言來檢查FIF從不下溢。這種安全性違例將由高層要求加以識別。然而，通過形式性地驗證高層要求，高層要求違例的根源就能得以跟蹤。例如，如果針對高層要求在影響錐中包含了FIFO，那么導致高層要求不能滿足的下溢條件將被檢測到。

　　理想的形式驗證工具要求具有一定的規(guī)模，以便窮盡地檢查所有可能的輸入條件以及設計中任意點的可控性和可視性(見表1)。我們的旗艦產(chǎn)品，例如JasperGold，就采用了高性能和大規(guī)模的形式驗證技術(shù)，能夠窮盡地驗證模塊是否滿足源自微架構(gòu)的高層要求。這款產(chǎn)品使用數(shù)學算法，因為不需要使用仿真測試平臺或激勵。

　　表1：仿真與形式驗證的比較

　　本文小結(jié)

　　形式驗證要求你以不同的方式思考。例如，仿真是完全經(jīng)驗主義的做法，也就是說，你通過反復試驗試圖查明缺陷，這要花相當多的時間嘗試所有可能的組合，因此永遠不會完整。另外，由于工程師必須定義和產(chǎn)生大量輸入條件，他們的工作重點將是如何在非設計目標基礎(chǔ)上分解設計。另一方面，形式驗證是窮盡式數(shù)學技術(shù)，允許工程師僅關(guān)注設計意圖，或“什么是設計的正確行為?”。

　　驗證實現(xiàn)工作包括將多種輸入條件定義為測試計劃的一部分、創(chuàng)建功能覆蓋模型、開發(fā)測試平臺、創(chuàng)建輸入激勵發(fā)生器、編寫指導性測試以及執(zhí)行測試、分析覆蓋率指標、調(diào)整激勵發(fā)生器以面向未驗證的設計部分，然后反復這一過程。純形式驗證技術(shù)則相反，專注于證實模塊的端到端、直接對應微架構(gòu)規(guī)范的高層要求，幫助用戶戲極大提高項目的設計和驗證產(chǎn)能，同時確保正確性。