J4 ›› 2012, Vol. 39 ›› Issue (5): 192-196.doi: 10.3969/j.issn.1001-2400.2012.05.032

• 研究论文 • 上一篇    

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

张南1,2;段振华1,2   

  1. (1. 西安电子科技大学 计算理论与技术研究所,陕西 西安  710071;
    2. 西安电子科技大学 综合业务网理论及关键技术国家重点实验室,陕西 西安  710071)
  • 收稿日期:2012-03-27 出版日期:2012-10-20 发布日期:2012-12-13
  • 通讯作者: 张南
  • 作者简介:张南(1984-),女,西安电子科技大学博士研究生,E-mail: nanzhang@stu.xidian.edu.cn.
  • 基金资助:

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

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

ZHANG Nan1,2;DUAN Zhenhua1,2   

  1. (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)
  • Received:2012-03-27 Online:2012-10-20 Published:2012-12-13
  • Contact: ZHANG Nan

摘要:

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

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

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.

Key words: temporal logic, compositional verification, carry-save adder, carry look-ahead adder

中图分类号: 

  • TP301