%%%%%%%
%
%    Temporal Logic Programming Language Tokio		
%
%				Fri Jun  6 1986
%				S.Kono
%				The Faculty of Engineering
%				The University of Tokyo
%				a83793@tansei.u-tokyo.csnet
%%%%%%%

     1.  Hardware description using Temporal Logic

     2.  Interval Temporal Logic

     3.  Execution of Interval Temporal Logic Tokio

     4.  How to write Hardware description in Tokio

	4.1  simple examples

	4.2  two way description of Tokio

	4.3  pipeline merge sorter

     5.    Support tool for Tokio

______________________________________________________
1.  Hardware description using Temporal Logic

       Logic Circuit <---> Logic Programming

       Declarative meaning in Classical Logic
       Control Information  in Modal Logic

       Much suitable for automatic Verification, Synthesis
       and early time Simulation.

   Verification/Synthesis -----   Propositional Logic (decidable)
   Low Level Simulation

   High Level Simulation  -----   1st order Logic (non decidable)

______________________________________________________
2.  Interval Temporal Logic

    local ITL (  B. Moszkowski 1983  )

    three main modal logic operator

	chop(&&)  next(@)  empty

    other modal logic operator

	<>p <-> (true & p) 
	#p <-> ~ <> ~p
	fin(p)   <->	#(empty->p)
	keep(p)   <->	#(~empty->p)
	halt(p)   <->	#(empty->p,p->empty)

    Advantage of ITL

	It is easy to write sequentiality.
	   ---> more suitable for Programming Language than other
		temporal logic

______________________________________________________
3.  Execution of Interval Temporal Logic Tokio

    Unification on Temporal Logic Variable
    Refutation on next operator
    Refutation on chop operator

    Extended Horn Clause for temporal operator

    Compilation to Prolog

______________________________________________________
4.  How to write Hardware description in Tokio

	4.1  simple examples

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%   No.0	always operator   #
%		length operator
%
%   1   1   1   1   1   1
%   |---|---|---|---|---|---->

t0 :- #write(1),length(5).


%   No.1	chop operator
%		
%   0   0   0   0
%               1   1   1   1   1   1
%   |---|---|---|---|---|---|---|---|---->

t1 :- #write(0),length(3) && #write(1),length(5).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%   No.2	fin and keep
%		
%   0   0   0
%               1
%               2   2   2   2   2   2
%                                   3
%   |---|---|---|---|---|---|---|---|---->

t2 :- keep(write(0)), fin(write(1)), length(3)
	&& #write(2), fin(write(3)), length(5).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%   No.3	next operator
%		
%   0   1   2   3   4   5
%   |---|---|---|---|---|---->

t3 :- length(5), I = 1, counter(I), #write(I).

    counter(I) :- keep( @I = I+1 ).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%   No.4	stable operator
%		
%   2   2   2   2   2   2
%   |---|---|---|---|---|---->

t4 :- length(5), I = 2, stable(I), #write(I).

% stable(I) :- keep( @I = I ).    (defined internally)


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%   No.5	temporal assignment
%		
% A 0           1       0
%   |---|---|---|---|---|---->
% B 1           0       1
%   |---|---|---|---|---|---->

t5 :- A = 0, B = 1, 
	( A <- B, B <- A, length(3) &&
	  A <- B, B <- A, length(2) && true ),
     #write((A,B)).

%  A <- B :- C = B, stable(C), fin( A = C ).
%     (defined internally)


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%   No.6	interval join 
%		

t6 :-	length(8),
	N=3,(N gets N+1, halt( N=5 ) && stable(N)),
	M=0,(M gets M+1, fin( M=6 )  && stable(M)),
	#write((N,M)).

% A gets B :- keep(@A=B).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%   No.7	back track to the past
%		
 
t7:-	length(5),
	fin(M=N),
	N=3,(N gets N+1 && stable(N)),
	M=0,(M gets M+1 && stable(M)),
	#write((N,M)).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

4.2  two way description of Tokio

   
Example of two different descriptions of
	calculating magnitude of vector 

1) algorithm description using "chop operator"
		loosely timing

magasync(A,B,Res):-
	(if A < 0 
	   then Aab <- - A
	   else Aab <- A ),
	(if B < 0 
	   then Bab <- - B
	   else Bab <- B )
    &&
	(if Aab > Bab 
	   then G <- Aab, L <- Bab
	   else G <- Bab, L <- Aab)
    &&
     	Sqs <- G * 7 / 8 + L / 2 , G <- G
    &&
	(if G > Sqs 
	   then Res <- G
	   else Res <- Sqs).

