隨著工藝的高速發展和技術的升級迭代，晶片工業正變得日趨龐大複雜，而這一變化也在深刻地改變著數字晶片的設計。如何在晶片製造成本呈現指數型上升，同時上市時間（Time To Market）爭分奪秒的今天，正確而高效地完成數字前端的工程實施， 對於無論是設計和驗證團隊的管理，還是其中的工程方法學，都提出了艱鉅的挑戰。

在如今的數字晶片前端開發流程中，驗證工程師通常需要在整個研發設計週期，與設計工程師一同通力合作達成目標。在主流的基於動態模擬的方法論中，驗證工程師在初期就需要對驗證框架和環境進行設計和配置，以確保驗證能在專案初期就介入設計流程，在專案早期捕捉問題。

圖1。動態模擬簡例

作為主流的驗證方法，動態模擬手段具有很好的泛用性。但在上圖中我們也可以觀察到這一方法論的缺點：

• 模擬器往往包含多個元件的環境部署，至少包含激勵生成器、驅動、DUT、參照模型、監測、檢查器

• 需要隨機激勵生成器生成激勵，且只能覆蓋較有限的情況

• 依賴參照模型檢驗DUT生成的波形是否符合預期

在過去的三四十年間，隨著形式化驗證的技術的成熟，形式方法越來越多地滲透到了越來越多的驗證場景中。一個典型的形式驗證方法，包含：

• SVA形式規約描述：基於SVA的斷言檔案

• DUT：RTL設計程式碼

• 形式檢查工具：檢查斷言和設計的一致性，生成覆蓋率和功能驗證報告

圖2。形式化驗證簡例

在上圖中我們可以看到，一方面，形式驗證在驗證架構上做了顯著的簡化，這大大地提高了驗證環境搭建的成本和安全性；另一方面，當驗證未透過時，形式化工具提供了很好的反例路徑追溯手段。

除此之外，形式驗證還有一個傳統手段無可比擬的優勢：

不同於模擬方法中的激勵生成+逐次核對的方式，形式驗證在理論上可以覆蓋全體狀態空間，從而從根源上避免了類似奔騰FDIV的高危隱患。

事實上，在那次臭名昭著的漏洞事件之後，英特爾也開始重視並極為廣泛地引入了形式化團隊和工具，為自己的晶片設計驗證提供強有力支援。

對於現如今對安全效能要求越來越高的數字晶片，這一優勢在許多場合無疑是至關重要的。

如果你初次接觸形式化驗證，「遍歷狀態空間」這一特性可能會令人困惑而著迷。

我們來舉一個經典的例子，來說明形式化方法是如何實現這一看似不可能的任務的。考慮一個多元布林函式

f：{0，1}ⁿ → {0，1}， （x_1，。。。x_n） ↦ y

我們嘗試用一種稱為二元決策樹（

BDD

，

B

inary

D

ecision

D

iagram）的資料結構來表示它：

圖片來源：維基百科 二元決策圖

比如在上圖的這個例子中，我們把右側的用列表形式表示的布林函式f，用左邊的二叉樹表示出來。

具體方法為：

1。定義所有布林變數的一個偏序：比如這裡我們定義x_1>x_2>x_3。表現在圖上，x_1出現在第一層作為父節點，x_2出現在第二層，以此類推；

2。確定每個葉節點值：每一條到達葉節點的路徑，對應函式f的一次取值 —— 當路徑從x_i出發後進入其左子樹上時，表示引數x_i取值為0，否則為1。葉節點的值即為函式在這條路徑對應的（x_i）上的取值。

這樣，我們就用一個一棵二叉樹表示了f。現在我們的想法是使用演算法，在保留所有資訊的情況下，對這個圖進行簡化。比如我們可以反覆地使用下面的規則：

1。如果兩個節點是葉節點且具有相同的值，或者是內部節點且具有相同的子節點，則將它們合併；

2。如果從內部節點出發且代表1的邊和代表0的邊指向相同的子節點，則將該節點從圖中刪除，並將其父節點重定向到子節點。

直至這兩條規則無法再被應用，我們最終得到了一個稱為既約偏序二元決策圖（ROBDD，

R

educed

O

rdered

B

inary

D

ecision

D

iagram）的資料結構。在我們的例子中，最終的ROBDD形如下圖：

在許多現實情況下，透過ROBDD這一資料結構，大型邏輯電路對應的布林函式的儲存表示得到了簡化，從而為RTL綜合等流程中的邏輯等價性問題中提供了有力的處理手段。同樣的，在功能屬性驗證問題上，形式方法都採用了各種不同的資料結構和演算法，將狀態空間進行抽象規約，從而在不丟失資訊的情況化簡化和解決問題。

當然，由於狀態爆炸等問題，形式驗證方法在實際使用過程中仍有一些技術和工程限制，目前更多地使用在模組級驗證上。在當前先進的驗證方法學中，形式方法、動態模擬和硬體加速等方法，正在更為積極地產生交融，取長補短，共同為晶片前端驗證提供支援。

目前，望安科技基於k-framework，正著力研發System Verilog語法檢查、功能屬性驗證、資料流安全等功能的晶片形式化驗證APP工具。秉持將領先的形式化技術服務深入服務和支援數字晶片研發的信心，我們歡迎廣大晶片和EDA廠商與我們聯絡溝通，合作共贏，在高速發展的晶片行業中搶佔領先身位。

浙江望安科技有限公司

浙江望安科技有限公司是以“形式化驗證”為核心技術的安全服務及產品提供商。公司致力於為國家重大專案、關鍵系統及行業企業提供安全認證保障。業務覆蓋航空、航天、國防、軌道交通、區塊鏈、物聯網、工業控制、晶片設計製造等重大領域。

公司可提供資訊科技安全評估標準CC EAL1-EAL7級安全保障級別諮詢與技術服務。公司擁有自主研發、自主智慧財產權的覆蓋軟體全生命週期的望安形式化驗證平臺W-AVC、符合CC認證體系的標準化實施平臺系統W-CaaS等重要核心資產。核心技術已應用於C919國產大飛機、載人航天工程、中航工業集團、航天科技集團、元心科技、中國移動、小米科技等，已覆蓋相對廣泛的合作領域和企業。

TAG: 驗證節點晶片形式化設計