Until a few years ago, automatic formal verification of arithmetic datapath circuits was considered an unsolvable problem. It was indeed impossible to formally verify custom-designed arithmetic circuits, automatically, beyond even 16-bit datapath word-lengths. Computational techniques quickly encountered exponential space and time explosion of complexity. In the past couple of years, the state-of-the-art in this area has witnessed a significant leap in verification capacity, facilitating verification for up to 500-bit word-lengths. Algebraic Geometry has played a fundamental role in this success -- helping us understand the nature of the problem, and enabling algorithmic implementations to exploit domain-specific knowledge for efficiency and scalability.
Algorithms in computational algebraic geometry exhibit very high complexity; e.g., Groebner bases are doubly-exponential in general. However, datapath designs exhibit some form of structure and symmetry in their functions and implementations. We show that the powerful Groebner basis reasoning helps us discover this "structure and symmetry", which can be exploited to simplify the solutions -- thus enabling scalability. In this talk, I will describe the verification context, the problem formulations, our discoveries, and results. I will conclude the talk with discussions on other significant problems that can be solved by analyzing word-level abstractions of hardware designs using algebraic geometry.
Priyank Kalla is an Associate Professor in the Electrical & Computer Engineering department at the Univ. of Utah. His areas of interests are in electronic design automation and hardware verification. He received the B.E. degree in Electronics from Sardar Patel University in India (1993) and M.S. and Ph.D. from the Univ. of Massachusetts Amherst in 1998 and 2002, respectively. He has worked with AMD K-7 and the DEC Alpha microprocessor CAD & Test groups. He's a recipient of the US NSF CAREER award and the ACM Trans. on Design Automation best paper award. He was the chair of IEEE technical committee on computer-aided network design and currently also serves as an associate editor for IEEE Trans. on CAD.