Mechanically verifying safety and liveness properties of delay insensitive circuits

Abstract

This paper describes, by means of an example, how one may mechanically verify delay insensitive circuits on an automated theorem prover. It presents the verification of both the safety and liveness properties of an n-node delay insensitive fifo circuit [8]. The proof system used is a mechanized implementation of Unity [2] on the Boyer-Moore prover [1], described in [5]. This paper describes the circuit formally in the Boyer-Moore logic and presents the mechanically verified correctness theorems. The formal description also captures the protocol that the circuit expects its environment to obey and specifies a class of suitable initial states. This paper demonstrates how a general purpose automated proof system for concurrent programs may be used to mechanically verify both the safety and liveness properties of arbitrary sized delay insensitive circuits.