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

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

介紹便攜式覆蓋

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

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

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

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

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

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

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

審核編輯：郭婷