電子發(fā)燒友網(wǎng)>電子資料下載>可編程邏輯>FPGA/ASIC>FPGA形式驗(yàn)證工具Questa Formal產(chǎn)品比較

FPGA形式驗(yàn)證工具Questa Formal產(chǎn)品比較

1683909 2014-06-11 | doc | 0KB | 次下載 | 10積分

資料介紹

同類(lèi)產(chǎn)品主要廠家主要有Averant、Cadence. 其相關(guān)產(chǎn)品對(duì)應(yīng)為Solidify、IFV。Solidify是Averant公司的形式驗(yàn)證分析工具，主要針對(duì)小型設(shè)計(jì)進(jìn)行模塊級(jí)的靜態(tài)形式驗(yàn)證，支持的設(shè)計(jì)容量有限。IFV是Cadence公司的形式驗(yàn)證分析工具，支持中小型設(shè)計(jì)的形式驗(yàn)證分析，但僅支持NC仿真器用戶(hù)。

序號(hào) 型號(hào)及生產(chǎn)廠比較項(xiàng)目（型號(hào)）v10.0a （型號(hào)）v5.1.0 （型號(hào)）v8.1

（廠家）Mentor Graphics （廠家）Averant （廠家）Cadence

從以上三家的產(chǎn)品來(lái)做比較，Mentor公司的產(chǎn)品具有更多的優(yōu)勢(shì)，體現(xiàn)在如下方面：

Averant相對(duì)于Mentor、Cadence是一個(gè)小型的EDA公司，其產(chǎn)品的應(yīng)用客戶(hù)非常有限，因此對(duì)于航空航天可靠性要求高的設(shè)計(jì)場(chǎng)合，說(shuō)服力不強(qiáng)，同時(shí)從以上的表格所列出的比較項(xiàng)目上可以看出，其產(chǎn)品能力較弱，不適合復(fù)雜的大規(guī)模FPGA設(shè)計(jì)的驗(yàn)證，而且由于缺乏良好的調(diào)試手段，因此不易于使用；

Mentor 具有完整的形式驗(yàn)證解決方案，可以將靜態(tài)Formal應(yīng)用于模塊級(jí)，動(dòng)態(tài)Formal應(yīng)用于芯片級(jí)。而Cadence只有靜態(tài)Formal. 對(duì)于復(fù)雜的大型設(shè)計(jì)，僅采用靜態(tài)形式驗(yàn)證會(huì)有驗(yàn)證深度的限制，而利用動(dòng)態(tài)形式驗(yàn)證則可以很好地?cái)U(kuò)大驗(yàn)證深度，發(fā)現(xiàn)更深層次的設(shè)計(jì)bug，因此動(dòng)態(tài)形式驗(yàn)證可以支持芯片級(jí)的設(shè)計(jì)驗(yàn)證，有更好的設(shè)計(jì)容量的支持；

Questa形式驗(yàn)證工具具有良好的圖形化的界面，跟Questa非常相似，因此對(duì)于用過(guò)Questa的工程師來(lái)說(shuō)，交互界面極易操作。與此同時(shí)，我所已經(jīng)購(gòu)買(mǎi)了Mentor公司的Questa工具，因而購(gòu)買(mǎi)Mentor公司的Questa形式驗(yàn)證產(chǎn)品更有利；

Mentor Questa形式驗(yàn)證工具內(nèi)嵌Questa仿真器，無(wú)需考慮和仿真工具的連接問(wèn)題；

Mentor Questa形式驗(yàn)證工具支持PSL、SVA、OVL、QVL、CheckWare全部標(biāo)準(zhǔn)斷言形式，因此無(wú)論驗(yàn)證工程師采用何種語(yǔ)言都可以利用Questa Formal進(jìn)行驗(yàn)證，而Cadence與Averant公司的產(chǎn)品對(duì)PSL語(yǔ)言的支持很弱，因此應(yīng)用會(huì)有局限性。同時(shí)，Questa Formal豐富的斷言IP庫(kù)是Cadence與Averant公司無(wú)法比擬的，這些斷言IP庫(kù)使得形式驗(yàn)證的斷言設(shè)計(jì)變得更為簡(jiǎn)單，減少了驗(yàn)證工程師的工作量與人為編寫(xiě)斷言可能引入的錯(cuò)誤；

Mentor Questa形式驗(yàn)證工具支持最全面的驗(yàn)證策略。其中，測(cè)試平臺(tái)排序(testbench ranking)和斷言密度(Assertion Density)是Cadence與Averant所不具備的。通過(guò)testbench排序，設(shè)計(jì)者可以清楚地判定哪一個(gè)testbench最為有效，同時(shí)還可得到每一個(gè)testbench所覆蓋范圍的交集等信息。另外，斷言密度可以使得設(shè)計(jì)者明確地知道設(shè)計(jì)中哪些模塊的斷言是不全面的。借助于這兩個(gè)策略，可以指導(dǎo)驗(yàn)證計(jì)劃的進(jìn)一步完善；

由于Mentor Questa工具中有統(tǒng)一的覆蓋率數(shù)據(jù)庫(kù)UCDB機(jī)制保證所有仿真驗(yàn)證過(guò)程產(chǎn)生的覆蓋率信息可以很好地被分析，而形式驗(yàn)證本身是對(duì)仿真驗(yàn)證的補(bǔ)充，因此如何將形式驗(yàn)證環(huán)節(jié)所產(chǎn)生的驗(yàn)證覆蓋率數(shù)據(jù)與Questa仿真驗(yàn)證過(guò)程中產(chǎn)生的覆蓋率數(shù)據(jù)統(tǒng)一進(jìn)行分析成為發(fā)現(xiàn)驗(yàn)證漏洞的關(guān)鍵點(diǎn)。由于Questa形式驗(yàn)證工具可以很好地與Questa等主流仿真器相結(jié)合，因此可以很好地實(shí)現(xiàn)測(cè)試覆蓋率數(shù)據(jù)的合并、排序，從而統(tǒng)一地分析所有測(cè)試結(jié)果，更快地發(fā)現(xiàn)驗(yàn)證漏洞。