芯天成形式验证平台EsseFormal
EsseFECT
EsseFCEC
EsseFPV
EsseCC
EsseUNR
产品简介
芯天成组合逻辑等价性验证工具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追踪 ，通过端到端的验证可确保设计功效的高准确率；
支持断言属性、约束属性、笼罩属性的验证 ，可在设计中更快地发明bug并提供反例；
人性化的用户图形界面 ，关于习惯图形化系统的用户更友好 ，利于debug调试。
应用计划
检查设计行为的断言；
约束形式化验证情形的假设；
用于监视预期事务的笼罩属性。
产品简介
芯天成毗连性检查工具EsseCC（CC ，Connectivity Checking） ，是一个高效的毗连性检查的验证工具 ，为用户提供快速的过失检测以及预期设计行为的信号到信号的验证。该产品以RTL电路和毗连规范作为输入 ，快速检查设计是否切合毗连规范。与古板验证方法相比 ，EsseCC具有高效率、高准确率 ，上手简朴便捷的优点。
焦点优势
快速、高效的验证流程；
直观易操作的用户界面；
支持反例天生和波形显示；
支持多种引擎的毗连性检查；
支持天生跨DFF的毗连关系天生。
产品功效
支持Verilog/SystemVerilog和VHDL的混淆编译；
支持物理路径及毗连属性的验证；
支持反向天生毗连；
支持毗连信号的笼罩率检查；
支持天生反例的 Testbench 及波形图；
GUI界面提供原理图、波形审查。
应用场景
SoC I/O 毗连性检查；
综合后网表毗连性检查；
验证Chiplet手艺下？榈呐连性检查；
全局时钟及复位信号毗连性检查；
总线寄存器的毗连性检查；
集成IP的毗连性检查。
产品简介
芯天成笼罩不可达性检查工具EsseUNR（Coverage Unreachability Checking） ，是一款高效的笼罩不可达性检查工具。使用古板的验证方法 ，在验证后期 ，通过编写测试用例提升验证笼罩率的难度蓦然上升。由此 ，使用EsseUNR工具 ，可更高效地对未笼罩的代码举行周全的不可达性检查。EsseUNR具有用率更高、更准确、更易上手的优点。
焦点优势
兼容性高、快速、高效；
直观易操作的用户界面；
适配主流仿真软的笼罩数据；
支持天生Testbench和波形显示；
支持RTL级的Formal不可达性检查。
产品功效
支持Verilog/SystemVerilog和VHDL的混淆编译；
支持使用主流仿真工具笼罩数据对未笼罩代码举行不可达性检查；
用形式验证的要领对RTL设计举行不可达性检查；
支持RTL设计Line/Condition/Fsm/Branch/Toggle类型的不可达性检查；
支持天生可达的检查点的Testbench及波形图；
支持通过GUI界面审查原理图、波形。
应用场景
支持ASIC/FPGA的不可达性检查；
通讯协议通讯状态的不可达性检查；
处置惩罚器控制单位的不可达性检查；
DMA控制器的不可达性检查；
寄存器状态的不可达性检查。
