整数乘法电路的形式化验证方法研究  

Formal Method Research on Integer Multiplier Verification

作　　者：王海霞[1] 韩承德[1] 

机构地区：[1]中国科学院计算技术研究所计算机系统结构研究室,北京100080

出　　处：《计算机研究与发展》2005年第3期404-410,共7页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(69896250-1)

摘　　要：采用基于决策图的模型检验方法对整数乘法器验证时会出现内存爆炸,解决该问题的一种有效途径是采用反向替换方法.函数替换算法是反向替换方法的核心算法,如果保证被替换变量位于被替换函数的决策图顶层,替换算法可以简化.通过设置变量序和限定变量替换顺序,提出了一种保证被替换变量始终位于被替换函数决策图的顶层的反向替换方法,可极大降低整数乘法器验证的运行时间和内存使用量.实验结果表明,采用改进的反向替换方法,在1GB内存下,可将Add-Step乘法器的验证规模从84×84位提高到256×256位,将Diagonal乘法器的验证规模从84×84位提高到206×206位.Model checking based on decision diagram causes memory explosion in integer multiplier verification. An efficient solution to this problem is backward substitution method. As the kernel of backward substitution method, the performance of function substitution algorithm is crucial to the efficiency of verification process using backward substitution method. If the variable to be substituted is ensured to be the top variable of the function to be substituted, the function substitution algorithm can be simplified. By setting variable order and variable substitution order, an improved backward substitution method is presented, where in each substitution, the variable substituted is the top variable of the decision diagram of function to be substituted. As experiment shows, under 1GB memory, the improved method enhances the scale of Add-Step multiplier which can be verified from 84 × 84 bits to 256 × 256 bits, and Diagonal multiplier from 84×84 bits to 206× 206 bits.

关 键 词：形式验证 决策图 ＊PHDD 反向替换方法 

分 类 号：TP391.7[自动化与计算机技术—计算机应用技术]