(相關(guān)資料圖)

應(yīng)用于芯片設(shè)計(jì)的功能特性驗(yàn)證，正在越來(lái)越多的應(yīng)用場(chǎng)景取代仿真驗(yàn)證。其使用方法是用戶根據(jù)設(shè)計(jì)要求提供驗(yàn)證所需的屬性和約束，用數(shù)學(xué)歸納和推理的方法回答這些屬性是否正確。如果不正確會(huì)自動(dòng)生成可用于仿真的激勵(lì)鏈，以便于查錯(cuò)。形式驗(yàn)證的數(shù)學(xué)嚴(yán)密性使它成為對(duì)安全可靠性要求極高的芯片設(shè)計(jì)的必備選擇。

相對(duì)于仿真驗(yàn)證，形式驗(yàn)證的優(yōu)點(diǎn)包括不需要用戶去生成測(cè)試激勵(lì)，一條屬性的真?zhèn)谓Y(jié)論是基于嚴(yán)格的數(shù)學(xué)證明 – 證明為真的屬性在任何激勵(lì)下再進(jìn)行仿真都不會(huì)出錯(cuò)。形式驗(yàn)證的完備性取決于屬性的完備性，而后者可以基于設(shè)計(jì)要求建立清晰和明確的模型，這和一直困擾仿真驗(yàn)證的從本質(zhì)上無(wú)法完善的仿真覆蓋率相比有極大的優(yōu)勢(shì)。由于屬性可以基于設(shè)計(jì)內(nèi)部的任何信號(hào)和運(yùn)行場(chǎng)景，形式驗(yàn)證還具有白箱驗(yàn)證的優(yōu)點(diǎn)，而仿真只能在輸出端決定對(duì)錯(cuò)。另外，功能特性形式驗(yàn)證適用于設(shè)計(jì)的各個(gè)階段，特別是早期在模塊級(jí)設(shè)計(jì)階段，極難建立仿真環(huán)境的情況下，有利于早期發(fā)現(xiàn)設(shè)計(jì)錯(cuò)誤，減少設(shè)計(jì)迭代。

阿卡思AveMC形式化驗(yàn)證工具包含了20多種先進(jìn)的引擎算法，同時(shí)可以通過(guò)引擎并行，使多引擎驗(yàn)證同一屬性。此外，AveMC還能處理最為廣義的斷言空泛，保障驗(yàn)證的完整性。

形式化驗(yàn)證方法邏輯

特點(diǎn)和優(yōu)勢(shì)

形式驗(yàn)證工具現(xiàn)在被美國(guó)EDA企業(yè)壟斷，比如Cadence的IFV和JasperGold，Synopsys的VC Formal等。AveMC以目前業(yè)內(nèi)最先進(jìn)的產(chǎn)品為起點(diǎn)，除了功能和性能競(jìng)爭(zhēng)力之外，還有以下優(yōu)勢(shì)：

1.可以用圖形化的方式，幫助用戶快速建立屬性和約束模型，數(shù)據(jù)表明這一塊占了形式驗(yàn)證時(shí)間的三分之一；

2.更為精確的模型和計(jì)算速度，能發(fā)現(xiàn)其他工具忽略的屬性完備性檢查漏洞；

3.開(kāi)放的構(gòu)架，用戶可以根據(jù)具體的設(shè)計(jì)和驗(yàn)證場(chǎng)景構(gòu)建自己的工具；

4.支持云計(jì)算模式，用戶可以根據(jù)需求配置最為合理的計(jì)算能力。

關(guān)鍵詞：