基于WGLs的字级描述的形式验证  

Formal verification of word-level specifications based on weighted generalized lists

作　　者：马光胜[1] 焦金良[1] 冯刚[1] 王冠军 

机构地区：[1]哈尔滨工程大学计算机科学与技术学院,黑龙江哈尔滨150001

出　　处：《哈尔滨工程大学学报》2007年第5期548-552,共5页Journal of Harbin Engineering University

基　　金：国家自然科学基金资助项目(60273081);哈尔滨工程大学基础研究基金资助项目(04088)

摘　　要：在电路的设计过程中,形式验证已经成为重要的步骤.为提高设计的正确性,对高层次硬件描述语言(HDL)如VHDL的验证变得更加重要.文章给出的一个完整的数据通路操作的指令集能够在基于WGLs(weighted generalized lists)模型下进行形式验证的方法,讨论了字级函数和HDL操作符的WGL表示.所提到的技术允许直接地把HDL描述转化为WGLs,模运算和除法运算可以用基于WGLs的算法进行表示,此操作为有效验证过程的核心操作.文中所给出的验证工具是完全自动的,实验结果显示了该方法的有效性.Formal verification has become one of the most important steps in circuit design. As a result, verification of high-level hardware description languages （HDL）, like VHDL, is becoming increasingly important to ensure effective tools for circuit design. A complete set of datapath operations are presented in this paper that can make a formal verification based on weighted generalized lists（WGLs）. The WGL representation of world-level functions and HDL operations are also discussed. The techniques allows a direct transformation of HDL to WGLs. A new algorithm is proposed based on WGLs for modulus operation and division. These operations are the core of an efficient verification procedure proposed in this paper. The verification tool is completely automatic and experimental results verify the efficiency of this approach.

关 键 词：符号多项式操作 形式验证 WGLs 

分 类 号：TP302.1[自动化与计算机技术—计算机系统结构]