Skip to content

Commit

Permalink
Release 1.6
Browse files Browse the repository at this point in the history 
* Random Stimuli Generation for the Verification of Quantum Ciruits (ASP-DAC 2021)
* Introduce option for explicitly storing the statevector as a result of simulation methods
* Fixed some file headers
* Unified JSON handling
* Removed some unneccessary members which are also in the Configuration struct

Signed-off-by: Lukas Burgholzer <lukas.burgholzer@jku.at>
  • Loading branch information
@burgholzer
burgholzer committed Nov 17, 2020
1 parent 64e0619 commit 7f5b692
Show file tree
Hide file tree
Showing 26 changed files with 1,040 additions and 259 deletions.
2 changes: 1 addition & 1 deletion CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ if(${CMAKE_VERSION} VERSION_LESS 3.12)
endif()

project(qcec
VERSION 1.5.0
VERSION 1.6.0
DESCRIPTION "A JKQ tool for quantum circuit equivalence checking (JKQ QCEC)"
LANGUAGES CXX)

Expand Down
36 changes: 31 additions & 5 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,18 +2,21 @@
[![Travis (.com) branch](https://img.shields.io/travis/com/iic-jku/qcec/master?logo=travis&style=plastic)](https://travis-ci.com/iic-jku/qcec)
[![Codecov branch](https://img.shields.io/codecov/c/github/iic-jku/qcec/master?label=codecov&logo=codecov&style=plastic)](https://codecov.io/gh/iic-jku/qcec)
![GitHub](https://img.shields.io/github/license/iic-jku/qcec?style=plastic)
[![toolset: JKQ](https://img.shields.io/badge/toolset-JKQ-blue?style=plastic)](https://github.com/iic-jku/jkq)
[![arXiv](https://img.shields.io/static/v1?label=arXiv&message=2004.08420&color=inactive&style=plastic)](https://arxiv.org/abs/2004.08420)
[![arXiv](https://img.shields.io/static/v1?label=arXiv&message=2009.02376&color=inactive&style=plastic)](https://arxiv.org/abs/2009.02376)
[![toolset: JKQ](https://img.shields.io/badge/toolset-JKQ-blue?style=plastic)](https://github.com/iic-jku/jkq)
[![arXiv](https://img.shields.io/static/v1?label=arXiv&message=2011.07288&color=inactive&style=plastic)](https://arxiv.org/abs/2011.07288)

# JKQ QCEC - A JKQ tool for **Q**uantum **C**ircuit **E**quivalence **C**hecking

A JKQ tool for Quantum Circuit Equivalence Checking by the [Institute for Integrated Circuits](http://iic.jku.at/eda/) at the [Johannes Kepler University Linz](https://jku.at) based on methods proposed in [[1]](https://arxiv.org/abs/2004.08420), [[2]](https://arxiv.org/abs/2009.02376).
A JKQ tool for Quantum Circuit Equivalence Checking by the [Institute for Integrated Circuits](http://iic.jku.at/eda/) at the [Johannes Kepler University Linz](https://jku.at) based on methods proposed in [[1]](https://arxiv.org/abs/2004.08420), [[2]](https://arxiv.org/abs/2009.02376), [[3]](https://arxiv.org/abs/2011.07288).

[[1]](https://arxiv.org/abs/2004.08420) L. Burgholzer and R. Wille. **"Advanced Equivalence Checking for Quantum Circuits"**. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems (TCAD), 2021 (pre-print [arXiv:2004.08420](https://arxiv.org/abs/2004.08420))

[[2]](https://arxiv.org/abs/2009.02376) L. Burgholzer, R. Raymond, and R. Wille. **"Verifying Results of the IBM Qiskit Quantum Circuit Compilation Flow"**. In International Conference on Quantum Computing and Engineering (QCE), 2020 (pre-print [arXiv:2009.02376](https://arxiv.org/abs/2009.02376))

[[3]](https://arxiv.org/abs/2011.07288) L. Burgholzer, R. Kueng, and R. Wille. **"Random Stimuli Generation for the Verification of Quantum Circuits"**. In Asia and South Pacific Design Automation Conference (ASP-DAC), 2021 (pre-print [arxiv:2011.07288](https://arxiv.org/abs/2011.07288))

This tool can be used for checking the equivalence of two quantum circuits provided in any of the following formats:
* `Real` (e.g. from [RevLib](http://revlib.org)),
* `OpenQASM` (e.g. used by IBM's [Qiskit](https://github.com/Qiskit/qiskit)),
Expand All @@ -22,12 +25,15 @@ This tool can be used for checking the equivalence of two quantum circuits provi

with the following available methods:
- **Reference** - Construct and compare the DD for both circuits [[1, Section III.B]](https://arxiv.org/pdf/2004.08420.pdf#page=5),
- ![G \rightarrow \mathbb{I} \leftarrow G'](https://render.githubusercontent.com/render/math?math=G%20%5Crightarrow%20%5Cmathbb%7BI%7D%20%5Cleftarrow%20G') - Starting from the identity *I*, either apply gates from *G* or (inverted) gates from *G'* according to one of the following strategies [[1, Section IV.A]](https://arxiv.org/pdf/2004.08420.pdf#page=6)
- ![G \rightarrow \mathbb{I} \leftarrow G'](https://render.githubusercontent.com/render/math?math=G%20%5Crightarrow%20%5Cmathbb%7BI%7D%20%5Cleftarrow%20G') - Starting from the identity *I*, either apply gates from *G* or (inverted) gates from *G'* according to one of the following strategies [[1, Section IV.A]](https://arxiv.org/pdf/2004.08420.pdf#page=6):
- **Naive** - Alternate between applications of *G* and *G'* [[1, Section V.A]](https://arxiv.org/pdf/2004.08420.pdf#page=8),
- **Proportional** - Proportionally apply gates according to the gate count ratio of *G* and *G'* [[1, Section V.B]](https://arxiv.org/pdf/2004.08420.pdf#page=8),
- **Lookahead** - Always apply the gate yielding the smaller DD [[1, Section V.C]](https://arxiv.org/pdf/2004.08420.pdf#page=8),
- **Simulation** - Conduct simulation runs to prove non-equivalence or give a strong indication of equivalence [[1, Section IV.B]](https://arxiv.org/pdf/2004.08420.pdf#page=7),
- **Verification of compilation results** - A dedicated scheme for verifying results of the IBM Qiskit Compilation Flow explicitly exploiting certain knowledge about the compilation process. [[2]](https://arxiv.org/abs/2009.02376)
- **Simulation** - Conduct simulation runs to prove non-equivalence or give a strong indication of equivalence [[1, Section IV.B]](https://arxiv.org/pdf/2004.08420.pdf#page=3) using:
- **Classical Stimuli** - computational basis states [[1, Section IV.B]](https://arxiv.org/pdf/2004.08420.pdf#page=7), [[3, Section 3.1]](https://arxiv.org/pdf/2011.07288.pdf#page=3)
- **Local Quantum Stimuli** - each qubit value is independently chosen from any of the six basis states (|0>, |1>, |+>, |->, |L>, |R>) [[3, Section 3.2]](https://arxiv.org/pdf/2011.07288.pdf#page=4)
- **Global Quantum Stimuli** - random stabilizer states [[3, Section 3.3]](https://arxiv.org/pdf/2011.07288.pdf#page=4)
- **Verification of compilation results** - A dedicated scheme for verifying results of the IBM Qiskit Compilation Flow explicitly exploiting certain knowledge about the compilation process. [[2]](https://arxiv.org/pdf/2009.02376.pdf)

The tool builds upon [our decision diagram (DD) package](https://github.com/iic-jku/dd_package.git) as well as [our quantum functionality representation (QFR)](https://github.com/iic-jku/qfr.git). For more information, please visit [iic.jku.at/eda/research/quantum_verification](http://iic.jku.at/eda/research/quantum_verification). If you want to visually explore decision diagrams for quantum computing, check out our installation-free web-tool [JKQ DDVis](https://iic.jku.at/eda/research/quantum_dd/tool/).

Expand Down Expand Up @@ -56,8 +62,11 @@ Params:
tolerance – Numerical tolerance used during computation
nsims – Number of simulations to conduct (for simulation method)
fidelity – Fidelity limit for comparison (for simulation method)
stimuliType - Type of stimuli to use (for simulation method: *classical* | localquantum | globalquantum)
csv – Create CSV string for result
statistics – Print statistics
storeCEXinput: Store counterexample input state vector (for simulation method)
storeCEXoutput: Store resulting counterexample state vectors (for simulation method)
swapGateFusion – Optimization pass reconstructing SWAP operations
singleQubitGateFusion – Optimization pass fusing consecutive single qubit gates
removeDiagonalGatesBeforeMeasure – Optimization pass removing diagonal gates before measurements
Expand All @@ -70,8 +79,11 @@ def verify(file1: Union[str, bytes, PathLike],
tolerance: float = 1e-13,
nsims: int = 16,
fidelity: float = 0.999,
stimuliType: StimuliType = StimuliType.classical,
csv: bool = False,
statistics: bool = False,
storeCEXinput: bool = False,
storeCEXoutput: bool = False,
swapGateFusion: bool = False,
singleQubitGateFusion: bool = False,
removeDiagonalGatesBeforeMeasure: bool = False) -> object
Expand Down Expand Up @@ -150,6 +162,7 @@ In order to build the library execute the following in the project's main direct
```
The following CMake targets are available
- `qcec_app`: The commandline executable
- `qcec_sim_app`: Commandline tool dedicated for simulative verification
- `qcec`: The standalone library
- `qcec_example`: A small commandline demo example
- `qcec_test`: Unit tests using GoogleTest
Expand Down Expand Up @@ -199,5 +212,18 @@ If you use our tool for your research, we will be thankful if you refer to it by

</details>

<details open>
<summary>[3] L. Burgholzer, R. Kueng, and R. Wille. "Random Stimuli Generation for the Verification of Quantum Circuits". Asia and South Pacific Design Automation Conference (ASP-DAC), 2021</summary>

```bibtex
@inproceedings{burgholzer2021randomStimuliGenerationQuantum,
title = {Random stimuli generation for the verification of quantum circuits},
booktitle = {Asia and South Pacific Design Automation Conf.},
author = {Burgholzer, Lukas and Richard, Kueng and Wille, Robert},
year = {2021}
}
```

</details>


11 changes: 11 additions & 0 deletions apps/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,3 +20,14 @@ install(TARGETS ${PROJECT_NAME}_app
RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR})

set_target_properties(${PROJECT_NAME}_app PROPERTIES EXPORT_NAME ${PROJECT_NAME}_app)

add_executable(${PROJECT_NAME}_sim_app ${CMAKE_CURRENT_SOURCE_DIR}/sim_app.cpp)
target_compile_features(${PROJECT_NAME}_sim_app PUBLIC cxx_std_14)
set_target_properties(${PROJECT_NAME}_sim_app PROPERTIES CXX_EXTENSIONS OFF)
target_link_libraries(${PROJECT_NAME}_sim_app PRIVATE JKQ::${PROJECT_NAME})
if(MSVC)
target_compile_options(${PROJECT_NAME}_sim_app PUBLIC "/W4" "$<$<CONFIG:RELEASE>:/O2 /GL>")
target_link_options(${PROJECT_NAME}_sim_app PUBLIC "$<$<CONFIG:Release>:/LTCG>")
else()
target_compile_options(${PROJECT_NAME}_sim_app PUBLIC -Wall $<$<CONFIG:DEBUG>:-g3 -Og -Wextra -Wpedantic -pedantic> $<$<CONFIG:RELEASE>:-O3 -mtune=native -march=native -DNDEBUG -g0>)
endif()
58 changes: 42 additions & 16 deletions apps/app.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,26 +14,29 @@
#include "PowerOfSimulationEquivalenceChecker.hpp"

void show_usage(const std::string& name) {
std::cerr << "Usage: " << name << " <PATH_TO_FILE_1> <PATH_TO_FILE_2> (--method <method>) " << std::endl;
std::cerr << "Supported file formats: " << std::endl;
std::cerr << " .real " << std::endl;
std::cerr << " .qasm " << std::endl;
std::cerr << " .tfc " << std::endl;
std::cerr << " .qc " << std::endl;
std::cerr << "Available methods: " << std::endl;
std::cerr << " reference " << std::endl;
std::cerr << " naive " << std::endl;
std::cerr << " proportional (default) " << std::endl;
std::cerr << " lookahead " << std::endl;
std::cerr << " simulation " << std::endl;
std::cerr << " compilationflow " << std::endl;
std::cerr << "Result Options: " << std::endl;
std::cerr << " --ps: Print statistics " << std::endl;
std::cerr << " --csv: Print results as csv string " << std::endl;
std::cerr << "Usage: " << name << " <PATH_TO_FILE_1> <PATH_TO_FILE_2> (--method <method>) " << std::endl;
std::cerr << "Supported file formats: " << std::endl;
std::cerr << " .real " << std::endl;
std::cerr << " .qasm " << std::endl;
std::cerr << " .tfc " << std::endl;
std::cerr << " .qc " << std::endl;
std::cerr << "Available methods: " << std::endl;
std::cerr << " reference " << std::endl;
std::cerr << " naive " << std::endl;
std::cerr << " proportional (default) " << std::endl;
std::cerr << " lookahead " << std::endl;
std::cerr << " simulation (using 'classical', 'localquantum', or 'globalquantum' stimuli) " << std::endl;
std::cerr << " compilationflow " << std::endl;
std::cerr << "Result Options: " << std::endl;
std::cerr << " --ps: Print statistics " << std::endl;
std::cerr << " --csv: Print results as csv string " << std::endl;
std::cerr << " --storeCEXinput: Store counterexample input state vector (for simulation method) " << std::endl;
std::cerr << " --storeCEXoutput: Store resulting counterexample state vectors (for simulation method)" << std::endl;
std::cerr << "Verification Parameters: " << std::endl;
std::cerr << " --tol e (default 1e-13): Numerical tolerance used during computation " << std::endl;
std::cerr << " --nsims r (default 16): Number of simulations to conduct (for simulation method)" << std::endl;
std::cerr << " --fid F (default 0.999): Fidelity limit for comparison (for simulation method) " << std::endl;
std::cerr << " --stimuliType s (default 'classical'): Type of stimuli to use (for simulation method) " << std::endl;
std::cerr << "Optimization Options: " << std::endl;
std::cerr << " --swapGateFusion: reconstruct SWAP operations " << std::endl;
std::cerr << " --singleQubitGateFusion: fuse consecutive single qubit gates " << std::endl;
Expand Down Expand Up @@ -146,6 +149,29 @@ int main(int argc, char** argv){
show_usage(argv[0]);
return 1;
}
} else if(cmd == "--stimuliType") {
++i;
if (i >= argc) {
show_usage(argv[0]);
return 1;
}
cmd = argv[i];
std::transform(cmd.begin(), cmd.end(), cmd.begin(), [](unsigned char c) { return ::tolower(c); });

if (cmd == "classical") {
config.stimuliType = ec::Classical;
} else if (cmd == "localquantum") {
config.stimuliType = ec::LocalQuantum;
} else if (cmd == "globalquantum") {
config.stimuliType = ec::GlobalQuantum;
} else {
show_usage(argv[0]);
return 1;
}
} else if(cmd == "--storeCEXinput") {
config.storeCEXinput = true;
} else if(cmd == "--storeCEXoutput") {
config.storeCEXoutput = true;
} else if (cmd == "--swapGateFusion") {
config.swapGateFusion = true;
} else if (cmd == "--singleQubitGateFusion") {
Expand Down
Loading

0 comments on commit 7f5b692

Please sign in to comment.