EDA2俠客島官網(wǎng)https://xiakedao.eda2.com/

為打破產(chǎn)業(yè)和學(xué)術(shù)界限，促進政企校高度結(jié)合，芯華章聯(lián)合EDA平方、黃大年茶思屋，打造EDA2俠客島，致力于打通EDA競賽、課題、實驗平臺、社區(qū)論壇等多生態(tài)場景，通過EDA2共享廣闊資源。

芯華章科技

芯華章聚焦EDA數(shù)字驗證領(lǐng)域，打造從芯片到系統(tǒng)的敏捷驗證解決方案，申請自主研發(fā)專利超160件，發(fā)布十?dāng)?shù)款基于平臺化、智能化、云化底層構(gòu)架的商用級驗證產(chǎn)品，可提供完整數(shù)字驗證全流程EDA工具。目前，芯華章在北京、上海、南京、深圳等地建立了九大研發(fā)中心，集結(jié)了一支500余人的全球化精英團隊，其中八成為尖端研發(fā)人員，碩博比例高達70%。

難題Chair介紹

劉軍，現(xiàn)任芯華章科技高級研發(fā)總監(jiān)，芯華章研究院研究員。目前在芯華章研究院主持高性能形式化求解引擎研究工作，并致力于使用機器學(xué)習(xí)技術(shù)提高形式化求解引擎性能，畢業(yè)于上海交通大學(xué)，獲微電子碩士學(xué)位，江蘇省集成電路學(xué)會會員。

曾就職于Synopsys美國山景城研發(fā)總部，任芯片驗證事業(yè)部高級研發(fā)工程師，回國后主要研究方向為硬件形式化驗證以及芯片靜態(tài)檢測技術(shù)。

帶領(lǐng)團隊從0到1實現(xiàn)了芯華章形式驗證產(chǎn)品GalaxFV/GalaxEC, 長期從事高性能形式化求解引擎，隨機約束求解引擎相關(guān)研究工作，獲多項國家發(fā)明專利。

芯華章難題介紹

隨著芯片設(shè)計的復(fù)雜度越來越高，芯片驗證的難度也越來越大。形式化驗證（Formal Verification）作為一種高效的驗證方法，在芯片驗證中已經(jīng)被越來越廣泛應(yīng)用，成為數(shù)字驗證流程中重要的組成部分。傳統(tǒng)的邏輯仿真存在覆蓋率難以保證的問題，使用形式化驗證方法可以發(fā)現(xiàn)硬件設(shè)計尤其是關(guān)鍵設(shè)計路徑（Critical Path）中可能存在的缺陷和錯誤，大幅縮短驗證周期并提高設(shè)計可靠性。

形式化驗證的其中一種方法是模型檢測（Model Checking），用戶利用 SVA 斷言描述清楚需要證明的設(shè)計規(guī)格，通過編譯 RTL 和基于 SVA 的斷言語言，建立數(shù)學(xué)模型，以數(shù)學(xué)證明的方式，通過對所有可能的狀態(tài)空間進行遍歷，保證驗證沒有死角，實現(xiàn)驗證的完備化、自動化。

現(xiàn)階段限制模型檢測技術(shù)大幅推廣和采用的一個根本原因是驗證收斂性問題。工業(yè)級芯片設(shè)計往往非常復(fù)雜，且數(shù)據(jù)通路繁重，由于模型檢測工具采取詳盡空間探索方式進行驗證，常常會碰到狀態(tài)空間爆炸問題，導(dǎo)致驗證不收斂。

算力的提升以及算法級創(chuàng)新是解決模型檢測收斂性問題的最重要途徑，我們希望能通過本次賽題打榜方式，可以有更多的專家學(xué)者或者新生力量一起參與解決工業(yè)級形式化驗證求解難題，更好地促進產(chǎn)學(xué)研合作，加速推進學(xué)術(shù)研究產(chǎn)業(yè)化。

芯華章2023年俠客島難題挑戰(zhàn)正式開啟，我們將以“面向工業(yè)級設(shè)計的可擴展硬件模型檢測引擎”為主線，長遠(yuǎn)持續(xù)更新芯片驗證模型檢測技術(shù)相關(guān)求解難題，推廣形式化驗證方法學(xué)，歡迎世界各地的學(xué)生、老師持續(xù)關(guān)注，揭榜挑戰(zhàn)。

對形式驗證感興趣的同學(xué)，推薦閱讀如下技術(shù)分享：

一種用于隨機約束仿真的SAT增強的字級求解器

形式化驗證漫談：仿真之外，驗證之內(nèi)