● 摘要
在软硬件工程领域,传统的设计与测试技术只能做有限的质量保证,而形式化设 计与验证方法能够从理论上保证设计的正确性。在 CPU 设计与验证领域,形式化验证 是相对成熟的技术,而形式化设计和形式化综合的研究刚刚起步。把形式化规格、设计 和形式化验证作为完整过程的研究和项目几乎没有,本论文首次尝试将这些要素统一 到一起。
论文以交互式定理证明工具 PVS 作为工作环境,描述了以 MIPS ISA 规格为参考, 形式化设计与验证单周期 CPU 的过程和框架;并且以验证完成的单周期 CPU 为参考, 形式化设计与验证流水线 CPU 的过程和框架。通过分层的设计与验证工作,论文证明 了流水线 CPU 的设计符合 ISA 规范,并在这个证明过程中调试和修复了若干 BUG,得 到了一个没有缺陷的流水线 CPU 设计模型。针对流水线 CPU 形式化设计工作的难点, 论文提出了以译码信号为基础的、系统化的冲突分析与转发、暂停信号的生成方案;针 对流水线 CPU 形式化验证的难点,论文在完成函数法的基础上新增一个不变属性验证 层,用于验证转发的结果是符合预期的。基于论文的这些创新,流水线 CPU 的形式化 设计与验证工作变得系统和简单,并且具有良好的可伸缩性。
相关内容
相关标签