芯天成形式驗證平臺EsseFormal
EsseFECT
EsseFCEC
EsseFPV
EsseCC
EsseUNR
產(chǎn)品簡介
芯天成形式化等價性驗證工具FECT（Formal Equivalence Checking Tool），可以對黃金參考模型（C-Model）和Verilog實現(xiàn)做形式化等價驗證，以保證兩個實現(xiàn)功能完全形式等價，消除由于仿真驗證不全面而帶來的功能驗證風險。
核心優(yōu)勢
+10年研發(fā)，Silicon proven（+4代圖芯Vivante GPUs、+8家GPU/CPU/DSP、3個silicon bug）；
運算單元(浮點)完備解決方案
黃金C-Model（IEEE-754協(xié)議的C-Model、半/單/雙精度浮點、bfloat）；
完備證明服務(FDIV、FMA等)；
應用場景
客戶案例
產(chǎn)品簡介
芯天成組合邏輯等價性驗證工具EsseFCEC（FCEC，F(xiàn)ormal Combinational Equivalence Checking），可為各類技術節(jié)點提供穩(wěn)定、準確和高速的工業(yè)級芯片等價性驗證方案，以應對芯片設計與驗證過程中的面積優(yōu)化、功耗優(yōu)化和驗證速度瓶頸問題。
該產(chǎn)品基于可滿足性算法及電路優(yōu)化算法，可以支持綜合工具對電路的低功耗優(yōu)化、面積優(yōu)化等各種先進優(yōu)化策略，能夠驗證超大規(guī)模電路之間的等價性，為芯片設計與驗證提供高精度的解決方案。
核心優(yōu)勢
穩(wěn)定、準確、高速的驗證流程；
支持綜合工具的各種先進綜合策略；
方便快捷的驗證結(jié)果調(diào)試；
簡潔易用的圖形用戶界面；
適用于各個階段電路之間的驗證。
產(chǎn)品功能
支持System Verilog、VHDL等多種設計格式讀??；
支持組合邏輯等價性驗證與時序等價性驗證；
支持fsm recoding、clock-gating、retiming等先進綜合優(yōu)化的驗證；
支持使用designware IP電路的驗證；
支持邏輯錐圖形顯示等多種結(jié)果調(diào)試方法。
應用方案
ASIC/FPGA FLOW設計綜合前后的等價性驗證；
ASIC/FPGA FLOW設計PR前后的等價性驗證；
ASIC/FPGA FLOW設計ECO前后的等價性驗證。
產(chǎn)品簡介
芯天成模型檢查工具EsseFPV（FPV，F(xiàn)ormal property verification），使用形式化技術驗證 SystemVerilog 斷言 (SVA) 屬性，為用戶提供快速的錯誤檢測以及預期設計行為的端到端的驗證。
核心優(yōu)勢
快速定位設計bug；
支持多種驗證引擎；
人性化的用戶圖形界面；
可定制化的屬性驗證服務。
產(chǎn)品功能
可在仿真之前就能實現(xiàn)驗證，適合早期的bug追蹤，通過端到端的驗證可確保設計功能的高正確率；
支持斷言屬性、約束屬性、覆蓋屬性的驗證，可在設計中更快地發(fā)現(xiàn)bug并提供反例；
人性化的用戶圖形界面，對于習慣圖形化系統(tǒng)的用戶更友好，利于debug調(diào)試。
應用方案
檢查設計行為的斷言；
約束形式化驗證環(huán)境的假設；
用于監(jiān)視預期事件的覆蓋屬性。
產(chǎn)品簡介
芯天成連接性檢查工具EsseCC（CC，Connectivity Checking），是一個高效的連接性檢查的驗證工具，為用戶提供快速的錯誤檢測以及預期設計行為的信號到信號的驗證。該產(chǎn)品以RTL電路和連接規(guī)范作為輸入，快速檢查設計是否符合連接規(guī)范。與傳統(tǒng)驗證方式相比，EsseCC具有高效率、高準確率，上手簡單便捷的優(yōu)點。
核心優(yōu)勢
快速、高效的驗證流程；
直觀易操作的用戶界面；
支持反例生成和波形顯示；
支持多種引擎的連接性檢查；
支持生成跨DFF的連接關系生成。
產(chǎn)品功能
支持Verilog/SystemVerilog和VHDL的混合編譯；
支持物理路徑及連接屬性的驗證；
支持反向生成連接；
支持連接信號的覆蓋率檢查；
支持生成反例的 Testbench 及波形圖；
GUI界面提供原理圖、波形查看。
應用場景
SoC I/O 連接性檢查；
綜合后網(wǎng)表連接性檢查；
驗證Chiplet技術下模塊的連接性檢查；
全局時鐘及復位信號連接性檢查；
總線寄存器的連接性檢查；
集成IP的連接性檢查。
產(chǎn)品簡介
芯天成覆蓋不可達性檢查工具EsseUNR（Coverage Unreachability Checking），是一款高效的覆蓋不可達性檢查工具。使用傳統(tǒng)的驗證方式，在驗證后期，通過編寫測試用例提升驗證覆蓋率的難度陡然上升。由此，使用EsseUNR工具，可更高效地對未覆蓋的代碼進行全面的不可達性檢查。EsseUNR具有效率更高、更準確、更易上手的優(yōu)點。
核心優(yōu)勢
兼容性高、快速、高效；
直觀易操作的用戶界面；
適配主流仿真軟的覆蓋數(shù)據(jù)；
支持生成Testbench和波形顯示；
支持RTL級的Formal不可達性檢查。
產(chǎn)品功能
支持Verilog/SystemVerilog和VHDL的混合編譯；
支持利用主流仿真工具覆蓋數(shù)據(jù)對未覆蓋代碼進行不可達性檢查；
用形式驗證的方法對RTL設計進行不可達性檢查；
支持RTL設計Line/Condition/Fsm/Branch/Toggle類型的不可達性檢查；
支持生成可達的檢查點的Testbench及波形圖；
支持通過GUI界面查看原理圖、波形。
應用場景
支持ASIC/FPGA的不可達性檢查；
通信協(xié)議通信狀態(tài)的不可達性檢查；
處理器控制單元的不可達性檢查；
DMA控制器的不可達性檢查；
寄存器狀態(tài)的不可達性檢查。
