Self-referential verification of gate-level implementations of arithmetic circuits

ABSTRACT

Verification of gate-level implementations of arithmetic circuits is challenging due to a number of reasons: the existence of some hard-to-verify arithmetic operators (e.g. multiplication), the use of different operand ordering, the incorporation of merged arithmetic with cross-operator implementations, and the employment of circuit transformations based on arithmetic relations. It is hence a peculiar problem that does not fit quite well into the existing RTL-to-gate equivalence checking methodology. In this paper, we propose a self-referential functional verification approach which uses the gate-level implementation of the arithmetic circuit under verification to verify itself. Specifically, the verification task is decomposed into a sequence of equivalence checking subproblems, each of which compare circuit pairs derived from the implementation under verification based on the proposed self-referential functional equations. A decomposition-based heuristic using structural information is employed to guide the verification process for better efficiency. Experimental results on a number of implementations of the multiply-add units and the inner product units with different architectures demonstrate the versatility of this approach.

References

1. Special issue on verification of arithmetic hardware. Formal Methods in System Design, 14(1), 1999.
2. D. Brand. Verification of large synthesized designs. In Proceedings of the International Conference on Computer-Aided Design (ICCAD), pages 534--537, November 1993.
3. R. K. Brayton. The future of logic synthesis and verification. In Logic Synthesis and Verification, pages 403--434. Kluwer Academic Publishers, 2002.
4. R. E. Bryant. Graph-based algorithm for boolean function manipulation. IEEE Trans. on Computers, C-35(8):677--691, 1986.
5. R. E. Bryant. On the complexity of VLSI implementations and graph representations of boolean functions with application to integer multiplication. IEEE Trans. on Computers, 40(2):205--213, 1991.
6. R. E. Bryant and Y. A. Chen. Verification of arithmetic circuits with binary moment diagrams.In Proceedings of the 32nd ACM/IEEE Design Automation Conference (DAC), pages 535--541, 1995.
7. Y.-T. Chang and K.-T. Cheng. Induction-based gate-level verification of multipliers. In Proceedings of International Conference on Computer-Aided Design (ICCAD), pages 190--193, November 2001.
8. M. Fujita. Verification of arithmetic circuits by comparing two similar circuits. In Proceedings of the 8th International Conference on Computer Aided Verification (CAV), pages 159--168, 1996.
9. K. Hamaguchi, A. Morita, and S. Yajma. Efficient construction of binary moment diagrams for verifying arithmetic circuits. In Proceedings of International Conference on Computer-Aided Design (ICCAD), pages 78--82, November 1995.
10. T. Kim, W. Jao, and S. Tjiang. Arithmetic optimization using carry-save adders. In Proceedings of the 35th ACM/IEEE Design Automation Conference (DAC), pages 433--438, 1998.
11. S. Kimura. Residue BDD and its application to the verification of arithmetic circuits. In Proceedings of the 32nd ACM/IEEE Design Automation Conference (DAC), pages 542--545, 1995.
12. A. Migdall. Correlated-photon metrology without absolute standards. Physics Today, 52(1):41--46, 1999.
13. B. Parhami. Computer Arithmetic: Algorithms and Hardware Designs. Oxford University Press, 1999.
14. M. Potkonjak and J. Rabaey. Optimizing resource utilization using transformations. IEEE Trans. on CAD, 13(3):277--292, 1994.
15. F. Somenzi. CUDD: CU decision diagram package Release 2.3.1. University of Colorado at Boulder, 2001.
16. T. Stanion. Implicit verification of structurally dissimilar arithmetic circuits. In Proceedings of IEEE International Conference on Computer Design (ICCD), pages 46--50, 1999.
17. E. E. J. Swartzlander. Merged arithmetic. IEEE Transactions on Computers, 29(10):946--950, 1980.
18. J. Um, T. Kim, and C.-L. Liu. Optimal allocation of carry-save-adders in arithmetic optimization. In Proceedings of International Conference on Computer Aided Design (ICCAD), pages 410--413, November 1999.
19. Z. Zhou and W. Burleson. Equivalence checking of datapaths based on canonical arithmetic expressions. In Proceedings of the 32nd ACM/IEEE Design Automation Conference (DAC), pages 546--551, 1998.

Index Terms

• Hardware

  • Hardware validation

    • Functional verification