@inproceedings{bf22f70092aa4624a7f078dada5e13a8,
title = "Formal verification of tree-structured carry-lookahead adders",
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 parameterized and describe tree-structured adders having arbitrarily large inputs and outputs. The descriptions are formally verified using the HOL theorem prover.",
author = "Kim, {Sae Hwan} and Chin, {Shiu Kai}",
year = "1999",
language = "English (US)",
isbn = "0769501044",
series = "Proceedings of the IEEE Great Lakes Symposium on VLSI",
publisher = "IEEE Computer Society",
pages = "232--233",
booktitle = "Proceedings of the IEEE Great Lakes Symposium on VLSI",
address = "United States",
note = "Proceedings of the 1999 9th Great Lakes Symposium on VLSI (GLSVLSI '99) ; Conference date: 04-03-1999 Through 06-03-1999",
}