SQbricks

SQbricks is a research prototype for automated equivalence checking of hybrid quantum circuits.

In SQbricks, a hybrid circuit refers to a quantum circuit that includes quantum operations (unitaries), measurements, and classical control.

SQbricks is composed of two complementary tools: SQbricks-Lift (SQL) and SQbricks-Verif (SQV).

Technical documentation | Documentation technique | Roadmap

SQbricks-Lift (SQL)

SQbricks-Lift implements a transformation based on the deferred measurement principle, which pushes all Initialization (I) to the beginning and Measurements (M) to the end of the circuit. This enables the use of standard unitary verification tools in the broader context of hybrid circuits — effectively lifting them to this extended setting.

Two transformation modes are provided:

IUM: Returns an Initialization–Unitary–Measurement (IUM) decomposition of the circuit.
U: Returns only the unitary part of the circuit.

SQbricks-Verif (SQV)

SQbricks-Verif is used to verify the equivalence of two unitary circuits, even if they differ in the number of qubits. This supports the common scenario where auxiliary or "garbage" qubits are added for intermediate computations.

Two verification algorithms are available:

Parallel Algorithm (par): Executes both circuits on the same input and compares their outputs.
Sequence Algorithm (seq): Executes one circuit followed by the inverse of the other and verifies that the output matches the initial input state. The seq algorithm typically yields better results than par, but requires that at least one of the circuits has no ancilla.

Research and provenance

SQbricks was initially developed in the Qbricks repository, under Artifacts/SQbricks/SQbricks. This focused repository places SQbricks at its root while preserving the history of the SQbricks subproject, its copyright notices, and its license.

The main scientific references are:

Jérome Ricciardi, Sébastien Bardin, Christophe Chareton, and Benoît Valiron, Quantum Circuit Equivalence Checking: A Tractable Bridge From Unitary to Hybrid Circuits, arXiv:2511.22523, 2025;
Jérome Ricciardi, Practical verification of quantum circuit transformations, doctoral thesis, 2026.

The inspection prototype uses Quantikz2 for LaTeX circuit diagrams. Its reference is Alastair Kay, Tutorial on the Quantikz Package, arXiv:1809.03842.

For academic use, CITATION.cff provides machine-readable citation metadata.

License

SQbricks is distributed under the GNU Lesser General Public License version 2.1; see LICENSE. Third-party tools and benchmark sources retain their own licenses:

Docker: licence
OCaml: licence
Qiskit: licence
OpenQASM: licence
Matplotlib: licence
AutoQ: licence
Feynman: licence
PyZX: licence
QCEC: licence
QASMBench: licence
VeriQBench: Git
VeriQC: Git

Features

Supports input in OpenQASM 2.0 format.
Packaged as a Docker container with all necessary dependencies.
Provides a prototype inspection workflow for comparing two QASM files and exporting circuits and path-sums to text, LaTeX, and PDF.

Installation

Install Docker: https://docs.docker.com/get-started/get-docker/
Build the Docker image:

make build

Alternative, pull the Docker image:

make pull

Start a container from the current worktree:

make container

The container is removed automatically when the shell exits. To start from the pulled image instead of the local image:

make container-pull

Usage

Compilation (inside the container)

dune build

Inspection workflow prototype

The inspection script runs SQbricks on two QASM files and stores the artifacts needed to inspect the comparison:

bash scripts/inspect-sqbricks.sh --mode auto left.qasm right.qasm

Manual mode accepts explicit metadata:

bash scripts/inspect-sqbricks.sh --mode manual --algo seq --equiv s \
  --inputs1 "[0;1]" --inputs2 "[0;1]" --outputs1 "[0]" --outputs2 "[0]" \
  --meas1 "[]" --meas2 "[]" left.qasm right.qasm

The output directory is _tmp/inspection/<timestamp>/ by default. Important files include:

report.txt: human-readable summary;
commands.sh: replayable commands;
sqv.stdout: full SQV trace;
pathsum-left.stdout and pathsum-right.stdout: input path-sums;
final-path-sums.txt: final path-sums extracted from SQV;
circuit-left.tex, circuit-right.tex, circuits.tex, and circuits.pdf: prototype Quantikz2 circuit export when circuits are small enough;
path-sums.tex and path-sums.pdf: prototype LaTeX/PDF export.

