Formal Verification and Verilog Code Generation for Coq-based Carry-Lookahead Adder Algorithm

This article describes the application of customized proof techniques for proving theorems related to arithmetic circuits in the Coq theorem prover and generating Verilog code from Coq. By illustrating the correctness verification process of a carry-lookahead adder (CLA) as an example, this set of proof strategies not only significantly simplifies the proof process but also enhances the efficiency of Coq formal verification in general. It is also possible to generate Verilog code for CLA of arbitrary size (up to 128 bits) based on Signal type. Additionally, the Verilog code for CLA generated from Coq can be run directly, has been synthesized and simulated in Quartus.