中文摘要：

在电路的设计过程中，形式验证已经成为重要的步骤．为提高设计的正确性，对高层次硬件描述语言（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.