形式化等價性驗證工具EsseFECT是一種用于驗證兩個設計實現是否在功能上完全一致的工具。它對黃金參考模型（C-Model）和Verilog實現進行形式化等價驗證，確保兩者在功能上完全一致，消除因仿真驗證不全面所帶來的功能驗證風險。FECT主要應用于C-to-RTL/RTL-to-Netlist兩個場景，具體而言：
C-to-RTL：即C模型與RTL驗證。在軟硬件協同設計中，對照黃金參考模型（通常是C語言實現）與硬件描述語言（如Verilog或VHDL）實現，確保它們在功能上的等價性。
RTL-to-Netlist：即RTL與網表驗證。在集成電路設計過程中，從RTL（寄存器傳輸級）代碼到門級網表的轉換過程中，確保兩者在功能上沒有偏差。
產品特征
十年研發積淀，久經市場考驗：歷經10年研發，已成功應用于4代圖芯Vivante GPUs，服務超過8家GPU/CPU/DSP企業，發現并解決了3個硅片級別的bug。
運算單元（浮點）完備解決方案：
-提供符合IEEE-754標準的C-Model，支持半精度、單精度、雙精度浮點以及bfloat等格式。
-完備的證明服務，包括但不限于FDIV（浮點除法）、FMA（浮點乘加）等運算單元。
-889.png)
