Design of the Sequential System Automata using Temporal Equivalence Classes

Abstract

A design method of sequential system automata using temporal logic specifications is proposed in this paper. The method is based on well-known Z.Manna and P.Wolper temporal logic satisfiability analysis procedure and is extended to include past time temporal operators. A new specification method which uses temporal equivalence classes is proposed to specify the behaviour of large digital circuits.The impact of the composition and decomposition operations of the temporal equivalence classes on the final automata has been studied. A case study is carried out which deals with the design of the synchronous bus arbiter circuit element. The SMV tool has been used to verify the temporal properties of the obtained automata. Key words: Temporal Logic, Temporal Equivalence Classes, Temporal Logic Specifications, Sequential Systems, Automata.