知行融创论坛第六期活动成功举办

基础软件与系统重点实验室党支部于2025年11月26日上午成功举办了“知行融创”论坛第六期活动。本期活动延续论坛宗旨，聚焦基础软件与系统领域的前沿研究与关键技术挑战，两位同志分别分享了他们在集成电路设计验证形式化方法、概率程序终止性分析等方面的最新研究进展，为与会者带来了深刻启发。

（图为活动现场图片）

陈志瀚：Datapath Combinational Equivalence Checking With Hybrid Sweeping Engines and Parallelization

组合等价性检验（CEC）是现代集成电路设计与验证流程中的基石环节，而数据路径电路因其密集的异或（XOR）结构对传统的SAT-sweeping方法构成显著挑战。为克服这一难题，本研究将精确概率模拟（EPS）与SAT求解器相结合，并提出了一种基于XOR链密度的动态引擎选择启发式策略。此外，我们对SAT和EPS引擎均进行了并行化处理，以进一步加速验证过程。在工业基准测试上的实验结果表明，本方法在40%的测试例上实现了高达100倍的加速，在14%的测试例上加速超过1000倍，其并行版本在使用64线程时缩放比最高可达70倍。

（图中为陈志瀚）

吴昊：Termination Analysis of Probabilistic Programs

概率程序在传统程序控制流之上引入了概率赋值和概率分支，主要用于对随机系统进行建模和描述随机化算法。在概率程序的验证与分析中，判定程序是否终止是一个基础且困难的理论问题，其终止行为相比确定性程序展现出更复杂的特性。本报告将回顾该领域重要的理论结果，并介绍围绕此问题的主要分析技术。

（图中为吴昊）

本期“知行融创”论坛围绕集成电路形式化验证、程序分析等基础软件与系统的核心方向，展示了实验室同志在应对工业验证难题、探索程序理论前沿方面的创新思考与实践。论坛持续为实验室的同志构建了活跃的学术交流平台，有效促进了不同研究领域间的思想碰撞与知识融合，是推动党建与科研业务深度融合的又一次生动实践，激励着大家在服务国家重大战略需求的科研征程上攻坚克难、勇攀高峰。