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

主要研究領域:

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

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. Tian-Fu Chen, Jie-Hong R. Jiang, “Boolean Matching Reversible Circuits: Algorithm and Complexity,” 61st ACM/IEEE Design Automation Conference (DAC), 1, San Francisco CA USA, Jun. 2024
  2. Yu-Shan Huang, Jie-Hong R. Jiang, “Circuit Learning: From Decision Trees to Decision Graphs,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 42, 3985, Nov. 2023
  3. Tian-Fu Chen, Chun-Yu Wei, Jie-Hong R. Jiang, “VanQiRA: A Vanishing-State-Based Framework for Quantum Circuit Runtime Assertion,” IEEE International Conference on Quantum Computing and Engineering (QCE), 1033, Bellevue, WA, USA, Sept. 2023
  4. Yu-Shan Huang, Jie-Hong R. Jiang, Alan Mishchenko, “Quantized Neural Network Synthesis for Direct Logic Circuit Implementation,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 42, 473, Feb. 2023
  5. Jie-Hong R. Jiang, “Second-Order Quantified Boolean Logic,” 37th AAAI Conference on Artificial Intelligence (AAAI), 4007, Washington, DC, USA, Feb. 2023
  6. Che Cheng, Jie-Hong R. Jiang, “Lifting (D)QBF Preprocessing and Solving Techniques to (D)SSAT,” 37th AAAI Conference on Artificial Intelligence (AAAI), 3906, Washington, DC, USA, Feb. 2023
  7. Yu-Wei Fan, Jie-Hong R. Jiang, “SharpSSAT: A Witness-Generating Stochastic Boolean Satisfiability Solver,” 37th AAAI Conference on Artificial Intelligence (AAAI), 3949, Washington, DC, USA, Feb. 2023
  8. Giovanni De Micheli, Jie-Hong R. Jiang, Robert Rand, Kaitlin N. Smith, Mathias Soeken, “Advances in Quantum Computation and Quantum Technologies: A Design Automation Perspective,” IEEE Journal on Emerging and Selected Topics in Circuits and Systems, 12, 584, Sept. 2022
  9. Tian-Fu Chen, Jie-Hong R. Jiang, Min-Hsiu Hsieh, “Partial Equivalence Checking of Quantum Circuits,” IEEE International Conference on Quantum Computing and Engineering (QCE), 594, Broomfield, CO, USA, Sept. 2022
  10. Yuan-Hung Tsai, Jie-Hong R. Jiang, Chiao-Shan Jhang, “Bit-Slicing the Hilbert Space: Scaling Up Accurate Quantum Circuit Simulation,” 58th ACM/IEEE Design Automation Conference (DAC), 439, San Francisco, CA, USA, Dec. 2021
  11. Nian-Ze Lee, Jie-Hong R. Jiang, “Constraint Solving for Synthesis and Verification of Threshold Logic Circuits,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 40, 904, May 2021
  12. Nian-Ze Lee, Jie-Hong R. Jiang, “Dependency Stochastic Boolean Satisfiability: A Logical Formalism for NEXPTIME Decision Problems with Uncertainty,” 35th AAAI Conference on Artificial Intelligence (AAAI), 3877, Virtual, Feb. 2021
  13. Jie-Hong R. Jiang, Victor N. Kravets, Nian-Ze Lee, “Engineering Change Order for Combinational and Sequential Design Rectification,” Design, Automation & Test in Europe Conference & Exhibition (DATE), 726, Grenoble, France, Mar. 2020
  14. Chia-Chih Chi, Jie-Hong R. Jiang, “Logic synthesis of binarized neural networks for efficient circuit implementation,” Proceedings of the International Conference on Computer-Aided Design, undefined, 1, Nov. 2018
  15. C.-C. Chi, J.-H. R. Jiang, “Logic Synthesis of Binarized Neural Networks for Efficient Circuit Implementation,” In Proc. Int’l Conf. on Computer-Aided Design (ICCAD), 84:1, San Diego, USA, Nov. 2018
  16. H.-E. Wang, S.-Y. Chen, F. Yu, J.-H. R. Jiang, “A Symbolic Model Checking Approach to the Analysis of String and Length Constraints,” In Proc. International Conference on Automated Software Engineering (ASE), 623, Montpellier, France, Sept. 2018
  17. Nian-Ze Lee, Jie-Hong R. Jiang, “Towards Formal Evaluation and Verification of Probabilistic Design,” IEEE Trans. Computers, 67(8), 1202, Aug. 2018
  18. Tai-Yin Chiu and Jie-Hong R. Jiang, “Logic Synthesis of Recombinase Based Genetic Circuits,” Scientific Reports, 7, Article No. 12873, doi:10.1038/s41598-017-07386-3, Oct. 2017
  19. Yi-Hsiang Lai, Chi-Chuan Chuang, Jie-Hong R. Jiang, “Scalable Synthesis of PCHB-WCHB Hybrid Quasi-Delay Insensitive Circuits,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 35(11): 1797-1810, Nov. 2016
  20. Hung-En Wang, Tzung-Lin Tsai, Chun-Han Lin, Fang Yu, Jie-Hong R. Jiang, “String Analysis via Automata Manipulation with Logic Circuit Representation,” Proc. Int'l Conf. on Computer Aided Verification (CAV), vol. 1, pages 241-260, Toronto, Canada, Jul. 2016
  21. Grace Wu, Yi-Tin Sun, and Jie-Hong R. Jiang, “Design Partitioning for Large Scale Equivalence Checking and Functional Correction,” Proc. Design Automation Conference (DAC), 23:1-23:6, Austin, TX, USA, Jun. 2016
  22. Chun-Hong Shih, Yi-Hsiang Lai, and Jie-Hong R. Jiang, “SPOCK: Static Performance analysis and deadlOCK verication for ecient asynchronous circuit synthesis,” Proc. International Conference on Computer- Aided Design (ICCAD), Austin, TX, USA, Nov. 2015
  23. Ting-Wei Chiang and Jie-Hong R. Jiang, “Property-Directed Synthesis of Reactive Systems from Safety Specications,” Proc. International Conference on Computer- Aided Design (ICCAD), Austin, TX, USA, Nov. 2015
  24. Tai-Yin Chiu, Hui-Ju K. Chiang, Ruei-Yang Huang, Jie-Hong R. Jiang, François Fages, “Synthesizing Configurable Biochemical Implementation of Linear Systems from Their Transfer Function Specifications,” PLOS ONE, 10(9): e0137442, Sept. 2015
  25. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang, “QBF Resolution Systems and their Proof Complexities,” Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 154-169, Vienna, Austria, Jul. 2014
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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
  31. 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
  32. 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
  33. 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
  34. 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
  35. 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