江介宏教授的個人資料 - Profile of Jie-Hong Roland Jiang

江介宏 Jie-Hong Roland Jiang

國立台灣大學電機工程學系 教授
國立台灣大學電子工程學研究所 教授
國立台灣大學基因體與系統生物學學位學程 教授
Professor, Department of Electrical Engineering, National Taiwan University
Professor, Graduate Institute of Electronics Engineering, National Taiwan University
Professor, Genome and Systems Biology Degree Program, National Taiwan University

主要研究領域:

驗證理論與方法、硬體分析合成、最佳化方法應用、計算模型、量子/分子計算、系統與合成生物學

Major Research Areas:

formal verification, logic synthesis, optimization methods, computation models, quantum/molecular computation, systems and synthetic biology

研究領域摘要:

應用邏輯與計算實驗室(ALCom Lab)研究團隊強調理論突破與實務價值，自2005年後的研究重點整理如下：

Scalable Synthesis with Craig Interpolation

此為本研究團隊所開創的新領域，自相關論文發表以來，已受到很多國際研究團隊的重視 。受重視的主因是此新方法有前所遙不能及的scalability。我們提出一開創性的新方法，將Craig在1957年的數學邏輯內插理論首次運用在邏輯合成上。(此相關論文受ICCAD 2007最佳論文獎提名，為510篇投稿論文中受提名的9篇論文之一，亦獲中央社及各媒體報導。)此方法大幅提升函式相依性偵測的可行性，並已成功運用在業界實際電路最佳化 。本團隊更進一步將Craig interpolation運用在函式分解(bi-decomposition, Ashenhurst decomposition)上，以往只能處理30個變數的函式，如今我們可以分解300個甚至更多變數的函式。本團隊的研究重點將持續拓展Craig interpolation的新用途，繼續引領此新領域的發展。

Quantum Computation

以量子力學為計算基礎的演算法在特殊問題的求解上，比傳統電腦可有更低的計算複雜度，而能更快速的解決問題。其中資料庫的搜尋問題便是一例。Harmonic perturbation在量子理論為極重要的主題之一。雷射與核磁共振等科技即來自harmonic perturbation的原理，我們將量子計算新增至harmonic perturbation的應用名單上，提出第一個以fast time-varying Hamiltonian為計算基礎的量子演算法，為繼Grover在1997的quantum database search和Farhi 在 2000年的adiabatic computation後一個新的量子搜尋原理。在快速時變條件下薛丁格方程式往往無公式解而僅能作數值分析，然而Hamiltonian在巧妙設計下我們得以求得公式解，且達到量子計算的最佳運算複雜度。此計算模型提供了一個實現量子電腦的新觀點。

Formal Verification

時序重整(retiming)與再合成(resynthesis)是序向電路(sequential circuits)最佳化中最實際且最重要的方法，然而由於驗證的困難度，這些方法並未廣獲業界運用。數學歸納等同驗證法優於傳統的可至性分析(reachability analysis)驗證法，主要在於它能有效利用電路的相似性簡化問題。然而歸納驗證法並不完整，可能產生所謂的偽負結果(false negatives)，如何避免此特性為極重要的課題。本團隊探討序向電路經retiming與resynthesis操作後的等同性，將數學歸納法所能適用的完整驗證條件推至極限，以往僅知retiming的完整驗證條件，如今可推展到retiming+resynthesis+retiming的完整驗證，並且簡化驗證程序，使以往難以驗證的問題得以有效解決。能完整驗證以往所無法驗證的合成作用且能實際處理更大電路，助於提升合成方法於業界的運用。所提技術已被採納實現在UC Berkeley的邏輯合成與驗證系統ABC而廣為運用。

Design Optimization

我們提出一個以latch取代filp-flop的新設計自動化方法來提昇 design for yield (~30% improvement)。在處理design closure的重要課題上，我們提出新的 technology mapping 方法，相較於文獻具顯著改善 (39% delay improvement with 11% area penalty)。

 

[大學部專題生與研究生資訊；其它研究工作機會(如博士後研究、專任研究助理等職位)請洽江教授]

 

 

 

Research Summary:

ALCom Lab focuses on developing key techniques to advance the efficiency and quality of system design. Theoretical and experimental approaches are both taken. Among the broad interests, three main themes are particularly covered: 

Verification

Ensuring design correctness is crucial in all hardware and software designs. In fact, verification is the most time-consuming part of modern system design. Some recent statistics show verification may take up to 60~80% of the total design time and may require a 3-to-1 ratio between verification engineers and circuit designers. Therefore, developing effective verification techniques has great impact on system design. Sample topics include sequential equivalence checking, property checking, arithmetic circuit verification, etc.

Optimization 

As IC manufacturing process advances, design paradigms shift. Under stringent design criteria, exploiting optimal solutions in various abstraction levels is desperately needed. Sample topics include language equation solving for digital circuit optimization, statistical analysis and optimization for VLSI manufacturability, etc.

Foundations

Tomorrow's important technology breakthroughs stems from today's basic research. It is interesting to explore what we can build from emerging novel technologies. Sample topics include quantum computation models, heterogeneous system modeling, etc.

 

[For research openings, please contact Prof. Jiang.]

Photo of Jie-Hong Roland Jiang