我院软件工程组 2020 级博士研究生陆龙龙提出了一种面向异步芯片设计死锁问题的自动化验证方法 Verilock。该研究成果已被计算机体系结构领域 CCF - A 类国际期刊 IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems（ TCAD ）录用，南京大学为唯一署名单位。与传统测试方法相比，该工作基于 SystemVerilog 的形式化语义，创新地提出了层次化并行模型验证策略，从而能够高效地验证芯片模块间的通信行为正确性。

异步芯片是一种无需全局时钟信号、通过事件或数据到达自动触发电路状态变化的集成电路。异步芯片根据输入信号的实际到达时间触发电路状态变化，能够有效降低功耗、减少电磁干扰并提升系统鲁棒性，适用于传感器节点、可穿戴设备等电磁环境复杂、功耗严苛受限场景，在人机物深度融合系统中有着广泛的应用前景。然而，异步电路模块间的通信行为复杂，模块交互容易产生死锁，传统测试方法难以覆盖所有可能场景，缺陷芯片一旦生产将造成巨大的经济损失。现有的 EDA 工具与设计规范主要针对同步芯片优化，直接应用于异步芯片设计常受限制。因此，研究面向异步芯片的形式化验证理论与方法已成为亟待解决的关键问题。

Verilock验证方法概览图

为了保障异步芯片中不存在死锁，该工作定义 SystemVerilog 描述异步电路的形式化语义。基于该语义，Verilock 利用异步芯片中模块间通信独立的特性，将整个芯片划分为若干通信组。对每个通信组，根据形式化语义规则完整地检查所有可能的通信模式。一个通信组合验证完成后成为一个抽象模块供后续验证使用。当多个通信组间不存在共享信道时，可并行验证通信组以显著加速整个流程。实验结果表明，Verilock 可有效地发现异步芯片中的死锁问题。由于利用了异步芯片中通信行为局部性的特点，相较于现有的形式化验证工具，Verilock 在处理异步芯片验证任务时可实现数量级的性能提升。

陆龙龙博士生在潘敏学教授指导下完成了本研究。陆龙龙长期从事复杂系统异步并发场景的形式化验证，多次以第一作者身份在该领域国际学术期刊会议发表研究成果。