This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Taylor Expansion Diagrams: A Canonical Representation for Verification of Data Flow Designs
September 2006 (vol. 55 no. 9)
pp. 1188-1201
A Taylor Expansion Diagram (TED) is a compact, word-level, canonical representation for data flow computations that can be expressed as multivariate polynomials. TEDs are based on a decomposition scheme using Taylor series expansion that allows one to model word-level signals as algebraic symbols. This power of abstraction, combined with the canonicity and compactness of TED, makes it applicable to equivalence verification of dataflow designs. The paper describes the theory of TEDs and proves their canonicity. It shows how to construct a TED from an HDL design specification and discusses the application of TEDs in proving the equivalence of such designs. Experiments were performed with a variety of designs to observe the potential and limitations of TEDs for dataflow design verification. Application of TEDs to algorithmic and behavioral verification is demonstrated.

[1] R.E. Bryant, “Graph Based Algorithms for Boolean Function Manipulation,” IEEE Trans. Computers, vol. 35, no. 8, pp. 677-691, Aug. 1986.
[2] R.E. Bryant and Y.-A. Chen, “Verification of Arithmetic Functions with Binary Moment Diagrams,” Proc. Design Automation Conf., pp. 535-541, 1995.
[3] Y.A. Chen and R.E. Bryant, “*PHDD: An Efficient Graph Representation for Floating Point Verification,” Proc. Int'l Conf. Computer-Aided Design (ICCAD), 1997.
[4] R. Drechsler, B. Becker, and S. Ruppertz, “The K*BMD: A Verification Data Structure,” IEEE Design and Test, pp. 51-59, 1997.
[5] P. Kalla, “An Infrastructure for RTL Validation and Verification,” PhD thesis, Dept. of Electrical and Computer Eng., Univ. of Massachusetts Amherst, 2002.
[6] M. Ciesielski, P. Kalla, Z. Zeng, and B. Rouzeyre, “Taylor Expansion Diagrams: A Compact Canonical Representation with Applications to Symbolic Verification,” Proc. Design Automation and Test in Europe (DATE-02), pp. 285-289, 2002.
[7] B. Taylor, Methodus Incrementorum Directa et Inversa, 1715.
[8] E. Kryrszig, Advanced Engineering Mathematics. John Wiley & Sons, 1999.
[9] H. Enderton, A Mathematical Introduction to Logic. New York: Academic Press, 1972.
[10] T. Bultan et al., “Verifying Systems with Integer Constraints and Boolean Predicates: A Composite Approach,” Proc. Int'l Symp. Software Testing and Analysis, 1998.
[11] S. Devadas, K. Keutzer, and A. Krishnakumar, “Design Verification and Reachability Analysis Using Algebraic Manipulation,” Proc. Int'l Conf. Computer Design, 1991.
[12] G. Ritter, “Formal Verification of Designs with Complex Control by Symbolic Simulation,” Proc. Advanced Research Working Conf. Correct Hardware Design and Verification Methods (CHARME), 1999.
[13] R.E. Shostak, “Deciding Combinations of Theories,” J. ACM, vol. 31, no. 1, pp. 1-12, 1984.
[14] A. Stump, C.W. Barrett, and D.L. Dill, “CVC: A Cooperating Validity Checker,” Proc. 14th Int'l Conf. Computer Aided Verification (CAV), E. Brinksma and K. Guldstrand Larsen, eds., pp. 500-504, 2002.
[15] M. Chandrashekhar, J.P. Privitera, and J.W. Condradt, “Application of Term Rewriting Techniques to Hardware Design Verification,” Proc. Design Automation Conf., pp. 277-282, 1987.
[16] Z. Zhou and W. Burleson, “Equivalence Checking of Datapaths Based on Canonical Arithmetic Expressions,” Proc. Design Automation Conf., 1995.
[17] S. Vasudevan, “Automatic Verification of Arithmetic Circuits in RTL Using Term Rewriting Systems,” MS thesis, Univ. of Texas, Austin, 2003.
[18] J. Burch and D. Dill, Automatic Verification of Pipelined Microprocessor Control. Springer-Verlag, 1994.
[19] R. Bryant, S. German, and M. Velev, “Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic,” ACM Trans. Computational Logic, vol. 2, no. 1, pp. 1-41, 2001.
[20] M. Velev and R. Bryant, “Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors,” J. Symbolic Computation, vol. 35, no. 2, pp. 73-106, 2003.
[21] R. Bryant, S. Lahiri, and S. Seshia, “Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions,” Proc. Int'l Conf. Computer Aided Verification (CAV), 2002.
[22] M. Moskewicz, C. Madigan, L. Zhang, Y. Zhao, and S. Malik, “Chaff: Engineering an Efficient SAT Solver,” Proc. 38th Design Automation Conf., pp. 530-535, June 2001.
[23] E. Goldberg and Y. Novikov, “BerkMin: A Fast and Robust Sat-Solver,” Proc. Design Automation and Test in Europe (DATE-02), pp.142-149, 2002.
[24] C.-Y. Huang and K.-T. Cheng, “Using Word-Level ATPG and Modular Arithmetic Constraint Solving Techniques for Assertion Property Checking,” IEEE Trans. Computer Aided Design, vol. 20, pp. 381-391, 2001.
[25] M. Iyer, “RACE: A Word-Level ATPG-Based Constraints Solver System for Smart Random Simulation,” Proc. Int'l Test Conf. (ITC-03), pp. 299-308, 2003.
[26] R. Brinkmann and R. Drechsler, “RTL-Datapath Verification Using Integer Linear Programming,” Proc. Asia and South Pacific Design Automation Conf. (ASP-DAC), 2002.
[27] Z. Zeng, P. Kalla, and M. Ciesielski, “LPSAT: A Unified Approach to RTL Satisfiability,” Proc. Design Automation and Test in Europe Conf. (DATE), pp. 398-402, Mar. 2001.
[28] F. Fallah, S. Devadas, and K. Keutzer, “Functional Vector Generation for HDL Models Using Linear Programming and 3-Satisfiability,” Proc. Design Automation Conf., pp. 528-533, 1998.
[29] K.S. Brace, R. Rudell, and R.E. Bryant, “Efficient Implementation of the BDD Package,” Proc. Design Automation Conf. (DAC), pp. 40-45, 1990.
[30] O. Coudert and J.C. Madre, “A Unified Framework for the Formal Verification of Sequential Circuits,” Proc. Int'l Conf. Computer Aided Design (ICCAD), pp. 126-129, 1990.
[31] H.J. Touati, H. Savoj, B. Lin, R.K. Brayton, and A. Sangiovanni-Vincentelli, “Implicit State Enumeration of Finite State Machines Using BDDs,” Proc. Int'l Conf. Computer Aided Design (ICCAD), pp.130-133, 1990.
[32] E.A. Emerson, “Temporal and Modal Logic,” Formal Models and Semantics, J. van Leeuwen, ed., vol. B of Handbook of Theoretical Computer Science, pp. 996-1072, Elsevier Science, 1990.
[33] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[34] R.K. Brayton, G.D. Hachtel, A. Sangiovanni-Vencentelli, F. Somenzi, A. Aziz, S-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. Ranjan, S. Sarwary, G. Shiple, S. Swamy, and T. Villa, “VIS: A System for Verification and Synthesis,” Computer Aided Verification, 1996.
[35] A. Narayan et al., “Partitioned ROBDDs: A Compact Canonical and Efficient Representation for Boolean Functions,” Proc. Int'l Conf. Computer Aided Design (ICCAD), 1996.
[36] Y-T. Lai, M. Pedram, and S.B. Vrudhula, “FGILP: An ILP Solver Based on Function Graphs,” Proc. Int'l Conf. Computer Aided Design (ICCAD), pp. 685-689, 1993.
[37] U. Kebschull, E. Schubert, and W. Rosentiel, “Multilevel Logic Synthesis Based on Functional Decision Diagrams,” Proc. European Design Automation Conf. (EDAC), pp. 43-47, 1992.
[38] R. Drechsler, A. Sarabi, M. Theobald, B. Becker, and M.A. Perkowski, “Efficient Representation and Manipulation of Switching Functions Based on Order Kronecker Function Decision Diagrams,” Proc. Design Automation Conf. (DAC), pp. 415-419, 1994.
[39] E.M. Clarke, K.L. McMillan, X. Zhao, M. Fujita, and J. Yang, “Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping,” Proc. Design Automation Conf. (DAC), pp. 54-60, 1993.
[40] I. Bahar, E.A. Frohm, C.M. Gaona, G.D. Hachtel, E. Macii, A. Pardo, and F. Somenzi, “Algebraic Decision Diagrams and Their Applications,” Proc. Int'l Conf. Computer Aided Design (ICCAD), pp.188-191, Nov. 1993.
[41] S. Horeth and R. Drechsler, “Formal Verification of Word-Level Specifications,” Proc. Design Automation and Test in Europe (DATE), pp. 52-58, 1999.
[42] Y.-A. Chen and R. Bryant, “PHDD: An Efficient Graph Representation for Floating Point Circuit Verification,” Proc. IEEE Int'l Conf. Computer-Aided Design, pp. 2-7, 1997.
[43] G. Bioul and M. Davio, “Taylor Expansion of Boolean Functions and of Their Derivatives,” Philips Research Reports, vol. 27, no. 1, pp. 1-6, 1972.
[44] A. Thayse and M. Davio, “Boolean Differential Calculus and Its Application to Switching Theory,” IEEE Trans. Computers, vol. 22, no. 4, pp. 409-420, Apr. 1973.
[45] J. Smith and G. DeMicheli, “Polynomial Methods for Compontent Matching and Verification,” Proc. Int'l Conf. Computer-Aided Design (ICCAD '98), 1998.
[46] J. Smith and G. DeMicheli, “Polynomial Methods for Allocating Complex Compontents,” Proc. Design Automation and Test in Europe Conf. (DATE '99), 1999.
[47] A. Peymandoust and G. DeMicheli, “Application of Symbolic Computer Algebra in High-Level Data-Flow Synthesis,” IEEE Trans. Computer-Aided Design, vol. 22, no. 9, pp. 1154-1165, Sept. 2003.
[48] Maple, http:/www.maplesoft.com, 2006.
[49] Mathematica, http:/www.wri.com, 2006.
[50] The MathWorks, “Matlab,” http:/www.mathworks.com, 2006.
[51] F. Winkler, Polynomial Algorithms in Computer Algebra. Springer, 1996.
[52] G. Fey, R. Drechsler, and M. Ciesielski, “Algorithms for Taylor Expansion Diagrams,” Proc. IEEE Int'l Symp. Multi-Valued Logic (ISMVL '04), 2004.
[53] F. Brown, Boolean Reasoning. Kluwer Academic, 1990.
[54] D. Pradhan, S. Askar, and M. Ciesielski, “Mathematical Framework for Representing Discrete Functions as Word-Level Polynomials,” Proc. IEEE Int'l High Level Design Validation and Test Workshop (HLDVT-03), pp. 135-139, 2003.
[55] LESTER, Université de Bretagne Sud, “GAUT, Architectural Synthesis Tool,” http:/lester.univ-ubs.fr:8080, 2004.
[56] F. Somenzi, “Colorado Decision Diagram Package,” computer program, 1997.
[57] R. Rudell, “Dynamic Variable Ordering for Binary Decision Diagrams,” Proc. Int'l Conf. Computer-Aided Design, pp. 42-47, Nov. 1993.
[58] D. Gomez-Prado, Q. Ren, S. Askar, M. Ciesielski, and E. Boutillon, “Variable Ordering for Taylor Expansion Diagrams,” Proc. IEEE Int'l High Level Design Validation and Test Workshop (HLDVT-04), pp. 55-59, 2004.
[59] P. Jain, “Parameterized Motion Estimation Architecture for Dynamically Varying Power and Compression Requirements,” MS thesis, Dept. of Electrical and Computer Eng., Univ. of Massachusetts, 2002.
[60] M. Ciesielski, S. Askar, E. Boutillon, and J. Guillot, “Behavioral Transformations for Hardware Synthesis and Code Optimization Based on Taylor Expansion Diagrams,” Dec. 2005, Patents pending, USSN 11/292,493 and PCT/US05/43860.
[61] J. Guillot, E. Boutillon, D. Gomez-Prado, S. Askar, Q. Ren, and M. Ciesielski, “Efficient Factorization of DSP Transforms Using Taylor Expansion Diagrams,” Proc. Design Automation and Test in Europe Conf. (DATE-06), 2006.
[62] M. Ciesielski, S. Askar, D. Gomez-Prado, and Q. Ren, “TEDify— Software for Construction and Optimization of TEDs, with Application to Verification and Synthesis of Behavioral Designs,” http://tango.ecs.umass.edu/TED/Dochtml, 2006.

Index Terms:
Register transfer level—design aids, verification; arithmetic and logic structures—verification; symbolic and algebraic manipulation.
Citation:
Maciej Ciesielski, Priyank Kalla, Serkan Askar, "Taylor Expansion Diagrams: A Canonical Representation for Verification of Data Flow Designs," IEEE Transactions on Computers, vol. 55, no. 9, pp. 1188-1201, Sept. 2006, doi:10.1109/TC.2006.153
Usage of this product signifies your acceptance of the Terms of Use.