This repository contains guidelines for running various resubstitution engines in ABC.
The engines are exercised on the level of individual Boolean transforms. The focus is not high performance on specific circuits but rather conceptual understanding and implementation flexiblity needed for building efficient optimization frameworks based on Boolean resubstitution.
| ABC Command | Short Description | Publication |
|---|---|---|
| resub_unate | Fast resub based on detecting unate divisors | paper |
| resub_core | Generic high-effort resub engine based on support selection | paper |
| twoexact | SAT-based exact synthesis with side-divisors | paper |
The first engine is the fastest one among those presented here. It works well when the resulting resub function contains only a few nodes. It is good for developing rewriting-style optimizations when relatively small (possibly six-input) cuts are computed, followed by collecting a set of divisors supported by each cut. The divisor functions can be represented using truth tables (in the case of six-input cuts, each truth table is one 64-bit machine word). The fast unate resub can be applied to reexpress a target node in terms of other divisors supported by the cut. An efficient GPU-based implementation of this engine may be developed.
The second engine uses more effort to perform two steps. Given a target node and a set of divisors, the first step is to compute a small support (or a good-quality support if the divisors have non-unit weights) sufficient for expressing the target node. The second step is to find the new function of the node in terms of the support variables. This engine works for incompletely-specified functions. It can be iterated to find solutions for multi-output functions. The engine was used to derive ECO patch functions, winning the first place in 2017 ICCAD CAD competition (Problem A).
The third engine is running high-effort SAT-based exact synthesis applicable to multi-output Boolean functions and relations with side-divisors, that is, usable divisors other than primary inputs. (The original formulation of exact synthesis did not consider side-divisors). This engine computes a minimum-size implementation of the resub functions in terms of the number of nodes in an and-inverter graph (AIG) or an xor-and-inverter graph (XAIG). It is the only engine capable of true multi-output logic synthesis, in the sense that it does not iterate resub for each output, but considers the whole multi-output relation as the specification and derives a minimum-node circuit satisfying this relation. An obvious limitation of this engine that it only works for functions up to six input and up to 10 nodes in the synthesized circuit.
The three engines presented here can be applied to individual resub instances specified using a common representation format.
The input format is a modified version of Espresso PLA format (.type fr).
The modifications include
- Representation of Boolean relations
- For this some input combinations can be duplicated and listed with different output combinations.
- Input patterns are represented as minterms rather than cubes
- This restriction works well when simulation signatures are used. It may be removed in the future.
Examples of completely-specified functions, incompletely-specified functions, and Boolean relations represented by the proposed format can be found in Figure 1 of the following technical report.
The output format for a synthesized circuit is an (X)AIGs represented as an array of fanin pairs for the nodes listed in a topological order.
An example of the AIG produced by a resubstitution engine can be found in Section V of the technical report.
The resulting circuits can be written into a file in the AIGER format.
The results produced by the resub engines can be verified using command "resub_check".
Three representative sets of resub benchmarks are currently available:
- Resub instances generated by command "resub"
- These instances are useful to test the fast resub engine (command "resub_unate")
- Resub instances generated by command "runeco"
- These instances are useful to test the high-effort resub engine (command "resub_core")
- Boolean relations generated by command "&genrel"
- These instances are useful to test SAT-based exact synthesis (command "twoexact")
This work is done in collaboration with Yukio Miyasaka (UC Berkeley), Alessandro Tempia Calvino (EPFL), and Andrea Costamagna (EPFL). It is supported at UC Berkeley by the SRC Contract 3173.001 "Standardizing Boolean transforms to improve quality and runtime of CAD tools" and the NSA Grant "Novel methods for synthesis and verification in cryptanalytic applications".