形式验证@eda论坛聚焦于eda中的形式验证技术，包括sat/smt求解、硬件模型检测、等价性验证、基于断言的形式验证、指令集一致性形式验证、信息安全性质形式验证、缓存一致性协议形式验证、乘除法器和浮点计算单元形式验证、指令集语义形式建模、硬件设计形式验证案例研究等。eda软件对于芯片设计开发至关重要，属于中国急需突破的卡脖子技术。形式验证是保证计算机软硬件系统正确性与安全性的非常重要的手段，已经成为eda软件芯片设计验证工具不可或缺的组成部分，全世界三大eda软件厂商cadence、synopsis、siemens的eda软件均包含成熟的芯片设计形式验证工具。本论坛的长期举办希望能推动eda中的形式验证技术在中国的发展，促进相关研究社区的形成，为缓解eda卡脖子问题贡献力量。
01
论坛组织委员会
李建文（华东师范大学）
张弘策（香港科技大学（广州））
李暾（国防科技大学）
02
论坛议程
03
论坛报告嘉宾简介
徐强
报告题目：电路学习驱动的sat求解器
报告摘要：
布尔可满足性问题（sat）作为电子设计自动化（eda）、软件验证等多个领域的基础问题，长期以来吸引了广泛的研究关注。然而，近年来传统sat求解器的性能提升逐渐趋于瓶颈，缺乏突破性进展，难以应对不断增长的工业规模实例。本报告提出了一种电路学习驱动的sat求解器，旨在通过引入电路学习技术，突破传统方法的局限性。具体而言，我们利用深度学习模型对电路网表进行特征提取与模式识别，结合启发式搜索方法，显著减少了sat问题空间的搜索复杂度从而有效加速sat求解过程。实验结果表明，该方法在多个工业规模的基准测试中展示了显著的性能提升，尤其在求解速度和资源消耗方面展现了巨大的优化潜力，证明了电路学习在sat求解中的广泛应用前景。
报告人简介：
徐强，香港中文大学计算机科学与工程系教授，国家集成电路设计自动化技术创新中心首席科学家。当前研究兴趣集中在人工智能和电子设计自动化领域。他已经发表了180多篇论文，累计引用近万次，其中包括多篇顶级会议最佳论文奖和iccad十年回顾最具影响力论文奖。他指导了超过20名博士，多位学生获得过杰出博士论文奖或提名（edaa以及ieee tttc）。
储著飞
报告题目：逻辑综合工具中的sat求解器与仿真器应用
报告摘要：
逻辑综合工具是数字集成电路前端设计的核心，主要解决在逻辑功能等价前提下布尔函数的表示、优化和工艺映射等问题，sat求解器和逻辑功能仿真器是逻辑综合推理中重要的引擎，报告通过介绍逻辑综合工具的发展历史、基础问题、学术界和工业界进展等出发，探讨sat求解器和仿真器在逻辑综合工具中的应用，以及对未来的展望。
报告人简介：
储著飞，宁波大学信息科学与工程学院教授，博士生导师。研究方向为集成电路设计自动化(eda)，包括逻辑综合与优化，物理设计，逻辑等价性验证等。担任eda开放创新合作机制“数字逻辑设计与验证”分委会主任，《eda技术白皮书》领域主编，全国集成电路标准化技术委员会/eda工作组委员、dac、date等会议技术委员会委员，在开源平台开源了自研的逻辑综合工具also。研究成果获得浙江省技术发明二等奖1次，宁波市科学技术进步奖一等奖2次，指导研究生获得smacd竞赛奖，ccfdac最佳论文奖，iseda荣誉论文奖等。
吴志林
报告题目：算术单元chisel设计的参数化形式验证
报告摘要：
chisel是一种嵌入在scala中的开源硬件描述语言，可以用于实现参数化和可重用的数字电路设计。chisel变得越来越流行，已被广泛用于risc-v处理器的设计，比如rocketchip、boom、xiangshan等。虽然chisel硬件设计抽象层次较高，但其验证目前仍然需要转换到相对低层的语言（比如verilog）来进行。我们提出了一种对算术单元chisel设计进行高层形式化验证的方法，实现了参数化验证，即对所有位宽一次性进行验证，而不是每个位宽单独进行验证。我们方法的核心思想是将算术单元chisel 设计转换为模拟其行为的scala 软件代码，然后使用scala的形式化验证工具 stainless来进行证明。我们在stainless中开发了关于整数非线性算术和线性表数据结构的证明库，并基于这种方法验证了rocketchip 和 xiangshan 的除法器和乘法器的功能正确性。
报告人简介：
吴志林，中国科学院软件研究所基础软件与系统重点实验室研究员，博士生导师， 2020年“ccf-ieee cs”青年科学家奖获得者。博士毕业于中国科学院软件研究所计算机科学国家重点实验室，先后在中国科学院自动化研究所中法计算机科学、自动化与应用数学联合实验室和法国波尔多第一大学labri实验室从事博士后研究。2014-2015在法国巴黎第七大学irif实验室担任国家留学基金委公派访问学者。长期从事计算机软硬件系统形式化验证、计算逻辑、自动机理论等相关研究，在知名国际会议和期刊上发表论文40余篇，包括lics、popl、cav、dac、information and computation、ijcar、cade、concur等。先后主持多项国家级项目，包括国家重点研发计划课题、中科院先导a项目课题、“十三五”全军共用信息系统装备预先研究项目等。中国计算机学会形式化方法专业委员会秘书长，国际会议atva 2022、tase 2025程序委员会共同主席，cav、concur、atva等国际会议的程序委员会委员。
隋兵才
报告题目：形式化验证在高性能通用处理器中的实践与应用
报告摘要：
形式化验证作为一种全新的验证方法，近年来在芯片开发中快速发展，正逐渐取代传统的仿真方法。对形式化技术而言，如何能够取代动态验证技术，以更低的成本实现更高质量的signoff，如何在高性能处理器中利用形式化方法加速设计迭代，将是比较有挑战性的问题。本次报告中我们将分享高性能通用处理器设计实现中相关形式化验证的相关实践应用以及经验总结，并从实践角度对形式化验证进行相关的展望。
报告人简介：
隋兵才，国防科技大学计算机学院副研究员，ccf高级会员，ccf集成电路设计专委执行委员, 2010年获国防科学技术大学微电子学与固体电子学博士学位。现为国防科技大学计算机学院微电子所中央处理器微架构研究室主任。长期从事通用高性能处理器芯片研制，主要研究方向为高性能通用处理器系统结构、微体系结构、通用处理器设计与实现。获国家科技进步一等奖1项，省部级二等奖1项。
魏星
报告题目：形式验证技术在eda逻辑功能等价验证工具中的应用
报告摘要：
形式验证是一种基于严格数学推理的设计验证技术，它通过静态、全面的逻辑分析来确保设计的正确性，显著降低了对庞大测试集的需求，并力求实现接近完美的验证覆盖率，在eda逻辑功能等价验证工具中的应用非常广泛且重要。通过充分利用形式验证技术的优势，结合其他验证手段，可以显著提升设计验证的效率和质量，确保芯片设计的正确性和可靠性。本报告主要介绍形式验证技术在eda逻辑功能等价验证工具中的具体应用以及优势与挑战。
报告人简介：
魏星，奇捷科技（深圳）有限公司联合创始人兼ceo。本科和硕士就读于清华大学计算机系eda实验室；博士就读于香港中文大学eda实验室，曾在2012、2013、2014和2021年共四次获得国际知名会议iccad举办的cad比赛世界冠军。魏星博士设计开发的逻辑功能变更工具（functional eco），成功解决了多个世界级技术难题，并成功转化成产品，正式付费的商业客户（顶级芯片设计企业）已达数十家，遍布中国大陆、中国台湾、韩国、美国等多个国家和地区。
04
论坛组织委员会简介
论坛主席：李建文
个人简介：
李建文，华东师范大学研究员，博士生导师，入选上海市青年人才计划，获得上海市浦江人才荣誉称号，主持国家自然科学基金面上项目、青年项目、重点项目子课题各一项。研究方向主要为形式化自动验证技术，可用于保障计算机软硬件系统的正确性和安全性，重点应用场景包括芯片、航天、轨道交通等安全攸关领域。担任2024年cav、fm等形式化领域国际顶级会议的pc。
论坛主席：张弘策
个人简介：
张弘策，香港科技大学（广州）功能枢纽微电子学域助理教授。博士毕业于普林斯顿大学电子与计算机工程系，主要研究方向为数字芯片的形式化验证方法。研究成果发表于dac，cav，iccad，tcad等eda领域顶级国际会议与期刊，曾获得2020年美国计算机学会电子设计自动化期刊todaes的最佳文章奖，担任了cav、dac、fmcad等国际会议的技术程序委员会成员。
论坛主席：李暾
个人简介：
李暾，国防科技大学教授，博士生导师。ccf集成电路设计专委执行委员。主要研究方向为微处理器rtl及之上层次设计的设计验证方法与技术，包括系统级与rtl等价性检查、模拟激励自动生成、微处理器敏捷设计方法、模糊测试技术、verilog代码自动修复等。相关工作在tcad、date、glsvlsi、aspdac等eda领域期刊与会议发表50余篇论文。
