芯天成形式化等价性验证工具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)
