// ************************************************************************** //
//                                                                            //
//    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/AsyncArbiterBoch82CS.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 AsyncArbiterBoch82CS(bool usr1_req,usr2_req,trf1_ack,trf2_ack,src_ack,
                                 usr1_ack,usr2_ack,trf1_req,trf2_req,src_req,
                                 ?react){
    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;
    }
    || Client(react,usr1_req,usr1_ack);
    || Client(react,usr2_req,usr2_ack);
    || Server(react,trf1_req,trf1_ack);
    || Server(react,trf2_req,trf2_ack);
    || Server(react,src_req,src_ack);
} satisfies {
// ------------------------------------------------------------------------
// specification of the arbiter's four cycle protocol [Bochmann, 1982]
// ------------------------------------------------------------------------
    FourCycleProtocol:
            assert A (G F react ->
                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 G!(usr1_ack & usr2_ack);
    MutexParameterTransfer:
            assert A G !(trf1_req & trf2_req);
    SafeParameterTransfer1:
            assert A 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 F react ->
                G ((usr1_req -> F (usr1_req & trf1_req & src_req)) &
                (usr2_req -> F (usr2_req & trf2_req & src_req)) )
            );
}