芯天成形式驗證平臺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）；
時鐘和時序電路；
所有考慮低功耗的設計。
