Empyrean FormalEC

         在ASIC/SoC和FPGA设计流程中，成功经过功能验证的代码称之为Golden RTL代码。逻辑综合工具执行RTL到网表的转换，会对电路结构进行优化和变动。特别是针对复杂的大规模设计，综合优化程度将会很高，比如寄存器的复制、状态机增加校验位、电路加固等。为了确保这一过程功能的等效，必须采用等效性检查工具将Golden RTL代码与综合的网表进行等效性功能验证。在综合之后布局布线往往需要人工的参与，因此为了保证修改之后的网表和综合之后的网表在功能上的一致性，也有必要执行综合后的网表文件和布局布线之后的网表做等效性检查，保证设计在功能上的正确性与一致性。

         组合逻辑等价性验证工具Empyrean Formal™EC集成多种先进的证明和优化引擎和求解器，并通过多级属性和引擎并行化在多核、多机、LSF组成的证明环境上提供了更强的可扩展性。同时支持客户定制的形式引擎和求解器的插件，通过其Open-API架构快速适应定制的多引擎验证策略，可用于每个设计过程前后的rtl2rtl、rtl2netlist、netlist2netlist逻辑等价性验证。FormalEC支持通用硬件设计语言、支持位级和字级建模、支持多个国外和国产FPGA厂家的工艺库。