zbMATH — the first resource for mathematics

Functional verification of high performance adders in Coq. (English) Zbl 1437.68191
Summary: Addition arithmetic design plays a crucial role in high performance digital systems. The paper proposes a systematic method to formalize and verify adders in a formal proof assistant Coq. The proposed approach succeeds in formalizing the gate-level implementations and verifying the functional correctness of the most important adders of interest in industry, in a faithful, scalable, and modularized way. The methodology can be extended to other adder architectures as well.
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
94D10 Boolean functions
Coq; CoqMTU; Coquet; PREVAIL
Full Text: DOI
[1] Hunt, W. A.; Brock, B. C.; Leeser, M.; Brown, G., The verification of a bit-slice ALU, Hardware Specification, Verification and Synthesis: Mathematical Aspects. Hardware Specification, Verification and Synthesis: Mathematical Aspects, Lecture Notes in Computer Science, 408, 282-306 (1990), New York, NY, USA: Springer, New York, NY, USA
[2] Borrione, D.; Pierre, L.; Salem, A., Formal verification of VHDL descriptions in the prevail environment, IEEE Design & Test of Computers, 9, 2, 42-56 (1992)
[3] Camilleri, A.; Gordon, M.; Melham, T., Hardware Verification Using Higher-Order Logic (1986), Cambridge, UK: Computer Laboratory, University of Cambridge, Cambridge, UK
[4] Curzon, P., Experiences formally verifying a network component, Proceedings of the 9th Annual Conference on Computer Assurance (COMPASS ’94)
[5] Paulin-Mohring, C.; Berardi, S.; Coppo, M., Circuits as streams in Coq: verification of a sequential multiplier, Types for Proofs and Programs. Types for Proofs and Programs, Lecture Notes in Computer Science, 1158, 216-230 (1996), Berlin, Germany: Springer, Berlin, Germany · Zbl 1407.68439
[6] Coupet-Grimal, S.; Jakubiec, L., Certifying circuits in type theory, Formal Aspects of Computing, 16, 4, 352-373 (2004) · Zbl 1061.68105
[7] The Coq Development Team, The Coq proof assistant, reference manual, version 8.4 (2012), Roquencourt, France: INRIA, Roquencourt, France
[8] Braibant, T.; Jouannaud, J.-P.; Shao, Z., Coquet: a coq library for verifying hardware, Certified Programs and Proofs. Certified Programs and Proofs, Lecture Notes in Computer Science, 7086, 330-345 (2011), Berlin, Germany: Springer, Berlin, Germany · Zbl 1350.68226
[9] Milne, G. J., Formal Specification and Verification of Digital Systems (1993), New York, NY, USA: McGraw-Hill, New York, NY, USA
[10] O’Donnell, J. T.; Rünger, G., Functional pearl derivation of a logarithmic time carry lookahead addition circuit, Journal of Functional Programming, 14, 6, 697-713 (2004) · Zbl 1063.68039
[11] Liu, F.; Tan, Q.; Chen, G., Formal proof of prefix adders, Mathematical and Computer Modelling, 52, 1-2, 191-199 (2010) · Zbl 1201.68163
[12] Chen, G., Formalization of a parameterized parallel adder within the Coq theorem prover, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 29, 1, 149-153 (2010)
[13] Kapur, D.; Subramaniam, M., Mechanical verification of adder circuits using rewrite rule laboratory, Formal Methods in System Design, 13, 2, 127-158 (1998)
[14] Hinze, R.; Kozen, D., An algebra of scans, Mathematics of Program Construction. Mathematics of Program Construction, Lecture Notes in Computer Science, 3125, 186-210 (2004), Berlin, Germany: Springer, Berlin, Germany
[15] Barras, B.; Jouannaud, J. P.; Strub, P. Y.; Wang, Q., CoQMTU: a higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory, Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS ’11)
[16] Wang, Q.; Barras, B.; Rocca, S. R. D., Semantics of intensional type theory extended with decidable equational theories, Computer Science Logic (CSL ’13). Computer Science Logic (CSL ’13), Leibniz International Proceedings in Informatics (LIPIcs), 23, 653-667 (2013), Dagstuhl, Germany: Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany
[17] Ling, H., High-speed binary adder, IBM Journal of Research and Development, 25, 3, 156-166 (1981)
[18] Jackson, R.; Talwar, S., High speed binary addition, Proceedings of the Conference Record of the 38th Asilomar Conference on Signals, Systems and Computers
[19] Koren, I., Computer Arithmetic Algorithms (2002), Hyderabad, India: Universities Press, Hyderabad, India
[20] Kogge, P. M.; Stone, H. S., A parallel algorithm for the efficient solution of a general class of recurrence equations, IEEE Transactions on Computers, 2, 8, 786-793 (1973) · Zbl 0262.68015
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.