芯天成形式驗證平臺EsseFormal
EsseFECT
EsseFCEC
EsseFPV
EsseCC
EsseUNR
產(chǎn)品簡介
芯天成形式化等價性驗證工具FECT（Formal 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)定、準(zhǔn)確和高速的工業(yè)級芯片等價性驗證方案，以應(yīng)對芯片設(shè)計與驗證過程中的面積優(yōu)化、功耗優(yōu)化和驗證速度瓶頸問題。
該產(chǎn)品基于可滿足性算法及電路優(yōu)化算法，可以支持綜合工具對電路的低功耗優(yōu)化、面積優(yōu)化等各種先進(jìn)優(yōu)化策略，能夠驗證超大規(guī)模電路之間的等價性，為芯片設(shè)計與驗證提供高精度的解決方案。
核心優(yōu)勢
穩(wěn)定、準(zhǔn)確、高速的驗證流程；
支持綜合工具的各種先進(jìn)綜合策略；
方便快捷的驗證結(jié)果調(diào)試；
簡潔易用的圖形用戶界面；
適用于各個階段電路之間的驗證。
產(chǎn)品功能
支持System Verilog、VHDL等多種設(shè)計格式讀?。?/p>
支持組合邏輯等價性驗證與時序等價性驗證；
支持fsm recoding、clock-gating、retiming等先進(jìn)綜合優(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è)計功能的高正確率；
支持?jǐn)嘌詫傩?、約束屬性、覆蓋屬性的驗證，可在設(shè)計中更快地發(fā)現(xiàn)bug并提供反例；
人性化的用戶圖形界面，對于習(xí)慣圖形化系統(tǒng)的用戶更友好，利于debug調(diào)試。
應(yīng)用方案
檢查設(shè)計行為的斷言；
約束形式化驗證環(huán)境的假設(shè)；
用于監(jiān)視預(yù)期事件的覆蓋屬性。
產(chǎn)品簡介
芯天成連接性檢查工具EsseCC（CC，Connectivity Checking），是一個高效的連接性檢查的驗證工具，為用戶提供快速的錯誤檢測以及預(yù)期設(shè)計行為的信號到信號的驗證。該產(chǎn)品以RTL電路和連接規(guī)范作為輸入，快速檢查設(shè)計是否符合連接規(guī)范。與傳統(tǒng)驗證方式相比，EsseCC具有高效率、高準(zhǔn)確率，上手簡單便捷的優(yōu)點。
核心優(yōu)勢
快速、高效的驗證流程；
直觀易操作的用戶界面；
支持反例生成和波形顯示；
支持多種引擎的連接性檢查；
支持生成跨DFF的連接關(guān)系生成。
產(chǎn)品功能
支持Verilog/SystemVerilog和VHDL的混合編譯；
支持物理路徑及連接屬性的驗證；
支持反向生成連接；
支持連接信號的覆蓋率檢查；
支持生成反例的 Testbench 及波形圖；
GUI界面提供原理圖、波形查看。
應(yīng)用場景
SoC I/O 連接性檢查；
綜合后網(wǎng)表連接性檢查；
驗證Chiplet技術(shù)下模塊的連接性檢查；
全局時鐘及復(fù)位信號連接性檢查；
總線寄存器的連接性檢查；
集成IP的連接性檢查。
產(chǎn)品簡介
芯天成覆蓋不可達(dá)性檢查工具EsseUNR（Coverage Unreachability Checking），是一款高效的覆蓋不可達(dá)性檢查工具。使用傳統(tǒng)的驗證方式，在驗證后期，通過編寫測試用例提升驗證覆蓋率的難度陡然上升。由此，使用EsseUNR工具，可更高效地對未覆蓋的代碼進(jìn)行全面的不可達(dá)性檢查。EsseUNR具有效率更高、更準(zhǔn)確、更易上手的優(yōu)點。
核心優(yōu)勢
兼容性高、快速、高效；
直觀易操作的用戶界面；
適配主流仿真軟的覆蓋數(shù)據(jù)；
支持生成Testbench和波形顯示；
支持RTL級的Formal不可達(dá)性檢查。
產(chǎn)品功能
支持Verilog/SystemVerilog和VHDL的混合編譯；
支持利用主流仿真工具覆蓋數(shù)據(jù)對未覆蓋代碼進(jìn)行不可達(dá)性檢查；
用形式驗證的方法對RTL設(shè)計進(jìn)行不可達(dá)性檢查；
支持RTL設(shè)計Line/Condition/Fsm/Branch/Toggle類型的不可達(dá)性檢查；
支持生成可達(dá)的檢查點的Testbench及波形圖；
支持通過GUI界面查看原理圖、波形。
應(yīng)用場景
支持ASIC/FPGA的不可達(dá)性檢查；
通信協(xié)議通信狀態(tài)的不可達(dá)性檢查；
處理器控制單元的不可達(dá)性檢查；
DMA控制器的不可達(dá)性檢查；
寄存器狀態(tài)的不可達(dá)性檢查。
