深層解析形式驗證

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

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

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

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

　　功能性驗證挑戰

　　邊際情形(corner-case)的缺陷是仿真偽像，由于以仿真為基礎的驗證具有非窮盡的固有特性，因此邊際情形無法被檢測到。事實上，不管你用多少時間仿真，也不管你的測試平臺和發生器有多么智能，通過仿真驗證設計意圖對于最小電路以外的所有電路來說都是不完整的。基本的仿真偽像可以被分成三類：窮盡型、可控型和可觀察型，如下表1所示。

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

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

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

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

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

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

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

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

　　* 創建特定的直接測試

　　* 成年累月的仿真

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

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

　　圖1：彈性緩存框圖

　　高層要求

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

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

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

　　1. 高層要求關系到微架構中的要求

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

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

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

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

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

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

　　本文小結

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

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