Abstract
The size and the complexity of digital circuits are increasing rapidly. This makes the circuits highly error-prone. As a result, proving the correctness of a circuit is of utmost importance after the design phase. Arithmetic circuits are among the most challenging designs to verify due to their high complexity and big size. In recent years, several formal methods have been proposed to verify arithmetic circuits. However, time and space complexity bounds are still unknown for most of these approaches, resulting in performance unpredictability. In this paper, we clarify the importance of polynomial formal verification for digital designs particularly arithmetic circuits. We also introduce an Arithmetic Logic Unit (ALU) and prove that formal verification of this circuit is possible in polynomial time. Finally, we confirm the correctness of the complexity bounds by experimental results.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Brace KS, Rudell RL, Bryant RE (1990) Efficient implementation of a BDD package. In: Design automation conference, pp 40–45
Bryant RE (1995) Binary decision diagrams and beyond: enabling technologies for formal verification. In: International conference on computer-aided design, pp 236–243
Disch S, Scholl C (2007) Combinational equivalence checking using incremental SAT solving, output ordering, and resets. In: ASP design automation conference, pp 938–943
Drechsler R (2004) Advanced formal verification. Kluwer Academic Publishers
Drechsler R (2017) Formal system verification: state-of the-art and future trends. Springer
Drechsler R (2021) PolyAdd: polynomial formal verification of adder circuits. In: IEEE symposium on design and diagnostics of electronic circuits and systems, pp 99–104
Drechsler R (2021) Polynomial circuit verification using BDDs. arXiv:2104.03024
Drechsler R, Becker B, Ruppertz S (1997) The K*BMD: a verification data structure. IEEE Des Test Comput 14(2):51–59
Drechsler R, Dominik C (2021) Edge verification: ensuring correctness under resource constraints. In: Symposium on integrated circuits and system design
Drechsler R, Sieling D (2001) Binary decision diagrams in theory and practice. Int J Softw Tools Technol Transf 3(2):112–136
Goldberg EI, Prasad MR, Brayton RK (2001) Using SAT for combinational equivalence checking. In: Design, automation and test in Europe, pp 114–121
Höreth S, Drechsler R (1999) Formal verification of word-level specifications. In: Design, automation and test in Europe, pp 52–58
Kapur D, Subramaniam M (1998) Mechanical verification of adder circuits using rewrite rule laboratory. Formal Meth Syst Des 13(2):127–158
Kaufmann D, Biere A (2020) Nullstellensatz-proofs for multiplier verification. In: Computer algebra in scientific computing. Lecture notes in computer science, vol 12291. Springer, pp 368–389
Kaufmann D, Biere A, Kauers M (2019) Verifying large multipliers by combining SAT and computer algebra. In: International conference on formal methods in CAD, pp 28–36
Keim M, Drechsler R, Becker B, Martin M, Molitor P (2003) Polynomial formal verification of multipliers. Formal Meth Syst Des 22(1):39–58
Koren I (2001) Computer arithmetic algorithms. A. K. Peters, Ltd., 2nd edn
Mahzoon A, Drechsler R (2021) Late breaking results: polynomial formal verification of fast adders. In: Design automation conference
Mahzoon A, Drechsler R (2021) Polynomial formal verification of area-efficient and fast adders. In: Reed-Muller workshop
Mahzoon A, Große D, Drechsler R (2018) PolyCleaner: clean your polynomials before backward rewriting to verify million-gate multipliers. In: International conference on computer-aided design, pp 129:1–129:8
Mahzoon A, Große D, Drechsler R (2019) RevSCA: Using reverse engineering to bring light into backward rewriting for big and dirty multipliers. In: Design automation conference, pp 185:1–185:6
Mahzoon A, Große D, Drechsler R (2021) RevSCA-2.0: SCA-based formal verification of non-trivial multipliers using reverse engineering and local vanishing removal. IEEE Trans Comput-Aided Des Integr Circuits Syst
Mahzoon A, Große D, Scholl C, Drechsler R (2020) Towards formal verification of optimized and industrial multipliers. In: Design, automation and test in Europe, pp 544–549
Pavlenko E, Wedler M, Stoffel D, Kunz W, Wienand O, Karibaev E (2008) Modeling of custom-designed arithmetic components in ABL normalization. In: Forum on specification and design languages, pp 124–129
Somenzi F (2018) CUDD: CU decision diagram package release 2.7.0. available at https://github.com/ivmai/cudd
Stoffel D, Kunz W (2004) Equivalence checking of arithmetic circuits on the arithmetic bit level. IEEE Trans Comput Aided Des Circuits Syst 23(5):586–597
Temel M, Slobodová A, Hunt WA (2020) Automated and scalable verification of integer multipliers. In: Computer aided verification, pp 485–507
Vasudevan S, Viswanath V, Sumners RW, Abraham JA (2007) Automatic verification of arithmetic circuits in RTL using stepwise refinement of term rewriting systems. IEEE Trans Comput 56(10):1401–1414
Wegener I (2000) Branching Programs and Binary Decision Diagrams. SIAM
Wilhelm U, Ebel S, Weitzel A (2016) Functional safety of driver assistance systems and ISO 26262. In: Handbook of driver assistance systems: basic information, components and systems for active safety and comfort. Springer, pp 109–131
Wolf C (2015) Yosys open synthesis suit. http://www.clifford.at/yosys/
Zimmermann R (1997) Binary adder architectures for cell-based VLSI and their synthesis. PhD thesis, Swiss Federal Institute of Technology
Acknowledgements
This work was supported by the German Research Foundation (DFG) within the Reinhart Koselleck Project PolyVer: Polynomial Verification of Electronic Circuits (DR 287/36-1).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Drechsler, R., Mahzoon, A., Weingarten, L. (2022). Polynomial Formal Verification of Arithmetic Circuits. In: Chaki, N., Devarakonda, N., Cortesi, A., Seetha, H. (eds) Proceedings of International Conference on Computational Intelligence and Data Engineering. Lecture Notes on Data Engineering and Communications Technologies, vol 99. Springer, Singapore. https://doi.org/10.1007/978-981-16-7182-1_36
Download citation
DOI: https://doi.org/10.1007/978-981-16-7182-1_36
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-16-7181-4
Online ISBN: 978-981-16-7182-1
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)