A new model for verification  

作　　者：杜振军 马光胜 冯刚 

机构地区：[1]School of Computer Science & Technology,Dalian Maritime University [2]College of Computer Science & Technology,Harbin Engineering University

出　　处：《Journal of Harbin Institute of Technology(New Series)》2007年第3期305-310,共6页哈尔滨工业大学学报（英文版）

基　　金：Sponsored by the National Natural Science Foundation of China(Grant No.69973014and60273081);the Natural Science Foundation of Heilongjiang Province(Grant No.F0209);HEU Foundation(Grant No.HEUF04088).

摘　　要：Formal verification is playing a significant role in IC design.However,the common models for verification either have their complexity problems or have applicable limitations.In order to overcome the deficiencies,a novel model-WGL(Weighted Generalized List)is proposed,which is based on the general-list decomposition of polynomials,with three different weights and manipulation rules introduced to effect node sharing and the canonicity.Timing parameters and operations on them are also considered.Examples show the word-level WGL is the only model to linearly represent the common word-level functions and the bit-level WGL is especially suitable for arithmetic intensive circuits.The model is proved to be a uniform and efficient model for both bit-level and word-level functions.Then based on the WGL model,a backward-construction verification approach is proposed,which reduces time and space complexity for multipliers to polynomial complexity(time complexity is less than O(n3.6)and space complexity is less than O(n1.5))without hierarchical partitioning.Both the model and the verification method show their theoretical and applicable significance in IC design.Formal verification is playing a significant role in IC design.However,the common models for verification either have their complexity problems or have applicable limitations.In order to overcome the deficiencies,a novel model-WGL（Weighted Generalized List）is proposed,which is based on the general-list decomposition of polynomials,with three different weights and manipulation rules introduced to effect node sharing and the canonicity.Timing parameters and operations on them are also considered.Examples show the word-level WGL is the only model to linearly represent the common word-level functions and the bit-level WGL is especially suitable for arithmetic intensive circuits.The model is proved to be a uniform and efficient model for both bit-level and word-level functions.Then based on the WGL model,a backward-construction verification approach is proposed,which reduces time and space complexity for multipliers to polynomial complexity（time complexity is less than O（n^3.6）and space complexity is less than O（n^1.5））without hierarchical partitioning.Both the model and the verification method show their theoretical and applicable significance in IC design.

关 键 词：polynomial symbolic manipulations VERIFICATION WGL word-level polynomial 

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