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

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

芯華章科技

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

難題Chair介紹

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

曾就職于Synopsys美國(guó)山景城研發(fā)總部，任芯片驗(yàn)證事業(yè)部高級(jí)研發(fā)工程師，回國(guó)后主要研究方向?yàn)橛布问交?yàn)證以及芯片靜態(tài)檢測(cè)技術(shù)。

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

芯華章難題介紹

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

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

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

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

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

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

一種用于隨機(jī)約束仿真的SAT增強(qiáng)的字級(jí)求解器

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