運用二元決策圖進行可逆邏輯合成和量子電路驗證

Abstract

量子技術的迅速進展引發了各種量子計算應用的出現。與此同時，傳統計算機在處理量子資料的指數級複雜性方面面臨著挑戰。隨著決策圖在傳統電子設計自動化領域中提供了處理布林函數指數級複雜性的緊湊高效之數據結構，近年來在量子計算領域中，決策圖也受到了越來越多的關注。它們展示了在表示高維量子資料和實現各種量子任務(如量子電路模擬和驗證)方面的有效性。本研究探討了二進制決策圖在量子計算中的應用。我們擴展了最近的基於位元切片的布林決策圖框架，來支援積之互斥或表示式的合成用於布林預示實現、 量子斷言電路合成和量子電路驗證。整合的框架借助決策圖的優勢，在處理量子實體時提供了效率和可擴展性，以支持各種量子任務。此外，其精確性特性解決了先前方法中存在的精度損失問題，實現了精確計算，增強了該框架在驗證場景中的適用性。實驗結果顯示，所提出的布林積之互斥或表示式合成方法在運行時間方面提供高達29倍（平均12倍）的加速，並且在記憶體使用方面改進了28倍（平均13倍）。對於完全指定的函數，所獲得的解的品質接近於通過詳盡探索獲得的精確最優解。此外，對於不完全指定的函數，該方法能夠大幅簡化布林積之互斥或表示式考慮不指定部分。關於量子運行時間斷言電路合成，所提出的方法有效地處理高達一百個量子位元電路，並且能夠在斷言電路大小和錯誤檢測率之間取得平衡。此外，在量子電路驗證方面，我們的方法在處理大型電路方面表現優於先前的方法，並能夠實現精確的等效性檢查結果。

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.