Towards a Design Flow for Reversible Logic (eBook)

Preface 5
Acknowledgements 7
Contents 8
Acronyms 11
Introduction 12
Preliminaries 18
Background 18
Reversible Functions 18
Reversible Circuits 20
Quantum Circuits 24
Decision Diagrams 27
Binary Decision Diagrams 28
Quantum Multiple-valued Decision Diagrams 30
Satisfiability Solvers 32
Boolean Satisfiability 32
Extended SAT Solvers 33
SMT Solvers for Bit-vector Logic 34
QBF Solvers 35
SWORD Solver 35
Note on Benchmarks 37
Synthesis of Reversible Logic 38
Current Synthesis Steps 39
Embedding Irreversible Functions 39
Transformation-based Synthesis 41
BDD-based Synthesis 42
General Idea 43
Exploiting BDD Optimization 45
Shared Nodes 45
Complement Edges 47
Reordering of BDDs 48
Theoretical Consideration 48
Experimental Results 50
Effect of BDD Optimization 51
Shared Nodes 51
Complement Edges 51
Reordering of BDDs 52
Comparison to Previous Synthesis Approaches 54
SyReC: A Reversible Hardware Language 57
The SyReC Language 58
The Software Language Janus 58
The Hardware Language SyReC 59
Synthesis of the Circuits 61
Reversible Assignment Operations 61
Binary Operations 62
Conditional Statements, Loops, Call/Uncall 63
Experimental Results 64
Summary and Future Work 67
Exact Synthesis of Reversible Logic 68
Main Flow 69
SAT-based Exact Synthesis 72
Encoding for Toffoli Circuits 72
Encoding for Quantum Circuits 76
Handling Irreversible Functions 79
Experimental Results 81
Synthesis of Quantum Circuits 81
Handling of Irreversible Functions 81
Effect of Double Gates 83
Comparison with Previous Work 84
Synthesis of Toffoli Circuits 85
Comparison to Exact Approaches 85
Comparison to Heuristic Approaches 85
Improved Exact Synthesis 87
Exploiting Higher Levels of Abstractions 88
Limits of Common SAT and SMT Solvers 89
Dedicated Solve Techniques for Toffoli Circuit Synthesis 90
Decision Strategies 90
Propagation Strategies 91
Quantified Exact Synthesis 92
Quantified Problem Formulation 92
Implementations 94
Using QBF Solvers 94
Using BDDs 94
Experimental Results 95
Exploiting Higher Levels of Abstractions 95
Quantified Exact Synthesis 96
Run-time Comparison 96
Quantum Costs of Resulting Circuits 98
Synthesis with Extended Libraries 99
Summary and Future Work 102
Embedding of Irreversible Functions 103
The Embedding Problem 104
Don't Care Assignment 106
Methods 106
Greedy Method 106
Applying the Hungarian Algorithm 108
XOR-based Method 108
Incomplete Don't Care Assignment 109
Experimental Results 109
Synthesis with Output Permutation 110
General Idea 112
Exact Approach 114
Heuristic Approach 115
Experimental Results 116
SWOP with Garbage Outputs 117
Exact SWOP 117
Heuristic SWOP 119
Reductions Achieved by SWOP 120
Summary and Future Work 121
Optimization 122
Adding Lines to Reduce Circuit Cost 123
General Idea 123
Algorithm 125
Experimental Results 126
Reducing the Number of Circuit Lines 133
General Idea 134
Algorithm 136
Determine an Appropriate Sub-circuit 136
Re-synthesize the Sub-circuit 138
Insert the Sub-circuit and Merge the Lines 139
Experimental Results 139
Optimizing Circuits for Linear Nearest Neighbor Architectures 140
NNC-optimal Decomposition 142
Optimizing NNC-optimal Decomposition 143
Exploiting Exact Synthesis 143
Reordering Circuit Lines 145
Global Reordering 145
Local Reordering 146
Experimental Results 147
Summary and Future Work 147
Formal Verification and Debugging 151
Equivalence Checking 152
The Equivalence Checking Problem 153
QMDD-based Equivalence Checking 153
The Completely Specified Case 153
Constant Inputs, Garbage Outputs 154
Don't Care Conditions 155
SAT-based Equivalence Checking 156
The Completely Specified Case 156
Constant Inputs, Garbage Outputs, and Don't Care Conditions 157
Experimental Results 158
Automated Debugging and Fixing 162
The Debugging Problem 163
Problem Description 163
Debugging of Traditional Circuits 164
Determining Error Candidates 165
SAT Formulation 165
Improvements for Control Line Errors 168
Determining Error Locations 169
Limits of Error Candidates 170
Approach 170
Fixing Erroneous Circuits 173
Experimental Results 175
Single Errors 175
Multiple Errors 177
Automatic Fixing 180
Summary and Future Work 181
Summary and Conclusions 183
References 185
Index 191