为了实现多项式数据通路的初始算术规范与其相应的寄存器传输级实现之间的等价性验证,提出了一个有序的、简化的和正则的带权值广义表模型表达字级多项式,同时给出了该模型的化简、加法和乘法运算规则,基于这些规则对寄存器传输级电路构建其相应有序的、简化的和正则的带权值广义表模型。实验结果表明,该模型对寄存器传输级电路的等价性验证与^*BMD相比,不论是在存储空间还是在CPU时间花费上均有明显的优势。
To implement the equivalence verification between initial arithmetic specifications for polynomial datapaths and their corresponding register transfer level implementation or the optimized counterparts, an ordered, reduced and canonical weighted generalized list model for word-level polynomial was presented. The operational rules for reduction, addition and multiplication were given. On the basis of these rules, we constructed the relevant ordered, reduced and canonical weighted generalized list model for register transfer level circuits. Experimental results demonstrated that, compared the equivalent verification with multiplicative binary moment diagram ( ^* BMD), the proposed method is obviously better than ^* BMD in CPU time consumption and in memory space occupancy.