Verified compilation of reversible circuits

Patent metadata

Field	Value
Publication number	US-10664249-B2
Application number	US-201615060408-A
Country	US
Kind code	B2
Filing date	Mar 3, 2016
Priority date	Nov 20, 2015
Publication date	May 26, 2020
Grant date	May 26, 2020

Abstract

The generation of reversible circuits from high-level code is desirable in a variety of application domains, including low-power electronics and quantum computing. However, little effort has been spent on verifying the correctness of the results, an issue of particular importance in quantum computing where such circuits are run on all inputs simultaneously. Disclosed herein are example reversible circuit compilers as well as tools and techniques for verifying the compilers. Example compilers disclosed herein compile a high-level language into combinational reversible circuits having a reduced number of ancillary bits (ancilla bits) and further having provably clean temporary values.

First claim

What is claimed is:

1. A computer-implemented method, comprising:
by a verification tool adapted to perform formal verification of a reversible circuit compiler and implemented by one or more computing devices:
verifying operation of the reversible circuit compiler, the reversible circuit compiler being configured to generate a reversible circuit from a high-level program description of the reversible circuit, the reversible circuit being a reversible circuit description including a reversible gate set implementable by a quantum computing device,
wherein the verifying includes verifying that an intermediate representation of the reversible circuit that is generated by the reversible circuit compiler satisfies one or more verification criteria relative to a higher-level intermediate representation of the reversible circuit that is also generated by the reversible circuit compiler;
generating the reversible gate set from the high level program; and
implementing the reversible gate set in a target reversible circuit architecture.

2. The computer-implemented method of claim 1 , wherein the one or more criteria include one or more of: (a) ensuring that the intermediate representation of the reversible circuit implements the same function as the higher-level intermediate representation; or (b) ensuring that all ancilla bits that are allocated by the intermediate representation of the reversible circuit are returned clean.

3. The computer-implemented method of claim 1 , wherein the verifying further includes type-checking the intermediate representation relative to the higher-level intermediate representation, ensuring application of functions to inputs of appropriate types, allowing only operations or transformations that do not violate the rules of a type system, wherein in the type system is specified by a set of type inference rules.

4. The computer-implemented method of claim 1 , wherein the verifying comprises performing one or more semantic checks of the intermediate representation relative to the higher-level intermediate representation.

5. The computer-implemented method of claim 4 , wherein the semantic checks are performed by a proof system that asserts the correctness of one or more transformations of the compiler as the compiler generates the reversible circuit from the high-level program.

6. The computer-implemented method of claim 1 , wherein the high-level program is an algorithmic description of the reversible circuit describing the behavior of the reversible circuit.

7. A system, comprising:
a processor; and
at least one memory coupled to the processor and having stored thereon processor-executable instructions for implementing a verification process for a reversible circuit compiler, the reversible circuit compiler being configured to generate a reversible circuit from a high-level behavioral description of the reversible circuit, the reversible circuit including a reversible gate set implementable in a target quantum circuit architecture, the compiler verification process comprising verifying that all ancilla bits that are allocated during reversible circuit compilation are returned to a clean state by the reversible gate set produced by the reversible circuit compiler; and
a reversible circuit controller coupled to the target reversible circuit architecture, the reversible circuit controller configured to implement the reversible circuit description in the target reversible circuit architecture.

8. The system of claim 7 , wherein the verification process further comprises verifying that the reversible gate set produced by the reversible circuit compiler performs the same function as the high-level behavioral description.

9. A reversible circuit compilation system, comprising:
a memory;
a reversible circuit compiler, the reversible circuit compiler being configured to:
input, into the memory, a program describing a desired computation to be performed in a target reversible circuit architecture using bits, transform the program into a reversible circuit description specifying one or more reversible gates that use the bits to achieve the desired computation, and store, in the memory, the reversible circuit description,

apply one or more ancilla-reducing techniques to reduce the number of ancillas used by the reversible circuit description as part of the transformation of the program into the reversible circuit description; and
generate a reversible circuit from the reversible circuit description, the reversible circuit including a reversible gate set implementable in the target quantum circuit architecture; and
a reversible circuit controller coupled to the target reversible circuit architecture, the reversible circuit controller configured to implement the reversible circuit description in the target reversible circuit architecture.

10. The reversible circuit compilation system of claim 9 , wherein one of the ancilla-reducing techniques applied comprises:
identifying an operation in the program that can be implemented as an exclusive-or operation of a target bit; and
generating a reversible circuit with a reversible ancilla bit to implement the operation.

11. The reversible circuit compilation system of claim 9 , wherein one of the ancilla-reducing techniques comprises rewriting AND operations from the program into a positive-polarity exclusive-sum-of-products form.

12. The reversible circuit compilation system of claim 9 , wherein one of the ancilla-reducing techniques comprises simplifying one or more of an XOR or AND expression, the simplification being performed by factoring the XOR or AND expression to reduce depth.

13. The reversible circuit compilation system of claim 9 , wherein the reversible circuit is further configured to, as part of the transformation of the program into the reversible circuit description, reduce sub-expressions in the program to Boolean expressions and apply the ancilla-reducing techniques to the Boolean expressions.

Assignees

• Microsoft Technology Licensing Llc

Inventors

• Amy Matthew
• Roetteler Martin
• Svore Krysta

Classifications

• G06F8/44 Primary

  Encoding · CPC title

• G06F8/436

  Semantic checking · CPC title

• G06N10/00

  Quantum computing, i.e. information processing based on quantum-mechanical phenomena · CPC title

• G06N10/40

  Physical realisations or architectures of quantum processors or components for manipulating qubits, e.g. qubit coupling or qubit control · CPC title

• G06N10/20 Primary

  Models of quantum computing, e.g. quantum circuits or universal quantum computers · CPC title