本帖最后由 仗剑天涯 于 2023-11-29 11:53 编辑
难题介绍 随着芯片设计的复杂度越来越高，芯片验证的难度也越来越大。形式化验证（Formal Verification）作为一种高效的验证方法，在芯片验证中已经被越来越广泛应用，成为数字验证流程中重要的组成部分。传统的逻辑仿真存在覆盖率难以保证的问题，使用形式化验证方法可以发现硬件设计尤其是关键设计路径（Critical Path）中可能存在的缺陷和错误，大幅缩短验证周期并提高设计可靠性。 形式化验证的其中一种方法是模型检测（Model Checking），用户利用 SVA 断言描述清楚需要证明的设计规格，通过编译 RTL 和基于 SVA 的断言语言，建立数学模型，以数学证明的方式，通过对所有可能的状态空间进行遍历，保证验证没有死角，实现验证的完备化、自动化。 现阶段限制模型检测技术大幅推广和采用的一个根本原因是验证收敛性问题。工业级芯片设计往往非常复杂，且数据通路繁重，由于模型检测工具采取详尽空间探索方式进行验证，常常会碰到状态空间爆炸问题，导致验证不收敛。算力的提升以及算法级创新是解决模型检测收敛性问题的最重要途径，我们希望能通过本次赛题打榜方式，可以有更多的专家学者或者新生力量一起参与解决工业级形式化验证求解难题，更好地促进产学研合作，加速推进学术研究产业化。 芯华章2023年EDA²侠客岛难题挑战正式开启，我们将以“面向工业级设计的可扩展硬件模型检测引擎”为主线，长远持续更新芯片验证模型检测技术相关求解难题，推广形式化验证方法学，欢迎世界各地的学生、老师持续关注，揭榜挑战。
难题标签
命题企业
难题Chair
刘军，现任芯华章科技研发总监，芯华章研究院研究员。目前在芯华章研究院主持高性能形式化求解引擎研究工作，并致力于使用机器学习技术提高形式化求解引擎性能，毕业于上海交通大学，获微电子硕士学位，江苏省集成电路学会会员。曾就职于Synopsys 美国山景城研发总部，任芯片验证事业部高级研发工程师，回国后主要研究方向为硬件形式化验证以及芯片静态检测技术。带领团队从0到1实现了芯华章形式验证产品 GalaxFV/GalaxEC, 长期从事高性能形式化求解引擎，随机约束求解引擎相关研究工作，获多项国家发明专利。
欢迎咨询
官方网站
奖项配置
其他事宜
关于EDA²
EDA²是在实现中国集成电路电子设计自动化长期竞争力的共同愿景下，由从事集成电路电子设计自动化的研究、设计、验证、测试、应用和服务的企事业单位、大学和科研院所、专业机构等单位自愿组成，专注于推动中国集成电路电子设计自动化产业发展的合作机制。
关于EDA²侠客岛
EDA²侠客岛与黄大年茶思屋，EDA²生态伙伴联合发布具备前瞻性的赛题与课题，通过提供产业界真实稀缺数据，打破产业和学术界限，促进政企校高度结合，基于强大的在线打榜平台，以持续进行的打榜模式，培养和挖掘领域精英，推动产业技术创新，让我们共同探索EDA产业难题，助力人才成长。
关于芯华章科技
芯华章聚焦EDA数字验证领域，打造从芯片到系统的敏捷验证解决方案，申请自主研发专利超160件，发布十数款基于平台化、智能化、云化底层构架的商用级验证产品，可提供完整数字验证全流程EDA工具。目前，芯华章在北京、上海、南京、深圳等地建立了九大研发中心，集结了一支500余人的全球化精英团队，其中八成为尖端研发人员，硕博比例高达70%。
| 
