Formal verification of tree-structured carry-lookahead adders

Sae Hwan Kim, Shiu Kai Chin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationProceedings of the IEEE Great Lakes Symposium on VLSI
PublisherIEEE Computer Society
Pages232-233
Number of pages2
ISBN (Print)0769501044
StatePublished - Dec 1 1999
EventProceedings of the 1999 9th Great Lakes Symposium on VLSI (GLSVLSI '99) - Ann Arbor, MI, USA
Duration: Mar 4 1999Mar 6 1999

Publication series

NameProceedings of the IEEE Great Lakes Symposium on VLSI
ISSN (Print)1066-1395

Other

OtherProceedings of the 1999 9th Great Lakes Symposium on VLSI (GLSVLSI '99)
CityAnn Arbor, MI, USA
Period3/4/993/6/99

ASJC Scopus subject areas

  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Formal verification of tree-structured carry-lookahead adders'. Together they form a unique fingerprint.

  • Cite this

    Kim, S. H., & Chin, S. K. (1999). Formal verification of tree-structured carry-lookahead adders. In Proceedings of the IEEE Great Lakes Symposium on VLSI (pp. 232-233). (Proceedings of the IEEE Great Lakes Symposium on VLSI). IEEE Computer Society.