Resolution Proofs as a Data Structure for Logic Synthesis

Slides

The results of modern synthesis tools are heavily influenced by the initial structure of the designs they are given. Many synthesis tools use And-Inverter Graphs (AIGs) as the underlying representation in the technology-independent phase of synthesis. Generally, AIGs can be compacted through a series of operations that merge equivalent nodes. Proving nodes to be equivalent can be a done with efficient SAT-based algorithms. However, when an AIG consists of very sparse logic, compaction is ineffective; few equivalent nodes are found. Recently, techniques for generating functional dependencies via Craig Interpolation have been proposed. Such methods first generate a resolution proof from a SAT instance. Interpolation is performed on the resolution proof to generate the dependency function. Unlike nodes in an AIG, determining whether an equivalent resolution node can be generated from other resolution nodes is a simple task. In this work, we study the use of resolution proofs as an underlying data structure for performing technology-independent synthesis, as opposed to just the front- end step. In order to represent multiple functions, we merge separate resolution proofs into a single, monolithic resolution proof and then perform restructuring operations. We analyze the effectiveness of our method on standard benchmark circuits. The results suggest that resolution proofs could be a very effective data structure for representing multiple target functions.