Implication and abstraction in generalized symbolic trajectory evaluation and synthesis of reversible logic by group theory

The thesis addresses the verification and synthesis problems that occur in digital computing systems. Mathematical modeling and analysis methods are used to solve these problems. We investigate the formal verification technique using the generalized symbolic trajectory evaluation and the synthesis of reversible logic circuits.; Generalized symbolic trajectory evaluation (GSTE) is an extension of symbolic trajectory evaluation (STE). Our contributions are summarized as follows. We establish some sufficient conditions to derive language-based and model-based implications for assertion graphs. We apply both model-based implication and language-based implication on real industrial circuits. We introduce the concept of a maximal model and present a provable algorithm to find all maximal models for a linear assertion graph. And we also present an algorithm to calculate a maximal model of any given assertion graph. A special abstraction, naturally-induced abstraction is introduced. The abstraction model can be intuitively expressed by directed graphs. An algorithm for computing minimum preserved abstraction is developed.; For the synthesis of digital systems, we investigate how to synthesize a reversible system which plays a key role in quantum computing systems. We establish the following contributions. We devise a novel technique that transforms the quantum logic synthesis problem from a multi-valued constrained optimization problem to a permutable representation. The transformation enables us to utilize group theory to exploit the symmetric properties of the synthesis problem. By reducing binary reversible logic synthesis problems to group theory problems, we use the powerful algebraic software GAP to solve such problems. Our approach is not only able to minimize for arbitrary cost functions of gates, but also faster than the existing approaches to reversible logic synthesis. In addition, we demonstrate that the Peres gate is a better choice than the standard Toffoli gate in libraries of universal reversible gates. We also prove the synthesis capacity of some well-known reversible gates by group theory. Finally, the synthesis of ternary reversible logic is investigated.