芯天成形式验证平台EsseFormal
EsseFECT
EsseFCEC
EsseFPV
EsseCC
EsseUNR
EsseCDC
EsseRDC
EsseLint
EsseLPV
产品简介
芯天成形式化等价性验证工具EsseFECT（FECT，Formal Equivalence Checking Tool），可以对黄金参考模型（C-Model）和Verilog实现做形式化等价验证，以保证两个实现功能完全形式等价，消除由于仿真验证不全面而带来的功能验证风险。
核心优势
+10年研发，Silicon proven（+4代图芯Vivante GPUs、+8家GPU/CPU/DSP、3个silicon bug）；
运算单元(浮点)完备解决方案：黄金C-Model（IEEE-754协议的C-Model、半/单/双精度浮点、bfloat）；完备证明服务(FDIV、FMA等)。
应用场景
客户案例
产品简介
芯天成组合逻辑等价性验证工具EsseFCEC（FCEC，Formal Combinational Equivalence Checking），可为各类技术节点提供稳定、准确和高速的工业级芯片等价性验证方案，以应对芯片设计与验证过程中的面积优化、功耗优化和验证速度瓶颈问题。
该产品基于可满足性算法及电路优化算法，可以支持综合工具对电路的低功耗优化、面积优化等各种先进优化策略，能够验证超大规模电路之间的等价性，为芯片设计与验证提供高精度的解决方案。
核心优势
稳定、准确、高速的验证流程；
支持综合工具的各种先进综合策略；
方便快捷的验证结果调试；
简洁易用的图形用户界面；
适用于各个阶段电路之间的验证。
产品功能
支持System Verilog、VHDL等多种设计格式读取；
支持组合逻辑等价性验证与时序等价性验证；
支持fsm recoding、clock-gating、retiming等先进综合优化的验证；
支持使用designware IP电路的验证；
支持逻辑锥图形显示等多种结果调试方法。
应用方案
ASIC/FPGA FLOW设计综合前后的等价性验证；
ASIC/FPGA FLOW设计PR前后的等价性验证；
ASIC/FPGA FLOW设计ECO前后的等价性验证。
产品简介
芯天成模型检查工具EsseFPV（FPV，Formal property verification），使用形式化技术验证 SystemVerilog 断言 (SVA) 属性，为用户提供快速的错误检测以及预期设计行为的验证。
核心优势
快速定位设计bug；
支持多种验证引擎；
人性化的用户图形界面；
可定制化的属性验证服务。
产品功能
可在仿真之前就能实现验证，适合早期的bug追踪，可提高设计功能的正确性；
支持断言属性、约束属性、覆盖属性的验证，提供反例testbench及波形文件；
人性化的用户图形界面，对于习惯图形化系统的用户更友好，利于debug调试。
应用方案
CPU/GPU/ASIC各类仲裁器的验证；
CPU/GPU/ASIC各类控制器的验证；
CPU/GPU/ASIC关键功能模块的验证。
产品简介
芯天成连接性检查工具EsseCC（CC，Connectivity Checking），是一个高效的连接性检查的验证工具，为用户提供快速的错误检测，对预期设计行为的信号到信号连接功能进行验证。该产品以RTL电路和连接规范(.csv文件)作为输入，快速检查设计是否符合连接要求。与传统验证方式相比，EsseCC具有高效率、高准确率、上手简单便捷的优点。
核心优势
快速、高效的验证流程；
直观易操作的用户界面；
支持反例生成和波形显示；
支持多种引擎的连接性检查；
支持生成跨DFF的连接关系生成。
产品功能
支持Verilog/SystemVerilog和VHDL的混合编译；
支持物理路径及连接属性的验证；
支持反向生成连接；
支持连接信号的翻转检查；
支持生成反例的 Testbench 及波形图；
GUI界面提供原理图、波形查看。
应用场景
SoC I/O 连接性检查；
网表的连接性检查；
全局时钟及复位信号连接性检查；
PAD复用的连接性检查；
集成IP的连接性检查。
产品简介
芯天成覆盖不可达性检查工具EsseUNR（UNR，Coverage Unreachability Checking），是一款高效的覆盖不可达性检查工具。使用传统的验证方式，在验证后期，通过编写测试用例提升验证覆盖率的难度陡然上升。使用EsseUNR工具，可更高效地对未覆盖的代码进行全面的不可达性检查。EsseUNR具有效率更高、更准确、更易上手的优点。
核心优势
兼容性高、快速、高效；
直观易操作的用户界面；
适配多个主流仿真软件的覆盖率数据库；
支持生成Testbench和波形显示；
支持直接验证RTL设计的不可达性。
产品功能
支持Verilog/System Verilog和VHDL的混合编译；
支持基于主流仿真工具的覆盖数据对未覆盖代码进行不可达性检查；
用形式验证的方法对RTL设计进行不可达性检查；
支持分析代码覆盖率和功能覆盖率；
支持通过GUI界面查看原理图、波形。
应用场景
支持CPU/GPU/DSP/ASIC/FPGA的系统级覆盖不可达性检查；
处理器控制单元的覆盖不可达性检查；
DMA控制器的覆盖不可达性检查；
产品简介
芯天成跨时钟域检查工具EsseCDC（CDC，Clock Domain Crossing），是专门针对集成电路中跨时钟域问题的产品。不同时钟域之间进行数据传输可能会出现亚稳态的问题，最终将导致功能异常，EsseCDC可对设计进行全面的跨域检查，可避免跨域产生亚稳态和毛刺等原因导致功能异常，增强设计的稳定性和确保设计的功能正确性。
核心优势
规则检查全面可降低潜在风险；
专有独特的CDC结构检查算法；
可快速高效地验证大规模Soc设计；
精准的违例报告更快定位问题；
功能丰富操作简单的图形化界面。
产品功能
支持解析不同版本的SDC语法；
支持RTL/Netlist阶段的CDC检查；
支持自动推断时钟域的CDC检查；
支持对report降噪处理，忽略不关心的违例；
提供GUI界面查看验证结果和Debug结果。
应用场景
高性能芯片跨时钟域的Glitch检查；
高性能芯片跨时钟域的数据检查；
常见跨域同步器的正确性检查；
自定义跨域同步器的正确性检查。
产品简介
芯天成跨复位域检查工具EsseRDC（RDC，Reset Domain Crossing），是专门针对集成电路中跨复位域问题的产品，用于对复位信号传播、复位信号状态的有效性、信号的收敛聚合等多类场景进行全面的检查和分析，避免由于复位信号导致数据传播存在异常，确保复位信号对数据传播控制更加可靠和有效，增强芯片设计整体的稳定性和功能正确性。
核心优势
规则检查全面可降低潜在风险；
高效的复位信号结构检查算法；
精准的违例报告更快定位问题；
功能丰富操作简单的图形化界面。
产品功能
支持解析不同版本的SDC语法；
支持RTL/Netlist阶段的SDC检查；
支持对report降噪处理，忽略不关心的违例；
提供GUI界面查看验证结果和Debug结果。
应用场景
多复位信号控制的芯片功能检查；
高性能芯片中复位信号的传播分析；
跨域同步器中复位信号正确性分析。
产品简介
芯天成设计规则检查工具EsseLint，是用于在芯片验证早期检测代码中潜在的错误的产品，主要针对代码风格、语法规范、可综合性、电路结构等问题进行全面详细的检查，避免因设计风格不一致、不合理的电路结构、仿真和综合差异导致潜在问题的发生，提高代码质量与可维护性，为保证芯片设计功能正确性和稳定性提供强有力的支撑。
核心优势
规则检查全面可识别潜在问题；
高效快速的设计规则检查算法；
详细的检查报告帮助定位问题；
标准化的TCL命令简化操作流程。
产品功能
语法检查；
编码规范和代码风格检查；
综合/仿真一致性问题检查；
电路结构问题检查；
提供详尽违例报告。
应用场景
设计阶段快速检测设计语法问题；
验证阶段识别潜在的电路结构问题；
验证阶段评估代码的质量；
辅助并加快完成验证sign-off；
适用于CPU/GPU/Ascii芯片的语法检查。
产品简介
芯天成形式化低功耗检查工具 EsseLPV（LPV，Lower Power Verification），是用于验证静态低功耗设计正确性和实现行为的工具。它在 RTL 阶段、综合后和布局布线后都能进行低功耗方面的规则检查，且使用 GUI 界面可一键自动完成验证过程，操作简单，可以帮助用户尽早发现和修复问题。
核心优势
兼容性高，能快速准确定位；
支持结果迭代处理；
支持 RTL 级和 netlist 级的检查；
支持不同策略的规则检查；
一键自动验证，操作简便。
产品功能
支持 Verilog/System Verilog 和 VHDL 的混合编译；
支持不同版本的 UPF 语法；
支持对设计不同阶段进行规则检查；
支持对指定的电源策略进行检查；
全面检查 RTL 是否存在违反功耗架构规则的信号；
GUI 界面提供原理图、结果树状图。
应用场景
处理器和逻辑单元（CPU）；
通信接口和收发器；
电源管理单元（PMU）；
时钟和时序电路；
所有考虑低功耗的设计。
