Long internship: verification of multipliers
Material from my long internship at Chalmers University of Technology (2002) on the formal verification of multiplier circuits with binary moment diagrams:
- the internship report (in French);
- the mulverif program;
- the slides of the talks given at ENS in May 2002 and December 2002;
- the annotated bibliography below, as compiled in 2003.
Papers on multiplier verification
-
Randal E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation”, IEEE Transactions on Computers, C-35(8):677-691, August 1986
For any ordering of the variables, some multiplier output has a BDD representation of an exponential size. BibTeX entry -
Randal E. Bryant and Yirng-An Chen, “Verification of Arithmetic Circuits with Binary Moment Diagrams”, Design Automation Conference, pp. 535-541, 1995
Component-level Verification : show that components (e.g., adders) are correct by comparing the *BMDs of their bit-level and word-level representations (with the necessary encodings). Experimental results : 30 min for standard 256 bits multipliers. BibTeX entry -
K. Hamaguchi, A. Morita and S. Yajima, “Efficient Construction of Binary Moment Diagrams for Verifying Arithmetic Circuits”, Proc. Int'l Conf. on CAD, pp. 78-82, 1995
Backward sweeping method for using *BMDs. Does not require any high-level information, therefore automatically usable. Experimental results : 1 min for a 16 bits multiplier. Asymptotic behavior for multipliers : O(n3.5). BibTeX entry -
D. Kapur and M. Subramaniam, “Mechanically verifying a Family of multiplier Circuits”, Proceedings of the 8th International Conference on Computer Aided Verification CAV, 1102:135-146, 1996
Proof of the correctness of a generic family of multipliers (with partial sum computation and partial sum addition components). Hand-made lemmas, only speculated to be automatically generated. BibTeX entry -
Martin Keim, Michael Martin, Bernd Becker, Rolf Drechsler and Paul Molitor, “Polynomial Formal Verification of Multipliers”, VLSI Test Symposium, Monterey, USA, 1997
Asymptotic O(n4) bound on the time of backward sweeping methods for Wallace-tree-like multipliers. Also a fixed bound (not asymptotic) on the size of corresponding *BMDs, which may be used to disprove the correctness of some multipliers. BibTeX entry -
Mary Sheeran and Anne Borälv, "How to Prove Properties of Recursively Defined Circuits Using Stålmarck's Method", Informal Proceedings Workshop on Formal Techniques for Hardware a nd Hardware-Like Systems, FHT'98, Marstrand, Sweden, june 1998
Use of n inductive steps to prove a n-bit multiplier. The structure of the circuit has to be known. Use of Stålmarck's method. BibTeX entry -
Ted Stanion, "Implicit Verification of Structurally Dissimilar Arithmetic Circuits", Proceedings of the 1999 IEEE International Conference on Computer Design (ICCD), pp.46-50, 1999
BibTeX entry -
Sandro Wefel and Paul Molitor, “Prove that a faulty multiplier is faulty!?”, Proceedings on the 10th GLS-VLSI, pp. 43-46, 2000
No answer to the question. Backward sweeping method can be (and is) be exponentially long on faulty multipliers. On Wallace-tree-like multipliers, Keim and al's results can be used. BibTeX entry -
Ying-Tsai Chang and Kwang-Ting Cheng, “Induction-based Gate-Level Verification of Multipliers”, Proc. Int'l Conf. on CAD, 2001
Use of n inductive steps to prove a n-bit multiplier. Heuristic methods to make the difference between multiplier and multiplicand. Inductive steps proofs use a BDD approach. Several hours to prove a standard 128 bit multiplier. BibTeX entry