近日，西門子數(shù)字化工業(yè)軟件與總部位于倫敦的Azini Capital簽訂了收購OneSpin Solution的協(xié)議， OneSpin Solutions 是一家領(lǐng)先的形式驗(yàn)證軟件供應(yīng)商，致力于幫助用戶確保集成電路(IC)的完整性，實(shí)現(xiàn)功能正確、安全、可信且可靠的IC設(shè)計(jì)。隨著OneSpin solution的加入，為西門子帶來功能強(qiáng)大的IC完整性驗(yàn)證解決方案和卓越的技術(shù)知識(shí)，以及廣泛的自動(dòng)化形式驗(yàn)證應(yīng)用組合。

為了更進(jìn)一步服務(wù)客戶，助力客戶提高驗(yàn)證效率，從而充滿信心地應(yīng)對(duì)快速變化的應(yīng)用領(lǐng)域。2021年9月24日，西門子旗下EDA產(chǎn)品OneSpin與客戶相會(huì)云端，帶來獨(dú)有的Quantify驗(yàn)證解決方案。

根據(jù)相關(guān)數(shù)據(jù)研究表明，缺乏較好的驗(yàn)證覆蓋率指標(biāo)，項(xiàng)目后期的bug會(huì)帶來災(zāi)難性的后果，預(yù)計(jì)將產(chǎn)生10倍-1000倍的損失。了解驗(yàn)證覆蓋率對(duì)于滿足IC完整性標(biāo)準(zhǔn)是至關(guān)重要的，然而將傳統(tǒng)的基于設(shè)計(jì)代碼在仿真過程中被激活的普通覆蓋率測(cè)量（Activation)作為唯一的質(zhì)量指標(biāo)是遠(yuǎn)遠(yuǎn)不夠的，不精準(zhǔn)的測(cè)量將最終導(dǎo)致驗(yàn)證質(zhì)量嚴(yán)重不佳。

OneSpin的Quantify解決方案為形式驗(yàn)證提供了精確、準(zhǔn)確的驗(yàn)證覆蓋率測(cè)量，是市場(chǎng)上獨(dú)樹一幟的高精確度、卓越性能解決方案。一般來說，Quantify提供：

空前的覆蓋精度，擁有專利的觀察覆蓋算法

與仿真的一鍵式集成，用于可達(dá)性分析和測(cè)試向量的生成

指導(dǎo)測(cè)試開發(fā)，對(duì)斷言質(zhì)量和驗(yàn)證漏洞進(jìn)行即時(shí)反饋

業(yè)界公認(rèn)的驗(yàn)證sign-off分析并與覆蓋率數(shù)據(jù)庫的集成。

Quantify解決方案采用“基于變異的覆蓋分析方法”，可以評(píng)估一組斷言被設(shè)計(jì)代碼中不正確行為觸發(fā)的有效性，同時(shí)還可以分析仿真和形式驗(yàn)證流程中設(shè)計(jì)結(jié)構(gòu)的可及性，檢查代碼是否已經(jīng)被激發(fā)或確定未被激發(fā)的原因，有效提升驗(yàn)證工程師的工作效率。

并且Quantify解決方案，采用簡(jiǎn)化的使用模式，無需改變代碼，就可快速評(píng)估驗(yàn)證進(jìn)度，并指導(dǎo)測(cè)試改進(jìn)指令，自動(dòng)檢測(cè)無法到達(dá)和冗余的代碼，增強(qiáng)了分析效果。與此同時(shí)，Quantify還可有效集成如西門子EDA的驗(yàn)證仿真工具，不受驗(yàn)證工具的影響與限制，是市場(chǎng)上獨(dú)有的解決方案。

Quantify也用于測(cè)量正式和基于仿真的驗(yàn)證環(huán)境的可達(dá)覆蓋率，在這種模式下，Quantify得以測(cè)試設(shè)計(jì)代碼中可能無法到達(dá)的領(lǐng)域, 通常也是問題所在區(qū)域。例如：與設(shè)計(jì)階段輸入斷開的死代碼或冗余代碼，Quantify將評(píng)估過度約束的測(cè)試環(huán)境，指示可能未測(cè)試的代碼區(qū)域。即使代碼得以到達(dá)，Quantify也將評(píng)估代碼是否在驗(yàn)證過程中實(shí)際到達(dá)?？蛇_(dá)性和觀察覆蓋率的結(jié)合為驗(yàn)證結(jié)束提供了準(zhǔn)確的衡量標(biāo)準(zhǔn)。