Cadence設(shè)計(jì)系統(tǒng)公司日前宣布，沖電氣工業(yè)株式會(huì)社（Oki）采納Incisive Formal Verifier做為其基于斷言的形式驗(yàn)證(ABV)標(biāo)準(zhǔn)。通過(guò)在設(shè)計(jì)初期階段采用Cadence Incisive Formal Verifier形式驗(yàn)證工具，Oki公司改善了產(chǎn)品交付和整體質(zhì)量。Incisive Formal Verifier使得Oki公司的設(shè)計(jì)團(tuán)隊(duì)能夠在模擬測(cè)試環(huán)境之前數(shù)月就開(kāi)始進(jìn)行驗(yàn)證，并迅速找出存在的設(shè)計(jì)缺陷。以前這些缺陷在產(chǎn)品交付周期中極難被發(fā)現(xiàn)，造成的代價(jià)極其高昂。

Oki公司的電信與汽車系統(tǒng)業(yè)務(wù)部電信大規(guī)模集成電路設(shè)計(jì)處經(jīng)理Yasuhiro Ohno表示：“快速可靠地驗(yàn)證VoIP LSI產(chǎn)品的DSP內(nèi)核，對(duì)于我們的業(yè)務(wù)極為重要。在過(guò)去，我們已經(jīng)通過(guò)基于斷言的動(dòng)態(tài)驗(yàn)證，在模擬過(guò)程中有效地提高了驗(yàn)證閉合。通過(guò)在模擬之前的工作流程中加入基于斷言的形式驗(yàn)證， Incisive Formal Verifier已經(jīng)可以將產(chǎn)品開(kāi)發(fā)進(jìn)度縮短數(shù)月并提高整體設(shè)計(jì)品質(zhì)。基于我們的經(jīng)驗(yàn)，我們將在設(shè)計(jì)與驗(yàn)證團(tuán)隊(duì)中大規(guī)模采用Incisive Formal Verifier形式驗(yàn)證工具，以縮短我們的產(chǎn)品上市周期。”

Incisive Formal Verifier適用于需要在整個(gè)設(shè)計(jì)過(guò)程初期增加功能驗(yàn)證能力的設(shè)計(jì)團(tuán)隊(duì)。作為基于斷言的完整驗(yàn)證流程的一部分，Incisive Formal Verifier能夠在模擬測(cè)試環(huán)境之前對(duì)設(shè)計(jì)模塊進(jìn)行驗(yàn)證，更早地并以更低的成本找出功能上的缺陷。Incisive Formal Verifier能夠支持廣泛的斷言語(yǔ)言，包括PSL(IEEE 1850)和SVA(IEEE 1800)，以及如Accellera的Open Verification Library等多種斷言庫(kù)，便于在任意流程中采用。Incisive Formal Verifier結(jié)合形式分析方法學(xué)，能夠加速模塊級(jí)開(kāi)發(fā)。隨著設(shè)計(jì)工作進(jìn)入模塊集成階段，同樣的斷言可以在形式驗(yàn)證、模擬和硬件加速/硬件仿真中重復(fù)使用，特別是通過(guò)減少集成與調(diào)試次數(shù)可以提高驗(yàn)證流程的效果。