Title :
Formal verification of tree-structured carry-lookahead adders
Author :
Kim, Sae Hwan ; Chin, Shiu-Kai
Author_Institution :
Dept. of Electr. Eng. & Comput. Eng., Syracuse Univ., NY, USA
Abstract :
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
Keywords :
adders; carry logic; formal verification; logic design; quadtrees; 4-bit components; HOL theorem power; carry-lookahead adders; formal verification; quad trees; specification; tree-structured carry-lookahead adders; Adders; Circuits; Concatenated codes; Formal verification; Hardware; Logic; Signal generators;
Conference_Titel :
VLSI, 1999. Proceedings. Ninth Great Lakes Symposium on
Conference_Location :
Ypsilanti, MI
Print_ISBN :
0-7695-0104-4
DOI :
10.1109/GLSV.1999.757419
