硬件设计的形式验证与时态逻辑

Formal Verification for Hardware Design and Temporal Logic

本文扼要介绍硬件验证技术的发展近况,着重介绍利用HOL系统验证硬件的方法以及如何用HOL系统实现时态逻辑,并给出一个采用已机械化的时态逻辑验证锁存器的实例。

This paper introduces the formal verification techniques for hardware designs using HOL ( Higher-Order Logic ) system. The implementation of a temporal logic in top level of HOL is described, and an example of verifying a latch using this mechanized temporal logic is given.