在近期舉行的設(shè)計自動化研討會(DAC)上,私人控股的EDA供應(yīng)商Averant公司展位前掛出了一幅含有牙刷和牙線的宣傳畫,附帶的文字說明是“牙刷牙線并用,效果才會最佳。”該公司的高層表示,其寓意是要突出仿真與形式驗(yàn)證之間的關(guān)系。該公司認(rèn)為,設(shè)計師需要同時采用這兩種技術(shù),才能獲得足夠的設(shè)計收斂。

“你可以把刷牙看成是隨機(jī)仿真。”Averant公司銷售副總裁Larry Lapides說道。就像牙醫(yī)說笑應(yīng)該只清潔你想保留的牙齒一樣,設(shè)計師也應(yīng)該只對希望取得成功的設(shè)計進(jìn)行靜態(tài)驗(yàn)證,Lapides指出。

Averant借助DAC的東風(fēng),推出了下一代Solidify工具。該工具可以使設(shè)計師更好地控制整個形式驗(yàn)證過程。Lapides及Averant公司總裁Ramin Hojati宣稱,Solidify 4.0是業(yè)界首個經(jīng)過指導(dǎo)驗(yàn)證的系統(tǒng),能讓設(shè)計師在設(shè)計周期早期執(zhí)行快速“缺陷搜尋”操作,稍后再做更徹底的斷言檢驗(yàn)。

“許多時候設(shè)計師會生成成千上成萬條特性語句,在一臺計算機(jī)上需要運(yùn)行一整晚的時間。”Hojati表示,“設(shè)計師有時候也真的想知道某條屬性語句是否馬上要通過,從而不得不在上面花費(fèi)很多時間。Solidify工具能讓設(shè)計師在確定需要花多少時間方面擁有更大的靈活性。”

新工具的增強(qiáng)功能

據(jù)Hojati分析,在設(shè)計周期早期的缺陷搜尋階段,用戶在一臺計算機(jī)上處理100條特性語句可能只需數(shù)秒時間。稍后當(dāng)重點(diǎn)轉(zhuǎn)移到全面徹底的檢驗(yàn)時,用戶可能需要數(shù)天和數(shù)臺計算機(jī)才能完成對這些特性的處理。通過有效地權(quán)衡完成度與精度和CPU時間之間的關(guān)系,Solidify可以提供早期反饋信息,同時盡可能充分地利用可用計算能力,他指出。

Solidify 4.0還包括其它一些增強(qiáng)功能,例如支持完整的SystemVerilog Assertion(SVA)語言。另外也支持在線SVA的使用、通過綁定命令連接的驗(yàn)證知識產(chǎn)權(quán)(IP)以及用SVA實(shí)現(xiàn)的開放式Verilog庫(OVL),Averant表示。

Hojati和Lapides宣稱,Solidify 4.0還提供另外一項(xiàng)業(yè)界首創(chuàng)功能:能夠在包括SVA、PSL、OVA、OVL和HPL在內(nèi)的多個特性語言之間進(jìn)行轉(zhuǎn)換。這樣,設(shè)計團(tuán)隊(duì)就能自由地選擇能夠最佳地滿足他們需要的特性語言,還能實(shí)現(xiàn)驗(yàn)證IP的保存與復(fù)用。

“Solidify 4.0可以讀取四種語言,輸出四種語言。”Hojati表示,“這點(diǎn)很有價值。用戶可以對他們的IP安全性更加自信。”

其它增強(qiáng)功能包括擴(kuò)展調(diào)試功能和時鐘交叉檢查以及對1.1版PSL的支持,Averant公司表示。Hojati解釋說,擴(kuò)展調(diào)試功能雖然類似于已有的商用調(diào)試器,但Solidify能讓用戶無須轉(zhuǎn)離他們自己的設(shè)計環(huán)境。

Solidify現(xiàn)在可以在同一設(shè)計中處理各種混合的Verilog描述,還支持Liberty的單元格式。Solidify 4.0可以運(yùn)行在Linux、Windows和Solaris平臺。Hojati透露,Averant公司“對產(chǎn)品做了少許的重新配置”,增加了類似于仿真中代碼覆蓋的特性代碼覆蓋,據(jù)稱這是靜態(tài)驗(yàn)證領(lǐng)域中的獨(dú)創(chuàng)之舉。

Lapides認(rèn)為,由于人們對形式驗(yàn)證在什么地方適合總體驗(yàn)證方法學(xué)有誤解,致使形式驗(yàn)證工具市場的發(fā)展受到了阻礙。“驗(yàn)證方法學(xué)確實(shí)在向覆蓋驗(yàn)證發(fā)展,總體目標(biāo)是100%的功能覆蓋。”Lapides表示,“雖然人們明白缺陷搜尋越早越好,但對于獨(dú)立工具而言卻屬于次要價值。”

作者:麥戴倫