基于幂表的并行加法器的归纳验证

张欢欢; 邵志清; 宋国新

您当前的位置：

首页 >

文章列表页 >

基于幂表的并行加法器的归纳验证

论文 | 更新时间：2025-07-16

- 基于幂表的并行加法器的归纳验证
- Inductive Verification of Powerlist-Based Carry Lookahead Adders
- 电子学报 2003年31卷第6期页码：932-936
- 作者机构：
  
  1. 华东理工大学计算机技术研究所,上海,200237
  2. 中国科学院软件研究所计算机科学重点实验室,北京,100080
  3. 华东理工大学计算机技术研究所上海,200237
  4. 中国科学院软件研究所计算机科学重点实验室北京,100080
- 作者简介：
- 基金信息：
  
  国家自然科学基金 (No.69903004);教育部优秀青年教师资助计划;教育部科学技术研究重点项目 (No.01077)
- DOI：
  中图分类号： TP332
- 纸质出版：2003
- 稿件说明：
移动端阅览
张欢欢, 邵志清, 宋国新. 基于幂表的并行加法器的归纳验证[J]. 电子学报, 2003,31(6):932-936.

ZHANG Huan-huan, SHAO Zhi-qing, SONG Guo-xin. Inductive Verification of Powerlist-Based Carry Lookahead Adders[J]. Acta Electronica Sinica, 2003, 31(6): 932-936.
张欢欢, 邵志清, 宋国新. 基于幂表的并行加法器的归纳验证[J]. 电子学报, 2003,31(6):932-936. DOI：

ZHANG Huan-huan, SHAO Zhi-qing, SONG Guo-xin. Inductive Verification of Powerlist-Based Carry Lookahead Adders[J]. Acta Electronica Sinica, 2003, 31(6): 932-936. DOI：

摘要

介绍了基于幂表和重写规则的并行加法器的功能描述

直接使用重写归纳证明技术验证了这些描述的正确性

为重写技术用于描述和验证更加复杂的硬件电路奠定了基础.

Abstract

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.

关键词

Keywords

references

浏览量

1071

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于电路三要素理论的三值绝热加法器设计

对数跳跃加法器的算法及结构设计

基于改进五输入择多门的QCA全加器设计及应用

基于XCFG的BPEL数据流属性分析与验证