向量定点运算单元的形式化验证

摘要

随着集成电路设计的复杂度和难度日益增大，验证作为设计过程中的关键环节，面临着巨大挑战。据统计，在芯片设计中，超过50％的人力和时间都投入到验证工作中，所以提高验证的效率和完整性，对于设计研发有着至关重要的意义。传统的模拟验证方法，其有效性很大程度上取决于测试向量的完备性，在面对大规模设计时，模拟验证逐渐暴露其难以覆盖所有测试向量的局限性。作为模拟验证的补充，形式验证能够高效地遍历整个状态空间，进而对设计进行完整的验证，近年来受到业界的广泛关注。
　　本文针对一款服务器处理器核的向量定点运算单元展开形式化验证方法研究，结合JasperGold和ATEC形式化验证工具，采用等价性检验的方法实现对该运算单元的功能验证。本文的主要研究内容有以下几点：
　　首先，根据向量定点运算单元的设计规范，完成参考模型的设计与验证。通过分析运算单元涉及的共138条指令功能，其中包括向量定点运算指令和少量浮点运算指令，使用C语言设计编写形式化验证中所需的参考模型。为了确保参考模型的有效性，利用定向测试和随机测试相结合的方法，完成对模型与设计规范功能一致性的验证。
　　其次，以向量定点运算单元为对象，研究基于等价性检验的形式验证技术，解决当前形式验证能力不足的问题。首先根据向量定点运算单元的规模与电路结构特点，提出合理的验证方案；其次，针对设计中的关键子模块，使用Verilog HDL语言描述其电路功能，并应用JasperGold中的SEC（Sequential Equivalence Checking）工具完成对关键子模块的功能验证；最后，针对整个运算单元，通过ATEC工具完成电路设计与参考模型之间的等价性检验。在验证初期，为了快速定位设计缺陷，利用对控制信号的过度约束来逐条验证指令功能实现的正确性；在设计趋于稳定后，解除形式验证中的过度约束，最终实现完备的功能验证。
　　与传统的模拟验证方法相比，形式化验证方法无需搭建复杂的验证平台和构建大量的测试向量，就能够快速找出反例，尤其是当模拟验证中随机测试难以覆盖边界情况时，该方法更加奏效。所以形式化验证方法在保证验证的完备性和提高验证效率方面具有极大优势。实验表明，本文为了解决设计规模和形式验证能力之间的矛盾所采用的利用过度约束有效分割状态空间的解决方案是行之有效的，此方案可为处理器其他运算单元的验证工作提供参考。

目录

声明

插图索引

表格索引

符号对照表

缩略语对照表

第一章 绪论

1.1选题背景

1.2形式验证方法概述

1.3国内外研究现状

1.4论文的主要工作和章节组织

第二章 向量定点运算单元

2.1向量定点运算单元功能介绍

2.2向量定点运算单元电路实现

2.3本章小结

第三章 参考模型设计与验证

3.1 C_model的设计与实现

3.2 C_model的验证与调试

3.3本章小结

第四章 向量定点运算单元的等价性检验

4.1验证方案

4.2基于JasperGold工具的等价性验证

4.3基于ATEC工具的等价性检验

4.4本章小结

第五章 总结与展望

5.1论文形式验证工作总结

5.2形式验证在其他计算模块应用的展望

参考文献

致谢

作者简介