Hierarchical verification of asynchronous circuits using temporal logic (Q1070998)

An automatic verification system is described, in which the specifications are expressed in a propositional temporal logic of branching time, called CTL (Computation Tree Logic). The syntax and the semantics CTL, as well as an efficient algorithm, called model checker for verifying temporal properties of an asynchronous circuit are presented. A simple step-by-step method to verify circuits and an example illustrating how some interesting properties of a self-timed FIFO queue element may be obtained, are given. A hierarchical method to verify large and complex circuits is introduced and some properties of the operation of restriction on a Kripke Structure are studied. The paper concludes with a discussion on some shortcomings of the proposed approach and different open problems.