Taylor expansion diagrams: A canonical representation for verification of data flow designs

被引：31
|
作者：
Ciesielski, Maciej [1 ]
Kalla, Priyank
Askar, Serkan
机构：
[1] Univ Massachusetts, Dept Elect & Comp Engn, Amherst, MA 01003 USA
[2] Univ Utah, Dept Elect & Comp Engn, Salt Lake City, UT 84112 USA
来源：
IEEE TRANSACTIONS ON COMPUTERS | 2006年 / 55卷 / 09期
基金：
美国国家科学基金会;
关键词：
register transfer level-design aids; verification; arithmetic and logic structures-verification; symbolic and algebraic manipulation;
D O I：
10.1109/TC.2006.153
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
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.
引用
收藏
页码：1188 / 1201
页数：14
相关论文
共 50 条
  • [1] Taylor Expansion Diagrams: A compact, canonical representation with applications to symbolic verification
    Ciesielski, MJ
    Kalla, P
    Zeng, ZH
    Rouzeyre, B
    DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, 2002 PROCEEDINGS, 2002, : 285 - 289
  • [2] Taylor Expansion Diagrams: A new representation for RTL verification
    Ciesielski, M
    Kalla, P
    Zeng, ZH
    Rouzeyre, B
    SIXTH IEEE INTERNATIONAL HIGH-LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS, 2001, : 70 - 75
  • [3] Data-flow transformations using Taylor expansion diagrams
    Ciesielski, M.
    Askar, S.
    Gomez-Prado, D.
    Guillot, J.
    Boutillon, E.
    2007 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION, VOLS 1-3, 2007, : 455 - +
  • [4] Binary Taylor Diagrams: An efficient implementation of Taylor expansion Diagrams
    Hooshmand, A. (arash@cad.ece.ut.ac.ir), Circuits and Systems Society, IEEE CASS; Science Council of Japan; The Inst. of Electronics, Inf. and Communication Engineers, IEICE; The Institute of Electrical and Electronics Engineers, Inc., IEEE (Institute of Electrical and Electronics Engineers Inc.):
  • [5] Binary Taylor Diagrams: An efficient implementation of Taylor expansion Diagrams
    Hooshmand, A
    Shamshiri, S
    Alisafaee, M
    Lotfi-Kamran, P
    Naderi, M
    Navabi, Z
    Alizadeh, B
    2005 IEEE INTERNATIONAL SYMPOSIUM ON CIRCUITS AND SYSTEMS (ISCAS), VOLS 1-6, CONFERENCE PROCEEDINGS, 2005, : 424 - 427
  • [6] Algorithms for Taylor Expansion Diagrams
    Fey, G
    Drechsler, R
    Ciesielski, M
    34TH INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC, PROCEEDINGS, 2004, : 235 - 240
  • [7] FORMAL DEFINITION AND VERIFICATION OF DATA FLOW DIAGRAMS
    TAO, YL
    KUNG, CH
    JOURNAL OF SYSTEMS AND SOFTWARE, 1991, 16 (01) : 29 - 36
  • [8] Semantic Specification and Verification of Data Flow Diagrams
    刘彤
    唐稚松
    Journal of Computer Science and Technology, 1991, (01) : 21 - 31
  • [9] High-level design verification using Taylor Expansion Diagrams: First results
    Kalla, P
    Ciesielski, M
    Boutillon, E
    Martin, E
    SEVENTH IEEE INTERNATIONAL HIGH-LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS, 2002, : 13 - 17
  • [10] Variable ordering for Taylor expansion diagrams
    Gomez-Prado, D
    Ren, Q
    Askar, S
    Ciesielski, M
    Boutillon, E
    NINTH IEEE INTERNATIONAL HIGH-LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS, 2004, : 55 - 59
12345