Professor
Department of Electrical & Computer Engineering
University of Massachusetts, Amherst, MA, USA

 

Webpage

Verification of Arithmetic Circuits: What makes it Difficult

Thursday, 10 December 2015 at 14:20 in BC 420

 

Abstract:

This talk presents an algebraic approach to functional verification of gate-level, integer arithmetic circuits. It is based on extracting a unique bit-level polynomial function computed by the circuit directly from its gate-level implementation. It is shown how function extraction and the test if the implementation satisfies the specification can be implemented using a backward algebraic rewriting.

Experiments were performed on multipliers, multiply-accumulate, squarers, and other arithmetic circuits with up to 512-bit operands and over 2 Million gates. The circuits were synthesized and mapped onto standard cells using ABC system with different degree of optimization. The results demonstrate good scalability of the method for lightly synthesized circuits.

However, the method is less efficient when applied to highly optimized bit-level circuits, mapped using commercial synthesis tools. It seems that synthesis which retains certain degree of redundancy in the circuit (in form of "vanishing polynomials"), may be useful in verification. Solving the verification problem for circuits synthesized with commercial tools remains a challenge, as these tools are more aggressive in removing such a redundancy. We hope that this talk will stimulate the discussion about the reason for this inefficiency.

About the speaker:

Maciej Ciesielski is Professor in the Department of Electrical & Computer Engineering (ECE) at the University of Massachusetts, Amherst. He received M.S. in Electrical Engineering from Warsaw Technical University, Poland, in 1974 and Ph.D. in Electrical Engineering from the University of Rochester, N.Y. in 1983. From 1983 to 1986 he worked at GTE Laboratories on the SILC silicon compiler project. He joined the University of Massachusetts in 1987. He teaches and conducts research in the area of electronic design automation, and specifically in synthesis, verification and simulation of VLSI circuits. In 2008 he received Doctorate Honoris Causa from the Universite de Bretagne Sud, Lorient, France, for his contribution to the development of EDA tools for high level synthesis.