江介宏教授的個人資料 - 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

代表性著作 Selected Publication

  1. Valeriy Balabanov, Hui-Ju K. Chiang, and Jie-Hong R. Jiang, “Henkin quantifiers and Boolean formulae: A certification perspective of DQBF,” Theoretical Computer Science (TCS), 523(2), pp. 86-100, Feb. 2014
  2. Tsung-Po Liu, Shuo-Ren Lin, and Jie-Hong R. Jiang, “Software Workarounds for Hardware Errors: Instruction Patch Synthesis,” IEEE Trans. on CAD of Integrated Circuits and Systems (TCAD), 32(12), pp. 1992-2003, Dec. 2013
  3. Shin-Yann Ho, Shuo-Ren Lin, Ko-Lung Yuan, Chien-Yen Kuo, Kuan-Yu Liao, Jie-Hong R. Jiang, and Chien-Mo James Li, “Automatic Test Pattern Generation for Delay Defects Using Timed Characteristic Functions,” Proc. IEEE/ACM International Conference on Computer-Aided Design (ICCAD), pp. 91-98, San Jose, CA, USA, Nov. 2013
  4. Ko-Lung Yuan, Chien-Yen Kuo, Jie-Hong R. Jiang, and Meng-Yen Li, “Encoding Multi-Valued Functions for Symmetry,” Proc. IEEE/ACM International Conference on Computer-Aided Design (ICCAD), pp. 771-778, San Jose, CA, USA, Nov. 2013
  5. Yi-Ting Chung and Jie-Hong R. Jiang, “Functional Timing Analysis Made Fast and General,” IEEE Trans. on CAD of Integrated Circuits and Systems (TCAD), 32(9), pp. 1421-1434, Sept. 2013
  6. Ruei-Yang Huang, De-An Huang, Hui-Ju Katherine Chiang, Jie-Hong R. Jiang, and Francois Fages, “Species Minimization in Computation with Biochemical Reactions,” Proc. International Workshop on Bio-Design Automation (IWBDA), London, UK, Jul. 2013
  7. Kuan-Hua Tu and Jie-Hong R. Jiang, “Synthesis of feedback decoders for initialized encoders,” Proc. ACM/IEEE Design Automation Conference (DAC), Austin, TX, USA, Jun. 2013
  8. De-An Huang, Jie-Hong R. Jiang, Ruei-Yang Huang, Chi-Yun Cheng, “Compiling Program Control Flows into Biochemical Reactions,” Proc. Int'l Conf. on Computer-Aided Design (ICCAD'12), pages 361-368, San Jose, CA, USA, Nov. 2012
  9. Hsiou-Yuan Liu, Yen-Cheng Chou, Chen-Hsuan Lin, and Jie-Hong R. Jiang, “Automatic Decoder Synthesis: Methods and Case Studies,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 31(9), pp. 1319-1331, Sept. 2012
  10. Valeriy Balabanov and Jie-Hong R. Jiang, “Unified QBF Certification and its Applications,” Formal Methods in System Design (FMSD), 41(1), pp. 45-65, Aug. 2012
  11. Cheng-Shen Han and Jie-Hong R. Jiang, “When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way,” Proc. International Conference on Computer Aided Verification (CAV'12), pages 410-426, Berkeley, USA, Jul. 2012
  12. Yi-Ting Chung and Jie-Hong R. Jiang, “Efficient Transformation of Various Timed Characteristic Functions for Satisfiability Solving,” Proc. Int'l Workshop on Logic and Synthesis (IWLS'12), Berkeley, USA, Jun. 2012
  13. Yi-Ting Chung and Jie-Hong R. Jiang, “Functional Timing Analysis Made Fast and General,” Proc. ACM/IEEE Design Automation Conference (DAC'12), pages 1055-1060, San Francisco, USA, Jun. 2012
  14. Valeriy Balabanov, Hui-Ju Katherine Chiang, and Jie-Hong R. Jiang, “Henkin Quantifiers and Boolean Formulae,” Proc. Int'l Conference on the Theory and Applications of Satisfiability Test (SAT'12), pages 129-142, Trento, Italy, Jun. 2012
  15. Alan Mishchenko, Robert Brayton, Jie-Hong R. Jiang, and Stephen Jang, “Scalable Don't-Care-Based Logic Optimization and Resynthesis,” ACM Transactions on Reconfigurable Technology and Systems (TRETS), 4(4):34, Dec. 2011
  16. Hsiou-Yuan Liu, Yen-Cheng Chou, Chen-Hsuan Lin, and Jie-Hong R. Jiang, “Towards Completely Automatic Decoder Synthesis,” Proc. IEEE/ACM Int'l Conf. on Computer Aided Design (ICCAD'11), pages 389-395, San Jose, USA, Nov. 2011
  17. Valeriy Balabanov and Jie-Hong R. Jiang, “Resolution Proofs and Skolem Functions in QBF Evaluation and Applications,” Proc. Int'l Conf. on Computer Aided Verification (CAV'11), pages 149-164, Salt Lake City, Jul. 2011
  18. Jie-Hong Roland Jiang, Hsuan-Po Lin, and Wei-Lun Hung, “Extracting Functions from Boolean Relations Using SAT and Interpolation,” Advanced Techniques in Logic Synthesis, Optimizations and Applications, Sunil Khatri and Kanupriya Gulati, editors, Springer, (book chapter, pages 287-307), 2011
  19. Hsuan-Po Lin, Jie-Hong Roland Jiang, and Ruei-Rung Lee, “Ashenhurst Decomposition Using SAT and Interpolation,” Advanced Techniques in Logic Synthesis, Optimizations and Applications, Sunil Khatri and Kanupriya Gulati, editors, Springer, (book chapter, pages 67-85), 2011
  20. Ruei-Rung Lee, Jie-Hong Roland Jiang, and Wei-Lun Hung, “Bi-decomposition Using SAT and Interpolation,” Advanced Techniques in Logic Synthesis, Optimizations and Applications, Sunil Khatri and Kanupriya Gulati, editors, Springer, (book chapter, pages 87-105), 2011
  21. Chih-Fan Lai, Jie-Hong R. Jiang, and Kuo-Hua Wang, “Boolean Matching of Function Vectors with Strengthened Learning,” Proc. Int'l Conf. on Computer-Aided Design (ICCAD'10), San Jose, USA, Nov. 2010
  22. Chih-Fan Lai, Jie-Hong R. Jiang, and Kuo-Hua Wang, “BooM: A Decision Procedure for Boolean Matching with Abstraction and Dynamic Learning,” Proc. ACM/IEEE Design Automation Conference (DAC'10), pages 499-504, Anaheim, USA, Jun. 2010
  23. Jie-Hong R. Jiang and Tiziano Villa, “Hardware Equivalence and Property Verification,” Boolean Methods and Models in Mathematics, Computer Science and Engineering, Y. Crama and P. L. Hammer, editors, Cambridge University Press, (book chapter, pages 599-674), May 2010
  24. Jie-Hong R. Jiang, Chih-Chun Lee, Alan Mishchenko, and Chung-Yang Huang, “To SAT or Not to SAT: Scalable Exploration of Functional Dependency,” IEEE Transactions on Computers (TCOM), vol. 59, no. 4, pages 457-467, Apr. 2010
  25. Jie-Hong R. Jiang, Hsuan-Po Lin, and Wei-Lun Hung, “Interpolating Functions from Large Boolean Relations,” Proc. Int'l Conf. on Computer-Aided Design (ICCAD'09), San Jose, USA, Nov. 2009
  26. Jie-Hong R. Jiang, “Quantifier Elimination via Functional Composition,” Proc. Int'l Conf. on Computer Aided Verification (CAV'09), pages 383-397, Grenoble, France, Jun. 2009
  27. Hsuan-Po Lin, Jie-Hong R. Jiang, and Ruei-Rung Lee, “To SAT or Not to SAT: Ashenhurst Decomposition in a Large Scale,” Proc. IEEE/ACM Int'l Conf. on Computer-Aided Design (ICCAD'08), pages 32-37, San Jose, USA, Nov. 2008
  28. Sz-Cheng Huang and Jie-Hong R. Jiang, “A Dynamic Accuracy-Refinement Approach to Timing-Driven Technology Mapping,” Proc. IEEE Int'l Conf. on Computer Design (ICCD'08), pages 538-543, Lake Tahoe, USA, Oct. 2008
  29. Ruei-Rung Lee, Jie-Hong R. Jiang, and Wei-Lun Hung, “Bi-Decomposing Large Boolean Functions via Interpolation and Satisfiability Solving,” Proc. ACM/IEEE Design Automation Conference (DAC'08), pages 636-641, Anaheim, USA, Jun. 2008
  30. Chih-Chun Lee, Jie-Hong R. Jiang, Chung-Yang Huang, and Alan Mishchenko, “Scalable Exploration of Functional Dependency by Interpolation and Incremental SAT Solving,” Proc. IEEE/ACM Int'l Conf. on Computer-Aided Design (ICCAD'07), pages 227-233, San Jose, USA, Nov. 2007
  31. Jie-Hong R. Jiang and Wei-Lun Hung, “Inductive Equivalence Checking under Retiming and Resynthesis,” Proc. IEEE/ACM Int'l Conf. on Computer-Aided Design (ICCAD'07), pages 326-333, San Jose, USA, Nov. 2007
  32. Jie-Hong R. Jiang, Dah-Wei Chiou, and Cheng-En Wu, “Quantum Mechanical Search and Harmonic Perturbation,” Quantum Information Processing, vol. 6, issue 5, pages 349-362, Oct. 2007
  33. Chin-Hsiung Hsu, Szu-Jui Chou, Jie-Hong R. Jiang, Yao-Wen Chang, “A Statistical Approach to the Timing-Yield Optimization of Pipeline Circuits,” Proc. Int'l Workshop on Power And Timing Modeling, Optimization and Simulation (PATMOS'07), pages 148-159, Göteborg, Sweden, Sept. 2007
  34. Jie-Hong R. Jiang and Robert K. Brayton, “Retiming and Resynthesis: A Complexity Perspective,” IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems (TCAD), vol. 25, no. 12, pages 2674-2686, Dec. 2006
  35. Jie-Hong R. Jiang, “On Some Transformation Invariants under Retiming and Resynthesis,” Proc. Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), pages 413-428, Edinburgh, UK, Apr. 2005
  36. Jie-Hong R. Jiang, Alan Mishchenko, and Robert K. Brayton, “On Breakable Cyclic Definitions,” Proc. IEEE/ACM Int'l Conf. on Computer-Aided Design (ICCAD'04), pages 411-418, San Jose, USA, Nov. 2004
  37. Jie-Hong R. Jiang and Robert K. Brayton, “Functional Dependency for Verification Reduction,” Proc. Int'l Conf. on Computer Aided Verification (CAV'04), pages 268-280, Boston, USA, Jul. 2004
  38. Jie-Hong R. Jiang and Robert K. Brayton, “On the Verification of Sequential Equivalence,” IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems (TCAD), vol. 22, no. 6, pages 686-697, Jun. 2003