Computer Algebra knows Arithmetic Better

Thursday, 15 December 2016 at 14:15 in room INF 328

Cunxi Yu, PhD Student, University of Massachusetts, Amherst, MA, USA

Abstract:

Despite a considerable progress in verification of logic designs, advances in formal verification of arithmetic designs have been lagging. Boolean methods, such as BDDs and SAT, require “bit blasting,” i.e., flattening the design to a bit-level netlist, which makes verification of arithmetic circuits computationally expensive. In the past several years, computer algebraic method that rely on polynomial representation of the design has shown to be the best approach for analyzing arithmetic circuits. Algebraic methods overcome the bit-blasting limitation of the contemporary methods and commercial tools and provide several orders of magnitude speedup; they are already able to verify large integer multipliers with over two million gates. In this talk, I will describe the motivation of computer algebra research, review the formulation of the arithmetic verification problem, and will present our discoveries and results of analyzing integer arithmetic and finite field arithmetic implementations using computer algebraic method.

About the speaker:

Cunxi Yu is a 4th-year Ph.D. student under the supervision of Prof. Ciesielski. His Ph.D. research focuses on formal analysis of arithmetic circuits, including verification, debugging, abstraction, and reverse engineering. He also worked on hardware security and logic synthesis. His Ph.D. thesis topic is "Formal Analysis of Arithmetic Circuits using Computer Algebraic Approach - Verification, Debugging, and Abstraction". Chapter 4 in my thesis proposal was awarded by National Science Foundation 2016 ($450,000, 2016-2019). He has been a research intern at IBM T.J Watson Research Center in 2015 and 2016, where he worked on design automation research.

His research interests include formal verification, design automation, computer arithmetics, cryptography, formal methods for hardware security, design automation for approximate computing.