A Formal Proof of PG Recurrence Equations of Parallel Adders

Authors

Gang Chen, Nanjing University of Aeronautics and AstronauticsFollow
Xiaoyu Song, Portland State UniversityFollow
Guowu Yang, University of Electronic Science and Technology of ChinaFollow
Ting Wang, Portland State University
Xiaoqiao Mu, Portland State University
Yongqian Fan, Nanjing University of Aeronautics and Astronautics

Published In

IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

Document Type

Citation

Publication Date

8-11-2020

Abstract

Parallel adders are extensively used in high performance computer design and hardware acceleration for large-scale data processing. In the adder design theory, a key property of the group propagated carry and the group generated carry is based on the two recurrence equations. The property is fundamental to many parallel prefix adders. However, there is no proof of the property in the literature. This paper presents a rigorous and complete proof for it. The proof can leverage a solid ground for a formal verification methodology for parallel adder-based chip design.

Rights

© Copyright 2020 IEEE

Locate the Document

https://doi.org/10.1109/TCAD.2020.3015414

DOI

10.1109/TCAD.2020.3015414

Persistent Identifier

https://archives.pdx.edu/ds/psu/34261

Publisher

IEEE

Citation Details

Chen, G., Song, X., Yang, G., Wang, T., Mu, X., & Fan, Y. (2020). A Formal Proof of PG Recurrence Equations of Parallel Adders. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1–1. https://doi.org/10.1109/TCAD.2020.3015414