2) "Always operator" based description
		tightly synchronized module


/* data flow calculation */

magasync_dataflow(A,B,Res):-
	Aab = 0, Bab = 0, G = 0, Res = 0,
	L = 0, Sqs = 0, G1 = 0,  % initialize 
	#abs_unit(A,Aab),
	#abs_unit(B,Bab),
	#maxmin(Aab,Bab,G,L),
	#calc(G,L,Sqs),
	#delay(G,G1),
	#result(G1,Sqs,Res).

delay(G,G1):-
	@G1 = G.

abs_unit(I,O):-
	if I < 0 then @O = -I else @O = I .

maxmin(I1,I2,O1,O2):-
	if I1 > I2 then (@O1 = I1, @O2 = I2)
        	   else (@O1 = I2, @O2 = I1) .

calc(I1,I2,O):- 
	@O = I1 * 7 / 8 + I2 / 2 .
	
result(I1,I2,O):-
	if I1 > I2 then @O = I1 else @O = I2 .

___________________________
4.3  pipeline merge sorter


test :- Strdata = [10,20,5,100,1,6,2,3],
    datagen(Strdata,Data),
    pipe(Data,Out),
    length(18),
    #write(Out).

        % Data Generator

datagen([],[]).
datagen([H|T],Out) :-
    Out = [H],
    @T = T, @datagen(T,Out).

        % Pipeline Merge Sorter

pipe(I0,Out) :-
    I1 = [], I2 = [], Out = [],
    proc_start(I0,I1, 2,1),
    proc_start(I1,I2, 4,2),
    proc_start(I2,Out,8,4).

    % Processor Unit

proc_start(I,O,P,PP) :-
    X = [], Y = [], Z = [], T = 1,
    #proc(I,O,X,Y,Z,T,P,PP).

proc(I,O,X,Y,Z,T,P,PP) :- X=[],Y=[],I=[],!,
    @X=X, @Y=Y, @Z=Z, @O=[], @T=1.
proc(I,O,X,Y,Z,T,P,PP) :-
     load(I,O,X,Y,Yn,Z,Zn,T,P,PP),
    merge(I,O,X,Y,Yn,Z,Zn,T,P,PP).

load(I,O,X,Y,Yn,Z,Zn,T,P,PP) :- T=<PP, !,
    append(Z,I,Zn), @Z=Zn, Yn=Y,
    @T=T+1.
load(I,O,X,Y,Yn,Z,Zn,T,P,PP) :- 
    append(Y,I,Yn), @Z=[],
    if T<P then @T=T+1 else @T=1.

merge(I,O,X,Y,Yn,Z,Zn,T,P,PP) :-X=[],Yn=[],!,
    @O=[], @Y=Yn,
    if T=PP then @X=Zn else @X=X.
merge(I,O,X,Y,Yn,Z,Zn,T,P,PP) :- X=[A|L],Yn=[],!,
    @O=[A], @Y=Yn,
    if T=PP then @X=Zn else @X=L.
merge(I,O,X,Y,Yn,Z,Zn,T,P,PP) :-X=[],Yn=[B|N],!,
    @O=[B], @Y=N,
    if T=PP then @X=Zn else @X=X.
merge(I,O,X,Y,Yn,Z,Zn,T,P,PP) :-X=[A|L],Yn=[B|N],!,
    if A<B then
	@O=[A], @X=L, @Y=Yn
    else
	@O=[B], @Y=N, @X=X.

append(Nil,L,L1) :- Nil=[],L=L1.
append(X,L,Y) :-[H|T]=X,[H1|M]=Y,
     H=H1,append(T,L,M).


______________________________________________________
5.    Support tool for Tokio

	Verifier for Propositional Logic
	Synthesizer for Propositional Logic

	We use Cube description


REFERENCES
[1]
 B. Moszkowski, "A Temporal Logic for Multi Level Reasoning about
 Hardware", IEEE Computer Magazine, February 1985.
[2]
 B. Moszkowski, "Executing Temporal Logic Programs",
 Technical Report No. 55 University of Cambridge, Computer Laboratory 1984.
[3]
 M. Fujita, S. Kono, "Temporal Logic Programming Language: Tokio and
 its compilation to Prolog", ICLP'86