// ************************************************************************** //
//                                                                            //
//    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 an unsigned  //
// multiplication of two input words. The result are two output words 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 MULU(event ?ev1,?ev2,?ev3,?ev4, bv{WL} ?x1,?x2,!x3,!x4) {
    bv{WL} r1,r2,r3,r4;

    loop {
        assert(bv2nat(r4@r3) == bv2nat(r1) * bv2nat(r2));
        await(ev1 or ev2 or ev3 or ev4);
        let (v1 = (ev1 ? x1 : r1))
        let (v2 = (ev2 ? x2 : r2))
        let (v3 = nat2bv(bv2nat(v1) * bv2nat(v2),2*WL)) {
            next(r1) = v1;
            next(r2) = v2;
            next(r3) = v3{WL-1:0};
            next(r4) = v3{2*WL-1:WL};
            if(ev3) x3 = r3;
            if(ev4) x4 = r4;
        }
   }
}