BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Functional Verification of Integer Arithmetic Circuits: an Algebra
 ic Approach
DTSTART:20150415T140000
DTEND:20150415T150000
DTSTAMP:20260408T070937Z
UID:dbe4f4d5ce1684b5f0826f315a28e50a6b3674f060b0c7e1b47c064c
CATEGORIES:Conferences - Seminars
DESCRIPTION:Bio: Maciej Ciesielski is Professor in the Department of Elect
 rical & Computer Engineering (ECE) at the University of Massachusetts\, Am
 herst. He received M.S. in Electrical Engineering from Warsaw Technical Un
 iversity\, Poland\, in 1974 and Ph.D. in Electrical Engineering from the U
 niversity of Rochester\, N.Y. in 1983. From 1983 to 1986 he worked at GTE 
 Laboratories on the SILC silicon compiler project. He joined the Universit
 y of Massachusetts in 1987. He teaches and conducts research in the area o
 f electronic design automation\, and specifically in synthesis\, verificat
 ion and simulation of VLSI circuits. In 2008 he received Doctorate Honoris
  Causa from the Universite de Bretagne Sud\, Lorient\, France\, for his co
 ntribution to the development of EDA tools for high level synthesis.\nFor 
 more details please consult his web site: http://www.ecs.umass.edu/ece/lab
 s/vlsicad/ciesielski.html\nAbstract:\nFunctional verification of arithmeti
 c circuits and data paths remains a challenging problem in hardware verifi
 cation. Boolean logic techniques based on binary decision diagrams (BDDs) 
 and satisfiability (SAT) solvers\, cannot handle complex arithmetic design
 s as they require ``bit-blasting''\, i.e.\, flattening of the design into 
 bit-level netlists. Approaches that rely on computer algebra and Satisfiab
 ility Modulo Theories (SMT) methods are either too abstract to handle the 
 bit-level nature of arithmetic designs or require solving computationally 
 expensive decision problems. Similarly\, theorem provers require a signifi
 cant human interaction and intimate knowledge of the design to guide the p
 roof process.\nThis talk presents a fundamentally different approach to fu
 nctional verification of integer arithmetic circuits. It is based on a net
 work flow model\, where the computation performed by the circuit is viewed
  as a flow of binary data through the circuit. The symbolic expression rep
 resenting the data at the circuit inputs is transformed into a polynomial 
 expression at the primary outputs. For the circuit to be functionally corr
 ect\, the resulting expression must match the binary encoding at the prima
 ry outputs. The procedure conducted in the opposite direction (from the pr
 imary outputs to the primary inputs) will extract the arithmetic function 
 implemented by the circuit. Different transformation techniques will be di
 scussed\, depending on the type of circuit implementations (structured add
 er networks vs. purely gate-level circuits). We show that this technique c
 an verify large arithmetic circuits up to 512-bit multipliers with over 2 
 million gates.
LOCATION:BC 420  https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR