作為一名驗(yàn)證工程師你一定經(jīng)歷過下面的靈魂拷問

驗(yàn)證網(wǎng)表和RTL代碼是否一致？邏輯仿真是否為最優(yōu)解？

每一個步驟后都有新的邏輯加入到netlist中，但新的邏輯的加入不能改變原netlist的邏輯功能，如何能進(jìn)一步保證綜合后的網(wǎng)表與RTL之間的邏輯一致性？

當(dāng)芯片規(guī)模越來越大，設(shè)計(jì)復(fù)雜性的不斷增加，BUG表現(xiàn)的方式各不相同帶來驗(yàn)證周期大幅增長，設(shè)計(jì)過程中的實(shí)際調(diào)試工作耗費(fèi)大量的時間和精力，為了能夠最大程度的使得驗(yàn)證收斂，我們也有越來越多的驗(yàn)證方法..

相比邏輯仿真，形式驗(yàn)證更適用于哪些場景？

形式驗(yàn)證如何比較兩個設(shè)計(jì)是否等價？

本期的技術(shù)視頻將圍繞形式化驗(yàn)證工具和大家展開分享等價性驗(yàn)證GalaxEC如何有效提升設(shè)計(jì)和驗(yàn)證效率，你想了解的知識點(diǎn)這里都有！

Part 1 :?芯華章數(shù)字驗(yàn)證全流程工具平臺介紹

芯華章提供完整的數(shù)字驗(yàn)證全流程工具平臺以滿足不同階段和不同需求的驗(yàn)證。通過多工具融合與協(xié)同，提高驗(yàn)證效率和準(zhǔn)確性，從而縮短芯片設(shè)計(jì)周期和降低成本。

Part 2：從RTL到門級網(wǎng)表的等價性驗(yàn)證

在完整的芯片設(shè)計(jì)流程中，等價性驗(yàn)證工具被廣泛應(yīng)用到設(shè)計(jì)流程中的各個不同階段。諸如系統(tǒng)C模型級對RTL級、RTL級對RTL級、RTL級對門級以及門級實(shí)現(xiàn)之間，工程師需要檢驗(yàn)變換前后的功能一致性，證明設(shè)計(jì)的變換或優(yōu)化沒有產(chǎn)生功能的變化。

Part 3：貫穿IC設(shè)計(jì)全流程的三大等價檢查功能?SEC、LEC、HEC

GalaxEC已具備當(dāng)下各類主流等價性驗(yàn)證工具的所有核心功能，服務(wù)場景貫穿于數(shù)字芯片設(shè)計(jì)從系統(tǒng)級到前后端設(shè)計(jì)的各個階段，可一站式滿足用戶全流程等價性驗(yàn)證需求，避免多工具切換成本，幫助工程師確保不同層次設(shè)計(jì)之間的一致性，支持遍歷式驗(yàn)證，發(fā)現(xiàn)深層次的臨界設(shè)計(jì)錯誤，確保設(shè)計(jì)的正確性并實(shí)現(xiàn)正式簽核。

Part 4：GalaxEC深度結(jié)合芯華章智V驗(yàn)證平臺各工具

芯華章智V驗(yàn)證平臺提供的統(tǒng)一底層框架、統(tǒng)一覆蓋率數(shù)據(jù)庫和調(diào)試系統(tǒng)，F(xiàn)usion Debug可直接支持GalaxEC等價性的結(jié)果調(diào)試，自動載入雙設(shè)計(jì)數(shù)據(jù)對比，在SEC場景中進(jìn)行源和目標(biāo)的代碼對比，從LEC報告中選擇有差異的邏輯錐并進(jìn)行電路對比。