VERIFIED COMPILATION OF REVERSIBLE CIRCUITS

• US 20170147303A1
• Filed: 03/03/2016
• Published: 05/25/2017
• Est. Priority Date: 11/20/2015
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Inventors: Amy, Matthew, Roetteler, Martin, Svore, Krysta
• Granted Patent: US 10,664,249 B2
• Time in Patent Office: Days
• CPC Class Codes: G06F 8/436 Semantic checking
• CPC Class Codes: G06F 8/44 Encoding
• CPC Class Codes: G06N 10/00 Quantum computing, i.e. information processing based on quantum-mechanical phenomena

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.

Claims

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,

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.

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. The computer-implemented method of claim 1, wherein the method further comprises:

generating, by the verified reversible circuit compiler, the reversible gate set from the high-level program; and

implementing the reversible gate set in a target reversible circuit architecture.

8. 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 compile a behavioral description of a reversible circuit into 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.

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

10. A reversible circuit compilation system, comprising:

a memory; and

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, the reversible circuit compiler being further configured to, as part of the transformation of the program into the reversible circuit description;

apply one or more ancilla-reducing techniques to reduce the number of ancillas used by the reversible circuit description.

11. The reversible circuit compilation system of claim 10, 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.

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

13. The reversible circuit compilation system of claim 10, 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.

14. The reversible circuit compilation system of claim 10, 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.

15. The reversible circuit compilation system of claim 10, further comprising a reversible circuit controller coupled to the target reversible circuit architecture and configured to implement the reversible circuit description in the target reversible circuit architecture.

16. A computer-implemented method, comprising, with a reversible circuit compiler, generating an output reversible circuit from a high-level program, the reversible circuit compiler being verified at all levels of intermediate internal representation.

17. The method of claim 16, further comprising verifying the reversible circuit compiler by:

(a) asserting that an output reversible circuit implements the target function as specified by the high-level program and (b) asserting that all ancilla bits that are allocated by the output reversible circuit implementation are returned clean.

18. The method of claim 16, wherein the generating comprises translating the high-level program into a Toffoli network upon successful verification and type-checking of the reversible circuit compiler that performs the generating of the reversible circuits, the Toffoli network comprising at least one of a Toffoli gate, NOT gate, or CNOT gate.

19. The method of claim 16, further comprising verifying the reversible circuit compiler by applying semantic checks performed by a proof system to assert the correctness of the transformations of the compiler.

20. The method of claim 16, wherein the reversible circuit compiler is verified by proofs that are coded into source code for the reversible circuit compiler.