請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/91495完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 江介宏 | zh_TW |
| dc.contributor.advisor | Jie-Hong Roland Jiang | en |
| dc.contributor.author | 魏駿宇 | zh_TW |
| dc.contributor.author | Chun-Yu Wei | en |
| dc.date.accessioned | 2024-01-28T16:15:33Z | - |
| dc.date.available | 2024-02-24 | - |
| dc.date.copyright | 2024-01-27 | - |
| dc.date.issued | 2023 | - |
| dc.date.submitted | 2023-07-28 | - |
| dc.identifier.citation | [1] D. Aharonov. A Simple Proof that Toffoli and Hadamard are Quantum Universal, 2003. arXiv: quant-ph/0301040.
[2] G. Aleksandrowicz et al. Qiskit: An Open-source Framework for Quantum Com- puting, 2019. [3] L. Amarú et al. The EPFL Combinational Benchmark Suite. In Proceedings of the International Workshop on Logic and Synthesis, 2015. [4] M. Boule, J.-S. Chenard, and Z. Zilic. Assertion Checkers in Verification, Silicon Debug and In-Field Diagnosis. In 8th International Symposium on Quality Electronic Design (ISQED’07), pages 613–620. IEEE, 2007. [5] P.O.Boykinetal.ANewUniversalandFault-TolerantQuantumBasis.Inf.Process. Lett., 75(3):101–107, 2000. [6] R. Brayton et al. ABC: An Academic Industrial-Strength Verification Tool. In Proceedings of the Computer Aided Verification, pages 24–40, 2010. [7] R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677–691, 1986. [8] L. Burgholzer, R. Raymond, I. Sengupta, and R. Wille. Efficient Construction of Functional Representations for Quantum Algorithms. In Proceedings of the Reversible Computation, pages 227–241, 2021. [9] L.BurgholzerandR.Wille.AdvancedEquivalenceCheckingforQuantumCircuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, PP:1–1, 10 2020. [10] L. Burgholzer and R. Wille. The Power of Simulation for Equivalence Checking in Quantum Computing. In Proceedings of the Design Automation Conference, pages 1–6, 2020. [11] L.BurgholzerandR.Wille.AdvancedEquivalenceCheckingforQuantumCircuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 40(9):1810–1824, 2021. [12] T.-F. Chen, C.-Y. Wei, and J.-H. R. Jiang. VanQiRA: A Vanishing-State-Based Framework for Quantum Circuit Runtime Assertion. In Proceedings of the IEEE International Conference on Quantum Computing and Engineering, 2023. [13] C. Condrat et al. Logic Synthesis for Integrated Optics. In Proceedings of the Great Lakes Symposium on Great Lakes Symposium on VLSI, page 13–18, 2011. [14] O. Coudert and J. Madre. A Unified Framework for the Formal Verification of Se- quential Circuits. In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design., pages 126 – 129, 1990. [15] C. Developers. Cirq: An Open Source Framework for Programming Quantum Com- puters, 2021. [16] R. Drechsler. Pseudo-Kronecker Expressions for Symmetric Functions. IEEE Transactions on Computers, 48(9):987–990, 1999. [17] R. Duncan, A. Kissinger, S. Perdrix, and J. van de Wetering. Graph-theoretic Sim- plification of Quantum Circuits with the ZX-Calculus. Quantum, 4:279, June 2020. [18] J. D. A. Espinoza, K. Groenland, M. Mazzanti, K. Schoutens, and R. Gerritsma. High-Fidelity Method for a Single-Step n-bit Toffoli Gate in Trapped Ions. Physical Review A, 103(5):052437, 2021. [19] K. Fazel, M. A. Thornton, and J. E. Rice. ESOP-based Toffoli Gate Cascade Gener- ation. In Proceedings of the Pacific Rim Conference, pages 206–209, 2007. [20] H. D. Foster, A. C. Krolnik, and D. J. Lacey. Assertion-based Design. Springer Science & Business Media, 2004. [21] E.Goldberg,M.Prasad,andR.Brayton.UsingSATforCombinationalEquivalence Checking. In Proceedings of the Design, Automation and Test in Europe Conference, pages 114–121, 2001. [22] P. Gupta et al. An Algorithm for Synthesis of Reversible Logic Circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 25(11):2317–2330, 2006. [23] X. Hong et al. A Tensor Network Based Decision Diagram for Representation of Quantum Circuits. Transactions on Design Automation of Electronic Systems, 27(6), 2022. [24] X. Hong, Y. Feng, S. Li, and M. Ying. Equivalence Checking of Dynamic QuantumCircuits. In Proceedings of the International Conference on Computer-Aided Design, 2022. [25] X.Hong,M.Ying,Y.Feng,X.Zhou,andS.Li.ApproximateEquivalenceChecking of Noisy Quantum Circuits. In Proceedings of the Design Automation Conference, pages 637–642, 2021. [26] G. Li, L. Zhou, N. Yu, Y. Ding, M. Ying, and Y. Xie. Proq: Projection-based Runtime Assertions for Debugging on a Quantum Computer. arXiv preprint arXiv:1911.12855, 2019. [27] J. Liu, G. T. Byrd, and H. Zhou. Quantum Circuits for Dynamic Runtime Asser- tions in Quantum Computation. In Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems, pages 1017–1030, 2020. [28] J. Liu and H. Zhou. Systematic Approaches for Precise and Approximate Quantum State Runtime Assertion. In 2021 IEEE International Symposium on High-Performance Computer Architecture (HPCA), pages 179–193. IEEE, 2021. [29] R. W. Lucas Berent, Lukas Burgholzer. Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond, 2022. arXiv: quant-ph/2203.00698. [30] G. Meuli et al. Evaluating ESOP Optimization Methods in Quantum Compilation Flows. In Proceedings of Reversible Computation, pages 191–206, 2019. [31] G. Meuli et al. Xor-And-Inverter Graphs for Quantum Compilation. npj Quantum Information, 8:1–11, 2022. [32] S.-i. Minato. Zero-Suppressed BDDs for Set Manipulation in Combinatorial Prob- lems. In Proceedings of the Design Automation Conference, page 272–277. Asso- ciation for Computing Machinery, 1993. [33] A. Mishchenko and M. Perkowski. Fast Heuristic Minimization of Exclusive-Sums- of-Products. In Proceedings of the International Reed-Muller Workshop, 2001. [34] T. Mizuki et al. An Application of ESOP Expressions to Secure Computations. Journal of Circuits, Systems, and Computers, 16:191–198, 2007. [35] P. Niemann, R. Wille, D. M. Miller, M. A. Thornton, and R. Drechsler. QMDDs: Efficient Quantum Function Representation and Manipulation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 35(1):86–99, 2016. [36] T. Peham, L. Burgholzer, and R. Wille. Equivalence Checking of Quantum Circuits With the ZX-Calculus. IEEE Journal on Emerging and Selected Topics in Circuits and Systems, 12(3):662–675, 2022. [37] Y.-A. C. Randal E. Bryant. Verification of Arithmetic Circuits with Binary Moment Diagrams. In Proceedings of the Design Automation Conference, pages 535–541, 1995. [38] S. Rasmussen, K. Groenland, R. Gerritsma, K. Schoutens, and N. Zinner. Single- Step Implementation of High-Fidelity n-bit Toffoli Gates. Physical Review A, 101(2):022308, 2020. [39] H. Riener, R. Ehlers, B. d. O. Schmitt, and G. D. Micheli. Exact Synthesis of ESOP Forms, pages 177–194. Springer International Pub- lishing, 2020. [40] T. Sasao. And-Exor Expressions and their Optimization, pages 287–312. Springer, 1993. [41] T.SasaoandM.Fujita.RepresentationsofLogicFunctionsUsingEXOROperators, pages 29–54. Springer, US, 1996. [42] B. Schmitt et al. Scaling-up ESOP Synthesis for Quantum Compilation. In Proceedings of the IEEE International Symposium on Multiple-Valued Logic, pages 13–18, 2019. [43] M.Soekenetal.CompilingPermutationsforSuperconductingQPUs.InProceedings the Design, Automation and Test in Europe Conference, pages 1349–1354, 2019. [44] M. Soeken et al. LUT-Based Hierarchical Reversible Logic Synthesis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 38(9):1675–1688, 2019. [45] M. Soeken et al. The EPFL Logic Synthesis Libraries., 2022. arXiv:1805.05121v3. [46] F. Somenzi. CUDD: CU decision diagram package (release 2.4.2). University of Colorado at Boulder, 2005. [47] N. Song and M. Perkowski. Minimization of Exclusive Sum-of-Products Ex- pressions for Multiple-Valued Input, Incompletely Specified Functions. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 15(4):385–395, 1996. [48] D. S. Steiger and T. H. M. Troyer. ProjectQ: An Open Source Software Framework for Quantum Computing, 2018. [49] S. Stergiou and J. Jain. Optimizing Routing Tables on Systems-on-Chip with Content-Addressable Memories. In Proceedings of the International Symposium on System on Chip, pages 1–6, 2008. [50] Y.-H. Tsai, J.-H. R. Jiang, and C.-S. Jhang. Bit-Slicing the Hilbert Space: Scaling Up Accurate Quantum Circuit Simulation. In Proceedings of the Design Automation Conference, pages 439–444, 2021. [51] G.Viamontes,I.Markov,andJ.Hayes.High-PerformanceQuIDD-basedSimulation of Quantum Circuits. In Proceedings of the Design, Automation and Test in Europe Conference, volume 2, pages 1354–1355, 2004. [52] L. Vinkhuijzen, T. Grurl, S. Hillmich, S. Brand, R. Wille, and A. Laarman. Efficient Implementation of LIMDDs for Quantum Circuit Simulation. In Proceedings of the International Symposium on Model Checking of Software, 2023. [53] S.-A. Wang, C.-Y. Lu, I.-M. Tsai, and S.-Y. Kuo. An XQDD-Based Verification Method for Quantum Circuits. IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, E91-A(2):584–594, 2008. [54] C.-Y. Wei and J.-H. R. Jiang. Don’t-Care Aware ESOP Extraction via Reduced Decomposition-Tree Exploration. In Proceedings of the the Design Automation Conference, 2023. [55] C.-Y.Wei,Y.-H.Tsai,C.-S.Jhang,andJ.-H.R.Jiang.AccurateBDD-BasedUnitary Operator Manipulation for Scalable and Robust Quantum Circuit Verification. In Proceedings of the the Design Automation Conference, page 523–528, 2022. [56] R. Wille, L. Burgholzer, S. Hillmich, T. Grurl, A. Ploier, and T. Peham. The Ba- sis of Design Tools for Quantum Computing: Arrays, Decision Diagrams, Tensor Networks, and ZX-Calculus. In Proceedings of the Design Automation Conference, page 1367–1370, 2022. [57] R. Wille, D. Große, L. Teuber, G. W. Dueck, and R. Drechsler. RevLib: An Online Resource for Reversible Functions and Reversible Circuits. In Proc. Int. Symp. on Multi-Valued Logic, pages 220–225, 2008. [58] H. Witharana, Y. Lyu, S. Charles, and P. Mishra. A Survey on Assertion-based Hardware Verification. ACM Computing Surveys (CSUR), 54(11s):1–33, 2022. [59] S. Yamashita and I. L. Markov. Fast Equivalence-Checking for Quantum Circuits. Quantum Information and Computation, 10(9):721–734, 2010. [60] A. Zulehner et al. Accuracy and Compactness in Decision Diagrams for Quan- tum Computation. In Proceedings of the Design, Automation and Test in Europe Conference, pages 280–283, 2019. [61] A.Zulehner,S.Hillmich,andR.Wille.HowtoEfficientlyHandleComplexValues? Implementing Decision Diagrams for Quantum Computing. In Proceedings of the International Conference on Computer-Aided Design, pages 1–7, 2019. [62] A. Zulehner and R. Wille. Advanced Simulation of Quantum Computations. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 38(5):848–859, 2019. | - |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/91495 | - |
| dc.description.abstract | 量子技術的迅速進展引發了各種量子計算應用的出現。與此同時，傳統計算機在處理量子資料的指數級複雜性方面面臨著挑戰。隨著決策圖在傳統電子設計自動化領域中提供了處理布林函數指數級複雜性的緊湊高效之數據結構，近年來在量子計算領域中，決策圖也受到了越來越多的關注。它們展示了在表示高維量子資料和實現各種量子任務(如量子電路模擬和驗證)方面的有效性。本研究探討了二進制決策圖在量子計算中的應用。我們擴展了最近的基於位元切片的布林決策圖框架，來支援積之互斥或表示式的合成用於布林預示實現、 量子斷言電路合成和量子電路驗證。整合的框架借助決策圖的優勢，在處理量子實體時提供了效率和可擴展性，以支持各種量子任務。此外，其精確性特性解決了先前方法中存在的精度損失問題，實現了精確計算，增強了該框架在驗證場景中的適用性。實驗結果顯示，所提出的布林積之互斥或表示式合成方法在運行時間方面提供高達29倍（平均12倍）的加速，並且在記憶體使用方面改進了28倍（平均13倍）。對於完全指定的函數，所獲得的解的品質接近於通過詳盡探索獲得的精確最優解。此外，對於不完全指定的函數，該方法能夠大幅簡化布林積之互斥或表示式考慮不指定部分。關於量子運行時間斷言電路合成，所提出的方法有效地處理高達一百個量子位元電路，並且能夠在斷言電路大小和錯誤檢測率之間取得平衡。此外，在量子電路驗證方面，我們的方法在處理大型電路方面表現優於先前的方法，並能夠實現精確的等效性檢查結果。 | zh_TW |
| dc.description.abstract | The rapid progress in quantum technologies has led to the emergence of diverse applications leveraging quantum computation. Concurrently, classical computers encounter challenges in handling the exponential growth complexity of quantum entities. With the success of decision diagrams in offering compact and efficient data structures for handling the exponential growth complexity of Boolean functions in the traditional Electronic Design Automation (EDA) field, their significance has expanded in recent years, gaining increased attention in the field of quantum computing. They have demonstrated their effectiveness in representing high-dimensional quantum entities and enabling efficient computations across various quantum tasks, such as quantum circuit simulation and verification.
This work investigates the application of the Binary Decision Diagram (BDD) in quantum computing. We extend the capabilities of the recent bit-slicing BDD-based framework, a framework for manipulating quantum entities based on BDD, to support ESOP synthesis for Boolean oracle implementation, quantum assertion circuit synthesis, and quantum circuit verification. The integrated framework, leveraging the advantages of decision diagrams, offers efficiency and scalability in managing quantum entities to support various quantum tasks. Additionally, its exactness properties address precision loss issues observed in prior methods, enabling precise computations and augmenting the framework’s applicability in verification scenarios.Experimental results show the proposed ESOP synthesis method offers up to 29x (average 12x) runtime and 28x (average 13x) memory improvement, maintaining quality close to exact optima for fully-specified functions.For incompletely-specified functions, significant ESOP simplification is achieved while considering don't-cares.The proposed assertion circuit synthesis flow efficiently handles up to one hundred qubit circuits, balancing circuit size and error-detection rate. For quantum circuit verification, our method excels in handling large circuits compared to prior approaches, delivering precise equivalence checking results. | en |
| dc.description.provenance | Submitted by admin ntu (admin@lib.ntu.edu.tw) on 2024-01-28T16:15:33Z No. of bitstreams: 0 | en |
| dc.description.provenance | Made available in DSpace on 2024-01-28T16:15:33Z (GMT). No. of bitstreams: 0 | en |
| dc.description.tableofcontents | Contents
Certificate ... i Acknowledgements ... iii 中文摘要 ... v Abstract ... vii Contents ... ix Chapter 1 Introduction ... 1 1.1 Decision Diagrams in Electronic Design Automation ... 1 1.2 Decision Diagrams in Quantum Computing ... 2 1.3 Our Contributions ... 2 1.4 Thesis Organization ... 3 Chapter 2 Background ... 5 Boolean Logic ... 5 2.1.1 Boolean Function ... 5 2.1.2 Binary Decision Diagram ... 6 2.2 Quantum Basics ...8 2.2.1 Quantum State and Quantum Circuit ... 8 2.2.2 Tensor Network ... 9 2.2.3 Boolean Oracle ... 11 2.3 Bit-Slicing BDD Framework ... 12 2.3.1 BDD-based Tensor Representation ... 13 2.3.2 Contracting Gates via Boolean Formulas ... 14 Chapter 3 ESOP Synthesis ... 17 3.1 Overview ... 17 3.2 Previous Work ... 19 3.2.1 Pseudo-Kronecker Expression ... 19 3.2.2 BDD-Based ESOP Extraction ... 20 3.3 Our Contributions ... 22 3.4 Reduction for Decomposition-Tree Exploration ... 22 3.4.1 Cost Estimation ... 23 3.4.2 Cost Look-Ahead ... 24 3.4.3 Refinement ... 25 3.5 Divide-and-Minimize for Large ESOPs ... 26 3.6 Generalization for Incompletely-Specified Functions ... 27 3.6.1 Recursive Careset Characterization ... 29 3.6.2 Algorithm ... 31 3.7 Experimental Results ... 33 3.7.1 Extraction for Completely-Specified Boolean Functions ... 33 3.7.2 Extraction for Incompletely-Specified Boolean Functions ... 36 3.7.3 Minimization of Large ESOPs ... 38 3.8 Chapter Remarks ... 39 Chapter 4 Quantum Assertion Circuit Synthesis ... 41 4.1 Overview ... 41 4.2 Problem Formation ... 42 4.2.1 Quantum Runtime Assertion ... 42 4.2.2 Vanishing-State-based Framework ... 44 4.3 Our Contributions ... 44 4.4 Sparsity Checking ... 45 4.5 Assertion Circuit Synthesis ... 47 4.5.1 Simulation ... 47 4.5.2 Sparsity Checking ... 48 4.5.3 ESOP-based Boolean Oracle Synthesis .. 48 4.6 Experiments Results ... 49 4.6.1 Efficiency of Assertion Cirvuit Synthesis ... 49 4.6.2 Trade-off between Coverage and Assertion Cost ... 50 4.7 Chapter Remarks ... 51 Chapter 5 Quantum Circuit Verification ... 53 5.1 Overview ... 53 5.2 Previous Work ... 54 5.2.1 Check by Functionality Construction ... 55 5.2.2 Check by Miter Construction ... 56 5.2.3 Check by Simulation ... 56 5.3 Our Contributions ... 57 5.4.1 Canonicity Proof ... 58 5.4.2 Make r and k consistent ... 59 5.5 Checking by Functionality Construction ... 64 5.6 Checking by Simulation ... 66 5.7 Checking by Miter Construction ... 67 5.8 Experimental Results ... 69 5.8.1 Performance ... 69 5.8.2 Reliability ... 72 5.9 Chapter Remarks ... 75 Chapter 6 Conclusion ... 81 List of Figures ... 83 List of Tables ... 85 References ... 87 | - |
| dc.language.iso | en | - |
| dc.subject | 量子電路驗證 | zh_TW |
| dc.subject | 積之互斥或表示式 | zh_TW |
| dc.subject | 量子計算 | zh_TW |
| dc.subject | 布林決策圖 | zh_TW |
| dc.subject | 量子運行斷言 | zh_TW |
| dc.subject | Binary Decision Diagram (BDD) | en |
| dc.subject | Quantum Runtime Assertion | en |
| dc.subject | Quantum Circuit Verification | en |
| dc.subject | Quantum Computing | en |
| dc.subject | Exclusive-Or Sum-of-Products (ESOPs) | en |
| dc.title | 運用二元決策圖進行可逆邏輯合成和量子電路驗證 | zh_TW |
| dc.title | Reversible Logic Synthesis and Quantum Circuit Verification with Binary Decision Diagrams | en |
| dc.type | Thesis | - |
| dc.date.schoolyear | 111-2 | - |
| dc.description.degree | 碩士 | - |
| dc.contributor.oralexamcommittee | 管希聖;鄭皓中 | zh_TW |
| dc.contributor.oralexamcommittee | Hsi-Sheng Goan;Hao-Chung Cheng | en |
| dc.subject.keyword | 布林決策圖,量子計算,積之互斥或表示式,量子運行斷言,量子電路驗證, | zh_TW |
| dc.subject.keyword | Binary Decision Diagram (BDD),Quantum Computing,Exclusive-Or Sum-of-Products (ESOPs),Quantum Runtime Assertion,Quantum Circuit Verification, | en |
| dc.relation.page | 94 | - |
| dc.identifier.doi | 10.6342/NTU202302148 | - |
| dc.rights.note | 同意授權(全球公開) | - |
| dc.date.accepted | 2023-07-31 | - |
| dc.contributor.author-college | 電機資訊學院 | - |
| dc.contributor.author-dept | 電子工程學研究所 | - |
| dc.date.embargo-lift | 2028-07-26 | - |
| 顯示於系所單位： | 電子工程學研究所 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-111-2.pdf 此日期後於網路公開 2028-07-26 | 2.19 MB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。