English  |  正體中文  |  简体中文  |  Items with full text/Total items : 54367/62174 (87%)
Visitors : 13700284      Online Users : 57
RC Version 6.0 © Powered By DSPACE, MIT. Enhanced by NTHU Library IR team.
Scope Tips:
  • please add "double quotation mark" for query phrases to get precise results
  • please goto advance search for comprehansive author search
  • Adv. Search
    HomeLoginUploadHelpAboutAdminister Goto mobile version
    National Tsing Hua University Institutional Repository > 電機資訊學院 > 電機工程學系 > 期刊論文 >  AQUILA: An equivalence checking system for large sequential designs


    Please use this identifier to cite or link to this item: http://nthur.lib.nthu.edu.tw/dspace/handle/987654321/12067


    Title: AQUILA: An equivalence checking system for large sequential designs
    Authors: Huang,Shi-Yu
    Cheng,Kwang-Ting
    Chen,Kuang-Chien
    Huang,Chung-Yang
    Brewer,Forrest
    教師: 黃錫瑜
    Date: 2000
    Publisher: Institute of Electrical and Electronics Engineers Computer Society
    Relation: Computers, IEEE Transactions on Volume 49, Issue 5, May 2000 Page(s):443 - 464
    Keywords: Sequential machines
    Equivalence classes
    Computational complexity
    Decision theory
    Logic gates
    Flip flop circuits
    Finite automata
    Mathematical models
    Abstract: In this paper, we present a practical method for verifying the functional equivalence of two synchronous sequential designs. This tool is based on our earlier framework that uses Automatic Test Pattern Generation (ATPG) techniques for verification. By exploring the structural similarity between the two designs under verification, the complexity can be reduced substantially. We enhance our framework by three innovative features. First, we develop a local BDD-based technique which constructs Binary Decision Diagram (BDD) in terms of some internal signals, for identifying equivalent signal pairs. Second, we incorporate a technique called partial justification to explore not only combinational similarity, but also sequential similarity. This is particularly important when the two designs have a different number of flip-flops. Third, we extend our gate-to-gate equivalence checker for RTL-to-gate verification. Two major issues are considered in this extension: 1) how to model and utilize the external don't care information for verification; and 2) how to extract a subset of unreachable states to speed up the verification process. Compared with existing approaches based on symbolic Finite State Machine (FSM) traversal techniques, our approach is less vulnerable to the memory explosion problem and, therefore, is more suitable for a lot of real-life designs. Experimental results of verifying designs with hundreds of flip-flops will be presented to demonstrate the effectiveness of this approach.
    URI: http://nthur.lib.nthu.edu.tw/handle/987654321/12067
    Appears in Collections:[電機工程學系] 期刊論文
    [積體電路設計技術研發中心] 期刊論文

    Files in This Item:

    File SizeFormat
    2030172010005.pdf31KbAdobe PDF973View/Open


    在NTHUR中所有的資料項目都受到原著作權保護,僅提供學術研究及教育使用,敬請尊重著作權人之權益。若須利用於商業或營利,請先取得著作權人授權。
    若發現本網站收錄之內容有侵害著作權人權益之情事,請權利人通知本網站管理者(smluo@lib.nthu.edu.tw),管理者將立即採取移除該內容等補救措施。

    SFX Query

    與系統管理員聯絡

    DSpace Software Copyright © 2002-2004  MIT &  Hewlett-Packard  /   Enhanced by   NTU Library IR team Copyright ©   - Feedback