// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
//                                                                            //
// filename:    ./ComputerArchitecture/AsynchronousCircuits/                  //
//              AsyncArbiterBoch82/AsyncArbiterBoch82.qrz                     //
// author:      Manuel Gesell                                                 //
//                                                                            //
// description:                                                               //
// This Quartz file implements an asynchronous arbiter circuit as given in    //
// the following references                                                   //
//  * G.V. Bochmann: Hardware Specification with Temporal Logic:              //
//    An Example, IEEE Transactions on Computers, 1982                        //
//  * D.L. Dill and E.M. Clarke: "Automatic Verification of Asynchronous      //
//    Circuits using Temporal Logic, Proceedings of the IEEE, 1986            //
//                                                                            //
// ************************************************************************** //
import ComputerArchitecture.AsynchronousCircuits.AsyncArbiterBoch82.*;

// -- macros for specifying the protocol from the client's view
macro CLIENT1(req,ack) = ( req -> [req WU (req & ack)]);
macro CLIENT2(req,ack) = (!req -> [(!req) WU (!req & !ack)]);
macro CLIENT3(req,ack) = (ack -> F !req);
macro CLIENT(req,ack)  = G(CLIENT1(req,ack) & CLIENT2(req,ack) & CLIENT3(req,ack) );

// -- macros for specifying the protocol from the server's view
macro SERVER1(req,ack) = ( ack -> [ack WU (ack & !req)]);
macro SERVER2(req,ack) = (!ack -> [(!ack) WU (!ack & req)]);
macro SERVER3(req,ack) = ((req -> F ack) & (!req -> F !ack));
macro SERVER4(req,ack) = (SERVER1(req,ack) & SERVER2(req,ack) & SERVER3(req,ack) );
macro SERVER(req,ack)  = (!ack & G SERVER4(req,ack));

module AsyncArbiterBoch82(bool  usr1_req, usr2_req, trf1_ack, trf2_ack, src_ack,
                                usr1_ack,usr2_ack,!trf1_req,!trf2_req,!src_req) {
    bool ME_in1,ME_in2,ME_out1,ME_out2,
         OR3_in1,OR3_in2;
    loop {
        if(src_ack==trf1_ack) usr1_ack=src_ack;
        if(src_ack==trf2_ack) usr2_ack=src_ack;
        ME_in1 = usr1_ack | usr1_req;
        ME_in2 = usr2_ack | usr2_req;
        if(!(ME_in1&ME_in2)) {
            next(ME_out1) = ME_in1;
            next(ME_out2) = ME_in2;
        } else if(ME_in1&ME_in2&!ME_out1&!ME_out2) {
            choose next(ME_out1) = true;
            else   next(ME_out2) = true;
        }
        trf1_req = ME_out1 & usr1_req;
        trf2_req = ME_out2 & usr2_req;
        if(trf1_ack==usr1_req) OR3_in1=usr1_req;
        if(trf2_ack==usr2_req) OR3_in2=usr2_req;
        src_req = OR3_in1 | OR3_in2;
        pause;
    }
} satisfies {
    FourCycleProtocol:
        assert A (CLIENT(usr1_req,usr1_ack) & CLIENT(usr2_req,usr2_ack) &
                  SERVER(trf1_req,trf1_ack) & SERVER(trf2_req,trf2_ack) &
                  SERVER(src_req,src_ack)
                  ->
                  SERVER(usr1_req,usr1_ack) & SERVER(usr2_req,usr2_ack) &
                  CLIENT(trf1_req,trf1_ack) & CLIENT(trf2_req,trf2_ack) &
                  CLIENT(src_req,src_ack)
        );
    MutexAcknowledge:
        assert A (CLIENT(usr1_req,usr1_ack) & CLIENT(usr2_req,usr2_ack) &
                  SERVER(trf1_req,trf1_ack) & SERVER(trf2_req,trf2_ack) &
                  SERVER(src_req,src_ack)
                  ->
                  G!(usr1_ack & usr2_ack)
        );
    MutexParameterTransfer:
        assert A G !(trf1_req & trf2_req);
    SafeParameterTransfer1:
        assert A (G (CLIENT(usr1_req,usr1_ack) & CLIENT(usr2_req,usr2_ack) &
                     SERVER(trf1_req,trf1_ack) & SERVER(trf2_req,trf2_ack) &
                     SERVER(src_req,src_ack))
                  ->
                  G (src_req & !src_ack -> trf1_req & trf1_ack
                     | trf2_req & trf2_ack) );
/*    SafeParameterTransfer2:
        assert A G ((trf1_req -> [trf1_req WU trf1_ack]) &
                    (trf2_req -> [trf2_req WU trf2_ack]) );
    Liveness:
        assert A G ((usr1_req -> F (usr1_req & trf1_req & src_req)) &
                    (usr2_req -> F (usr2_req & trf2_req & src_req)) );*/
}

// module ArbiterStructure(bool  usr1_req, usr2_req, trf1_ack, trf2_ack, src_ack,
//              &usr1_ack,&usr2_ack,&trf1_req,&trf2_req,&src_req)
// implements ArbiterSpec(usr1_req,usr2_req,trf1_ack,trf2_ack,src_ack,
//             usr1_ack,usr2_ack,trf1_req,trf2_req,src_req) {
// bool ME_in1,ME_in2,ME_out1,ME_out2,
//      OR3_in1,OR3_in2;
//      C1   : C_Element(src_ack,trf1_ack,usr1_ack);
//   || C2   : C_Element(src_ack,trf2_ack,usr2_ack);
//   || OR1  : OrGate(usr1_ack,usr1_req,ME_in1);
//   || OR2  : OrGate(usr2_ack,usr2_req,ME_in2);
//   || ME   : ME_Element(ME_in1,ME_in2,ME_out1,ME_out2);
//   || AND1 : AndGate(ME_out1,usr1_req,trf1_req);
//   || AND2 : AndGate(ME_out2,usr2_req,trf2_req);
//   || C3   : C_Element(trf1_ack,usr1_req,OR3_in1);
//   || C4   : C_Element(trf2_ack,usr2_req,OR3_in2);
//   || OR3  : OrGate(OR3_in1,OR3_in2,src_req);
// }


// ------------------------------------------------------------------------
// specification of the arbiter's four cycle protocol [Bochmann, 1982]
// ------------------------------------------------------------------------