第一期EDA²侠客岛的难题挑战共有4个挑战赛道，涉及的范围都来自企业实际项目。
EDA²侠客岛
为打破产业和学术界限，促进政企校高度结合，芯华章联合EDA平方、黄大年茶思屋，打造EDA²侠客岛，致力于打通EDA竞赛、课题、实验平台、社区论坛等多生态场景，通过EDA²共享广阔资源。
本项目将结合芯华章推动EDA发展创新中遇到的实际挑战，发布具备前瞻性的赛题与课题，提供产业界真实稀缺数据，基于强大的在线打榜平台，以长期、持续进行的打榜模式，培养和挖掘领域精英，推动产业技术创新，共同探索EDA产业难题，培养和挖掘领域精英，助力人才成长。
赛题背景
四道赛题的赛题涵盖故障仿真、鲲鹏、DFT、大规模稀疏矩阵、Gauss消去法、形式验证、模型检测、SAT等关键技术领域，赛题Chair均来自各大知名企业的专家。
其中，海思EDA首席架构师黄宇担任“基于ARM多核CPU架构的故障仿真并行加速” 难题Chair，芯华章科技研发总监，芯华章研究院研究员刘军负责“面向工业级设计的可扩展硬件模型检测引擎”。
难题一介绍
难题：基于ARM多核CPU架构的故障仿真并行加速
难题标签：鲲鹏，DFT，故障仿真，并行，分布式，自动测试向量生成
赞助企业：集成电路EDA设计精英挑战赛
难题Chair：黄宇（海思EDA首席架构师）
难题一Chair介绍
黄宇博士是华为半导体科学家，海思EDA首席架构师和EDA实验室主任。
曾任美国Mentor Graphics Sr. Key Expert，研究领域包括VLSI SoC测试，压缩，诊断，良率分析、机器学习和AI芯片。
获得美国爱荷华大学电子和计算机工程博士学位，拥有70+项专利，并发表140多篇国际论文。他是IEEE高级会员，曾担任DAC，ITC，VTS，ATS，ETS，ASPDAC，NATW等多个国际会议的组委会委员，他也是中国复旦大学微电子学院和西电微电子学院的兼职教授和企业博导。
难题二介绍
难题：面向工业级设计的可扩展硬件模型检测引擎
难题标签：形式验证，模型检测，SAT，SMT，并行/分布式求解加速
命题企业：芯华章科技股份有限公司
难题Chair：刘军（芯华章科技研发总监，芯华章研究院研究员）
难题咨询窗口：yiyang@x-epic.com
随着芯片设计的复杂度越来越高，芯片验证的难度也越来越大。形式化验证（Formal Verification）作为一种高效的验证方法，在芯片验证中已经被越来越广泛应用，成为数字验证流程中重要的组成部分。传统的逻辑仿真存在覆盖率难以保证的问题，使用形式化验证方法可以发现硬件设计尤其是关键设计路径（Critical Path）中可能存在的缺陷和错误，大幅缩短验证周期并提高设计可靠性。
形式化验证的其中一种方法是模型检测（Model Checking），用户利用 SVA 断言描述清楚需要证明的设计规格，通过编译 RTL 和基于 SVA 的断言语言，建立数学模型，以数学证明的方式，通过对所有可能的状态空间进行遍历，保证验证没有死角，实现验证的完备化、自动化。
现阶段限制模型检测技术大幅推广和采用的一个根本原因是验证收敛性问题。工业级芯片设计往往非常复杂，且数据通路繁重，由于模型检测工具采取详尽空间探索方式进行验证，常常会碰到状态空间爆炸问题，导致验证不收敛。
算力的提升以及算法级创新是解决模型检测收敛性问题的最重要途径，我们希望能通过本次赛题打榜方式，可以有更多的专家学者或者新生力量一起参与解决工业级形式化验证求解难题，更好地促进产学研合作，加速推进学术研究产业化。
芯华章2023年侠客岛难题挑战正式开启，我们将以“面向工业级设计的可扩展硬件模型检测引擎”为主线，长远持续更新芯片验证模型检测技术相关求解难题，推广形式化验证方法学，欢迎世界各地的学生、老师持续关注，揭榜挑战。
对形式验证感兴趣的同学，推荐阅读如下技术分享：
难题二Chair介绍
刘军，现任芯华章科技高级研发总监，芯华章研究院研究员。目前在芯华章研究院主持高性能形式化求解引擎研究工作，并致力于使用机器学习技术提高形式化求解引擎性能，毕业于上海交通大学，获微电子硕士学位，江苏省集成电路学会会员。
曾就职于Synopsys美国山景城研发总部，任芯片验证事业部高级研发工程师，回国后主要研究方向为硬件形式化验证以及芯片静态检测技术。
带领团队从0到1实现了芯华章形式验证产品GalaxFV/GalaxEC, 长期从事高性能形式化求解引擎，随机约束求解引擎相关研究工作，获多项国家发明专利。
难题挑战流程
其他事宜
