// ************************************************************************** // // // // 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 // // // // ************************************************************************** // import ComputerArchitecture.AsynchronousCircuits.AsyncArbiter.*; //ArbiterInContext module AsyncArbiter (bool usr1_req, usr2_req, tok1_ack, tok2_ack, src_ack, usr1_ack,usr2_ack,tok1_req,tok2_req,src_req, ?del1,?del2,?del3,?del4,?del5,?del6,?del7,?del8,?del9,?del10){ T1 : Server(false,tok1_req,tok1_ack); || T2 : Server(false,tok2_req,tok2_ack); || SR : Server(false,src_req,src_ack); || U1 : Client(usr1_ack,usr1_req); || U2 : Client(usr2_ack,usr2_req); || AR : CorrectedArbiter(usr1_req,usr2_req,tok1_ack,tok2_ack,src_ack, usr1_ack,usr2_ack,tok1_req,tok2_req,src_req, del1,del2,del3,del4,del5,del6,del7,del8,del9,del10); } satisfies { // mutex : // A G !(usr1_ack & usr2_ack); // -------------------------------------------------------- // four-phase protocol with user one // -------------------------------------------------------- ack_until_no_req_usr1 : assert A G (usr1_ack -> [usr1_ack WU (!usr1_req)]); no_ack_until_req_usr1 : assert A G (!usr1_ack -> [(!usr1_ack) WU usr1_req]); // counterexample: // // del1 _____________________|| // del2 _____________________|| // del3 _____________-------_|| // del4 _____________--______|| // del5 _____________________|| // del6 _____________________|| // // usr1_req __-------_-_-________|| // usr1_ack ________-------_____-|| // // usr2_req _____________________|| // usr2_ack _____________________|| // // tok1_req ____-------_-___-----|| // tok1_ack _____-------_-___----|| // // tok2_req _____________________|| // tok2_ack _____________________|| // // src_req ______-------_-___---|| // src_ack _______-------_-___--|| // -------------------------------------------------------- // four-phase protocol with user two // -------------------------------------------------------- // ack_until_no_req_usr2 : // A G (usr2_ack -> [usr2_ack WU (!usr2_req)]); // no_ack_until_req_usr2 : // A G (!usr2_ack -> [(!usr2_ack) WU usr2_req]); // req_until_ack_tok1 : // A G (tok1_req -> [tok1_req WU (tok1_ack)]); // req_until_ack_tok2 : // A G (tok2_req -> [tok2_req WU (tok2_ack)]); // req_until_ack_src : // A G (src_req -> [src_req WU (src_ack)]); }