Verifying a Carry Look-Ahead Adder with Propositional Projection Temporal Logic

This paper presents a case study for verifying a carry look-ahead adder using the axiom system of Propositional projection temporal logic (PPTL). To this end, the syntax, semantics and axiom system of PPTL are briefly introduced. Further, functions and architectures of the carry look-ahead adder are presented. In addition, four lemmas are proved with the axiom system of PPTL. Finally, the correctness of the adder is verified based on the lemmas and the axiom system of PPTL. The case study shows that the axiom system for PPTL is workable.