The LaTeX export size thresholds can be tuned with:

SQBRICKS_INSPECT_LATEX_MAX_CHARS=30000 bash scripts/inspect-sqbricks.sh \
  --mode auto left.qasm right.qasm

For circuit drawings, the prototype uses Quantikz2 and skips circuits above SQBRICKS_INSPECT_CIRCUIT_MAX_QUBITS or SQBRICKS_INSPECT_CIRCUIT_MAX_GATES. Wide circuits are wrapped across several Quantikz2 blocks; the default wrap limit is SQBRICKS_INSPECT_CIRCUIT_WRAP_GATES=12. Classical bits written by simple measure q[i] -> c[j] operations are drawn as classical wires and connected to their measurement. It does not expand custom gate definitions. The Docker image installs the current Quantikz2 TikZ library from CTAN in a final layer.

SQbricks-Lift

Generate U/IUM:

-sql <dm> <in.qasm> <out.qasm>

Applies the deferred measurement to [in.qasm].

in.qasm: Input QASM file
out.qasm: Output QASM file
dm: Deferred Measurement type, u (unitary circuit) or ium (initialised-unitary-measurement circuit)
Return: List of measurements index

Example: Teleportation

Input = q0, Output = q2.

Input Circuit (tele.qasm)

OPENQASM 2.0;
include "qelib1.inc";
qreg q[3];
creg c0[1];
creg c1[1];
reset q[1];
reset q[2];
h q[1];
cx q[1], q[2];
cx q[0], q[1];
h q[0];
measure q[0] -> c0[0];
measure q[1] -> c1[0];
if (c1 == 1) x q[2];
if (c0 == 1) u1(pi/1) q[2];

Transformation to IUM (Initialization-Unitary-Measurement)

dune exec -- ./bin/main.exe -sql ium \
    benchmarks/minimal-examples/tele.qasm \
    benchmarks/minimal-examples/tele-ium.qasm

Output Circuit (tele-ium.qasm)

OPENQASM 2.0;
include "qelib1.inc";
qreg q[3];
creg c0[1];
creg c1[1];

// Initialization
reset q[1];
reset q[2];

// Unitary
h q[1];
cx q[1], q[2];
cx q[0], q[1];
h q[0];
cx q[1], q[2];
cu1(pi/1) q[0], q[2];

// Measurement
measure q[0] -> c0[0];
measure q[1] -> c1[0];

Transformation to U (Unitary)

dune exec -- ./bin/main.exe -sql u \
    benchmarks/minimal-examples/tele.qasm \
    benchmarks/minimal-examples/tele-u.qasm

Output Circuit (tele-u.qasm)

OPENQASM 2.0;
include "qelib1.inc";
qreg q[3];

// Unitary
h q[1];
cx q[1], q[2];
cx q[0], q[1];
h q[0];
cx q[1], q[2];
cu1(pi/1) q[0], q[2];

SQbricks-Verif

dune exec -- ./bin/main.exe -sqv <a> <e> <c1.qasm> <c2.qasm> [in1] [in2] [out1] [out2] [m1] [m2] <v>

Parameters

a: Algorithm type, seq (sequential) or par (parallel)
e: Equivalence type, s (SubCircuit), or g (GlobalPhase)
c1: Path to first QASM file (e.g. qft.qasm)
c2: Path to second QASM file (e.g. qft_owm.qasm)
in1: Input qubits for first circuit (e.g. [0;1])
in2: Input qubits for second circuit (e.g. [0;1])
out1: Output qubits for first circuit (e.g. [0;1])
out2: Output qubits for second circuit (e.g. [0;1])
m1: Measured qubits for first circuit (e.g. [0;1])
m2: Measured qubits for second circuit (e.g. [0;1])
v: Enable verbose output (e.g. true)

The size of the lists [in2] and [out2] must be equal to the size of the register of c2.

The result of an equivalence check can be either GlobalPhaseEquivalent or SubCircuitEquivalent. The first does not take into account the global phase (up to global phase), while the second does take into account the global phase.

