基于高阶逻辑的硬件验证方法

HARDWARE SPECIFICATION AND VERIFICATION USING HIGHER-ORDER LOGIC

本文讨论了如何利用高阶逻辑描述硬件的行为及结构,提出了硬件验证的一般方法,高阶逻辑不仅可以作为一种描述语言用来描述硬件的行为及结构,而且可以作为证明系统用来验证硬件设计的正确性,文中给出的用以说明描述及验证的例子包括CMOS反相器、复位的奇偶校验器。

In this paper,a general method for hardware verification is presented ,which can be used both as a hardware description language and as a deduction system for design verification.Examples used to illustrate various specification and verification techniques include a CMOS inverter,and a resetable parity checker.