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

Features

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

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

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

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

但是，形式驗(yàn)證需要使用斷言（SystemVerilog Assertion），工程師必須熟悉語法，并且對工具內(nèi)部的引擎有一定熟悉度，這對使用門檻和開發(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ī)范的情況下，可以自動進(jìn)行語法解析、設(shè)計(jì)綜合、斷言解析，并且基于分布式計(jì)算理論自動調(diào)度引擎求解斷言，加速驗(yàn)證收斂，從而降低形式驗(yàn)證工具的使用門檻。