```// ************************************************************************** //
//                                                                            //
//    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 multiplication of 2-complement numbers   //
// by Booth recoding. In addition to Booth recoding, we also further optimize //
// the Booth recoding by bit-pair recoding so that the number of zeros is     //
// increased and as many as possible additions can be skipped.                //
// Note that the Booth multiplier has depth O(M+N) and size O(M*N) and is thus//
// not optimal and concerning the worst case complexity comparable to the     //
// paper-and-pencil methods. In practice, it is reported to behave better due //
// to the high probability of numbers with small absolute values. Such numbers//
// have 2-complement representations with large blocks of 1's or 0's so that  //
// the Booth multiplier can simply skip these blocks.                         //
// ************************************************************************** //

macro M = 5;    // number of digits used
macro N = 3;    // number of digits used
macro dval(x,i,k) = (i==k-1 ? -(x[i]?1:0) : (x[i]?1:0));
macro intval(x,k) = sum(i=0..k-1) (dval(x,i,k) * exp(2,i));

module IntMulBooth([M]bool ?x,[N]bool ?y,[M+N]bool p) {
event [M]int{2} bx;     // Booth recoding of x
event [M]int{2} bpx;    // bit-pair optimization of bx
event [M-1][N]bool pp;  // digits of partial products
event [M][N-1]bool cp;  // carries for summation
event sM;

// Booth encoding of x
bx[0] = (x[0] ? -1 : 0);
for(i=1..M-1)
bx[i] = (x[i] <-> x[i-1] ? 0 : (x[i] ? -1 : +1));

// bit-pair optimization of Booth encoding
for(i=0..(M/2)-1)
case
(bx[2*i+1] == +1 & bx[2*i] == -1) do {
bpx[2*i+1] = 0;
bpx[2*i]   = +1;
}
(bx[2*i+1] == -1 & bx[2*i] == +1) do {
bpx[2*i+1] = 0;
bpx[2*i]   = -1;
}
default {
bpx[2*i+1] = bx[2*i+1];
bpx[2*i]   = bx[2*i];
}
if(2*(M/2) != M)
bpx[M-1] = bx[M-1];

// construct M x N multiplier array
for(i=0..M-1) {
// IntAdd/IntSub of pp[i-1][N-1..0] and y[N-1..0] depending on bpx[i]
for(j=0..N-1) {
let(doSkp = bpx[i] == 0)
let(doSub = bpx[i] == -1)
let(yj   = !doSkp & (doSub xor y[j]))
let(xyin = (j==N-1 ? !yj : yj))
let(pin  = (i==0 ? (j==N-1) : pp[i-1][j]))
let(cin  = (j==0 ? doSub : cp[i][j-1]))
let(pout = (j==0 | i==M-1 ? p[i+j] : pp[i][j-1]))
let(cout = (j==N-1 ? (i==M-1 ? sM : pp[i][N-1]) : cp[i][j]))
FullAdd(xyin,pin,cin,cout,pout);
}
}
p[M+N-1] = !sM;
// check the result
assert(intval(p,M+N) == intval(x,M) * intval(y,N));
}
```