QCEC: A JKQ tool for quantum circuit equivalence checking

被引:5
作者
Burgholzer, Lukas [1 ]
Wille, Robert [1 ,2 ]
机构
[1] Johannes Kepler Univ Linz, Inst Integrated Circuits, A-4040 Linz, Austria
[2] Software Competence Ctr Hagenberg GmbH SCCH, A-4232 Hagenberg, Austria
关键词
Quantum computing; Equivalence checking; Decision diagrams;
D O I
10.1016/j.simpa.2020.100051
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Quantum computing is gaining serious momentum in these days. With increasing capabilities of corresponding devices also comes the need for efficient and automated tools to design them. Verification, i.e., ensuring that the originally intended functionality of a quantum algorithm/circuit is preserved throughout all layers of abstraction during the design process, is a vital part of the quantum software stack. In this work, we present QCEC, a tool for quantum circuit equivalence checking which is part of the JKQ toolset for quantum computing. By exploiting characteristics unique to quantum computing, the tool allows users to efficiently verify the equivalence of two quantum circuits using a variety of methods and strategies.
引用
收藏
页数:3
相关论文
共 50 条
[31]   Automated equivalence checking of switch level circuits [J].
Jolly, S ;
Parashkevov, A ;
McDougall, T .
39TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2002, 2002, :299-304
[32]   Equivalence Checking of Array-Intensive Programs [J].
Karfa, C. ;
Banerjee, K. ;
Sarkar, D. ;
Mandal, C. .
2011 IEEE COMPUTER SOCIETY ANNUAL SYMPOSIUM ON VLSI (ISVLSI), 2011, :156-161
[33]   Equivalence Checking for Compiler Transformations in Behavioral Synthesis [J].
Yang, Zhenkun ;
Hao, Kecheng ;
Cong, Kai ;
Ray, Sandip ;
Xie, Fei .
2013 IEEE 31ST INTERNATIONAL CONFERENCE ON COMPUTER DESIGN (ICCD), 2013, :491-494
[34]   Combinational equivalence checking through function transformation [J].
Kwak, HH ;
Moon, IH ;
Kukula, JH ;
Shiple, TR .
IEEE/ACM INTERNATIONAL CONFERENCE ON CAD-02, DIGEST OF TECHNICAL PAPERS, 2002, :526-533
[35]   AQUILA: An equivalence checking system for large sequential designs [J].
Huang, SY ;
Cheng, KT ;
Chen, KC ;
Huang, CY ;
Brewer, F .
IEEE TRANSACTIONS ON COMPUTERS, 2000, 49 (05) :443-464
[36]   Memory modeling in ESL-RTL equivalence checking [J].
Koelbl, Alfred ;
Burch, Jerry R. ;
Pixley, Carl .
2007 44TH ACM/IEEE DESIGN AUTOMATION CONFERENCE, VOLS 1 AND 2, 2007, :205-+
[37]   Sequential Equivalence Checking of Clock-Gated Circuits [J].
Dai, Yu-Yun ;
Khoo, Kei-Yong ;
Brayton, Robert K. .
2015 52ND ACM/EDAC/IEEE DESIGN AUTOMATION CONFERENCE (DAC), 2015,
[38]   Proving Termination via Measure Transfer in Equivalence Checking [J].
Milovanovic, Dragana ;
Fuhs, Carsten ;
Bucev, Mario ;
Kuncak, Viktor .
INTEGRATED FORMAL METHODS, IFM 2024, 2025, 15234 :75-84
[39]   Probabilistic equivalence checking of multiple-valued functions [J].
Dubrova, E ;
Sack, H .
JOURNAL OF MULTIPLE-VALUED LOGIC AND SOFT COMPUTING, 2004, 10 (04) :395-414
[40]   On Neural Network Equivalence Checking Using SMT Solvers [J].
Eleftheriadis, Charis ;
Kekatos, Nikolaos ;
Katsaros, Panagiotis ;
Tripakis, Stavros .
FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, FORMATS 2022, 2022, 13465 :237-257