54 lines
3.2 KiB
ReStructuredText
54 lines
3.2 KiB
ReStructuredText
Introduction
|
|
============
|
|
|
|
The `percy` library provides a collection of SAT based exact synthesis engines.
|
|
That includes engines based on conventional methods, as well as
|
|
state-of-the-art engines which can take advantage of DAG topology information
|
|
The aim of `percy` is to provide a flexible common interface that makes it easy
|
|
to construct a parameterizable synthesis engine suitable for different domains.
|
|
It is a header-only library, meaning that it can be used simply by including
|
|
the percy/include folder in your project. Internally, `percy` uses the `kitty`
|
|
library [#]_ to represent the truth tables of the functions to be synthesized.
|
|
|
|
Synthesis using `percy` concerns five main components:
|
|
|
|
1. *Specifications* -- Specification objects contain the information essential
|
|
to the synthesis process such as which functions to synthesize, I/O
|
|
information, and possibly optional parameters such as conflict limits for
|
|
time-bound synthesis, or topology information.
|
|
2. *Encoders* -- Encoders are objects which convert specifications to CNF
|
|
formulae. There are various ways to create such encodings, and by
|
|
separating their implementations it becomes simple to experiment with
|
|
different encodings in various settings.
|
|
3. *Solvers* -- Once an encoding has been created, we use a SAT solver to find
|
|
a solution. Currently supported are ABC's `bsat` solver [#]_, the
|
|
Glucose and Glucose-Syrup solvers, [#]_ and the CryptoMinisat solver. [#]_
|
|
Adding a new solver to `percy` is as simple as declaring a handful of
|
|
interface functions. [#]_
|
|
4. *Synthesizers* -- Synthesizers perform the task of composing encoders and
|
|
solvers. Different synthesizers correspond to different synthesis flows. For
|
|
example, some synthesizers may support synthesis flows that use topological
|
|
constraints, or allow for parallel synthesis flows. To perform synthesis
|
|
using `percy`, one creates a synthesizer object. Synthesizers are
|
|
parameterizable: we can change their encoder and solver backends. This
|
|
happens at compile time, so there is no runtime overhead.
|
|
5. *Chains* -- Boolean chains are the result of exact synthesis. A Boolean
|
|
chain is a compact multi-level logic representation that can be used to
|
|
represent multi-output Boolean functions.
|
|
|
|
A typical workflow will have some source for generating specifications, which
|
|
are then given to a synthesizer that converts the specifications into optimum
|
|
Boolean chains. Internally, the synthesizer will compose its underlying encoder
|
|
and SAT solver in its specific synthesis flow. For example, a resynthesis
|
|
algorithm might generate cuts in a logic network which serve as specifications.
|
|
They are then fed to a synthesizer, and if the resulting optimum Boolean chains
|
|
leads to an improvement, are replaced in the logic network. In optimizing this
|
|
workflow, `percy` makes it easy to swap out one synthesis flow for another, to
|
|
change CNF encodings, or to switch to a different SAT solver.
|
|
|
|
.. [#] https://github.com/msoeken/kitty
|
|
.. [#] https://github.com/berkeley-abc/abc
|
|
.. [#] http://www.labri.fr/perso/lsimon/glucose/
|
|
.. [#] https://github.com/msoos/cryptominisat
|
|
.. [#] Unfortunately some solvers may not compile on your favorite OS...
|