EDA2俠客島 ?

EDA2俠客島官網https://xiakedao.eda2.com/

為打破產業和學術界限，促進政企校高度結合，芯華章聯合EDA平方、黃大年茶思屋，打造EDA2俠客島，致力于打通EDA競賽、課題、實驗平臺、社區論壇等多生態場景，通過EDA2共享廣闊資源。

本項目將結合芯華章推動EDA發展創新中遇到的實際挑戰，發布具備前瞻性的賽題與課題，提供產業界真實稀缺數據，基于強大的在線打榜平臺，以長期、持續進行的打榜模式，培養和挖掘領域精英，推動產業技術創新，共同探索EDA產業難題，培養和挖掘領域精英，助力人才成長。

芯華章科技

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

難題Chair介紹

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

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

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

芯華章難題介紹

難題：面向工業級設計的可擴展硬件模型檢測引擎難題標簽：形式驗證，模型檢測，SAT，SMT，并行/分布式求解加速命題企業：芯華章科技股份有限公司難題Chair：劉軍（芯華章科技研發總監，芯華章研究院研究員）難題咨詢窗口：yiyang@x-epic.com

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

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

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

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

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

對形式驗證感興趣的同學，推薦閱讀如下技術分享：

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

形式化驗證漫談：仿真之外，驗證之內

難題挑戰流程獎項配置