一种复杂功能部件的形式化验证方法

摘要

文章给出一个通用的针对复杂功能部件的形式化验证方法.该方法基于寄存器传输级设计，利用设计中的结构信息将电路划分为控制部分和运算部分分别验证.文章给出了标识数据的时间标记法，针对控制部分中数据抽象的通用抽象规则，以及对运算部分进行分割处理的技术.本文的方法成功应用于龙芯3号处理器浮点乘加部件的验证，实践表明该方法能够发现传统模拟仿真方法难以发现的隐藏很深的错误，能够有效支持工业级功能部件的验证.