# Quartz

Quantum System: building automatic quantum compiler

Equivalent Circuit Classes (ECCs): a set of circuits that perform the same task

• subsumed transformation: valid transformation

• $(n,q)$-complete EECs: biggest EEC of certain function that has at most $n$ gates and $q$ qubits

Subcircuit: a collection of gates in a circuits that are executed in close neighborehood of computation graph. (If I execute subcircuit in appropriate time, it will never go wrong.)

Parametric gates: gates that needs input to define and construct. For a circuit with $m$ parameters and $q$ qubits, the circuit is written as:

[[C]]: \mathbb{R}^m \to \mathbb{C}^{2^q \times 2^q}

Equivalence: $|\psi\rangle$ and $e^{i\beta}|\psi\rangle$ is equivalent up to a global phase. From an observational point of view, they are identical.

Circuit: $C^{(n, q)}$

• fix gate set $G$

• fixed parameter expression $\Sigma$

Representative Circuit: an arbitrary circuit that is one of the smallest in a EEC set in which the functionality is what we care about. // TODO: you should put definition of representation in front. and you didn't define "previous round" to have EECs instead of one EEC.

Circuit Transformation: a tuple $(C_T, C_R)$ is a target and a rewrite. An EEC with $x$ circuit has $x(x-1)$ many transformations.

Fingerprint: randomly fix parameter $p_0$ and two quantum state, the finger print of a circuit is the following.

|\langle \psi_0 | [[C]](\vec{p_0})|\psi_1\rangle|

Pipeline: transformation generation and transformation applier

Generation:

• start from representation with $n$ gates

• add one gate to representation, now with $n+1$ gates but with redundant

• eliminate redundant representation to get new $n+1$ representation

• keep only simple random equivalence test
• pruning unused qubits
• pruning permutation of parameters
• remove transform that share parts of common transform
• ## verify that our new $n+1$ representation is actually correct by SMT solver

Applier:

• circuit pruning

• circuit optimizer: apply local transformation to the whole circuit based on cost before qubit mapping based on queue of cost using TASO. It applies transformation to some "almost-best" cost circuit (not seen before).

Performance: generation takes 30 min. Reduction gate count around 40%.

// QUESTION: why verifier?

// QUESTION: section related to phrase factor is unclear to me. Why SMT prover cannot prove Quartz

Directions

• fault tolerance = application
• physical level is not done

• quartz: logical

• mapping

Table of Content