
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
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. 11881201, September, 2006.  
BibTex  x  
@article{ 10.1109/TC.2006.153, author = {Maciej Ciesielski and Priyank Kalla and Serkan Askar}, title = {Taylor Expansion Diagrams: A Canonical Representation for Verification of Data Flow Designs}, journal ={IEEE Transactions on Computers}, volume = {55}, number = {9}, issn = {00189340}, year = {2006}, pages = {11881201}, doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2006.153}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Taylor Expansion Diagrams: A Canonical Representation for Verification of Data Flow Designs IS  9 SN  00189340 SP1188 EP1201 EPD  11881201 A1  Maciej Ciesielski, A1  Priyank Kalla, A1  Serkan Askar, PY  2006 KW  Register transfer level—design aids KW  verification; arithmetic and logic structures—verification; symbolic and algebraic manipulation. VL  55 JA  IEEE Transactions on Computers ER   
[1] R.E. Bryant, “Graph Based Algorithms for Boolean Function Manipulation,” IEEE Trans. Computers, vol. 35, no. 8, pp. 677691, Aug. 1986.
[2] R.E. Bryant and Y.A. Chen, “Verification of Arithmetic Functions with Binary Moment Diagrams,” Proc. Design Automation Conf., pp. 535541, 1995.
[3] Y.A. Chen and R.E. Bryant, “*PHDD: An Efficient Graph Representation for Floating Point Verification,” Proc. Int'l Conf. ComputerAided Design (ICCAD), 1997.
[4] R. Drechsler, B. Becker, and S. Ruppertz, “The K*BMD: A Verification Data Structure,” IEEE Design and Test, pp. 5159, 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 (DATE02), pp. 285289, 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. 112, 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. 500504, 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. 277282, 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. SpringerVerlag, 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. 141, 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. 73106, 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. 530535, June 2001.
[23] E. Goldberg and Y. Novikov, “BerkMin: A Fast and Robust SatSolver,” Proc. Design Automation and Test in Europe (DATE02), pp.142149, 2002.
[24] C.Y. Huang and K.T. Cheng, “Using WordLevel ATPG and Modular Arithmetic Constraint Solving Techniques for Assertion Property Checking,” IEEE Trans. Computer Aided Design, vol. 20, pp. 381391, 2001.
[25] M. Iyer, “RACE: A WordLevel ATPGBased Constraints Solver System for Smart Random Simulation,” Proc. Int'l Test Conf. (ITC03), pp. 299308, 2003.
[26] R. Brinkmann and R. Drechsler, “RTLDatapath Verification Using Integer Linear Programming,” Proc. Asia and South Pacific Design Automation Conf. (ASPDAC), 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. 398402, Mar. 2001.
[28] F. Fallah, S. Devadas, and K. Keutzer, “Functional Vector Generation for HDL Models Using Linear Programming and 3Satisfiability,” Proc. Design Automation Conf., pp. 528533, 1998.
[29] K.S. Brace, R. Rudell, and R.E. Bryant, “Efficient Implementation of the BDD Package,” Proc. Design Automation Conf. (DAC), pp. 4045, 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. 126129, 1990.
[31] H.J. Touati, H. Savoj, B. Lin, R.K. Brayton, and A. SangiovanniVincentelli, “Implicit State Enumeration of Finite State Machines Using BDDs,” Proc. Int'l Conf. Computer Aided Design (ICCAD), pp.130133, 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. 9961072, Elsevier Science, 1990.
[33] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[34] R.K. Brayton, G.D. Hachtel, A. SangiovanniVencentelli, F. Somenzi, A. Aziz, ST. 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] YT. Lai, M. Pedram, and S.B. Vrudhula, “FGILP: An ILP Solver Based on Function Graphs,” Proc. Int'l Conf. Computer Aided Design (ICCAD), pp. 685689, 1993.
[37] U. Kebschull, E. Schubert, and W. Rosentiel, “Multilevel Logic Synthesis Based on Functional Decision Diagrams,” Proc. European Design Automation Conf. (EDAC), pp. 4347, 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. 415419, 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. 5460, 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.188191, Nov. 1993.
[41] S. Horeth and R. Drechsler, “Formal Verification of WordLevel Specifications,” Proc. Design Automation and Test in Europe (DATE), pp. 5258, 1999.
[42] Y.A. Chen and R. Bryant, “PHDD: An Efficient Graph Representation for Floating Point Circuit Verification,” Proc. IEEE Int'l Conf. ComputerAided Design, pp. 27, 1997.
[43] G. Bioul and M. Davio, “Taylor Expansion of Boolean Functions and of Their Derivatives,” Philips Research Reports, vol. 27, no. 1, pp. 16, 1972.
[44] A. Thayse and M. Davio, “Boolean Differential Calculus and Its Application to Switching Theory,” IEEE Trans. Computers, vol. 22, no. 4, pp. 409420, Apr. 1973.
[45] J. Smith and G. DeMicheli, “Polynomial Methods for Compontent Matching and Verification,” Proc. Int'l Conf. ComputerAided 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 HighLevel DataFlow Synthesis,” IEEE Trans. ComputerAided Design, vol. 22, no. 9, pp. 11541165, 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. MultiValued 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 WordLevel Polynomials,” Proc. IEEE Int'l High Level Design Validation and Test Workshop (HLDVT03), pp. 135139, 2003.
[55] LESTER, Université de Bretagne Sud, “GAUT, Architectural Synthesis Tool,” http:/lester.univubs.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. ComputerAided Design, pp. 4247, Nov. 1993.
[58] D. GomezPrado, 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 (HLDVT04), pp. 5559, 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. GomezPrado, S. Askar, Q. Ren, and M. Ciesielski, “Efficient Factorization of DSP Transforms Using Taylor Expansion Diagrams,” Proc. Design Automation and Test in Europe Conf. (DATE06), 2006.
[62] M. Ciesielski, S. Askar, D. GomezPrado, 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.