The paper addresses a key aspect of efficient computation in logic synthesis and formal verification, namely, the integration of a circuit simulator and a Boolean satisfiability solver. A novel way of interfacing these is proposed along with a fast preprocessing step to detect easy SAT instances and a new hybrid SAT solver, which is more robust for hardware designs than are state-of-the-art CNF-based solvers. The proposed integration enables a 10x speedup in essential computation engines widely used in industrial EDA tools, including SAT sweeping, combinational and sequential equivalence checking, and computing structural choices for technology mapping. The speedup does not lead to a loss in quality because the computed equivalences are canonical.

In recent years SAT solving has been widely used to implement various circuit transformations in logic synthesis. However, off-the-shelf CNF-based SAT solvers often have suboptimal performance on these challenging optimization problems. This paper describes an application-specific circuit-based SAT solver for logic synthesis. The solver is based on Glucose, a state-of-the-art CNF-based solver and adds a number of novel features, which make it run faster on multiple incremental SAT problems arising in redundancy removal and logic restructuring among others. In particular, the circuit structure of the problem instance is leveraged in a new way to guide variable decisions and to converge to a solution faster for both satisfiable and unsatisfiable instances. Experimental results indicate that the proposed solver leads to a 2-4x speedup, compared to the original Glucose.

In modern integrated circuit design, bus routing is a challenge because of complex design rules and wiring constraints. Despite extensive research, state-of-the-art in bus routing is not effective when nonuniform tracks, various obstacles, wire width constraints, and multiple spacing rules should be handled simultaneously. A new bus routing framework proposed in this article is based on maze routing and Boolean satisfiability. It produces high-quality results quickly and allows for additional optimizations, such as minimizing wire length on the critical paths. A number of challenging bus routing benchmarks appeared in 2018 ICCAD Contest. Experiments on these benchmarks not only show that the framework is faster than the winners of the competition and previous work but also produces better results, improving the overall cost by 12% while at the same time minimizing the number of spacing violations.

Fanouts are an essential element for signal cloning to achieve logic sharing, but can be a very limited resource in certain emerging technologies, such as quantum circuits, superconducting electronic circuits, photonic integrated circuits, and biological circuits. Although fanout synthesis has been intensively studied for high performance circuit synthesis, prior methods often treat fanout as a soft constraint for critical path optimization or target on specific high-fanout nets such as clock and reset signals. They are not particularly suited for circuit synthesis of these emerging technologies. By treating fanouts as first class citizens, the problem of fanout-bounded logic synthesis was posed as a challenge in the 2019 IWLS Programming Contest. In this paper, we present our winning method, which achieved the overall best quality in the competition, based on fanout load redistribution among existing or expanded equivalent signals.

The increasing system complexity makes engineering change order (ECO) mostly inevitable and a common practice in integrated circuit design. Despite extensive research being made, prior methods are not effectively applicable to instances where rectification is to be done by simultaneously fixing multiple target points using intermediate signals. Moreover, how to efficiently generate low-cost patch functions is rarely addressed. These challenges are posed as a problem in the 2017 ICCAD CAD Contest. Based on Boolean satisfiability and interpolation, we propose a sound and complete algorithm for resource-aware patch generation of multi-target ECO. Experiments show our high quality results compared to other winning teams in the contest.