Circuit symmetries in synthesis and verification.

摘要

This dissertation explores the application of logical symmetries in the synthesis and verification of digital systems. Given a high-level description of a design, synthesis algorithms are employed to obtain a low-level description which is suitable for manufacture. To make the process computationally feasible, each step assumes a simplified model of the implementation platform. For example, many of the earlier steps disregard the fact that current technologies require that components are laid out in a two-dimensional plane, and therefore that the necessary wiring between components may become problematic. If the cost and performance requirements are not met, then the synthesis process is repeated, back-propagating the current results to refine any estimates for the next iteration.;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.