A Formal Proof of PG Recurrence Equations of Parallel Adders
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
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.
© Copyright 2020 IEEE
Locate the Document
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