Formal Analysis of End-Around-Carry Adder in Floating-Point Unit
Feng Liu, Xiaoyu Song, Qingping Tan, Gang Chen · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · 2010
End-around-carry (EAC) adder is extensively used in microprocessor's floating-point units. This paper presents an algebraic characterization of an EAC adder's algorithm. A novel symbolic analysis approach is presented to prove the EAC adder's correctness. Algebraic structures and first-order recursive equations are harnessed in proof derivations. A hybrid prefix/EAC architecture is considered.