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

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

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

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

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

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

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

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

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

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

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

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

作者:麥戴倫