06-陈韬宇.pdf

1、香山香山缓存系统的形式化验证缓存系统的形式化验证陈韬宇1 马锟1 陈熙23 王凯帆23李勇坚1 蔡少伟11中国科学院软件研究所2中国科学院计算技术研究所3北京开源芯片研究院2024年8月22日中国科学院软件研究所(ISCAS)2 2报告内容 香山缓存与形式化验证 基于香山缓存的形式化验证方案 阶段性成果 未来研究方向中国科学院软件研究所(ISCAS)3 3报告内容 香山缓存与形式化验证 香山缓存系统介绍 形式化验证：模型检测技术 基于香山缓存的形式化验证方案 阶段性成果 未来研究方向中国科学院软件研究所(ISCAS)4 4香山缓存系统介绍 建立了包含设计、实现、验证在内全开源工具敏捷开发流程

2、采用 Rocket Chip 的 Diplomacy 框架实现组件互联 处理器设计与验证在敏捷度上的差距持续扩大，形成一堵验证墙中国科学院软件研究所(ISCAS)5 5香山缓存系统介绍 HuanCun(南湖)CoupledL2(昆明湖)主流水线架构 Inclusive 策略 Directory basedCoupledL2 硬件结构 Diplomacy 框架 包括硬件实现和协商参数两部分 编译期确定所有参数 自动连接输入输出端口CoupledL2 实现的 TileLink 协议中国科学院软件研究所(ISCAS)6 6香山缓存系统介绍 敏捷开发带来的验证困难 验证覆盖率提升困难：事务繁多复杂，难

3、以找到极端的 Corner Case 问题定位困难：大型项目结构繁杂，问题定位环节仍需要大量人力 缓存系统所关注的一些性质 互斥性质：不同 cache 不能同时对同一地址的数据有写权限 死锁性质：系统中的每一个请求都应当在有限时间内被响应中国科学院软件研究所(ISCAS)7 7香山缓存系统与形式化验证 缓存系统所关注的一些性质 互斥性质：各缓存的状态需满足特定条件 死锁性质：各请求应在有限时间内被响应 形式化验证 基于数学严格证明的自动化技术，可全面、精确地验证硬件电路设计满足预定规范 完备性、可重复性、高效中国科学院软件研究所(ISCAS)8 8香山缓存系统与形式化验证 缓存系统所关注的一些

4、性质 互斥性质：各缓存的状态需满足特定条件 死锁性质：各请求应在有限时间内被响应典型安全性质（Safety）典型活性性质（Liveness）形式化验证 基于数学严格证明的自动化技术，可全面、精确地验证硬件电路设计满足预定规范 完备性、可重复性、高效中国科学院软件研究所(ISCAS)9 9形式化验证技术之一：模型检测需求系统属性规范系统模型模型检测满足内存不足违反+反例仿真定位错误形式化建模输入结果中国科学院软件研究所(ISCAS)1010形式化验证技术之一：模型检测需求系统属性规范系统模型模型检测形式化建模输入中国科学院软件研究所(ISCAS)1111形式化验证技术之一：模型检测模型检测满足内

5、存不足违反+反例结果中国科学院软件研究所(ISCAS)1212形式化验证技术之一：模型检测系统模型模型检测违反+反例仿真定位错误输入结果中国科学院软件研究所(ISCAS)1313报告内容 香山缓存与形式化验证 基于香山缓存的形式化验证方案 香山形式化验证的难点 系统建模与性质定义 验证加速方案 阶段性成果 未来研究方向中国科学院软件研究所(ISCAS)1414香山形式化验证的难点 缓存系统联系紧密 完整的缓存系统涵盖三级缓存和访存流水线，难以将L2、L3缓存隔离验证 缓存接口无法对接形式化验证接口香山缓存系统示意图Committed Store BufferLoad QueueData Cac

6、he访存单元Store QueueL2 Cache(CoupledL2)L3 Cache(HuanCun)RAM处理器核后端中国科学院软件研究所(ISCAS)1515香山形式化验证的难点 并发事务复杂多处理器核并行缓存内多Slice并行Slice内多MSHR并行 复杂错误极难找到，且不易复现状态空间指数级增加CoupledL2 缓存架构示意图中国科学院软件研究所(ISCAS)1616香山形式化验证的难点 形式化验证工具链不成熟 敏捷开发环境下对 Chisel 语言设计的形式化支持不够 硬件领域的大多数形式化验证生态建立在Verilog、SystemVerilog等语言上SystemVerilo