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

為了更進一步服務客戶，助力客戶提高驗證效率，從而充滿信心地應對快速變化的應用領域。2021年9月24日，西門子旗下EDA產品OneSpin與客戶相會云端，帶來獨有的Quantify驗證解決方案。

根據相關數據研究表明，缺乏較好的驗證覆蓋率指標，項目后期的bug會帶來災難性的后果，預計將產生10倍-1000倍的損失。了解驗證覆蓋率對于滿足IC完整性標準是至關重要的，然而將傳統的基于設計代碼在仿真過程中被激活的普通覆蓋率測量（Activation)作為唯一的質量指標是遠遠不夠的，不精準的測量將最終導致驗證質量嚴重不佳。

OneSpin的Quantify解決方案為形式驗證提供了精確、準確的驗證覆蓋率測量，是市場上獨樹一幟的高精確度、卓越性能解決方案。一般來說，Quantify提供：

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

與仿真的一鍵式集成，用于可達性分析和測試向量的生成

指導測試開發，對斷言質量和驗證漏洞進行即時反饋

業界公認的驗證sign-off分析并與覆蓋率數據庫的集成。

Quantify解決方案采用“基于變異的覆蓋分析方法”，可以評估一組斷言被設計代碼中不正確行為觸發的有效性，同時還可以分析仿真和形式驗證流程中設計結構的可及性，檢查代碼是否已經被激發或確定未被激發的原因，有效提升驗證工程師的工作效率。

并且Quantify解決方案，采用簡化的使用模式，無需改變代碼，就可快速評估驗證進度，并指導測試改進指令，自動檢測無法到達和冗余的代碼，增強了分析效果。與此同時，Quantify還可有效集成如西門子EDA的驗證仿真工具，不受驗證工具的影響與限制，是市場上獨有的解決方案。

Quantify也用于測量正式和基于仿真的驗證環境的可達覆蓋率，在這種模式下，Quantify得以測試設計代碼中可能無法到達的領域, 通常也是問題所在區域。例如：與設計階段輸入斷開的死代碼或冗余代碼，Quantify將評估過度約束的測試環境，指示可能未測試的代碼區域。即使代碼得以到達，Quantify也將評估代碼是否在驗證過程中實際到達。可達性和觀察覆蓋率的結合為驗證結束提供了準確的衡量標準。