最新形式驗證工具支援在多種特性語言之間轉換

在日前舉行的設計自動化研討會(DAC)上，EDA供應商Averant公司展位前掛著了一幅有牙刷和牙線的宣傳海報，附帶的文字說明牙刷與牙線‘二者並用，效果最佳！’根據該公司主管表示，其用意是要突顯出模擬與形式驗證之間的關係，因為設計師必須同時採用這兩種技術，才能獲得足夠的設計收斂。

“如果你將刷牙看成是隨機模擬。”Averant公司銷售副總裁Larry Lapides說道。就像牙醫開玩笑說你只需要用牙線清潔你還想保有的牙齒一樣，設計師對於希望取得成功的設計也應該使用靜態驗證，Lapides指出。

Averant藉由DAC的推波助瀾，發表其下一代Solidify工具。該工具可以使設計師更佳地控制整個形式驗證過程。Lapides與Averant公司的總裁Ramin Hojati均宣稱，Solidify 4.0是業界首款通過指導驗證的系統，能讓設計師在設計週期早期執行快速‘缺陷搜尋’作業，稍後再做更徹底的聲明檢驗。

“許多時候設計師會產生成千上萬條特性語句，而這在一台電腦上需要一整晚的時間來執行。”Hojati表示，“設計師有時候也真的想知道其中某條屬性語句是否可通過，因而不得不在上面花費很多時間。Solidify工具能讓設計師在確定需要花多少時間方面擁有更大的彈性。”

新工具的增強功能

據Hojati分析，在設計週期早期的缺陷搜尋階段，用戶在一台電腦上處理100條特性語句可能只需數秒時間。稍後當重點轉移到全面徹底的檢驗時，用戶可能需要數天和數台電腦才能完成對這些特性的處理。經由有效地在CPU時間內權衡完成度與精密度之間的關係，Solidify可以提供早期反饋資訊，同時盡可能充分地利用可用運算能力，他指出。

Solidify 4.0還包括其它一些增強功能，例如支援完整的SystemVerilog Assertion(SVA)語言。另外也支援線性SVA的使用、連結指令的驗證IP，以及以SVA所建置的的開放Verilog庫(OVL)，Averant表示。

Hojati和Lapides宣稱，Solidify 4.0還提供另外一項業界首創功能：能夠在SVA、PSL、OVA、OVL和HPL等多種特性語言之間進行轉換。因此，設計團隊就能自由地選擇最能夠滿足所需的特性語言，並實現驗證IP的保存與再使用。

“Solidify 4.0可以讀取四種語言，並輸出四種語言。”Hojati表示，“這點很有價值，可讓用戶對他們的IP安全性更具有信心。”

其它增強功能包括擴展除錯功能和時脈交叉檢查，以及對1.1版PSL的支援，Averant公司表示。Hojati解釋說，擴展除錯功能雖然類似於現有的商用除錯器，但Solidify能讓用戶無須改變他們自己的設計環境。

Solidify現在可以在同一設計中處理各種不同的Verilog描述，還支援Liberty的單元格式。Solidify 4.0可以執行在Linux、Windows和Solaris平台中。Hojati透露，Averant公司“對產品做了少許的重新配置”，增加了類似於模擬中程式碼覆蓋的特性碼覆蓋，據稱這是靜態驗證領域中的創舉。

要得到最佳的完整驗證效果，必須同時使用模擬與形式驗證工具