OneSpin Solutions的PortableCoverage，這是第一個(gè)與所有主要模擬器、覆蓋數(shù)據(jù)庫和查看器以及芯片設(shè)計(jì)驗(yàn)證規(guī)劃工具集成的形式驗(yàn)證解決方案，使用戶能夠選擇他們選擇的供應(yīng)商或多個(gè)供應(yīng)商。

“仿真和形式驗(yàn)證對于我們的芯片設(shè)計(jì)驗(yàn)證策略至關(guān)??重要，”博世傳感器技術(shù)公司的驗(yàn)證專家 Thomas Klotz 說?！拔覀冃枰掷m(xù)評估整體驗(yàn)證進(jìn)度，以確定下一步并根據(jù)我們的時(shí)間表衡量進(jìn)度。OneSpin 的 PortableCoverage 在開放式驗(yàn)證流程中為我們提供了這種能力，因此我們可以使用來自多個(gè)供應(yīng)商的一流工具。”

介紹便攜式覆蓋

“形式驗(yàn)證現(xiàn)在是主流流程的一部分，并被許多驗(yàn)證工程師使用，因此它必須與基于仿真的工具集成，”O(jiān)neSpin Solutions 總裁兼首席執(zhí)行官 （CEO） Raik Brinkmann 博士評論道?！肮こ處熜枰獜?qiáng)大、靈活的流程來快速滿足新要求。OneSpin 的 PortableCoverage 提供了將形式無縫集成到高效、面向未來的驗(yàn)證流程中的自由?！?/p>

PortableCoverage 支持形式和模擬的集成，以實(shí)現(xiàn)精確、定量的驗(yàn)證評估和驗(yàn)證進(jìn)度的全面視圖。這最大限度地減少了正式工作和模擬工作之間的重疊，從而減少了整體驗(yàn)證工作。PortableCoverage 在覆蓋率數(shù)據(jù)庫中集成了正式和模擬覆蓋率指標(biāo)，以統(tǒng)一查看覆蓋率狀態(tài)。

兩個(gè)新的正式應(yīng)用程序，驗(yàn)證覆蓋率集成 （VCI） 應(yīng)用程序和覆蓋率關(guān)閉加速器 （CCA） 應(yīng)用程序，使這成為可能。一旦 VCI 應(yīng)用程序?qū)?OneSpin 的 Quantify 覆蓋率指標(biāo)添加到用戶的覆蓋率數(shù)據(jù)庫中，覆蓋率查看器就會顯示集成的形式和模擬指標(biāo)，從而提供覆蓋率狀態(tài)的統(tǒng)一視圖。

CCA 應(yīng)用程序可識別無法到達(dá)的覆蓋點(diǎn)并將其提供給模擬器，從而加速覆蓋范圍的關(guān)閉，同時(shí)消除試圖命中無法到達(dá)的覆蓋點(diǎn)的浪費(fèi)精力。

PortableCoverage 還包括 OneSpin 的驗(yàn)證計(jì)劃集成 （VPI） 應(yīng)用程序，該應(yīng)用程序?qū)?OneSpin 工具的正式結(jié)果注釋到驗(yàn)證計(jì)劃中。集成的形式和模擬結(jié)果提供了驗(yàn)證計(jì)劃的全面視圖。它還通過提供跟蹤驗(yàn)證結(jié)果與設(shè)計(jì)規(guī)范的鏈接來確保工程師滿足嚴(yán)格的安全標(biāo)準(zhǔn)。

Quantify App 使用正式的基于模型的變異覆蓋來準(zhǔn)確評估斷言質(zhì)量和完整性。覆蓋數(shù)據(jù)可以與傳統(tǒng)的結(jié)構(gòu)覆蓋度量集成。

OneSpin 的所有應(yīng)用程序都利用了 OneSpin 360 DV-Inspect 和 OneSpin 360 DV-Verify 產(chǎn)品提供的形式驗(yàn)證技術(shù)。

審核編輯：郭婷