Example: Teleportation

Input = q0, Output = q2.

Sequence Algorithm (s)

dune exec -- ./bin/main.exe -sqv seq s \
  benchmarks/minimal-examples/tele-u.qasm \
  benchmarks/minimal-examples/id.qasm \
  "[0]" "[0]" "[2]" "[0]" "[0;1]" "[]" true

Output

...
Equiv: SubCircuitEquivalent, 
Execution time = 0.000265 seconds, Memory = 0.018910 MB

Parallel Algorithm (p)

dune exec -- ./bin/main.exe -sqv par s \
  benchmarks/minimal-examples/tele-u.qasm \
  benchmarks/minimal-examples/id.qasm \
  "[0]" "[0]" "[2]" "[0]" "[0;1]" "[]" true

Output

...
inputs1=[0], inputs2=[0], outputs1=[2], outputs2=[0], meas1=[0;1], meas2=[]
Equiv.parallel,
output_path_var_norm1 =
  phase = e^{2.π.i.(0)};
  ket =  |y0,y1,x0>;
  path_var = [y0;y1];

Equiv.parallel,
output_path_var_norm2 =
  phase = e^{2.π.i.(0)};
  ket =  |x0>;
  path_var = [];

Equiv: SubCircuitEquivalent, 
Execution time = 0.000056 seconds, Memory = 0.006889 MB

SQbricks: Hybrid Circuit Verification (SQL + SQV):

Parameters

Parameter	Type	Description	Required
`c1.qasm`, `c2.qasm`	File (QASM)	Path to input hybrid circuit.	Yes
`v`	Boolean (`true`/`false`)	Enable detailed logs and additional information during execution.	No

Algorithms

Sequence Algorithm (s):

dune exec -- ./bin/main.exe -sq s <c1.qasm> <c2.qasm> v

* c2 has no discard or initialization.

Parallel Algorithm (p):

dune exec -- ./bin/main.exe -sq p c1.qasm c2.qasm v

Example: Teleportation

Input = q0, Output = q2.

Sequence Algorithm (seq)

dune exec -- ./bin/main.exe -sq seq s \
  benchmarks/minimal-examples/tele.qasm \
  benchmarks/minimal-examples/id.qasm \
  true

Output

...
Equiv: SubCircuitEquivalent, 
Execution time = 0.000334 seconds, Memory = 0.018908 MB

Parallel Algorithm (par)

dune exec -- ./bin/main.exe -sqv par s \
  benchmarks/minimal-examples/tele.qasm \
  benchmarks/minimal-examples/tele.qasm \
  true

Output

...
Equiv: SubCircuitEquivalent, 
Execution time = 0.000054 seconds, Memory = 0.006890 MB

Experimentation

Structure

Designation	Location	Description
Source Code	`lib/`	Core source code of SQbricks
Executable	`bin/`	Main entry point of SQbricks
Parser	`parser/`	Parsers for OpenQASM circuits and Path-Sum specifications
Scripts	`scripts/`	Contains helper scripts: benchmarks (`benchmarks.sh`), equivalence checking with QCEC (`mqt-qcec-qiskit.py`), and Qiskit transpilation scripts
Unit Tests	`tests/`	Test files for unit testing. Results are stored in `logs/`
Tools	`tools/`	External tool binaries used by SQbricks

Tests

Overview

Designation	Location	Description
Primitive Tests	`tests/primitives.ml`	Basic unit tests for primitive components
Functional (Unitary)	`tests/unitary.ml`, `tests/qiskit.ml`	Functional equivalence tests for unitary circuits
Functional (Hybrid)	`tests/mbqc.ml`	Functional equivalence tests for hybrid circuits
Functional (Specifications)	`tests/verif.ml`	Functional tests for specification-based verification (Path-Sum)

Usage

Command	Description
`make tests_prim`	Run unit tests on primitive components
`make tests_unit`	Run functional equivalence tests on unitary circuits
`make tests_qiskit`	Run functional equivalence tests between an original circuit and its Qiskit-transformed version
`make tests_mbqc`	Run functional equivalence tests on hybrid circuits with discard
`make tests_verif`	Run functional tests for specification-based verification (Path-Sum)
`make tests`	Run all tests

