| Summary: | 博士 === 國立臺灣大學 === 電機工程學研究所 === 98 === The increasing popularity of System-on-Chip (SoC) circuits results in many new design challenges. One major challenge is to ensure the functional correctness of such complicated circuits. While most existing verification techniques work well at the Register Transfer (RT) and gate levels, the growing trend is to extend verification to higher-level design abstractions in order to catch bugs early on. In this dissertation, we describe several innovative techniques to address the high-level verification problems for SoC designs. First, we propose a framework called BugHunter that consists of several enhancements and methodologies to improve the scalability and efficiency of high-level verification using symbolic simulation. To better leverage the power of high-level symbolic simulation, we develop a technique that can perform formal code-statement reachability analysis on designs and testbenches directly. This technique can detect bugs at high-level code directly, thus reducing verification time. Once unreachability is found, however, debugging is still an issue because the nature of unreachability prevents the
generation of counterexamples. To address this problem, we propose an innovative diagnosis technique that can identify root causes of unreachability.
In addition to functional verification, another issue that began to emerge in SoC circuits is the design nondeterminism problem. In order to save power or reduce routing congestion, a popular design methodology is to
reset important registers only. However, the uninitialized registers may cause nondeterminism in circuit behavior and cause serious problems. To catch such problems, we propose a nondeterminism verification technique using symbolic simulation and SAT solvers, and it can scale to large designs due to the accompanied novel methodology.
To further improve SoC quality, we also develop algorithms that can automate the reset register reduction process.
One major characteristic in SoC designs is the existence of abundant don''t-cares. For example, the floating-point unit of a processor may never be used in a design that only requires integer multiplication. To utilize such don''t-cares, we utilize our formal reachability analysis methods to identify and remove redundant code under the given input constraints. Our case studies show that this technique can remove unused RTL code and thus reducing the synthesized block area and power consumption. In addition, it can also
facilitate hardware/software co-design and co-optimization, a feature that is useful in early SoC design phases.
It has been pointed out that, although considerable effort
is applied to design verification, bug may still be undetected until tape-out or even the chip is commercialized, causing serious problems. To solve the problem, we propose a software-based post-silicon bug repair methodology that can automatically generate constraints for software so that hardware bugs can be worked around. Since the constraint may be complicated,
we also propose a novel optimization method based on don''t-cares that can dramatically reduce the size of the constraint. In this way, software can be easily modified, either online or offline, so that it runs correctly on the buggy hardware.
|
|---|
