Rather than forcing designers and tools to make early decisions with incomplete and/or inaccurate information, we propose the use of logical symmetries to defer some decisions until more information is available. For example, instead of assuming a fixed circuit structure, we may use symmetries to permute wires during the final stages of synthesis, when wirelengths are known, to improve the design's performance. In addition, symmetries can be used to eliminate redundant cases during verification. For example, in verifying a traffic light controller, one may often assume that the rules are identical for all four directions and simply check for one of them.

The first part of this dissertation reviews the necessary mathematical underpinnings of group theory, allowing us to efficiently reason about symmetries. With this background, we introduce our approaches to find symmetry in circuits.

The second part presents the application of symmetries in synthesis and verification. We show how symmetries may be used in the technology mapping and placement stages, two major steps in synthesis. In technology mapping, we derive alternative representations of the design besides the local minimum obtained from technology independent optimization. In placement, we modify the circuit topology to reduce wirelength. In both cases, symmetries expand the design space with no loss in quality (assuming stable algorithms). Afterwards, we present our approach for improving so-called "symmetry breaking predicates" to speed up Boolean SAT solvers, which are heavily used in verification.