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

Features

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

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

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

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

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

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