芯天成形式驗證平臺EsseFormal
EsseFECT
EsseFCEC
EsseFPV
EsseCC
EsseUNR
EsseCDC
EsseRDC
EsseLint
EsseLPV
產(chǎn)品簡介
芯天成形式化等價性驗證工具EsseFECT（FECT，F(xiàn)ormal Equivalence Checking Tool），可以對黃金參考模型（C-Model）和Verilog實現(xiàn)做形式化等價驗證，以保證兩個實現(xiàn)功能完全形式等價，消除由于仿真驗證不全面而帶來的功能驗證風(fēng)險。
核心優(yōu)勢
+10年研發(fā)，Silicon proven（+4代圖芯Vivante GPUs、+8家GPU/CPU/DSP、3個silicon bug）；
運算單元(浮點)完備解決方案：黃金C-Model（IEEE-754協(xié)議的C-Model、半/單/雙精度浮點、bfloat）；完備證明服務(wù)(FDIV、FMA等)。
應(yīng)用場景
客戶案例
產(chǎn)品簡介
芯天成組合邏輯等價性驗證工具EsseFCEC（FCEC，F(xiàn)ormal Combinational Equivalence Checking），可為各類技術(shù)節(jié)點提供穩(wěn)定、準確和高速的工業(yè)級芯片等價性驗證方案，以應(yīng)對芯片設(shè)計與驗證過程中的面積優(yōu)化、功耗優(yōu)化和驗證速度瓶頸問題。
該產(chǎn)品基于可滿足性算法及電路優(yōu)化算法，可以支持綜合工具對電路的低功耗優(yōu)化、面積優(yōu)化等各種先進優(yōu)化策略，能夠驗證超大規(guī)模電路之間的等價性，為芯片設(shè)計與驗證提供高精度的解決方案。
核心優(yōu)勢
穩(wěn)定、準確、高速的驗證流程；
支持綜合工具的各種先進綜合策略；
方便快捷的驗證結(jié)果調(diào)試；
簡潔易用的圖形用戶界面；
適用于各個階段電路之間的驗證。
產(chǎn)品功能
支持System Verilog、VHDL等多種設(shè)計格式讀取；
支持組合邏輯等價性驗證與時序等價性驗證；
支持fsm recoding、clock-gating、retiming等先進綜合優(yōu)化的驗證；
支持使用designware IP電路的驗證；
支持邏輯錐圖形顯示等多種結(jié)果調(diào)試方法。
應(yīng)用方案
ASIC/FPGA FLOW設(shè)計綜合前后的等價性驗證；
ASIC/FPGA FLOW設(shè)計PR前后的等價性驗證；
ASIC/FPGA FLOW設(shè)計ECO前后的等價性驗證。
產(chǎn)品簡介
芯天成模型檢查工具EsseFPV（FPV，F(xiàn)ormal property verification），使用形式化技術(shù)驗證 SystemVerilog 斷言 (SVA) 屬性，為用戶提供快速的錯誤檢測以及預(yù)期設(shè)計行為的驗證。
核心優(yōu)勢
快速定位設(shè)計bug；
支持多種驗證引擎；
人性化的用戶圖形界面；
可定制化的屬性驗證服務(wù)。
產(chǎn)品功能
可在仿真之前就能實現(xiàn)驗證，適合早期的bug追蹤，可提高設(shè)計功能的正確性；
支持斷言屬性、約束屬性、覆蓋屬性的驗證，提供反例testbench及波形文件；
人性化的用戶圖形界面，對于習(xí)慣圖形化系統(tǒng)的用戶更友好，利于debug調(diào)試。
應(yīng)用方案
CPU/GPU/ASIC各類仲裁器的驗證；
CPU/GPU/ASIC各類控制器的驗證；
CPU/GPU/ASIC關(guān)鍵功能模塊的驗證。
產(chǎn)品簡介
芯天成連接性檢查工具EsseCC（CC，Connectivity Checking），是一個高效的連接性檢查的驗證工具，為用戶提供快速的錯誤檢測，對預(yù)期設(shè)計行為的信號到信號連接功能進行驗證。該產(chǎn)品以RTL電路和連接規(guī)范(.csv文件)作為輸入，快速檢查設(shè)計是否符合連接要求。與傳統(tǒng)驗證方式相比，EsseCC具有高效率、高準確率、上手簡單便捷的優(yōu)點。
核心優(yōu)勢
快速、高效的驗證流程；
直觀易操作的用戶界面；
支持反例生成和波形顯示；
支持多種引擎的連接性檢查；
支持生成跨DFF的連接關(guān)系生成。
產(chǎn)品功能
支持Verilog/SystemVerilog和VHDL的混合編譯；
支持物理路徑及連接屬性的驗證；
支持反向生成連接；
支持連接信號的翻轉(zhuǎn)檢查；
支持生成反例的 Testbench 及波形圖；
GUI界面提供原理圖、波形查看。
應(yīng)用場景
SoC I/O 連接性檢查；
網(wǎng)表的連接性檢查；
全局時鐘及復(fù)位信號連接性檢查；
PAD復(fù)用的連接性檢查；
集成IP的連接性檢查。
產(chǎn)品簡介
芯天成覆蓋不可達性檢查工具EsseUNR（UNR，Coverage Unreachability Checking），是一款高效的覆蓋不可達性檢查工具。使用傳統(tǒng)的驗證方式，在驗證后期，通過編寫測試用例提升驗證覆蓋率的難度陡然上升。使用EsseUNR工具，可更高效地對未覆蓋的代碼進行全面的不可達性檢查。EsseUNR具有效率更高、更準確、更易上手的優(yōu)點。
核心優(yōu)勢
兼容性高、快速、高效；
直觀易操作的用戶界面；
適配多個主流仿真軟件的覆蓋率數(shù)據(jù)庫；
支持生成Testbench和波形顯示；
支持直接驗證RTL設(shè)計的不可達性。
產(chǎn)品功能
支持Verilog/System Verilog和VHDL的混合編譯；
支持基于主流仿真工具的覆蓋數(shù)據(jù)對未覆蓋代碼進行不可達性檢查；
用形式驗證的方法對RTL設(shè)計進行不可達性檢查；
支持分析代碼覆蓋率和功能覆蓋率；
支持通過GUI界面查看原理圖、波形。
應(yīng)用場景
支持CPU/GPU/DSP/ASIC/FPGA的系統(tǒng)級覆蓋不可達性檢查；
處理器控制單元的覆蓋不可達性檢查；
DMA控制器的覆蓋不可達性檢查；
產(chǎn)品簡介
芯天成跨時鐘域檢查工具EsseCDC（CDC，Clock Domain Crossing），是專門針對集成電路中跨時鐘域問題的產(chǎn)品。不同時鐘域之間進行數(shù)據(jù)傳輸可能會出現(xiàn)亞穩(wěn)態(tài)的問題，最終將導(dǎo)致功能異常，EsseCDC可對設(shè)計進行全面的跨域檢查，可避免跨域產(chǎn)生亞穩(wěn)態(tài)和毛刺等原因?qū)е鹿δ墚惓＃鰪娫O(shè)計的穩(wěn)定性和確保設(shè)計的功能正確性。
核心優(yōu)勢
規(guī)則檢查全面可降低潛在風(fēng)險；
專有獨特的CDC結(jié)構(gòu)檢查算法；
可快速高效地驗證大規(guī)模Soc設(shè)計；
精準的違例報告更快定位問題；
功能豐富操作簡單的圖形化界面。
產(chǎn)品功能
支持解析不同版本的SDC語法；
支持RTL/Netlist階段的CDC檢查；
支持自動推斷時鐘域的CDC檢查；
支持對report降噪處理，忽略不關(guān)心的違例；
提供GUI界面查看驗證結(jié)果和Debug結(jié)果。
應(yīng)用場景
高性能芯片跨時鐘域的Glitch檢查；
高性能芯片跨時鐘域的數(shù)據(jù)檢查；
常見跨域同步器的正確性檢查；
自定義跨域同步器的正確性檢查。
產(chǎn)品簡介
芯天成跨復(fù)位域檢查工具EsseRDC（RDC，Reset Domain Crossing），是專門針對集成電路中跨復(fù)位域問題的產(chǎn)品，用于對復(fù)位信號傳播、復(fù)位信號狀態(tài)的有效性、信號的收斂聚合等多類場景進行全面的檢查和分析，避免由于復(fù)位信號導(dǎo)致數(shù)據(jù)傳播存在異常，確保復(fù)位信號對數(shù)據(jù)傳播控制更加可靠和有效，增強芯片設(shè)計整體的穩(wěn)定性和功能正確性。
核心優(yōu)勢
規(guī)則檢查全面可降低潛在風(fēng)險；
高效的復(fù)位信號結(jié)構(gòu)檢查算法；
精準的違例報告更快定位問題；
功能豐富操作簡單的圖形化界面。
產(chǎn)品功能
支持解析不同版本的SDC語法；
支持RTL/Netlist階段的SDC檢查；
支持對report降噪處理，忽略不關(guān)心的違例；
提供GUI界面查看驗證結(jié)果和Debug結(jié)果。
應(yīng)用場景
多復(fù)位信號控制的芯片功能檢查；
高性能芯片中復(fù)位信號的傳播分析；
跨域同步器中復(fù)位信號正確性分析。
產(chǎn)品簡介
芯天成設(shè)計規(guī)則檢查工具EsseLint，是用于在芯片驗證早期檢測代碼中潛在的錯誤的產(chǎn)品，主要針對代碼風(fēng)格、語法規(guī)范、可綜合性、電路結(jié)構(gòu)等問題進行全面詳細的檢查，避免因設(shè)計風(fēng)格不一致、不合理的電路結(jié)構(gòu)、仿真和綜合差異導(dǎo)致潛在問題的發(fā)生，提高代碼質(zhì)量與可維護性，為保證芯片設(shè)計功能正確性和穩(wěn)定性提供強有力的支撐。
核心優(yōu)勢
規(guī)則檢查全面可識別潛在問題；
高效快速的設(shè)計規(guī)則檢查算法；
詳細的檢查報告幫助定位問題；
標準化的TCL命令簡化操作流程。
產(chǎn)品功能
語法檢查；
編碼規(guī)范和代碼風(fēng)格檢查；
綜合/仿真一致性問題檢查；
電路結(jié)構(gòu)問題檢查；
提供詳盡違例報告。
應(yīng)用場景
設(shè)計階段快速檢測設(shè)計語法問題；
驗證階段識別潛在的電路結(jié)構(gòu)問題；
驗證階段評估代碼的質(zhì)量；
輔助并加快完成驗證sign-off；
適用于CPU/GPU/Ascii芯片的語法檢查。
產(chǎn)品簡介
芯天成形式化低功耗檢查工具 EsseLPV（LPV，Lower Power Verification），是用于驗證靜態(tài)低功耗設(shè)計正確性和實現(xiàn)行為的工具。它在 RTL 階段、綜合后和布局布線后都能進行低功耗方面的規(guī)則檢查，且使用 GUI 界面可一鍵自動完成驗證過程，操作簡單，可以幫助用戶盡早發(fā)現(xiàn)和修復(fù)問題。
核心優(yōu)勢
兼容性高，能快速準確定位；
支持結(jié)果迭代處理；
支持 RTL 級和 netlist 級的檢查；
支持不同策略的規(guī)則檢查；
一鍵自動驗證，操作簡便。
產(chǎn)品功能
支持 Verilog/System Verilog 和 VHDL 的混合編譯；
支持不同版本的 UPF 語法；
支持對設(shè)計不同階段進行規(guī)則檢查；
支持對指定的電源策略進行檢查；
全面檢查 RTL 是否存在違反功耗架構(gòu)規(guī)則的信號；
GUI 界面提供原理圖、結(jié)果樹狀圖。
應(yīng)用場景
處理器和邏輯單元（CPU）；
通信接口和收發(fā)器；
電源管理單元（PMU）；
時鐘和時序電路；
所有考慮低功耗的設(shè)計。
