| 基于幂表的并行加法器的归纳验证 |
| |
| 引用本文： | 张欢欢,邵志清,宋国新. 基于幂表的并行加法器的归纳验证[J]. 电子学报, 2003, 31(6): 932-936 |
| |
| 作者姓名： | 张欢欢 邵志清 宋国新 |
| |
| 作者单位： | 1. 华东理工大学计算机技术研究所,上海 200237;2. 中国科学院软件研究所计算机科学重点实验室,北京 100080 |
| |
| 基金项目： | 国家自然科学基金 (No 6990 30 0 4 )，教育部优秀青年教师资助计划，教育部科学技术研究重点项目 (No 0 1 0 77) |
| |
| 摘 要： | 介绍了基于幂表和重写规则的并行加法器的功能描述,直接使用重写归纳证明技术验证了这些描述的正确性,为重写技术用于描述和验证更加复杂的硬件电路奠定了基础.
|
| 关 键 词： | 重写 归纳 加法器 描述 验证 |
| 文章编号： | 0372-2112(2003)06-0932-05 |
| 收稿时间： | 2001-12-30 |
Inductive Verification of Powerlist-Based Carry Lookahead Adders |
| |
| 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 |
| |
| Authors: | ZHANG Huan-huan SHAO Zhi-qing SONG Guo-xin |
| |
| Affiliation: | 1. Institute of Computer Technology,East China University of Science and Technology,Shanghai 200237,China;2. Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences,Beijing 100080,China |
| |
| 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: | rewriting induction adder specification verification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《电子学报》浏览原始摘要信息 |
|
点击此处可从《电子学报》下载免费的PDF全文 |
