电子设计自动化软件验证

---

电子设计自动化（EDA）软件在芯片设计和制作中具有重要的作用。对设计的芯片进行正确性保障是EDA软件的重要功能之一。形式化验证方法是实现芯片设计正确性保障的重要技术和手段。电子设计自动化软件验证论坛聚焦国内芯片验证软件最新行业进展和理论前沿，深度解析我国EDA软件形式化验证领域现状，研讨目前学术界的发展趋势、工业界的应用成果、主要问题和挑战等。论坛邀请了来自学术界和的工业界多位顶尖专家，旨在深化拓展学术研究成果与产业实践需求交叉，加强学术界与工业界合作，促进国产EDA验证软件理论研究、工具成果和行业实践应用的融合发展。

论坛主席：

蒲戈光（上海工业控制安全创新科技有限公司，华东师范大学）

论坛主持人：

蒲戈光（上海工业控制安全创新科技有限公司，华东师范大学）

论坛支持单位：

上海工业控制安全创新科技有限公司

华东师范大学

日程安排：

时间：2021年12月24日（星期五），14:00~18:00

论坛议程：

论坛报告嘉宾简介：

1. 报告人：袁军

题目：芯片形式验证技术及应用

摘要： 随着芯片集成度的快速提高及设计周期的不断缩短，芯片功能验证面临着巨大的挑战。形式验证相对于传统的仿真，包括硬件加速仿真，是一个比较新而且在技术及应用方面仍在不断发展的验证方法学。本文介绍上海阿卡思公司在形式验证方面的一些工作，包括已经商业化的属性验证和等价验证工具，和在研的其他工具。同时介绍工具的几个技术特点，在实现过程中遇到的一些问题，以及实用案例。

简介： 袁军，博士。从九十年代起即从事集成电路设计自动化(EDA)研究和应用，特别针对形式逻辑算法在集成电路功能验证方面的研究和应用。是业界数个著名的形式验证工具的主要研发和负责人，包括Motorola的Verdict/Simgen，Verplex的Blacktie，Japser的JaperGold，Atrenta的Periscope，以及Cadence的Incisive Formal.“基于约束的验证”(Constraint Based Verification)的作者，该书是基于约束验证领域的第一部学术著作，该领域最终成果即SystemVerilog/OVM/UVM，当前最为流行的集成电路验证方法。现为奥卡思微电科技有限公司的联合创始人和首席执行官。

2. 报告人：李选林

题目：硬件形式验证应用

摘要： 集成电路功能正确性至关重要，其产生的任何故障都可能导致极大的经济损失或物理损害。而针对集成电路的验证又存在极高的复杂性，尤其超大规模集成电路，仅通过软件仿真极难保证。形式验证已成为数字集成电路设计流程中至关重要一环。本报告重点介绍集成电路形式化证明应用现状，及面临的挑战：超大集成电路的形式验证求解算力不足、合理的约束和性质衡量标准等。

简介： 李选林，华为海思项目群总监，10+年数字芯片开发和工具设计经验，成功交付多颗大规模芯片。负责逻辑层工具链整体战略、计划和实施。

3. 报告嘉宾：刘军

题目：形式化工具在EDA领域最新发展方向研究

摘要： 芯片设计的复杂化和高速化对电子设计自动化方法(EDA)提出了新的要求, EDA研究是一个极具挑战性的领域。形式验证作为仿真技术的有利互补，越来越被广大验证工作者所接受。本报告将集中分享形式验证在EDA领域的一些最新发展方向。

简介： 刘军，毕业于上海交通大学，硕士。现任芯华章科技股份有限公司高级研发经理，主要研究方向为形式化验证方向。

5. 报告人：蔡少伟

题目：约束求解的一些进展

摘要： 命题逻辑可满足性问题（SAT）是计算机科学的一个核心问题，也是数理逻辑的基础问题，SAT求解器在工业中有重要应用，尤其是EDA领域的基础引擎，是芯片设计多个环节不可或缺的底层工具。本报告介绍SAT问题及其在EDA中的典型应用，并介绍常见的SAT算法以及近期在此方向的进展。

简介： 蔡少伟， 中国科学院软件研究所研究员, 博导，智源青年科学家，获得国家自然科学基金优青项目，中科院优秀导师，现任中科院青促会信息与管理分会会长。2012年于北京大学获博士学位，主要研究约束求解，组合优化，自动算法工程。曾获得AIJ “近五年最受欢迎”论文，SAT 会议最佳论文奖，在国际SAT比赛、MaxSAT比赛、SMT比赛多次获得冠军，获国际EDA比赛亚军，联合逻辑奥林匹克金牌。发表CCF A类论文40余篇。研究成果被应用于EDA，云计算，电子地图导航，频谱分配等多个实际场景。

6. 报告题目：李建文

题目：互补近似可达验证技术及其应用

摘要： 互补近似可达验证（简称CAR）是报告人近年来在形式化验证领域提出并主要研究的一种新型安全模型检查技术（safety model checking）。该技术和主流的IC3/PDR验证技术相比，具有更加清晰的理论框架和灵活的状态搜索策略。在给定测试集中CAR的性能和IC3/PDR相比也有很强的竞争力。本报告首先会简要介绍一个CAR的方法学和它的最新进展，之后会汇报CAR在轨道交通连锁系统验证和芯片设计验证领域中的初步应用结果。最后简要探讨形式化验证技术，尤其是模型检查技术在工业界应用前景的一些想法。

简介： 李建文，华东师范大学研究员，博士生导师，入选上海市青年人才计划，获得上海市浦江人才荣誉称号，主持国家自然科学基金青年项目、重点项目子课题各一项。研究方向主要为形式化自动验证技术，可用于保障计算机软硬件系统的正确性和安全性，重点应用场景包括芯片、航天、轨道交通等安全攸关领域

论坛主席与主持人介绍：

蒲戈光，上海工业控制安全创新科技有限公司总经理

简介： 华东师范大学计算机科学与软件工程学院副院长、教授、博士生导师。担任中国计算机协会形式化方法专委会副主任，入选上海青年科技启明星。主持核高基、可信软件基础研究等国家省部级项目10 余项。获2019 年上海市科技进步特等奖、2011 年获教育部自然科学一等奖、2007 年获上海市青年科技启明星。主持国家及省部级项目10 余项，参与1 项物联网领域IEEE 国际标准制定。