« zurück

Kolloquium |30.06.2009 11.00 Uhr | Rotunde
Prof. Priyank Kalla
Univsersity of Utah, Salt Lake City, Utah, U.S.A.

Verification of Finite-Precision (Bit-Vector) Arithmetic using Finite Integer Algebras

Arithmetic datapath computations are widely found in many practical, and critical, digital hardware and software systems; with applications in communication systems, signal processing, embedded systems, cryptography, etc. Such designs perform arithmetic computations where operands have finite-precision. While errors related to finite-precision may cause malfunctioning of designs, they also expose systems to security-related vulnerabilities, compromising, for example, cryptographic keys. Therefore, there is a need to provide robust CAD support for design and verification of finite-precision arithmetic. In this talk, we will describe our work on the application of number theory, computational commutative algebra and algebraic geometry for verification of arithmetic datapaths. We will show how finite-word length (bit-vector) arithmetic can be modeled as polynomial functions over finite integer rings, and how numeric and symbolic algebra based techniques can be automated applied to reason about such computations. We will describe the challenges of these problems, present our research results and contrast our approach against traditional (SMT-solver and theorem-proving-based) techniques. Finally, we will discuss some important open problems that require much research.

Biography
Priyank Kalla received the B.E. degree in Electronics Engineering from Sardar Patel University in India in 1993. He received M.S. and PhD degrees from the University of Massachusetts at Amherst, USA, in 1998 and 2002, respectively. Since 2002, he has been an Assistant Professor with the ECE Dept. at the University of Utah, Salt Lake City, USA. His academic interests are in Electronic Design Automation, with emphasis on synthesis, optimization and verification of digital VLSI systems. Prof. Kalla has also worked with AMD, Cadence, and Digital Semiconductor (Alpha Microprocessor CAD & Test group). He is a recipient of the US National Science Foundation's Faculty Early Career Development Award, and will receive the 2009 ACM Transactions on Design Automation (TODAES) best paper award.