Functional Verification of Integer Arithmetic Circuits: an Algebraic Approach
Event details
| Date | 15.04.2015 |
| Hour | 14:00 › 15:00 |
| Speaker |
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. 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. For more details please consult his web site: http://www.ecs.umass.edu/ece/labs/vlsicad/ciesielski.html |
| Location | |
| Category | Conferences - Seminars |
Abstract:
Functional verification of arithmetic circuits and data paths remains a challenging problem in hardware verification. Boolean logic techniques based on binary decision diagrams (BDDs) and satisfiability (SAT) solvers, cannot handle complex arithmetic designs as they require ``bit-blasting'', i.e., flattening of the design into bit-level netlists. Approaches that rely on computer algebra and Satisfiability 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 significant human interaction and intimate knowledge of the design to guide the proof process.
This talk presents a fundamentally different approach to functional verification of integer arithmetic circuits. It is based on a network flow model, where the computation performed by the circuit is viewed as a flow of binary data through the circuit. The symbolic expression representing the data at the circuit inputs is transformed into a polynomial expression at the primary outputs. For the circuit to be functionally correct, the resulting expression must match the binary encoding at the primary outputs. The procedure conducted in the opposite direction (from the primary outputs to the primary inputs) will extract the arithmetic function implemented by the circuit. Different transformation techniques will be discussed, depending on the type of circuit implementations (structured adder networks vs. purely gate-level circuits). We show that this technique can verify large arithmetic circuits up to 512-bit multipliers with over 2 million gates.
Functional verification of arithmetic circuits and data paths remains a challenging problem in hardware verification. Boolean logic techniques based on binary decision diagrams (BDDs) and satisfiability (SAT) solvers, cannot handle complex arithmetic designs as they require ``bit-blasting'', i.e., flattening of the design into bit-level netlists. Approaches that rely on computer algebra and Satisfiability 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 significant human interaction and intimate knowledge of the design to guide the proof process.
This talk presents a fundamentally different approach to functional verification of integer arithmetic circuits. It is based on a network flow model, where the computation performed by the circuit is viewed as a flow of binary data through the circuit. The symbolic expression representing the data at the circuit inputs is transformed into a polynomial expression at the primary outputs. For the circuit to be functionally correct, the resulting expression must match the binary encoding at the primary outputs. The procedure conducted in the opposite direction (from the primary outputs to the primary inputs) will extract the arithmetic function implemented by the circuit. Different transformation techniques will be discussed, depending on the type of circuit implementations (structured adder networks vs. purely gate-level circuits). We show that this technique can verify large arithmetic circuits up to 512-bit multipliers with over 2 million gates.
Practical information
- General public
- Free
Organizer
- EE Institute, Prof. Giovanni De Micheli