
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
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. 14011414, October, 2007.  
BibTex  x  
@article{ 10.1109/TC.2007.1073, author = {Shobha Vasudevan and Vinod Viswanath and Robert W. Sumners and Jacob A. Abraham}, title = {Automatic Verification of Arithmetic Circuits in RTL Using Stepwise Refinement of Term Rewriting Systems}, journal ={IEEE Transactions on Computers}, volume = {56}, number = {10}, issn = {00189340}, year = {2007}, pages = {14011414}, doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2007.1073}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Automatic Verification of Arithmetic Circuits in RTL Using Stepwise Refinement of Term Rewriting Systems IS  10 SN  00189340 SP1401 EP1414 EPD  14011414 A1  Shobha Vasudevan, A1  Vinod Viswanath, A1  Robert W. Sumners, A1  Jacob A. Abraham, PY  2007 KW  Verification KW  Hardware Description Languages KW  Register Transfer Level implementation KW  arithmetic logic unit. VL  56 JA  IEEE Transactions on Computers ER   
[1] D. Anastasakis, L. McIlwain, and S. Pilarski, “Efficient Equivalence Checking with Partitions and Hierarchical CutPoints,” Proc. 41st Ann. Conf. Design Automation (DAC '04), pp. 539542, 2004.
[2] S. Antoy and J. Gannon, “Using Term Rewriting to Verify Software,” IEEE Trans. Software Eng., vol. 20, no. 4, pp. 259274, 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. 96110, 1999.
[4] C.W. Barrett, D.L. Dill, and J.R. Levitt, “A Decision Procedure for BitVector Arithmetic,” Proc. 35th Ann. Conf. Design Automation (DAC '98), pp. 522527, 1998.
[5] A.D. Booth, “A Signed Binary Multiplication Technique,” J.Mechanics and Applied Math., pp. 236240, 1951.
[6] R.E. Bryant, “GraphBased Algorithms for Boolean Function Manipulation,” IEEE Trans. Computers, vol. 35, no. 8, pp. 677691, 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.205213, 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. 535541, 1995.
[9] J.R. Burch, “Using BDDS to Verify Multipliers,” Proc. 28th Conf. ACM/IEEE Design Automation Conf., pp. 408412, 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. 277282, 1987.
[11] J.C. Chen and Y.A. Chen, “Equivalence Checking of Integer Multipliers,” Proc. Asia and South Pacific Design Automation Conf. (ASPDAC '01), pp. 169174, 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. ComputerAided Design (ICCAD '97), pp. 27, 1997.
[13] E.M. Clarke, M. Fujita, and X. Zhao, “Hybrid Decision Diagrams,” Proc. IEEE/ACM Int'l Conf. ComputerAided Design (ICCAD '95), pp.159163, 1995.
[14] D. Cyrluk, “Microprocessor Verification in PVS: A Methodology and Simple Example,” Technical Report SRICSL9312, 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. 203222, 1994.
[16] D.M. Russinoff, “A Mechanically Checked Proof of IEEE Compliance of a RegisterTransferLevel Specification of the AMDK7 FloatingPoint Multiplication, Division, and Square Root Instructions,” LMS J. Computation and Math., vol. 1, pp. 148200, 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. 329345, July 1988.
[18] T. Genet and F. Klay, “Rewriting for Cryptographic Protocol Verification,” Proc. 17th Int'l Conf. Automated Deduction (CADE '00), pp. 271290, 2000.
[19] H. Anderson, P. Williams, and H. Hulgaard, “Equivalence Checking of Combinational Circuits Using Boolean Expression Diagrams,” IEEE Trans. ComputerAided 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. ComputerAided Design of Integrated Circuits and Systems, vol. 13, no. 4, pp. 401424, 1994.
[23] D. Kapur, “Theorem Proving Support for Hardware Verification,” Proc. Third Int'l Workshop FirstOrder 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. 91114, 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. 1116. Oxford Univ. Press, 1992.
[27] M. Kaufmann and D. Russinoff, “Verification of Pipeline Circuits,” Proc. ACL2 Workshop 2000, Technical Report TR0029, 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. 793794, 1995.
[29] Y. Matsunaga, “An Efficient Equivalence Checker for Combinational Circuits,” Proc. 33rd Conf. Design Automation (DAC '96), pp.629634, 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. 277287, 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. 129156, 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. 135146, 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 TRuby,” Proc. IFIP WG 10.5 Advanced Research Working Conf. Correct Hardware Design and Verification Methods, pp. 226241, 1993.
[35] X. Shen, “Design and Verification of Speculative Processors,” Proc. Workshop Formal Techniques for Hardware and HardwareLike Systems, June 1998.
[36] N. Takagi, H. Yasuura, and S. Yajima, “HighSpeed VLSI Multiplication Algorithm with a Redundant Binary Addition Tree,” IEEE Trans. Computers, vol. 34, no. 9, pp. 789796, 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. 124138, 2000.
[38] H. Yu and J.A. Abraham, “An Efficient 3BitScan Multiplier without Overlapping Bits, and Its $64\times64$ Bit Implementation,” Proc. Seventh Asia and South Pacific Design Automation Conf. (ASPDAC '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. 546551, 1995.