聚英才纵碧霄，决战EDA产业之巅

EDA?侠客岛官网https://xiakedao.eda2.com/

为打破产业和学术界限，促进政企校高度结合，芯华章联合EDA平方、黄大年茶思屋，打造EDA?侠客岛，致力于打通EDA竞赛、课题、实验平台、社区论坛等多生态场景，通过EDA?共享广阔资源。

芯华章科技

芯华章聚焦EDA数字验证领域，打造从芯片到系统的敏捷验证解决方案，申请自主研发专利超160件，发布十数款基于平台化、智能化、云化底层构架的商用级验证产品，可提供完整数字验证全流程EDA工具。目前，芯华章在北京、上海、南京、深圳等地建立了九大研发中心，集结了一支500余人的全球化精英团队，其中八成为尖端研发人员，硕博比例高达70%。

难题Chair介绍

刘军，现任芯华章科技高级研发总监，芯华章研究院研究员。目前在芯华章研究院主持高性能形式化求解引擎研究工作，并致力于使用机器学习技术提高形式化求解引擎性能，毕业于上海交通大学，获微电子硕士学位，江苏省集成电路学会会员。

曾就职于Synopsys美国山景城研发总部，任芯片验证事业部高级研发工程师，回国后主要研究方向为硬件形式化验证以及芯片静态检测技术。

带领团队从0到1实现了芯华章形式验证产品GalaxFV/GalaxEC, 长期从事高性能形式化求解引擎，随机约束求解引擎相关研究工作，获多项国家发明专利。

芯华章难题介绍

随着芯片设计的复杂度越来越高，芯片验证的难度也越来越大。形式化验证（Formal Verification）作为一种高效的验证方法，在芯片验证中已经被越来越广泛应用，成为数字验证流程中重要的组成部分。传统的逻辑仿真存在覆盖率难以保证的问题，使用形式化验证方法可以发现硬件设计尤其是关键设计路径（Critical Path）中可能存在的缺陷和错误，大幅缩短验证周期并提高设计可靠性。

形式化验证的其中一种方法是模型检测（Model Checking），用户利用 SVA 断言描述清楚需要证明的设计规格，通过编译 RTL 和基于 SVA 的断言语言，建立数学模型，以数学证明的方式，通过对所有可能的状态空间进行遍历，保证验证没有死角，实现验证的完备化、自动化。

现阶段限制模型检测技术大幅推广和采用的一个根本原因是验证收敛性问题。工业级芯片设计往往非常复杂，且数据通路繁重，由于模型检测工具采取详尽空间探索方式进行验证，常常会碰到状态空间爆炸问题，导致验证不收敛。

算力的提升以及算法级创新是解决模型检测收敛性问题的最重要途径，我们希望能通过本次赛题打榜方式，可以有更多的专家学者或者新生力量一起参与解决工业级形式化验证求解难题，更好地促进产学研合作，加速推进学术研究产业化。

芯华章2023年侠客岛难题挑战正式开启，我们将以“面向工业级设计的可扩展硬件模型检测引擎”为主线，长远持续更新芯片验证模型检测技术相关求解难题，推广形式化验证方法学，欢迎世界各地的学生、老师持续关注，揭榜挑战。

对形式验证感兴趣的同学，推荐阅读如下技术分享：

一种用于随机约束仿真的SAT增强的字级求解器

形式化验证漫谈：仿真之外，验证之内