99905银河[中国]精粹研究院|官方网站

产品与技术

P & T产品与技术

芯天成形式验证平台EsseFormal

全功能形式验证工具平台,平台包含C-to-RTL/RTL-to-Netlist等价验证工具、属性验证工具,以及各种实用验证Apps,贯穿于数字IC设计各个环节,为芯片设计各个环节提供验证工具。平台具有定制化和集成化两大特点,精准满足客户需求,大幅降低用户验证时间、提高验证完整性和准确性。
芯天成形式验证平台

EsseFECT

EsseFCEC

EsseFPV

EsseCC

EsseUNR

产品简介

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



1678928698163449.png


应用场景

1678928698270767.png



客户案例

1679538043720130.png




产品简介

芯天成组合逻辑等价性验证工具EsseFCEC(FCEC,Formal Combinational Equivalence Checking),可为各类技术节点提供稳定、准确和高速的工业级芯片等价性验证方案,以应对芯片设计与验证过程中的面积优化、功耗优化和验证速度瓶颈问题。

 该产品基于可满足性算法及电路优化算法,可以支持综合工具对电路的低功耗优化、面积优化等各种先进优化策略,能够验证超大规模电路之间的等价性,为芯片设计与验证提供高精度的解决方案。

核心优势

  • 稳定、准确、高速的验证流程;

  • 支持综合工具的各种先进综合策略;

  • 方便快捷的验证结果调试;

  • 简洁易用的图形用户界面;

  • 适用于各个阶段电路之间的验证。

1678928697638060.png





产品功能

  • 支持System Verilog、VHDL等多种设计格式读取;

  • 支持组合逻辑等价性验证与时序等价性验证;

  • 支持fsm recoding、clock-gating、retiming等先进综合优化的验证;

  • 支持使用designware IP电路的验证;

  • 支持逻辑锥图形显示等多种结果调试方法。


1678928697366389.png

应用方案

  • ASIC/FPGA FLOW设计综合前后的等价性验证;

  • ASIC/FPGA FLOW设计PR前后的等价性验证;

  • ASIC/FPGA FLOW设计ECO前后的等价性验证。




产品简介


芯天成模型检查工具EsseFPV(FPV,Formal property verification),使用形式化技术验证 SystemVerilog 断言 (SVA) 属性,为用户提供快速的错误检测以及预期设计行为的端到端的验证。

1678928698274467.png

核心优势

  • 快速定位设计bug;

  • 支持多种验证引擎;

  • 人性化的用户图形界面;

  • 可定制化的属性验证服务。




1678928698229030.png


产品功能

  • 可在仿真之前就能实现验证,适合早期的bug追踪,通过端到端的验证可确保设计功能的高正确率;

  • 支持断言属性、约束属性、覆盖属性的验证,可在设计中更快地发现bug并提供反例;

  • 人性化的用户图形界面,对于习惯图形化系统的用户更友好,利于debug调试。

1678928698244548.png


应用方案

  • 检查设计行为的断言;

  • 约束形式化验证环境的假设;

  • 用于监视预期事件的覆盖属性。



产品简介


芯天成连接性检查工具EsseCC(CC,Connectivity Checking),是一个高效的连接性检查的验证工具,为用户提供快速的错误检测以及预期设计行为的信号到信号的验证。该产品以RTL电路和连接规范作为输入,快速检查设计是否符合连接规范。与传统验证方式相比,EsseCC具有高效率、高准确率,上手简单便捷的优点。

3-1.jpg

核心优势

  • 快速、高效的验证流程;

  • 直观易操作的用户界面;

  • 支持反例生成和波形显示;

  • 支持多种引擎的连接性检查;

  • 支持生成跨DFF的连接关系生成。




3-2.jpg


产品功能

  • 支持Verilog/SystemVerilog和VHDL的混合编译;

  • 支持物理路径及连接属性的验证;

  • 支持反向生成连接;

  • 支持连接信号的覆盖率检查;

  • 支持生成反例的 Testbench 及波形图;

  • GUI界面提供原理图、波形查看。

3-3.jpg


应用场景

  • SoC I/O 连接性检查;

  • 综合后网表连接性检查;

  • 验证Chiplet技术下模块的连接性检查;

  • 全局时钟及复位信号连接性检查;

  • 总线寄存器的连接性检查;

  • 集成IP的连接性检查。




产品简介

芯天成覆盖不可达性检查工具EsseUNR(Coverage Unreachability Checking),是一款高效的覆盖不可达性检查工具。使用传统的验证方式,在验证后期,通过编写测试用例提升验证覆盖率的难度陡然上升。由此,使用EsseUNR工具,可更高效地对未覆盖的代码进行全面的不可达性检查。EsseUNR具有效率更高、更准确、更易上手的优点。

1.jpg


核心优势

  • 兼容性高、快速、高效;

  • 直观易操作的用户界面;

  • 适配主流仿真软的覆盖数据;

  • 支持生成Testbench和波形显示;

  • 支持RTL级的Formal不可达性检查。


2.jpg




产品功能

  • 支持Verilog/SystemVerilog和VHDL的混合编译;

  • 支持利用主流仿真工具覆盖数据对未覆盖代码进行不可达性检查;

  • 用形式验证的方法对RTL设计进行不可达性检查;

  • 支持RTL设计Line/Condition/Fsm/Branch/Toggle类型的不可达性检查;

  • 支持生成可达的检查点的Testbench及波形图;

  • 支持通过GUI界面查看原理图、波形。


1721026820940641.jpg



应用场景

  • 支持ASIC/FPGA的不可达性检查;

  • 通信协议通信状态的不可达性检查;

  • 处理器控制单元的不可达性检查;

  • DMA控制器的不可达性检查;

  • 寄存器状态的不可达性检查。



99905银河[中国]精粹研究院|官方网站
地址:深圳市南山区沙河西路1801号国实大厦15楼
电话:+86-0755-86328998
邮箱:sales@gwxeda.com
Copyright ©2022 99905银河[中国]精粹研究院|官方网站版权所有 备案号:粤ICP备2022085510号 粤公网安备 44030502009383号