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