EpicFV?是面向?Verilog?的形式化驗(yàn)證工具，目前支持在?Linux?系統(tǒng)上運(yùn)行。

Features

• 業(yè)界首款開源形式驗(yàn)證工具
• 分布式計(jì)算/并行計(jì)算加速驗(yàn)證收斂
• 自動(dòng)調(diào)度引擎，降低形式驗(yàn)證工具使用門檻
• 在易用性、實(shí)用性、穩(wěn)定性上提供專業(yè)技術(shù)支持

隨著芯片設(shè)計(jì)行業(yè)的高速發(fā)展，行業(yè)對(duì)芯片驗(yàn)證提出了更高的要求。動(dòng)態(tài)仿真，形式驗(yàn)證，原型設(shè)計(jì)，硬件加速是常見的幾大功能驗(yàn)證的手段。

其中，形式驗(yàn)證有著以下三種優(yōu)勢(shì)：

1. 形式驗(yàn)證是窮盡的，完備的；
2. 形式驗(yàn)證不需要任何復(fù)雜測(cè)試激勵(lì)環(huán)境的搭建，只需要寫約束和測(cè)試點(diǎn)即可；
3. 形式驗(yàn)證對(duì)設(shè)計(jì)收斂的效率是傳統(tǒng)仿真的倍數(shù)級(jí)；
4. 形式驗(yàn)證適合于設(shè)計(jì)人員在早期對(duì)于自己的模塊進(jìn)行功能驗(yàn)證。

但是，形式驗(yàn)證需要使用斷言（SystemVerilog Assertion），工程師必須熟悉語(yǔ)法，并且對(duì)工具內(nèi)部的引擎有一定熟悉度，這對(duì)使用門檻和開發(fā)技術(shù)的成熟度提出了較高的要求，導(dǎo)致無論是高校還是設(shè)計(jì)公司，雖然都希望能借形式驗(yàn)證工具來大大加速驗(yàn)證的收斂，卻因缺乏經(jīng)驗(yàn)而止步。

作為全球首款開源形式驗(yàn)證工具，“靈驗(yàn)”在用戶輸入RTL設(shè)計(jì)和SystemVerilog斷言描述設(shè)計(jì)規(guī)范的情況下，可以自動(dòng)進(jìn)行語(yǔ)法解析、設(shè)計(jì)綜合、斷言解析，并且基于分布式計(jì)算理論自動(dòng)調(diào)度引擎求解斷言，加速驗(yàn)證收斂，從而降低形式驗(yàn)證工具的使用門檻。