以有限环代数为理论基础,提出一个定点数据通路的等价验证算法.该算法能有效地对实现多项式运算的寄存器传输级(register transfer level,RTL)定点数据通路进行等价验证.理论分析表明该算法的时间复杂性优于文献中存在的算法;实验结果表明该算法不论是对等价的数据通路的验证还是对含有故障的数据通路的验证均比已有的算法节省CPU时间.
Based on finite ring algebra, an algorithm of equivalence verification for fixed-size datapaths was proposed. The proposed algorithm was effective for the RTL (register transfer level) fixed-point datapaths that implement polynomial computation. Theoretical analysis showed that the time complexity of the proposed algorithm was more optimal than the existent algo- rithm. Experimental results showed that the cost of CPU times for the proposed algorithm, not only for the equivalent datapaths but also for the datapaths which contain faults, was less than the existent algorithm.