文献类型：期刊文献

中文题名：基于重写归纳技术的串行加法器的描述和验证

英文题名：Specification and Verification of Ripple Carry Adders Based on Rewriting Induction Techniques

作者：张欢欢[1];邵志清[1];宋国新[1]

机构：[1]华东理工大学计算机科学与工程系,上海200237

年份：2003

卷号：29

期号：1

起止页码：59

中文期刊名：华东理工大学学报（自然科学版）

外文期刊名：Journal of East China University of Science and Technology

收录：CSTPCD;;Scopus;北大核心:【北大核心2000】；CSCD:【CSCD2011_2012】；

基金：国家自然科学基金(69903004);教育部科学技术重点研究项目;教育部优秀青年教师资助计划

语种：中文

中文关键词：重写归纳技术;串行加法器;验证;硬件电路;逻辑位;门电路;逻辑功能

外文关键词：rewriting; induction; adder; specification; verification

摘要：在用重写系统描述逻辑位、门电路、位串和自然数的基础上,对半加器、全加器和串行加法器等基本硬件电路的逻辑功能进行了刻画,并用基于重写归纳的推理技术证明了所有描述的正确性,为用重写技术正确描述和验证复杂硬件电路奠定了基础。最后给出与其他类似工作的分析和比较。
Based on rewriting induction techniques, an approach automatically verifying adder circuits is proposed. All involved concepts, including bits, gates, bit strings, natural numbers, half adders, full adders and ripple carry adders, are described using rewrite systems. Proofs of various properties are given using rewriting and induction. The correctness of ripple carry adders is established by showing that they actually implement addition on the natural numbers. Finally, a comparison with related works is made and the result shows that our approach has advantages in specifying and verifying hardware circuits.