摘要： 本文使用重写技术对不恢复余数阵列除法器进行了形式化描述并结合归纳法对该除法器的正确性进行了验证,整个工作是建立在串行加法器的描述和验证基础上的。不恢复余数阵列除法器的运算和控制有一定的复杂度,适合用大规模集成电路实现。本文成功地用重写归纳法对它进行了描述和验证,说明重写归纳法在硬件电路正确性验证方面有广阔的应用前景。
张欢欢 宋国新. 不恢复余数阵列除法器的形式化描述和验证方法[J]. 计算机科学, 2007, 34(6): 283-285. https://doi.org/
ZHANG Huan-Huan, SONG Guo-Xin （Department of Computer Science and Engineering,East China University of Science and Technology,Shanghai 200237）. [J]. Computer Science, 2007, 34(6): 283-285. https://doi.org/
首页