//*******************************************************************
//Proof of Correctness of a Floating Point Multiplier

//David M. Russinoff
//Advanced Micro Devices, Inc.
//February, 1999
//*******************************************************************

//This file contains the RTL model of the multiplier


module FMUL;

//*******************************************************************
// Declarations
//*******************************************************************

//Precision control:

`define SNG   1'b0        // single
`define DBL   1'b1        // double

//Rounding modes:

`define NRE   2'b00       // round to nearest
`define NEG   2'b01       // round to minus infinity
`define POS   2'b10       // round to plus infinity
`define CHP   2'b11       // truncate

//Inputs:

input x[79:0];             //first operand
input y[79:0];             //second operand
input rc[1:0];             //rounding control
input pc;                  //precision control
 
//Output:

output z[79:0];       //product


//*******************************************************************
// First Cycle 
//*******************************************************************

//Operand fields:

sgnx = x[79]; sgny = y[79];                      //signs
expx[14:0] = x[78:64]; expy[14:0] = y[78:64];    //exponents
sigx[63:0] <= x[63:0]; sigy[63:0] <= y[63:0];    //significands

//Sign of result:

sgnz <= sgnx ^ sgny;

//Biased exponent sum:

exp_sum[14:0] <= expx[14:0] + expy[14:0] + 15'h4001;

//Registers:

rc_C2[1:0] <= rc[1:0];
pc_C2 <= pc;


//*******************************************************************
// Second Cycle 
//*******************************************************************

//Rounding Constants//

//Overflow case -- single precision:

rconst_sing_of[127:0] = 
  case(rc_C2[1:0])
    `NRE : {25'b1, 103'b0};
    `NEG  : sgnz ? {24'b0, {104 {1'b1}}} : 128'b0;
    `POS  : sgnz ? 128'b0 : {24'b0, {104 {1'b1}}};
    `CHP : 128'b0;
  endcase;

//Overflow case -- double precision:

rconst_doub_of[127:0] = 
  case(rc_C2[1:0])
    `NRE : {54'b1, 74'b0};
    `NEG  : sgnz ? {53'b0, {75 {1'b1}}} : 128'b0;
    `POS  : sgnz ? 128'b0 : {53'b0, {75 {1'b1}}};
    `CHP : 128'b0;
  endcase;

//General overflow case:

rconst_of[127:0] <= case(pc_C2)
                      `SNG : rconst_sing_of[127:0];
                      `DBL : rconst_doub_of[127:0];  
                    endcase;

//No overflow:

rconst_nof[126:0] = rconst_of[127:1];

//Registers:

sgnz_C3 <= sgnz;
exp_sum_C3[14:0] <= exp_sum[14:0];
sigx_C3[63:0] <= sigx[63:0];
sigy_C3[63:0] <= sigy[63:0];
rc_C3[1:0] <= rc_C2[1:0];
pc_C3 <= pc_C2;


//*******************************************************************
// Third Cycle 
//*******************************************************************

//The output of an integer multiplier actually consists of two vectors,
//the sum of which is the product of the inputs sigx and sigy.  These
//vectors become available in the third cycle, when they are processed
//in parallel by three distinct adders.  The first of these produces
//the unrounded product, which is used only to test for overflow.
//The other two include rounding constants, assuming overflow and no
//overflow, respectively.  Thus, at the (hypothetical) implementation
//level, these three sums are actually generated in parallel:

prod[127:0] = {64'b0, sigx_C3[63:0]} * {64'b0, sigy_C3[63:0]};

add_of[128:0] <= {1'b0, prod[127:0]} + {1'b0, rconst_of[127:0]};

add_nof[127:0] <= prod[127:0] + rconst_nof[127:0];


//overflow indicator:

overflow <= prod[127];


//Sticky bit:

sticky_of <= case(pc_C3)
               `SNG : |(prod[102:0]);
               `DBL : |(prod[73:0]);
             endcase;

sticky_nof <= case(pc_C3)
                `SNG : |(prod[101:0]);
                `DBL : |(prod[72:0]);
              endcase;

//Registers:

rc_C4[1:0] <= rc_C3[1:0];
pc_C4 <= pc_C3;
sgnz_C4 <= sgnz_C3;
exp_sum_C4[14:0] <= exp_sum_C3[14:0];


//*******************************************************************
// Fourth Cycle 
//*******************************************************************

//Significand mask:

mask_of[127:0] =
  case (pc_C4)
    `SNG : (rc_C4[1:0] == `NRE) & ~sticky_of & ~add_of[103] ?
               {{23 {1'b1}}, 105'b0} : {{24 {1'b1}}, 104'b0};
    `DBL : (rc_C4[1:0] == `NRE) & ~sticky_of & ~add_of[74] ?
               {{52 {1'b1}}, 76'b0} : {{53 {1'b1}}, 75'b0};
  endcase;

mask_nof[126:0] = 
  case (pc_C4)
    `SNG : (rc_C4[1:0] == `NRE) & ~sticky_nof & ~add_nof[102] ?
               {{23 {1'b1}}, 104'b0} : {{24 {1'b1}}, 103'b0};
    `DBL : (rc_C4[1:0] == `NRE) & ~sticky_nof & ~add_nof[73] ?
               {{52 {1'b1}}, 75'b0} : {{53 {1'b1}}, 74'b0};
  endcase;

//Carry bit:

carry_of = add_of[128];
carry_nof = add_nof[127];

//Significand and exponent:

sig_of[128:0] = {1'b0, carry_of, 127'b0} | 
                (add_of[128:0] & {1'b0, mask_of[127:0]});
sig_nof[127:0] = {1'b0, carry_nof, 126'b0} | 
                 (add_nof[127:0] & {1'b0, mask_nof[126:0]});
sigz[63:0] = overflow ? sig_of[127:64] : sig_nof[126:63];

exp_of[14:0] = exp_sum_C4[14:0] + {14'b0, carry_of} + 15'b1;
exp_nof[14:0] = exp_sum_C4[14:0] + {14'b0, carry_nof};
expz[14:0] = overflow ? exp_of[14:0] : exp_nof[14:0];

//Final result:

z[79:0] = {sgnz_C4, expz[14:0], sigz[63:0]};

endmodule