文献类型：期刊文献

中文题名：基于幂表的并行加法器的归纳验证

英文题名：Inductive Verification of Powerlist-Based Carry Lookahead Adders

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

机构：[1]华东理工大学计算机技术研究所

年份：2003

卷号：31

期号：6

起止页码：932

中文期刊名：电子学报

外文期刊名：Acta Electronica Sinica

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

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

语种：中文

中文关键词：重写;归纳;加法器;描述;验证

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

摘要：介绍了基于幂表和重写规则的并行加法器的功能描述 ,直接使用重写归纳证明技术验证了这些描述的正确性 ,为重写技术用于描述和验证更加复杂的硬件电路奠定了基础 .
Based on functional specifications of carry lookahead adders,and it directly uses rewriting induction techniques to establish the correctness of these specifications by proving that they actually implement addition on the natural numbers.A brief comparison with related work is made and the results show that this approach has advantages in specifying and verifying hardware circuits.