| 进位保留加法器的命题投影时序逻辑组合验证 |
| |
| 引用本文： | 张南,段振华.进位保留加法器的命题投影时序逻辑组合验证[J].西安电子科技大学学报,2012,39(5):192-196. |
| |
| 作者姓名： | 张南 段振华 |
| |
| 作者单位： | 西安电子科技大学计算理论与技术研究所;西安电子科技大学综合业务网理论及关键技术国家重点实验室 |
| |
| 基金项目： | 国家重点基础研究发展计划973资助项目(2010CB328102);国家自然科学基金资助项目(60910004,61133001,61003078,61202038,61272117);综合业务网国家重点实验室基金资助项目(ISN Lab Grant No.ISN1102001) |
| |
| 摘 要： | 为保证硬件设计的正确性,提出了对硬件设计组合验证的新方法.该方法在命题投影时序逻辑的统一框架下,实现对硬件系统行为的建模,对所期望性质的形式化描述,并利用命题投影时序逻辑合理且完备的公理系统对系统性质进行验证,从而证明硬件系统满足期望的性质,保证设计的正确性.进位保留加法器的验证实例说明了该方法的可行性。
|
| 关 键 词： | 时序逻辑 组合验证 进位保留加法器 超前进位加法器 |
| 收稿时间： | 2012-03-27 |
Compositional verification of a carry-save adder with the propositional projection temporal logic |
| |
| ZHANG Nan,DUAN Zhenhua.Compositional verification of a carry-save adder with the propositional projection temporal logic[J].Journal of Xidian University,2012,39(5):192-196. |
| |
| Authors: | ZHANG Nan DUAN Zhenhua |
| |
| Affiliation: | (1. Inst. of Computing Theory & Technology, Xidian Univ., Xi'an 710071， China;
2. State Key Lab. of Integrated Service Networks, Xidian Univ., Xi'an 710071， China) |
| |
| Abstract: | To guarantee the correctness of hardware designs,a compositional methodology for hardware verification is proposed.This methodology uses the propositional projection temporal logic(PPTL) as the underlying logic.The hardware designs(implementations) and properties are formalized with PPTL formulas.The design is correct if the specification can be deduced from the system model in the axiom system of the propositional projection temporal logic.An example for a carry-save adder is given to illustrate the methodology is workable. |
| |
| Keywords: | temporal logic compositional verification carry-save adder carry look-ahead adder |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《西安电子科技大学学报》浏览原始摘要信息 |
|
点击此处可从《西安电子科技大学学报》下载全文 |
