进位保留加法器的命题投影时序逻辑组合验证  

Compositional verification of a carry-save adder with the propositional projection temporal logic

作　　者：张南[1,2] 段振华[1,2] 

机构地区：[1]西安电子科技大学计算理论与技术研究所,陕西西安710071 [2]西安电子科技大学综合业务网理论及关键技术国家重点实验室,陕西西安710071

出　　处：《西安电子科技大学学报》2012年第5期192-196,共5页Journal of Xidian University

基　　金：国家重点基础研究发展计划973资助项目(2010CB328102);国家自然科学基金资助项目(60910004;61133001;61003078;61202038;61272117);综合业务网国家重点实验室基金资助项目(ISN Lab Grant No.ISN1102001)

摘　　要：为保证硬件设计的正确性,提出了对硬件设计组合验证的新方法.该方法在命题投影时序逻辑的统一框架下,实现对硬件系统行为的建模,对所期望性质的形式化描述,并利用命题投影时序逻辑合理且完备的公理系统对系统性质进行验证,从而证明硬件系统满足期望的性质,保证设计的正确性.进位保留加法器的验证实例说明了该方法的可行性。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.

关 键 词：时序逻辑 组合验证 进位保留加法器 超前进位加法器 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]