請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/101240完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 江介宏 | zh_TW |
| dc.contributor.advisor | Jie-Hong Roland Jiang | en |
| dc.contributor.author | 陳天富 | zh_TW |
| dc.contributor.author | Tian-Fu Chen | en |
| dc.date.accessioned | 2025-12-31T16:26:19Z | - |
| dc.date.available | 2026-01-01 | - |
| dc.date.copyright | 2025-12-31 | - |
| dc.date.issued | 2025 | - |
| dc.date.submitted | 2025-12-01 | - |
| dc.identifier.citation | [1] Amazon Braket. https://aws.amazon.com/braket/. accessed Apr. 30, 2023.
[2] IBM Quantum. https://quantum-computing.ibm.com/. accessed Apr. 30, 2023. [3] L. G. Amaru. Improvements to the equivalence checking of reversible circuits. In New Data Structures and Algorithms for Logic Synthesis and Verification, chapter 6. Springer, 2017. [4] M. Amy. Towards large-scale functional verification of universal quantum circuits. arXiv preprint arXiv:1805.06908, 2018. [5] P. Andrés-Martínez and C. Heunen. Weakly measured while loops: peeking at quantum states. Quantum Science and Technology, 7(2):025007, 2022. [6] E. Ardeshir-Larijani, S. J. Gay, and R. Nagarajan. Verification of concurrent quantum protocols by equivalence checking. In Proc. TACAS, pages 500–514, 2014. [7] F. Bauer-Marquart, S. Leue, and C. Schilling. symQV: Automated symbolic verification of quantum programs. In Proc. FM, pages 181–198. Springer, 2023. [8] A. A. Bayazit and S. Malik. Complementary use of runtime validation and model checking. In Proc. ICCAD, pages 1052–1059, 2005. [9] L. Benini and G. De Micheli. A survey of Boolean matching techniques for library binding. ACM Transactions on Design Automation of Electronic Systems, 2(3):193–226, 1997. [10] C. H. Bennett. Logical reversibility of computation. IBM Journal of Research and Development, 17(6):525–532, 1973. [11] E. Bernstein and U. Vazirani. Quantum complexity theory. In Proc. STOC, pages 11–20, 1993. [12] A. Bocharov, M. Roetteler, and K. M. Svore. Efficient synthesis of universal repeat-until-success quantum circuits. Physical Review Letters, 114(8):080502, 2015. [13] A. R. Bradley. SAT-based model checking without unrolling. In Proc. VMCAI, pages 70–87, 2011. [14] G. Brassard, P. Høyer, and A. Tapp. Quantum counting. In Proc. ICALP, pages 820–831. Springer, 1998. [15] R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 100(8):677–691, 1986. [16] H. Buhrman, R. Cleve, J. Watrous, and R. De Wolf. Quantum fingerprinting. Physical Review Letters, 87(16):167902, 2001. [17] L. Burgholzer and R. Wille. Improved DD-based equivalence checking of quantum circuits. In Proc. ASP-DAC, pages 127–132, 2020. [18] L. Burgholzer and R. Wille. The power of simulation for equivalence checking in quantum computing. In Proc. DAC, pages 1–6, 2020. [19] L. Burgholzer and R. Wille. Advanced equivalence checking for quantum circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 40(9):1810–1824, 2021. [20] L. Burgholzer and R. Wille. Handling non-unitaries in quantum circuit equivalence checking. In Proc. DAC, 2022. [21] T.-F. Chen, Y.-F. Chen, J.-H. R. Jiang, S. Jobranová, and O. Lengál. Accelerating quantum circuit simulation with symbolic execution and loop summarization. In Proc. ICCAD, 2024. [22] T.-F. Chen and J.-H. R. Jiang. Boolean matching reversible circuits: Algorithm and complexity. In Proc. DAC, pages 1–6, 2024. [23] T.-F. Chen and J.-H. R. Jiang. SliQSim: A quantum circuit simulator and solver for probability and statistics queries. In Proc. TACAS, pages 129–138. Springer, 2025. [24] T.-F. Chen, J.-H. R. Jiang, and M.-H. Hsieh. Partial equivalence checking of quantum circuits. In Proc. QCE, pages 594–604. IEEE, 2022. [25] T.-F. Chen, C.-Y. Wei, and J.-H. R. Jiang. VanQiRA: A vanishing-state-based framework for quantum circuit runtime assertion. In Proc. QCE, volume 1, pages 1033–1043. IEEE, 2023. [26] Y.-F. Chen, K.-M. Chung, O. Lengál, J.-A. Lin, and W.-L. Tsai. AutoQ: An automata-based quantum circuit verifier. In Proc. CAV, pages 139–153. Springer, 2023. [27] D. Deutsch and R. Jozsa. Rapid solution of problems by quantum computation. Proceedings of the Royal Society of London. Series A: Mathematical and Physical Sciences, 439(1907):553–558, 1992. [28] N. Een, A. Mishchenko, and R. Brayton. Efficient implementation of property directed reachability. In Proc. FMCAD, pages 125–134, 2011. [29] 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. [30] E. Farhi, J. Goldstone, and S. Gutmann. A quantum approximate optimization algorithm. arXiv preprint arXiv:1411.4028, 2014. [31] T. Fawcett. An introduction to ROC analysis. Pattern Recognition Letters, 27(8):861–874, 2006. [32] K. Fazel, M. A. Thornton, and J. E. Rice. ESOP-based Toffoli gate cascade generation. In Proc. PACRIM, pages 206–209, 2007. [33] O. Goldreich. On promise problems: A survey. In Theoretical Computer Science: Essays in Memory of Shimon Even, pages 254–290. Springer, 2006. [34] L. K. Grover. A fast quantum mechanical algorithm for database search. In Proc. STOC, pages 212–219, 1996. [35] H. Abraham et al. Qiskit: An open-source framework for quantum computing, 2019. doi: 10.5281/zenodo.2562111. [36] W. Hoeffding. Probability inequalities for sums of bounded random variables. The Collected Works of Wassily Hoeffding, pages 409–426, 1994. [37] X. Hong, Y. Feng, S. Li, and M. Ying. Equivalence checking of dynamic quantum circuits. In Proc. ICCAD, pages 1–8, 2022. [38] X. Hong, M. Ying, X. Z. Y. Feng, and S. Li. Approximate equivalence checking of noisy quantum circuits. In Proc. DAC, pages 637–642, 2021. [39] S.-Y. Huang and K.-T. T. Cheng. Formal Equivalence Checking and Design Debugging. Springer, 2012. [40] M. Incudini, F. Tarocco, R. Mengoni, A. Di Pierro, and A. Mandarino. Computing graph edit distance on quantum devices. Quantum Machine Intelligence, 4(2):24, 2022. [41] H. Katebi and I. L. Markov. Large-scale Boolean matching. In Proc. DATE, pages 771–776, 2010. [42] A. Kissinger and J. van de Wetering. Simulating quantum circuits with ZXcalculus reduced stabiliser decompositions. Quantum Science and Technology, 7(4):044001, 2022. [43] S. Krishnaswamy, H. Ren, N. Modi, and R. Puri. DeltaSyn: An efficient logic difference optimizer for ECO synthesis. In Proc. ICCAD, pages 789–796, 2009. [44] A. Kuehlmann and F. Krohm. Equivalence checking using cuts and heaps. In Proc. DAC, pages 263–268, 1997. [45] C.-F. Lai, J.-H. R. Jiang, and K.-H. Wang. BooM: A decision procedure for Boolean matching with abstraction and dynamic learning. In Proc. DAC, pages 499–504, 2010. [46] R. Landauer. Irreversibility and heat generation in the computing process. IBM Journal of Research and Development, 5(3):183–191, 1961. [47] H. Lee, K. C. Jeong, D. Han, and P. Kim. An algorithm for reversible logic circuit synthesis based on tensor decomposition. ACM Transactions on Quantum Computing, 5(3):1–28, 2024. [48] G. Li, L. Zhou, N. Yu, Y. Ding, M. Ying, and Y. Xie. Projection-based runtime assertions for testing and debugging quantum programs. In Proc. PACMPL (OOPSLA), volume 4, pages 1–29, 2020. [49] X. Li, V. Kulkarni, D. T. Chen, Q. Guan, W. Jiang, N. Xie, S. Xu, and V. Chaudhary. Efficient circuit wire cutting based on commuting groups. In Proc. QCE, 2024. [50] J. Liu, G. T. Byrd, and H. Zhou. Quantum circuits for dynamic runtime assertions in quantum computation. In Proc. ASPLOS, pages 1017–1030, 2020. [51] J. Liu and H. Zhou. Systematic approaches for precise and approximate quantum state runtime assertion. In Proc. HPCA, pages 179–193, 2021. [52] E. Magesan, J. M. Gambetta, and J. Emerson. Characterizing quantum gates via randomized benchmarking. Physical Review A, 85(4):042311, 2012. [53] K. L. McMillan. Interpolation and SAT-based model checking. In Proc. CAV, pages 1–13, 2003. [54] J. Mei, M. Bonsangue, and A. Laarman. Simulating quantum circuits by model counting. In Proc. CAV, pages 555–578. Springer, 2024. [55] D. M. Miller, D. Maslov, and G. W. Dueck. A transformation based algorithm for reversible logic synthesis. In Proc. DAC, pages 318–323, 2003. [56] D. M. Miller, R. Wille, and R. Drechsler. Reducing reversible circuit cost by adding lines. In Proc. ISMVL, pages 217–222, 2010. [57] A. Mishchenko, S. Chatterjee, R. Brayton, and N. Een. Improvements to combinational equivalence checking. In Proc. ICCAD, pages 836–843, 2006. [58] A. Mishchenko and M. Perkowski. Fast heuristic minimization of exclusivesums- of-products. In Proc. RM, 2001. [59] M. A. Nielsen and I. L. Chuang. Quantum Computation and Quantum Information. Cambridge University Press, 2010. [60] P. Niemann, R. Wille, and R. Drechsler. Equivalence checking in multi-level quantum systems. In Proc. RC, pages 201–215, 2014. [61] H. Pashayan, O. Reardon-Smith, K. Korzekwa, and S. D. Bartlett. Fast estimation of outcome probabilities for quantum circuits. PRX Quantum, 3(2):020361, 2022. [62] T. Peng, A. W. Harrow, M. Ozols, and X. Wu. Simulating large quantum circuits on a small quantum computer. Physical Review Letters, 125(15):150504, 2020. [63] A. Peruzzo, J. McClean, P. Shadbolt, M.-H. Yung, X.-Q. Zhou, P. J. Love, A. Aspuru-Guzik, and J. L. O＇brien. A variational eigenvalue solver on a photonic quantum processor. Nature Communications, 5(1):4213, 2014. [64] 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. [65] H. Riener et al. Exact synthesis of ESOP forms. In Proc. IWSBP, pages 177–194, 2020. [66] M. Saeedi and I. L. Markov. Synthesis and optimization of reversible circuits—a survey. ACM Computing Surveys, 45(2):1–34, 2013. [67] P. W. Shor. Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. SIAM Review, 41(2):303–332, 1999. [68] D. R. Simon. On the power of quantum computation. SIAM Journal on Computing, 26(5):1474–1483, 1997. [69] M. Sistla, S. Chaudhuri, and T. Reps. Symbolic quantum simulation with Quasimodo. In Proc. CAV, pages 213–225. Springer, 2023. [70] F. Somenzi. CUDD: CU decision diagram package (release 2.4.2), 2012. [71] W. Tang, T. Tomesh, M. Suchara, J. Larson, and M. Martonosi. CutQC: using small quantum computers for large quantum circuit evaluations. In Proc. ASPLOS, pages 473–486, 2021. [72] Y.-H. Tsai, J.-H. R. Jiang, and C.-S. Jhang. Bit-slicing the Hilbert space: Scaling up accurate quantum circuit simulation. In Proc. DAC, pages 439–444, 2021. [73] L. G. Valiant and V. V. Vazirani. NP is as easy as detecting unique solutions. In Proc. STOC, pages 458–463, 1985. [74] C. Van Eijk. Sequential equivalence checking based on structural similarities. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 19(7):814–819, 2000. [75] M. Venere, A. Barenghi, and G. Pelosi. A quantum method to match vector Boolean functions using Simon’s solver. In Proc. ICCD, pages 542–549. IEEE, 2024. [76] G. F. Viamontes, I. L. Markov, and J. P. Hayes. Checking equivalence of quantum circuits and states. In Proc. ICCAD, pages 69–74, 2007. [77] Q. Wang, R. Li, and M. Ying. Equivalence checking of sequential quantum circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 41(9):3143–3156, 2021. [78] Q. S. Wang, J. Y. Liu, and M. S. Ying. Equivalence checking of quantum finite-state machines. Journal of Computer and System Sciences, 116:1–21, 2021. [79] 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. [80] C.-Y. Wei and J.-H. R. Jiang. Don’t-care aware ESOP extraction via reduced decomposition-tree exploration. In Proc. DAC, 2023. [81] C.-Y. Wei, Y.-H. Tsai, C.-S. Jhang, and J.-H. R. Jiang. Accurate BDD-based unitary operator manipulation for scalable and robust quantum circuit verification. In Proc. DAC, pages 523–528, 2022. [82] D. Wierichs, C. Gogolin, and M. Kastoryano. Avoiding local minima in variational quantum eigensolvers with the natural gradient optimizer. Physical Review Research, 2(4):043246, 2020. [83] R. Wille, D. Große, D. M. Miller, and R. Drechsler. Equivalence checking of reversible circuits. In Proc. ISMVL, pages 324–330, 2009. [84] 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. ISMVL, pages 220–225, 2008. [85] H. Witharana, Y. Lyu, S. Charles, and P. Mishra. A survey on assertion-based hardware verification. ACM Computing Surveys, 54(11s):1–33, 2022. [86] S. Yamashita and I. L. Markov. Fast equivalence-checking for quantum circuits. In Proc. NANOARCH, pages 23–28, 2010. [87] M. Ying and Y. Feng. Model checking quantum systems: Principles and algorithms. Cambridge University Press, 2021. [88] N. Yu and J. Palsberg. Quantum abstract interpretation. In Proc. PLDI, pages 542–558, 2021. [89] S.-X. Zhang, J. Allcock, Z.-Q. Wan, S. Liu, J. Sun, H. Yu, X.-H. Yang, J. Qiu, Z. Ye, Y.-Q. Chen, et al. TensorCircuit: a quantum software framework for the NISQ era. Quantum, 7:912, 2023. [90] A. Zulehner et al. Accuracy and compactness in decision diagrams for quantum computation. In Proc. DATE, pages 280–283, 2019. [91] 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, 2018. | - |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/101240 | - |
| dc.description.abstract | 驗證對於確保量子計算系統的正確性至關重要。然而，不同於傳統計算系統的驗證技術之成熟，量子計算至今仍嚴重缺乏系統化和自動化的驗證方法。我們發展了量子電路驗證的方法與框架，同時涵蓋靜態與動態驗證技術，包括模擬、等價性檢查、布林匹配以及動態斷言。
我們的量子電路模擬工具允許使用者計算滿足自定義性質的量子態的精確機率或期望值，為量子程式設計與測試提供有效的手段。實驗中的案例研究顯示，我們的模擬工具能夠超越現有工具的能力，提供精確的量子電路分析和驗證。 針對形式化驗證方法，有鑑於現有的等價性檢查方法缺乏足夠的通用性，難以處理日趨複雜的高級電路特性，因此我們提出了一個組合量子電路的一般模型，並由此定義了量子電路的部分等價關係，以及開發了相應的等價性檢查演算法。我們相信這些技術能夠涵蓋絕大多數──若非全部──的組合量子電路應用場景。從等價性的另一個角度來說，我們提供了第一個針對可逆邏輯電路的布林匹配問題的完整研究，包含傳統或量子演算法及其計算複雜度。值得注意的是，針對尋找輸入端的取反與排列以使兩個電路等價的問題，我們開發了多項式時間的量子演算法，而其經典對應方法的複雜度則為指數級。此一結果可被認為是設計自動化領域中首個指數級加速的演算法。 針對動態驗證，藉由利用量子電路的消失態，我們提出了第一個量子電路動態斷言的通用框架，並能夠在錯誤偵測能力與斷言電路複雜度之間提供靈活的權衡空間。實驗顯示了我們的方法在通用性與有效性方面的獨特優勢，能夠提升量子電路在各類基準測試中的執行效率與成功率。 本研究為量子程式驗證的未來奠定了廣泛的基礎，並希望所提出的方法與框架能推動量子程式設計自動化的發展。 | zh_TW |
| dc.description.abstract | Verification is essential for ensuring the correctness of quantum computing systems, yet systematic and automated approaches remain far behind their classical counterparts. We present methods and frameworks for quantum circuit verification, covering both static and dynamic approaches, including simulation, equivalence checking, Boolean matching, and runtime assertion.
Our simulation tool allows users to query exact probabilities or expectation values of user-defined quantum state properties, thereby enhancing program design and testing. Case studies demonstrate its unique ability to support exact quantum circuit analysis and verification beyond the capabilities of existing tools. For formal verification, motivated by the lack of generality of existing equivalence checking methods in handling advanced circuit features, we propose a general model of composable quantum circuits, formalize partial equivalence relations, and develop corresponding algorithms, which are capable of encompassing most, if not all, composable quantum circuits. From another perspective on equivalence, we provide the first comprehensive characterization of algorithms and the computational complexity of Boolean matching reversible logic circuits. Notably, we develop polynomial-time quantum algorithms that identify input negations and permutations to make two circuits equivalent, while the classical complexity is exponential. This result arguably achieves the first exponential speedup for a design automation task. For dynamic verification, we introduce the first general framework for quantum circuit runtime assertion by exploring vanishing states of quantum programs, offering flexible trade-offs between error-detection power and assertion circuit complexity. Experiments show the unique benefits of our method in generality and effectiveness, improving quantum circuit execution efficiency and success rates in various benchmarks. This work establishes a versatile foundation for the future of quantum program verification, and we hope that the proposed methods and frameworks help advance the automation of quantum program design. | en |
| dc.description.provenance | Submitted by admin ntu (admin@lib.ntu.edu.tw) on 2025-12-31T16:26:19Z No. of bitstreams: 0 | en |
| dc.description.provenance | Made available in DSpace on 2025-12-31T16:26:19Z (GMT). No. of bitstreams: 0 | en |
| dc.description.tableofcontents | 致謝 i
摘要 iii Abstract v Contents vii List of Figures xi List of Tables xiii Chapter 1 Introduction 1 1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Our Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.3 An Overview of This Dissertation . . . . . . . . . . . . . . . . . . 8 Chapter 2 Related Work 11 Chapter 3 Background 15 3.1 Boolean Function and Binary Decision Diagram . . . . . . . . . . 15 3.2 Quantum Computation . . . . . . . . . . . . . . . . . . . . . . . 17 3.3 Bit-slicing and Algebraic Representations for Vectors and Matrices 19 Chapter 4 SliQSim: A Quantum Circuit Simulator and Solver for Probability and Statistics Queries 23 4.1 Tool Architecture . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 4.2 Features and Demo . . . . . . . . . . . . . . . . . . . . . . . . . . 25 4.3 Case Studies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 4.3.1 Grover’s Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . 32 4.3.2 Simon’s Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . 33 4.3.3 N-I Equivalence Boolean Matching . . . . . . . . . . . . . . . . 34 Chapter 5 Partial Equivalence Checking for Distributed and Dynamic Quantum Circuits 37 5.1 Model of Quantum Circuit Operation . . . . . . . . . . . . . . . 37 5.2 Partial Equivalence Between Quantum Circuits . . . . . . . . . . 47 5.3 Comparison of Different Equivalences . . . . . . . . . . . . . . . . 55 5.4 Necessary and Sufficient Conditions of Partial Equivalence . . . . 60 5.5 Algorithms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 5.5.1 Strong Partial Equivalence Checking Algorithm . . . . . . . . . 75 5.5.2 Unweighted, Clean-Ancilla-Free Strong Partial Equivalence Checking Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 5.5.3 RUS-Type Weak Partial Equivalence Checking Algorithm . . . . 79 5.6 Experimental Results . . . . . . . . . . . . . . . . . . . . . . . . 80 Chapter 6 Boolean Matching Reversible Circuits: Algorithm and Complexity 97 6.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 6.1.1 Simon’s Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . 97 6.2 Problem Formulation . . . . . . . . . . . . . . . . . . . . . . . . . 98 6.2.1 Boolean Matching Reversible Circuits without Ancilla Bits . . . 100 6.2.2 Boolean Matching Reversible Circuits with Ancilla Bits . . . . . 101 6.3 Equivalences without Ancilla Bits . . . . . . . . . . . . . . . . . . 103 6.3.1 I-N Equivalence without Ancilla Bits . . . . . . . . . . . . . . . 104 6.3.2 I-P Equivalence without Ancilla Bits . . . . . . . . . . . . . . . 105 6.3.3 I-NP Equivalence without Ancilla Bits . . . . . . . . . . . . . . 106 6.3.4 P-I Equivalence without Ancilla Bits . . . . . . . . . . . . . . . 107 6.3.5 N-I Equivalence without Ancilla Bits . . . . . . . . . . . . . . . 108 6.3.6 NP-I Equivalence without Ancilla Bits . . . . . . . . . . . . . . 115 6.3.7 P-N Equivalence without Ancilla Bits . . . . . . . . . . . . . . . 118 6.3.8 N-P Equivalence without Ancilla Bits . . . . . . . . . . . . . . . 118 6.3.9 Hardness of N-N Equivalence . . . . . . . . . . . . . . . . . . . 119 6.3.10 Hardness of P-P Equivalence . . . . . . . . . . . . . . . . . . . . 122 6.4 Equivalences with Ancilla Bits . . . . . . . . . . . . . . . . . . . 124 6.4.1 I-N Equivalence with Ancilla Bits . . . . . . . . . . . . . . . . . 125 6.4.2 I-P Equivalence with Ancilla Bits . . . . . . . . . . . . . . . . . 126 6.4.3 I-NP Equivalence with Ancilla Bits . . . . . . . . . . . . . . . . 128 6.4.4 N-I Equivalence with Ancilla Bits . . . . . . . . . . . . . . . . . 130 6.4.5 P-I Equivalence with Ancilla Bits . . . . . . . . . . . . . . . . . 131 6.4.6 NP-I Equivalence with Ancilla Bits . . . . . . . . . . . . . . . . 133 6.4.7 Hardness of N-P Equivalence and P-N Equivalences with Ancilla Bits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134 Chapter 7 VanQiRA: A Vanishing-State-Based Framework for Quantum Circuit Runtime Assertion 137 7.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 7.1.1 Vanishing States and State Sparsity Checking . . . . . . . . . . 137 7.1.2 Boolean Oracle Synthesis . . . . . . . . . . . . . . . . . . . . . . 138 7.2 Problem Formulation . . . . . . . . . . . . . . . . . . . . . . . . . 139 7.3 Vanishing-State-Based Quantum Runtime Assertion . . . . . . . 143 7.4 Vanishing State Generation . . . . . . . . . . . . . . . . . . . . . 148 7.4.1 Amplitude-Cancellation Method . . . . . . . . . . . . . . . . . . 148 7.4.2 Neighbor-Coupling Method . . . . . . . . . . . . . . . . . . . . . 150 7.5 BDD-Based Assertion Circuit Synthesis . . . . . . . . . . . . . . 152 7.6 Experimental Results . . . . . . . . . . . . . . . . . . . . . . . . 154 7.6.1 Effectiveness of Assertion . . . . . . . . . . . . . . . . . . . . . . 155 7.6.2 Comparison to Prior Work . . . . . . . . . . . . . . . . . . . . . 158 7.6.3 Efficiency of Assertion Circuit Generation . . . . . . . . . . . . 161 7.6.4 Effectiveness of Generated Assertion Circuits . . . . . . . . . . . 162 7.6.5 Effect of Assertion Positions . . . . . . . . . . . . . . . . . . . . 164 7.6.6 Trade-Off Between Coverage and Assertion Cost . . . . . . . . . 166 Chapter 8 Conclusion 167 References 171 | - |
| dc.language.iso | en | - |
| dc.subject | 量子計算 | - |
| dc.subject | 驗證 | - |
| dc.subject | 模擬 | - |
| dc.subject | 等價性檢查 | - |
| dc.subject | 布林匹配 | - |
| dc.subject | 動態斷言 | - |
| dc.subject | Quantum computation | - |
| dc.subject | Verification | - |
| dc.subject | Simulation | - |
| dc.subject | Equivalence checking | - |
| dc.subject | Boolean matching | - |
| dc.subject | Runtime assertion | - |
| dc.title | 量子電路驗證方法與架構：模擬、等價性檢查與動態斷言 | zh_TW |
| dc.title | Methods and Framework for Quantum Circuit Verification: Simulation, Equivalence Checking, and Runtime Assertion | en |
| dc.type | Thesis | - |
| dc.date.schoolyear | 114-1 | - |
| dc.description.degree | 博士 | - |
| dc.contributor.oralexamcommittee | 邱大維;鄭皓中;鐘楷閔;陳郁方;賴青沂 | zh_TW |
| dc.contributor.oralexamcommittee | Dah-Wei Chiou;Hao-Chung Cheng;Kai-Min Chung;Yu-Fang Chen;Ching-Yi Lai | en |
| dc.subject.keyword | 量子計算,驗證模擬等價性檢查布林匹配動態斷言 | zh_TW |
| dc.subject.keyword | Quantum computation,VerificationSimulationEquivalence checkingBoolean matchingRuntime assertion | en |
| dc.relation.page | 181 | - |
| dc.identifier.doi | 10.6342/NTU202501295 | - |
| dc.rights.note | 同意授權(全球公開) | - |
| dc.date.accepted | 2025-12-01 | - |
| dc.contributor.author-college | 重點科技研究學院 | - |
| dc.contributor.author-dept | 積體電路設計與自動化學位學程 | - |
| dc.date.embargo-lift | 2030-11-23 | - |
| 顯示於系所單位： | 積體電路設計與自動化學位學程 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-114-1.pdf 此日期後於網路公開 2030-11-23 | 1.6 MB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。