Output Location

Output

Example: Functional tests hybrid with discard

Testing `Symbolic execution'.
This run has ID `8RFVTPUJ'.

  [OK]          OWM vs Teleportation            0   h 0.
  [OK]          OWM vs Teleportation            1   h 2.
  [OK]          OWM vs Teleportation            2   hh 0.
  ...
  [OK]          Teleportation Parallel          0   h 0.
  ...
  [OK]          OWM Parallel                    0   id.
  ...
  [OK]          Teleportation                  72   qft4.
  [OK]          Teleportation                  73   false_teleportation qft4.

Full test results in `/sqbricks/_build_mbqc/default/test/_build/_tests/Symbolic execution'.
Test Successful in 1.110s. 377 tests run.

Tools

Tool	Version	Git Repository	Execution Path	Associated Paper
AutoQ	`POPL25`	AutoQ	`tools/AutoQ-POPL25` (Binaries)	Verifying Quantum Circuits with Level-Synchronized Tree Automata
AutoQ	`2.0`	AutoQ-2	`tools/AutoQ-2.0` (Binaries)	https://arxiv.org/abs/2411.09121
Feynman	`13-10-2022`	Feynman	`tools/Feynman_13-10-2022` (Binaries)	Towards Large-scale Functional Verification of Universal Quantum Circuits
Feynman	`28-11-2024`	Feynman	`tools/Feynman_28-11-2024` (Binaries)	Linear and non-linear relational analyses for Quantum Program Optimization
PyZX	`0.9.0`	PyZX	`python3 scripts/pyzx_verify.py`	PyZX: Large Scale Automated Diagrammatic Reasoning
QCEC	`2.8.1`	QCEC	`python3 scripts/mqt-qcec-qiskit.py`	Handling Non-Unitaries in Quantum Circuit Equivalence Checking

Circuits collection (OpenQASM 2)

Name	Location	Source	Description	Associated Paper
Feynman	`benchmarks/Feynman`	Feynman Library	Unitary circuits (Toffoli, GF2, Grover, …); extra Hadamard gates were added to test verification robustness.	Towards Large-scale Functional Verification of Universal Quantum Circuits
QASMBench	`benchmarks/QASMBench`	QASMBench	Unitary and hybrid circuits.	QASMBench: A Low-level QASM Benchmark Suite for NISQ Evaluation and Simulation
VeriQbench	`benchmarks/VeriQbench`	VeriQbench	Unitary and hybrid circuits.	VeriQBench: A Benchmark for Multiple Types of Quantum Circuits
VeriQC	`benchmarks/VeriQC`	VeriQC	Hybrid dynamic circuits.	Equivalence Checking of Dynamic Quantum Circuits

Sanity check {#sanity-check}

Usage

Command	Description
`make sanity-unit`	Sanity check sur les circuits unitaires
`make sanity-hybrid`	Sanity check sur les circuits hybrides
`make sanity-partial`	Sanity check sur les circuits hybrides avec discard
`make sanity`	Lance tous les sanity check

Output

The output of the sanity check (like benchmark results) is stored as a CSV file in a folder as benchmarks/result/<date>/.

The table below shows a portion of the output from the hybrid sanity check without discard.

The last column Time being empty indicates that the sanity check passed for all tools.
If a time appears in Time, the tool failed the sanity check, as it incorrectly verified equivalence between two non-equivalent circuits.

Column descriptions:

Program1 and Program2: Names of the programs under sanity check
Tool and Version: Tool name and version
Opt: Tool-specific options (DM = delayed measurement, OE = partial equivalence, Sequence = sequential algo, Parallel = parallel algo)
Lift: Indicates whether delayed measurement (SQL) was applied (standalone = no, lifting = yes)
Remaining columns: Gate counts

Program1	Program2	Tool	Version	Lift	Opt	CS	CCX	CU1	Gates	Time
shor_n5_ancillas	shor_n5_ancillas_FALSE_angle	QCEC	1.8.1	standalone	DM,OE	7	22	5	60	Err1
shor_n5_ancillas	shor_n5_ancillas_FALSE_angle	QCEC	1.8.1	standalone	DM,NoOE	7	22	5	60	Err1
shor_n5_ancillas	shor_n5_ancillas_FALSE_angle	QCEC	1.8.1	lifting	OE	7	22	5	60	NE
shor_n5_ancillas	shor_n5_ancillas_FALSE_angle	SQbricks	2025	lifting	Sequence	7	22	5	60	NC
shor_n5_ancillas	shor_n5_ancillas_FALSE_angle	SQbricks	2025	lifting	Parallel	7	22	5	60	NC
shor_n5_ancillas	shor_n5_ancillas_FALSE_angle	Feynman	28-11-2024	lifting	None	7	22	5	60	Err1
shor_n5_ancillas	shor_n5_ancillas_FALSE_angle	Feynman	13-10-2022	lifting	None	7	22	5	60	Err1
shor_n5_ancillas	shor_n5_ancillas_FALSE_angle	PyZX	0.9.0	lifting	None	7	22	5	60	NC
shor_n5_ancillas	shor_n5_ancillas_FALSE_angle	AutoQ	2.0	lifting	None	7	22	5	60	NE
shor_n5_ancillas	shor_n5_ancillas_FALSE_angle	AutoQ	POPL25	lifting	None	7	22	5	60	NE

To facilitate reading and extracting metrics, the CSV content can be imported into a spreadsheet file (.ods). Example spreadsheet files are provided in the benchmarks/result/ folder.

To prepare the CSV files for import, use the script: scripts/prepare-benchs.sh input-folder/.

For example: ./scripts/prepare-benchs.sh benchmarks/result/2025-04/

This script processes all CSV files in the folder and generates the results in a processed subfolder.

After processing, you can open the relevant CSV file with a spreadsheet application and copy its content into: benchmarks/result/benchmarks.ods.

The metrics can be found in the totals sheet:

Column	Description
`Lift`	When set to `lifting`, our deferred measurement function (`SQL`) is applied to the input circuits before verification. This transforms conditional operations into unitary gates for compatibility with verification tools.
`Opt`	Specifies tool-specific optimization options: • `OE`: Partial equivalence (outputs only qubits with final measurements). • `DM`: Deferred measurement (used by QCEC for hybrid circuits without discards). • `Sequence`: Uses the sequential algorithm (`s`). • `Parallel`: Uses the parallel algorithm (`p`).
`NE`	Not Equivalent: Number of cases where the tool correctly identified non-equivalent circuits.
`NC`	Inconclusive: Number of cases where the tool could not determine equivalence.
`TO`	Timeout: Number of cases where the tool exceeded the time limit.
`Fail`	Error: Number of cases where the tool returned an error (e.g., crashes, invalid inputs).
`Err`	False Positives: Number of times the tool incorrectly reported two circuits as equivalent.
`TT`	Total Time: Cumulative execution time (ms) for all equivalence checks.
`AT`	Average Time: Mean execution time (ms) per equivalence check.
`Check`	Validates that the number of tests run (`Greet`) matches the expected count (`Expected`).

Benchmark

Usage

Command	Description	Discard
`make owm`	Runs equivalence checks between a unitary circuit and its One Way Measurement counterpart (The Measurement Calculus). (`O(U)-U`)	One circuit
`make tele`	Verifies equivalence between a unitary circuit and a "teleported" version. (`T(U)-U`)	One circuit
`make unit-vs-hybrid`	Verifies equivalence between different instances of standard and hybrid QFT and QPE. (`U-DC`)	No discard
`make qiskit-hybrid`	Verifies equivalence between a hybrid circuit and a version transpiled with Qiskit. (`DC-Q(DC)`)	No discard
`make owm-vs-qiskit`	Runs equivalence checks between a unitary circuit transpiled with Qiskit and its One Way Measurement version. (`O(DC)-Q(DC)`)	One circuit
`make owm-vs-tele`	Runs equivalence checks between a "teleported" unitary circuit and its One Way Measurement version. (`O(U)-T(U)`)	Two circuits have discard
`make veriqc`	Runs all hybrid equivalence checks from the dynamic version of VeriQC.	No discard
`make benchmarks`	Runs all benchmarks.

SQbricks-only benchmarks

Three SQbricks-only benchmark levels are available when the goal is to check SQbricks itself without running the external verification tools used by scripts/benchmarks.sh: the short light non-regression benchmark, the selected large regression, and the full long benchmark.

Command	Description
`make regression-light`	Runs the short non-regression benchmark and writes a CSV result.
`make regression-light-baseline`	Builds the local baseline for the short non-regression benchmark.
`make regression-light-check`	Runs the short non-regression check against the local baseline.
`make benchmark-sqbricks TYPE=owm`	Runs one long SQbricks-only benchmark family.
`make benchmarks-sqbricks`	Runs all long SQbricks-only families listed in `LONG_TYPES`.
`make benchmark-regression-large TYPE=owm`	Runs one selected large-regression family.
`make regression-large`	Runs all selected large-regression families listed in `LARGE_TYPES`.
`make regression-large-baseline`	Builds per-family selected large-regression baselines.
`make regression-large-check`	Runs the selected large regression and compares it with those baselines.

The light baseline is local to the machine. Regenerate it after changing the light benchmark selection or timing policy.

The long SQbricks-only benchmark reuses the historical path files, including qiskit-hybrid and owm-vs-qiskit. Those two families still use scripts/qiskit-tr.py to generate transformed circuits, but Qiskit is not reported as a verification tool in the generated CSV.

The selected large regression currently reuses the SQbricks-only long runner with shorter path files in scripts/paths/regression-large/. It writes CSV results, stores per-family baselines in benchmarks/baseline/regression-large/, and checks that current rows do not lose functional capability or exceed the configured performance thresholds. Functional improvements are reported but do not fail the check. For sized families, the selection keeps up to the three largest representatives instead of only the largest one, so the check can still observe nearby cases when the largest case reaches the timeout or memory limit.

For ordered-size series, the long runner tracks Sequence and Parallel independently. After a timeout or memory limit, larger cases skip only the mode that failed and write SKIP_AFTER_RESOURCE_FAILURE; the other mode still runs. A conversion resource failure stops both modes. Series are scoped by source directory, so a Feynman failure does not stop the corresponding VeriQbench family. Other series continue to run.

Progress bars are printed on stderr and CSV data is written on stdout, so redirected result files stay clean.

Output

The results are processed identically to the sanity check. Please refer to the sanity check for detailed explanations.

An example of the final summary table displaying all sanity check results is shown below:

Name		Name	Last commit message	Last commit date
Latest commit History 74 Commits
.github/workflows		.github/workflows
benchmarks		benchmarks
bin		bin
doc		doc
lib		lib
scripts		scripts
test		test
tools		tools
.dockerignore		.dockerignore
.gitignore		.gitignore
.gitlab-ci.yml		.gitlab-ci.yml
.ocamlformat		.ocamlformat
.ocamlformat-ignore		.ocamlformat-ignore
AGENTS.md		AGENTS.md
CITATION.cff		CITATION.cff
Dockerfile		Dockerfile
LICENSE		LICENSE
Makefile		Makefile
README.md		README.md
ROADMAP.md		ROADMAP.md
TODO.md		TODO.md
container.sh		container.sh
dune-project		dune-project
requirements.txt		requirements.txt
sQbricks.opam		sQbricks.opam

Folders and files

Latest commit

History

Repository files navigation

SQbricks

SQbricks-Lift (SQL)

SQbricks-Verif (SQV)

Research and provenance

License

Features

Installation

Usage

Compilation (inside the container)

Inspection workflow prototype

SQbricks-Lift

Generate U/IUM:

Example: Teleportation

SQbricks-Verif

Parameters

Example: Teleportation

SQbricks: Hybrid Circuit Verification (SQL + SQV):

Parameters

Algorithms

Example: Teleportation

Experimentation

Structure

Tests

Overview

Usage

Output Location

Output

Tools

Circuits collection (OpenQASM 2)

Sanity check {#sanity-check}

Usage

Output

Benchmark

Usage

SQbricks-only benchmarks

Output

About

Topics

Resources

License

Uh oh!

Stars

Watchers

Forks

Releases

Packages 0

Uh oh!

Uh oh!

Contributors

Uh oh!

Languages

Packages