芯天成形式驗(yàn)證平臺(tái)EsseFormal
EsseFECT
EsseFCEC
EsseFPV
EsseCC
EsseUNR
產(chǎn)品簡(jiǎn)介
芯天成形式化等價(jià)性驗(yàn)證工具FECT（Formal 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），可為各類技術(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追蹤，通過(guò)端到端的驗(yàn)證可確保設(shè)計(jì)功能的高正確率；
支持?jǐn)嘌詫傩浴⒓s束屬性、覆蓋屬性的驗(yàn)證，可在設(shè)計(jì)中更快地發(fā)現(xiàn)bug并提供反例；
人性化的用戶圖形界面，對(duì)于習(xí)慣圖形化系統(tǒng)的用戶更友好，利于debug調(diào)試。
應(yīng)用方案
檢查設(shè)計(jì)行為的斷言；
約束形式化驗(yàn)證環(huán)境的假設(shè)；
用于監(jiān)視預(yù)期事件的覆蓋屬性。
產(chǎn)品簡(jiǎn)介
芯天成連接性檢查工具EsseCC（CC，Connectivity Checking），是一個(gè)高效的連接性檢查的驗(yàn)證工具，為用戶提供快速的錯(cuò)誤檢測(cè)以及預(yù)期設(shè)計(jì)行為的信號(hào)到信號(hào)的驗(yàn)證。該產(chǎn)品以RTL電路和連接規(guī)范作為輸入，快速檢查設(shè)計(jì)是否符合連接規(guī)范。與傳統(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)的覆蓋率檢查；
支持生成反例的 Testbench 及波形圖；
GUI界面提供原理圖、波形查看。
應(yīng)用場(chǎng)景
SoC I/O 連接性檢查；
綜合后網(wǎng)表連接性檢查；
驗(yàn)證Chiplet技術(shù)下模塊的連接性檢查；
全局時(shí)鐘及復(fù)位信號(hào)連接性檢查；
總線寄存器的連接性檢查；
集成IP的連接性檢查。
產(chǎn)品簡(jiǎn)介
芯天成覆蓋不可達(dá)性檢查工具EsseUNR（Coverage Unreachability Checking），是一款高效的覆蓋不可達(dá)性檢查工具。使用傳統(tǒng)的驗(yàn)證方式，在驗(yàn)證后期，通過(guò)編寫測(cè)試用例提升驗(yàn)證覆蓋率的難度陡然上升。由此，使用EsseUNR工具，可更高效地對(duì)未覆蓋的代碼進(jìn)行全面的不可達(dá)性檢查。EsseUNR具有效率更高、更準(zhǔn)確、更易上手的優(yōu)點(diǎn)。
核心優(yōu)勢(shì)
兼容性高、快速、高效；
直觀易操作的用戶界面；
適配主流仿真軟的覆蓋數(shù)據(jù)；
支持生成Testbench和波形顯示；
支持RTL級(jí)的Formal不可達(dá)性檢查。
產(chǎn)品功能
支持Verilog/SystemVerilog和VHDL的混合編譯；
支持利用主流仿真工具覆蓋數(shù)據(jù)對(duì)未覆蓋代碼進(jìn)行不可達(dá)性檢查；
用形式驗(yàn)證的方法對(duì)RTL設(shè)計(jì)進(jìn)行不可達(dá)性檢查；
支持RTL設(shè)計(jì)Line/Condition/Fsm/Branch/Toggle類型的不可達(dá)性檢查；
支持生成可達(dá)的檢查點(diǎn)的Testbench及波形圖；
支持通過(guò)GUI界面查看原理圖、波形。
應(yīng)用場(chǎng)景
支持ASIC/FPGA的不可達(dá)性檢查；
通信協(xié)議通信狀態(tài)的不可達(dá)性檢查；
處理器控制單元的不可達(dá)性檢查；
DMA控制器的不可達(dá)性檢查；
寄存器狀態(tài)的不可達(dá)性檢查。
