Reversible circuit is of interest due to the characteristics of low energy consumption. This paper proposes a new scheme for synthesizing fault tolerant reversible circuits. A two-step method is put forward to convert an irreversible function into a parity-preserving reversible circuit. By introducing model checking for linear temporal logic, we construct a finite state machine to synthesize small reversible gates from elementary 1-qubit and 2-qubit gates, which is more automatic than the methods proposed previously. Constrains are increased so as to reduce the synthesis time in the two step method. The parity-preserving gate constructed by the two-step method has characteristics of low quantum cost because the quantum representation obtained from the counterexample for a given function in each step has the minimum quantum cost. In order to further reduce the quantum cost and decrease the synthesis time, the semi parity-preserving gates are put forward for the first time. These gates are parity-preserving when the auxiliary input is set to 0 and opposite parity when 1. Maintaining good robustness of the system in performing specific function, semi parity-preserving gate is conducive to detecting the stuck-at fault and partial gate fault in reversible circuits. The innovation of this paper is introducing the formal method to synthesis small fault tolerant gate, so as to construct the circuit with robust (semi) parity-preserving gates.
Verifying safety of synchronous fault-tolerant algorithms by bounded model checking
