// --------------------------------------------------------------------
// This is an implementation of Booth's algorithm for multiplication.
// Note, however, that Booth's main motivation was to minimize the number
// which can be even further improved by Reitwiesner's encoding.
// Booth's algorithm is based on an encoding of the multiplicand as a
// signed digit number, i.e. a number where digits 0,1 and -1 may occur.
// Booth's observation was that only those positions in the multiplicant
// where the bits are changing either (01 or 10) must lead
// to an addition/subtraction of the correctly shifted multiplicant.
// Hence, Booth's algorithm makes also sense for unsigned numbers, if
// addition/subtraction is more expensive than simple shifting.
// --------------------------------------------------------------------

#ifndef abits
#define abits 4
#endif

#ifndef bbits
#define bbits 4
#endif

#define LSH(x) ((x){-2:0}@false)
#define RSH(x) (((x){-1})@(x){:1})
#define BvIntPlus(n,x,y)  ((bv)((int)(x) + (int)(y))){n-1:}
#define BvIntMinus(n,x,y) ((bv)((int)(x) - (int)(y))){n-1:}


module Monitor(int[abits] a, int[bbits] b,
	       int[abits+bbits] &p,&q, event &correct)
implements MonitorSpec(correct) {
   next(q) = a*b;
   BoothMult01((bv)a,(bv)b,(bv)p);
   if(p==q) emit correct;
}


spec MonitorSpec(event correct) {
   IsCorrect  : A F correct;
}


module BoothMult01(bv[abits] a, bv[bbits] b, bv[abits+bbits] &p) {
   bv[abits] x, bv[bbits] y, bool y_old;
   x = a;
   y = b;
   p = {false::abits+bbits};
   y_old = false;
   sequence(int i=1 .. bbits) {
      let (p1 = p{:-abits} )
      let (p2 = p{-1-abits:1} ) {
         if(y_old & !y{0})
            next(p) = BvIntPlus(abits+1,p1,x)@p2;
         else if(!y_old & y{0})
            next(p) = BvIntMinus(abits+1,p1,x)@p2;
         else
            next(p) = RSH(p);
         next(y_old) = y{0};
         next(y) = RSH(y);
      }
      pause;
   }
}