Formal verification of tree-structured carry-lookahead adders
S.H. Kim, Shiu‐Kai Chin · 2003
Quad trees-trees with four branches, are used to abstractly describe tree-structured carry-lookahead adders using 4-bit components. The specification and implementation descriptions are parametrized and tree-structured adders having arbitrarily large inputs and outputs are described. The descriptions are formally verified using the HOL theorem power.