Only available in German
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.
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.
Prof. Dr. Rolf Drechsler