IC/IEM Talk: Formal Verification and Debugging of Arithmetic Circuits
Event details
| Date | 03.09.2024 |
| Hour | 11:00 › 12:00 |
| Speaker | Prof. Maciej Ciesielski, Department of Electrical & Computer Engineering (ECE), University of Massachusetts, Amherst |
| Location | |
| Category | Conferences - Seminars |
| Event Language | English |
Abstract
Functional verification of arithmetic circuits is a challenging problem in hardware verification. Traditional Boolean logic techniques, based on binary decision diagrams (BDDs) and Boolean satisfiability (SAT) solvers, cannot handle complex arithmetic designs as they require ``bit-blasting'', i.e., flattening of the design into bit-level netlist. Verification techniques based on symbolic computer algebra (SCA) and algebraic rewriting also faces serious challenges in complex circuits, such as dividers and modular multipliers. Furthermore, while verification concentrates on confirming whether the circuit performs its intended function, the issue of debugging, i.e., localization and correction of functional errors in the circuit, remains an open problem. This presentation briefly describes these issues and presents a method that combines formal verification and sensitizability techniques, traditionally used in testing, to enable efficient verification and debugging of integer divider circuits.
Bio
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. In 2008 he received Doctorate Honoris Causa from the Universite de Bretagne Sud, Lorient, France, for contributions to the development of EDA tools for high level synthesis. His research interest is VLSI design and electronic design automation (EDA), and specifically logic and high-level synthesis and formal verification of arithmetic circuits.
For more details please consult his web site: http://www.ecs.umass.edu/ece/labs/vlsicad/ciesielski.html
Functional verification of arithmetic circuits is a challenging problem in hardware verification. Traditional Boolean logic techniques, based on binary decision diagrams (BDDs) and Boolean satisfiability (SAT) solvers, cannot handle complex arithmetic designs as they require ``bit-blasting'', i.e., flattening of the design into bit-level netlist. Verification techniques based on symbolic computer algebra (SCA) and algebraic rewriting also faces serious challenges in complex circuits, such as dividers and modular multipliers. Furthermore, while verification concentrates on confirming whether the circuit performs its intended function, the issue of debugging, i.e., localization and correction of functional errors in the circuit, remains an open problem. This presentation briefly describes these issues and presents a method that combines formal verification and sensitizability techniques, traditionally used in testing, to enable efficient verification and debugging of integer divider circuits.
Bio
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. In 2008 he received Doctorate Honoris Causa from the Universite de Bretagne Sud, Lorient, France, for contributions to the development of EDA tools for high level synthesis. His research interest is VLSI design and electronic design automation (EDA), and specifically logic and high-level synthesis and formal verification of arithmetic circuits.
For more details please consult his web site: http://www.ecs.umass.edu/ece/labs/vlsicad/ciesielski.html
Practical information
- General public
- Free