CIOPS (CIrcuit OPtimization System) is a tool for minimizing Boolean circuits and for the exact synthesis of Boolean circuits. CIOPS is based on using a QBF (Quantified Booelan Formula) encoding for finding minimal representations of given Boolean circuits.
To use CIOPS the following dependencies must be installed:
Additionally, at least on of the following QBF solvers need to be installed.
We recommend using the solver QFUN. In addition to installing a solver also the path to the binary needs to be set in utils.py.
To use ABC for inprocessing, the ABC synthesis and verification system needs to be installed. Additionally, the path to the ABC binary needs to be set in utils.py.
To read and write AIGs (And-Inverter Graph) the AIGER library is used.
We only provide instructions for building CIOPS on a LINUX system.
git clone --recursive https://github.com/fxreichl/ciops
cd ciops/aiger_io
mkdir build && cd build
cmake ..
make
CIOPS is mainly intended for circuit minimization but also supports exact synthesis. The goal of exact synthesis is to find a Boolean circuit that represents a given Boolean functions. The generated circuit needs to be minimal, i.e. there is no other circuit representation of the given function with fewer gates. Circuit minimization aims at reducing the number of gates in a given Boolean circuit. While in circuit minimization no guarantee is given that there is no smaller representation, minimization works with significantly larger circuits.
Exact Synthesis is realized in exactSynthesiser.py. To run this script use:
exactSynthesiser.py <Specification> <Result>
Specificationthe function to synthesize given in the Berkeley Logic Interchange Format (BLIF). While BLIF is a format for specifying circuits it can also be used to directly specify a Boolean function by a truth table if a single gate representing the function is used.Resultthe file to which the resulting circuit shall be written. By default, the result is given as a BLIF. If the option --aig is used the result is given in the AIGER format (if the filename has the .aag extension the ASCII AIGER format is used otherwise the binary AIGER format is used).
The available options are listed if -h is used.
Circuit Minimization is realized in reduce.py. To run this script use:
reduce.py <Specification> <Result> <Limit>
Specificationthe circuit to minimize. Given either in the BLIF or in the AIGER format.Resultthe file to which the resulting circuit shall be written. By default, the result is given as a BLIF. If the option --aig is used the result is given in the AIGER format (if the filename has the .aag extension the ASCII AIGER format is used otherwise the binary AIGER format is used).Limitthe available time budget given in seconds.
The available options are listed if -h is used.