This Article 
 Bibliographic References 
 Add to: 
Automatic Verification of Arithmetic Circuits in RTL Using Stepwise Refinement of Term Rewriting Systems
October 2007 (vol. 56 no. 10)
pp. 1401-1414
This paper presents a novel technique for proving the correctness of arithmetic circuit designs described at the Register Transfer Level (RTL). The technique begins with the automatic translation of circuits from a Verilog RTL description into a Term Rewriting System (TRS). We prove the correctness of the designs via an equivalence proof between TRSs for the implementation circuit design and a much simpler specification circuit design. We present this notion of equivalence between the TRSs and a stepwise refinement method for its decomposition, which we leverage in our tool Verifire. We demonstrate the effectiveness of our technique by using the tool for the verification of several multiplier designs that have hitherto been impossible to verify with existing approaches and tools.

[1] D. Anastasakis, L. McIlwain, and S. Pilarski, “Efficient Equivalence Checking with Partitions and Hierarchical Cut-Points,” Proc. 41st Ann. Conf. Design Automation (DAC '04), pp. 539-542, 2004.
[2] S. Antoy and J. Gannon, “Using Term Rewriting to Verify Software,” IEEE Trans. Software Eng., vol. 20, no. 4, pp. 259-274, Apr. 1994.
[3] T. Arts and J. Giesl, “Applying Rewriting Techniques to the Verification of Erlang Processes,” Proc. 13th Int'l Workshop Computer Science Logic (CSL '99), pp. 96-110, 1999.
[4] C.W. Barrett, D.L. Dill, and J.R. Levitt, “A Decision Procedure for Bit-Vector Arithmetic,” Proc. 35th Ann. Conf. Design Automation (DAC '98), pp. 522-527, 1998.
[5] A.D. Booth, “A Signed Binary Multiplication Technique,” J.Mechanics and Applied Math., pp. 236-240, 1951.
[6] R.E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Trans. Computers, vol. 35, no. 8, pp. 677-691, Aug. 1986.
[7] R.E. Bryant, “On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication,” IEEE Trans. Computers, vol. 40, no. 2, pp.205-213, Feb. 1991.
[8] R.E. Bryant and Y.-A. Chen, “Verification of Arithmetic Circuits with Binary Moment Diagrams,” Proc. 32nd Conf. Design Automation (DAC '95), pp. 535-541, 1995.
[9] J.R. Burch, “Using BDDS to Verify Multipliers,” Proc. 28th Conf. ACM/IEEE Design Automation Conf., pp. 408-412, 1991.
[10] M.S. Chandrasekhar, J.P. Privitera, and K.W. Conradt, “Application of Term Rewriting Techniques to Hardware Design Verification,” Proc. 24th ACM/IEEE Design Automation Conf., pp. 277-282, 1987.
[11] J.-C. Chen and Y.-A. Chen, “Equivalence Checking of Integer Multipliers,” Proc. Asia and South Pacific Design Automation Conf. (ASP-DAC '01), pp. 169-174, 2001.
[12] Y.-A. Chen and R.E. Bryant, “PHDD: An Efficient Graph Representation for Floating Point Circuit Verification,” Proc. IEEE/ACM Int'l Conf. Computer-Aided Design (ICCAD '97), pp. 2-7, 1997.
[13] E.M. Clarke, M. Fujita, and X. Zhao, “Hybrid Decision Diagrams,” Proc. IEEE/ACM Int'l Conf. Computer-Aided Design (ICCAD '95), pp.159-163, 1995.
[14] D. Cyrluk, “Microprocessor Verification in PVS: A Methodology and Simple Example,” Technical Report SRI-CSL-93-12, Menlo Park, Calif., 1993.
[15] D. Cyrluk, S. Rajan, N. Shankar, and M.K. Srivas, “Effective Theorem Proving for Hardware Verification,” Proc. Second Int'l Conf. Theorem Provers in Circuit Design, Theory, Practice, and Experience, pp. 203-222, 1994.
[16] D.M. Russinoff, “A Mechanically Checked Proof of IEEE Compliance of a Register-Transfer-Level Specification of the AMD-K7 Floating-Point Multiplication, Division, and Square Root Instructions,” LMS J. Computation and Math., vol. 1, pp. 148-200, Dec. 1998.
[17] S.J. Garland, J.V. Guttag, and J.A. Staunstrup, “Verification of VLSI Circuits Using LP,” Proc. IFIP WG 10.2 Working Conf.: The Fusion of Hardware Design and Verification, pp. 329-345, July 1988.
[18] T. Genet and F. Klay, “Rewriting for Cryptographic Protocol Verification,” Proc. 17th Int'l Conf. Automated Deduction (CADE '00), pp. 271-290, 2000.
[19] H. Anderson, P. Williams, and H. Hulgaard, “Equivalence Checking of Combinational Circuits Using Boolean Expression Diagrams,” IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 18, no. 7, 1999.
[20] N. Harman, “Correctness and Verification of Hardware Systems Using Maude,” technical report, Univ. of Wales, Swansea, 2000.
[21] J. Hoe and Arvind, “Hardware Synthesis from Term Rewriting Systems,” Proc. X IFIP Int'l Conf. VLSI (VLSI '99), Nov. 1999.
[22] J.R. Burch, E.M. Clarke, D.E. Long, K.L. MacMillan, and D.L. Dill, “Symbolic Model Checking for Sequential Circuit Verification,” IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 13, no. 4, pp. 401-424, 1994.
[23] D. Kapur, “Theorem Proving Support for Hardware Verification,” Proc. Third Int'l Workshop First-Order Theorem Proving (FTP '00), July 2000.
[24] D. Kapur and H. Zhang, “An Overview of Rewrite Rule Laboratory (RRL),” J. Computer and Math. with Applications, vol. 29, no. 2, pp. 91-114, 1995.
[25] M. Kaufmann and J. Moore, “ACL2: An Industrial Strength Version of NQTHM,” Proc. 11th Ann. Conf. Computer Assurance (COMPASS '96), p. 23, 1996.
[26] J. Klop, “Term Rewriting Systems,” Handbook of Logic in Computer Science, S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, eds., vol.2, pp. 1-116. Oxford Univ. Press, 1992.
[27] M. Kaufmann and D. Russinoff, “Verification of Pipeline Circuits,” Proc. ACL2 Workshop 2000, Technical Report TR-00-29, Dept. of Computer Sciences, Univ. of Texas at Austin, Oct. 2000.
[28] Z. Manna, N. Bjorner, A. Browne, E.Y. Chang, M. Colon, L. de Alfaro, H. Devarajan, A. Kapur, J. Lee, H. Sipma, and T.E. Uribe, “Step: The Stanford Temporal Prover,” Proc. Sixth Int'l Joint Conf. CAAP/FASE Theory and Practice of Software Development (TAPSOFT '95), pp. 793-794, 1995.
[29] Y. Matsunaga, “An Efficient Equivalence Checker for Combinational Circuits,” Proc. 33rd Conf. Design Automation (DAC '96), pp.629-634, 1996.
[30] M. Mutz, “Using the HOL Prove Assistant for Proving the Correctness of Term Rewriting Rules Reducing Terms of Sequential Behavior,” Proc. Third Int'l Workshop Computer Aided Verification (CAV '91), pp. 277-287, 1991.
[31] R. Boulton, A. Gordon, M.J.C. Gordon, J. Herbert, and J. van Tassel, “Experience with Embedding Hardware Description Languages in HOL,” Proc. Int'l Conf. Theorem Provers in Circuit Design: Theory, Practice, and Experience, pp. 129-156, 1992.
[32] J. Sawada and W.A. Hunt, “Processor Verification with Precise Exceptions and Speculative Execution,” Proc. 10th Int'l Computer Aided Verification Conf. (CAV '98), pp. 135-146, 1998.
[33] J.B. Saxe, S.J. Garland, J.V. Guttag, and J.J. Horning, “Using Transformations and Verification in Circuit Design,” Proc. Int'l Workshop Designing Correct Circuits, J. Staunstrup and R. Sharp, eds., 1992.
[34] R. Sharp and O. Rasmussen, “Rewriting with Constraints in T-Ruby,” Proc. IFIP WG 10.5 Advanced Research Working Conf. Correct Hardware Design and Verification Methods, pp. 226-241, 1993.
[35] X. Shen, “Design and Verification of Speculative Processors,” Proc. Workshop Formal Techniques for Hardware and Hardware-Like Systems, June 1998.
[36] N. Takagi, H. Yasuura, and S. Yajima, “High-Speed VLSI Multiplication Algorithm with a Redundant Binary Addition Tree,” IEEE Trans. Computers, vol. 34, no. 9, pp. 789-796, Sept. 1985.
[37] P.F. Williams, A. Biere, E.M. Clarke, and A. Gupta, “Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking,” Proc. 12th Int'l Conf. Computer Aided Verification (CAV '00), pp. 124-138, 2000.
[38] H. Yu and J.A. Abraham, “An Efficient 3-Bit-Scan Multiplier without Overlapping Bits, and Its $64\times64$ Bit Implementation,” Proc. Seventh Asia and South Pacific Design Automation Conf. (ASP-DAC '02), Jan. 2002.
[39] Z. Zhou, X. Song, F. Corella, E. Cerny, and M. Langevin, “Description and Verification of RTL Designs Using Multiway Decision Graphs,” Proc. IFIP Conf. Hardware Description Languages and Their Applications (CHDL '95), 1995.
[40] Z. Zhou and W. Burleson, “Equivalence Checking of Datapaths Based on Canonical Arithmetic Expressions,” Proc. 32nd ACM/IEEE Conf. Design Automation (DAC '95), pp. 546-551, 1995.

Index Terms:
Verification, Hardware Description Languages, Register Transfer Level implementation, arithmetic logic unit.
Shobha Vasudevan, Vinod Viswanath, Robert W. Sumners, Jacob A. Abraham, "Automatic Verification of Arithmetic Circuits in RTL Using Stepwise Refinement of Term Rewriting Systems," IEEE Transactions on Computers, vol. 56, no. 10, pp. 1401-1414, Oct. 2007, doi:10.1109/TC.2007.1073
Usage of this product signifies your acceptance of the Terms of Use.