Proving correctness of asynchronous circuits using temporal logic
Mark J. Bennett · 1986
The recent advances made in VLSI have prompted new ideas for hardware. As it becomes more difficult to rely upon a global clock and as the need for increased speed arises, asynchronous circuits become more attractive. Since asynchronous circuits operate at a speed determined by the input and gate delays only, they can operate faster than their synchronous counterparts and generate completion signals. Unfortunately current validation techniques are cumbersome and do not instill much confidence in designs. Proving correctness in a deductive system for propositional temporal logic (PTL) is shown here to be an attractive validation alternative. Axioms describing the behavior of atomic elements (gates or modules) are formulated in PTL. Desired properties of the circuit are formulated as specifications in PTL. As gates or modules are composed to form larger modules, their corresponding PTL formulas are combined using PTL theorems. Using the methods introduced here, the specifications can be proved correct with respect to the axioms. Verified examples range from latches to a self-timed asynchronous pipeline. A method for proving steady-state circuit properties is introduced which is based upon a deductive system for temporal logic. A method for proving global-time properties is also presented which is an extension of the steady-state method. Proving global-time properties involves a collection of heuristics such as forward reasoning for liveness, backward reasoning for safety, and proving transition safety and non-interference properties. PTL timing diagrams are introduced as a tool for informally reasoning about complex until-formulas. A graph representation of a circuit's execution is provided with the Execution Graph Method (EGM), which is introduced to address the lack of behavioral information in a circuit schematic. The execution graph is formed from a set of PTL formulas proved from the axioms. Safety and liveness properties can be shown to hold on the execution graph by using an algorithm which traverses paths in a depth-first manner. It is shown that EGM can be used to verify gate- or module-level circuits hierarchically.