Mentor Graphics增強(qiáng)Questa基于自動(dòng)化驗(yàn)證解決方案的形式驗(yàn)證的容量、性能和廣度。

2014年5月20日,俄勒岡州威爾遜維爾——先進(jìn)系統(tǒng)驗(yàn)證解決方案的領(lǐng)導(dǎo)者M(jìn)entor Graphics(Nasdaq:MENT)今天宣布推出形式驗(yàn)證的自動(dòng)化解決方案Mentor®組合中的最新產(chǎn)品Questa® PropGen以及Questa產(chǎn)品先進(jìn)形式引擎的增強(qiáng)容量及性能，其構(gòu)成了整個(gè)自動(dòng)化解決方案家族。

自動(dòng)化針對(duì)性解決方案

全自動(dòng)針對(duì)性驗(yàn)證解決方案使驗(yàn)證功能大幅提高，大大節(jié)省了工程時(shí)間的人月數(shù)及昂貴的再流片成本。這實(shí)現(xiàn)了對(duì)使用其他驗(yàn)證方法難以或無(wú)法進(jìn)行驗(yàn)證特定設(shè)計(jì)的完整性和驗(yàn)證的準(zhǔn)確性。Questa PropGen是該解決方案組合中最新的方案，有助于驗(yàn)證團(tuán)隊(duì)通過(guò)自動(dòng)化基于斷言的驗(yàn)證(ABV)過(guò)程使復(fù)雜SoC達(dá)到更高質(zhì)量。

“Mentor的形式驗(yàn)證技術(shù)在許多領(lǐng)域增強(qiáng)了我們傳統(tǒng)的驗(yàn)證流程，”三星半導(dǎo)體公司系統(tǒng)大規(guī)模集成部首席工程師NamDo Kim說(shuō)。“為了提高生產(chǎn)效率及設(shè)計(jì)質(zhì)量，我們已經(jīng)成功地利用了從全自動(dòng)形式驗(yàn)證到屬性檢查的廣泛的Questa應(yīng)用。”

傳統(tǒng)上，驗(yàn)證工程師一直依賴于設(shè)計(jì)人員主動(dòng)將斷言添加至代碼中。遺憾的是，編寫(xiě)此類(lèi)斷言所需要的精力和時(shí)間往往會(huì)阻止設(shè)計(jì)人員寫(xiě)出驗(yàn)證團(tuán)隊(duì)所需的斷言。 Questa PropGen通過(guò)利用其現(xiàn)有測(cè)試環(huán)境將驗(yàn)證團(tuán)隊(duì)視為駕馭者來(lái)自動(dòng)生成屬性。項(xiàng)目團(tuán)隊(duì)可借助Questa PropGen工具在其SoC仿真和硬件加速環(huán)境中體驗(yàn)基于屬性的驗(yàn)證(ABV)的所有功能，而無(wú)需耗時(shí)的手動(dòng)斷言編碼。

Questa Formal(形式化驗(yàn)證)引擎的性能和容量的飛躍

Questa Formal獨(dú)創(chuàng)的新形式驗(yàn)證引擎在棘手驗(yàn)證問(wèn)題方面提供了業(yè)界領(lǐng)先水平的性能。此類(lèi)引擎為Questa整套產(chǎn)品全自動(dòng)形式驗(yàn)證解決方案和形式驗(yàn)證強(qiáng)大的應(yīng)用提供了動(dòng)力。Questa Formal引擎的增強(qiáng)實(shí)現(xiàn)了整個(gè)自動(dòng)化解決方案的性能改進(jìn)，包括跨時(shí)鐘域(CDC)簽收的業(yè)界標(biāo)準(zhǔn)解決方案Questa CDC 驚人的6倍提升。為補(bǔ)充全方位驗(yàn)證技術(shù)，Questa Formal解決方案和引擎在最近宣布的Mentor 企業(yè)級(jí)驗(yàn)證平臺(tái)中還實(shí)現(xiàn)了仿真和硬件加速的緊密結(jié)合，以便使驗(yàn)證團(tuán)隊(duì)能以高水準(zhǔn)的質(zhì)量更有效地實(shí)現(xiàn)其總驗(yàn)證目標(biāo)。

“形式驗(yàn)證正在成為主流，并且技術(shù)仍在快速發(fā)展，”Oski Technology總裁兼首席執(zhí)行官Vigyan Singhal說(shuō)，“新發(fā)布的Questa Formal引擎所取得的結(jié)果給我們留下了深刻印象。在客戶項(xiàng)目上，我們已看到大幅提升了容量，拓寬了可解決問(wèn)題的范圍。”