Mentor Graphics公司強(qiáng)化其Questa工具，提升自動(dòng)化功能以擴(kuò)展用于芯片設(shè)計(jì)的涵蓋范圍，并簡(jiǎn)化形式驗(yàn)證技術(shù)。另一方面，此次的功能升級(jí)目標(biāo)也在于使形式驗(yàn)證工具能更廣泛地被采用。

根據(jù)2010年的一項(xiàng)研究報(bào)告指出，只有29%的芯片設(shè)計(jì)師采用形式驗(yàn)證工具。“因而對(duì)于采用這些技術(shù)，仍存在一個(gè)巨大的成長(zhǎng)商機(jī)，”Mentor首席科學(xué)家兼形式驗(yàn)證專家Harry Foster說(shuō)。

業(yè)界確實(shí)需要更好的測(cè)試驗(yàn)證工具。根據(jù)2007年和2010年的調(diào)查顯示，約有65%的芯片設(shè)計(jì)專案仍落后于預(yù)訂計(jì)劃，而大約有70%的設(shè)計(jì)還需重新設(shè)計(jì)。

“如果得再重新設(shè)計(jì)，你可能會(huì)完全錯(cuò)過(guò)上市時(shí)機(jī)，”Foster強(qiáng)調(diào)，一項(xiàng)設(shè)計(jì)工作可能耗時(shí)3個(gè)多月，且花費(fèi)上百萬(wàn)美元。

Mentor公司新的Questa CoverCheck可自動(dòng)發(fā)現(xiàn)無(wú)法進(jìn)行形式驗(yàn)證的程式碼。它還能顯示波形，并產(chǎn)生輸出向量。阿爾卡特朗訊(Alcatel-Lucent)也協(xié)助Mentor共同開發(fā)程式碼。

此外，最新版Questa AutoCheck支持平行機(jī)制更快速執(zhí)行于多核心處理器上。該工具還能自動(dòng)化查找常見錯(cuò)誤的程序，如在模擬時(shí)通常難以偵測(cè)到的資源鎖死(deadlock)和溢位(overflow)等問(wèn)題。

Mentor并擴(kuò)展Questa CDC工具，可用于發(fā)現(xiàn)SoC中使用IP模組與其它同步模組導(dǎo)致的時(shí)域交叉問(wèn)題。在這一功能方面，該新版本提升了5倍的性能。

“目前最大的測(cè)試問(wèn)題之一就發(fā)生在SoC整合中，”他說(shuō)。

他指出，從2007-2010年形式驗(yàn)證工具應(yīng)用已成長(zhǎng)了53%。“由于設(shè)計(jì)越來(lái)越復(fù)雜，業(yè)界必須采用更先進(jìn)的工具，”他說(shuō)。

“目前的工具所能處理的性能已顯著提升了-形式驗(yàn)證工具已能處理成千上百種狀態(tài)元素──但這是永遠(yuǎn)不夠的，所以隨時(shí)還得搭配模擬操作，”Foster說(shuō)。