Aid to hierarchial and structured logic design using temporal logic and Prolog

The paper describes a study of an aid for hardware logic design using temporal logic, called linear time temporal logic (LTTL), and Prolog. A review of specification techniques for synchronisation parts using LTTL is given. A temporal logic programming language called Tokio, which is based on LTTL and includes interval variables, is presented. As parallelisms are tedious to describe sequentially in LTTL, the notion of interval variables which express a finite number of successive times is introduced.