DocumentCode
336504
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
fYear
1999
fDate
4-6 Mar 1999
Firstpage
232
Lastpage
233
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;
fLanguage
English
Publisher
ieee
Conference_Titel
VLSI, 1999. Proceedings. Ninth Great Lakes Symposium on
Conference_Location
Ypsilanti, MI
ISSN
1066-1395
Print_ISBN
0-7695-0104-4
Type
conf
DOI
10.1109/GLSV.1999.757419
Filename
757419
Link To Document