// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// The following module implements a function unit that performs a signed     //
// division of two input words. The quotient and the remainder are stored in  //
// r3 and r4 such that the invariant mentioned in the code holds.             //
// As every ALU function unit, this unit waits until one of the event signals //
// ev1,ev2,ev3 or ev4 is present. Then, none, one, or both of the operands x1 //
// and x2 are fetched, and their result is computed. The result is stored in  //
// the two local registers r3 and r4 and the operands are stored in r1 and r2.//
// Note that the events trigger the following basic transport actions:        //
//      ev1: next(r1) = x1                                                    //
//      ev2: next(r2) = x2                                                    //
//      ev3: x3 = r3                                                          //
//      ev4: x4 = r4                                                          //
// The computation is done as a side effect to maintain the invariant.        //
// ************************************************************************** //

macro WL = 8;

module DIVS(event ?ev1,?ev2,?ev3,?ev4, bv{WL} ?x1,?x2,!x3,!x4) {
    bv{WL} r1,r2,r3,r4;

    loop {
        assert(bv2int(r1) == bv2int(r3) * bv2int(r2) + bv2int(r4));
        await(ev1 or ev2 or ev3 or ev4);
        let (v1 = (ev1 ? x1 : r1))
        let (v2 = (ev2 ? x2 : r2)) {
            next(r1) = v1;
            next(r2) = v2;
            next(r3) = int2bv(bv2int(v1) / bv2int(v2),WL);
            next(r4) = int2bv(bv2int(v1) % bv2int(v2),WL);
            if(ev3) x3 = r3;
            if(ev4) x4 = r4;
        }
   }
}