English  |  正體中文  |  简体中文  |  Items with full text/Total items : 54367/62174 (87%)
Visitors : 14553164      Online Users : 81
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
    教師: 黃錫瑜
    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 PDF986View/Open


    SFX Query


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