Plans regarding building packages related to boolean functions.
More...
Go to the source code of this file.
Detailed Description
Plans regarding building packages related to boolean functions.
See OKlib/Satisfiability/FiniteFunctions/plans/general.hpp for the central module regarding boolean functions (and generalisations).
 Todo:
 BDD's
 Todo:
 Aiger
 Todo:
 ABC
 Todo:
 Translations to SAT
 Todo:
 Boolean functions

DONE (now automatically installed) There is an Rpackage with Quine/McCluskey etc.

Installation (from CRAN)
> oklib R
# Within R environment
> install.packages("QCA")
This draws the package from external CRAN sources. The lpSolve package dependency seems to be already installed for R in oklib.

Installation (from source tarball)
ExternalSources/Installations/R> oklib R
# Within R environment (with QCA_0.50.tar.gz in the current directory)
> install.packages("QCA_0.50.tar.gz", repos=NULL)
Setting the "repos" parameter to null seems to force it to treat the package arguments as file paths to tar.gz packages.

http://www.dei.isep.ipp.pt/~ACC/bfunc/ seems not to be open source.

http://www.tcs.hut.fi/~tjunttil/circuits/index.html has translators and generators for boolean circuits.
 Todo:
 Logic synthesis

http://vlsicad.eecs.umich.edu/BK/Slots/slots/LogicSynthesis.html

Scherzo

Developed by Olivier Coudert (http://www.ocoudert.com/).

Uses implicit BDD representation for primes and reduction techniques to avoid blow up in size of problem due to large numbers of prime implicates.

Coudert has provided the code to MG, although it is not clear whether he would be willing to make it opensource.

The source builds with some minor Makefile changes but segfaults. This seems likely to be an issue with how MG is building it and the difference in architectures (Scherzo seems to have been developed for systems other than standard x86 / x86_64).

MG needs to email Coudert again to check whether he would be willing to opensource the application.

BOOM

Developed by Petr Fiser (http://service.felk.cvut.cz/vlsi/prj/BOOM/).

Nonexact boolean minimisation, but allows iterative minimisation.

According to experimental results on the project site, the software is highly competitive.

License requires authors reference particular papers if one uses the software, and one must provide details to download the software (MG hasn't done this).

Using genetic programming:

There are quite a few papes on finding (digital) circuits via genetic programming, but apparently no software.

Grigory Yaroslavtsev and Alexander Kulikov have written some software to find short circuits (over the full binary base for example).

egntott http://code.google.com/p/eqntott/
 Todo:
 Improve documentation for Espresso

We should improve the sourcecode, so that the option "version" is recognised.

At the ExternalSources page we need an indexpage for the various pieces of documentation we have.

We need to investigate what is in espressobookexamples.tar.gz:

This tarball contains a variety of different PLA files, which don't have any documentation along with them.

There is a book "Logic Minimization Algorithms for VLSI Synthesis" by Robert Brayton (the author of Espresso).

Given the name of the tarball, "Logic Minimization Algorithms for
VLSI Synthesis" seems a likely candidate for the "book" the filename refers to (MG has ordered a copy).

The PLA format:

The "PLA format" is documented at ExternalSources/sources/Boolean/Espresso/espresso.5.html with additional information in ExternalSources/sources/Boolean/Espresso/man_octtools_espresso.html.

Finite functions with boolean variables:

A PLA represents a partial finite function, f : {0,1}^n > {0,1}^m, by encoding the DNF of the relational viewpoint of f.

By the relational viewpoint, we mean representing the boolean function which takes both input and output bits and returns true iff f maps the given input to the given output. More precisely, representing f' : {0,1}^(n+m) > {0,1} such that f'((I,O)) = 1 if f(I) = O.

The "header" of the PLA file:

The number of input and output variables are specified first with lines of the form: where n and m are the positive integer number of input and output variables.

Additional lines such as ".type" (discussed below), and others discussed in the documentation, may also be specified in the "header" of the file.

The "clauses":

Each line after the header is:

a sequence of characters I in {1,0,} of size n; followed by

a space; followed by

a sequence of characters O in {1,0,} of size m.
where:

Each line encodes a DNF clause which is part of a DNF representation for the partial finite function using the relational viewpoint.

That is, each line encodes that f(I') = O', where I' and O' are the boolean vectors corresponding to the strings I and O for that line.

A "" in I indicates that f(I') = O' for both values of the corresponding variable.

A "" in O indicates that f(I') = O' but the output value, for the variable the "" corresponds to, is undefined.

Additional options:

".type X": specifies how to interpret total assignments left unspecified, where X is one of the following:

"f": unspecified and assignments with undefined ouputs are assumed to be false (0).

"r": unspecified and assignments with undefined outputs are assumed to be true (1).

"fd": unspecified assignments are assumed to be false (the default for espresso).

"fr": unspecified assignments are considered to be "don't care" values.

"fdr": there should be no unspecified values.

The PLA standard also allows one to provide names for variables, as well as other options which give Espresso information on how to minimise the finite function provided. These options are discussed in

Lines in a PLA file starting with the "#" symbol are comments.

Note here that there is a difference between "undefined" and "unspecified".

One can use "" for an output bit to explicitly *specify* that the partial finite function defined by the PLA is undefined for the corresponding input bits. A total assignment is unspecified if there is no espresso line which specifies its value.

Examples:

The DNF {{1,2,3},{1,4,5}} becomes
.i 5
.o 1
111 1
010 1

The two bit adder (from the espresso documentation):
# 2bit by 2bit binary adder (with no carry input)
.i 4
.o 3
0000 000
0001 001
0010 010
0011 011
0100 001
0101 010
0110 011
0111 100
1000 010
1001 011
1010 100
1011 101
1100 011
1101 100
1110 101
1111 110

At the maxima level:

Finite functions with multivalued variables:

The PLA format allows one to specify that certain boolean variables should be considered together as a single multivalued variable.

Rather than using ".i" and ".o" to specify the number of input and output variables, one specifies: where n is the total number of variables, nb is the number of boolean variables (always given first in the variable ordering), and di is the number of bits used to represent the i'th multivalued variable.

The function is then specified as before, but the bits in multivalued variables are separated by "" and the last multivalued variable is the output value (no spaceseparation).

For example (from the manual):
.mv 8 5 2 3 4
0010101000000
1010100101000

We need to better understand multivalued PLAs and relate it to our own considerations of nonboolean clausesets etc.

All remaining options allowed in a PLA file should be documented here and then this later moved to docus.

We need to fully specify (in our system, using our language) what "PLAs" are, and create documentation for that. Perhaps we also need that at Maximalevel.
 Bug:
 DONE (added additional entries to the configuration specific to the source directories) False build for Espresso

The directory names do not follow our standards.

In particular, espresso has the package name "espressoab1.02.3.tar.gz" and directory names "espressoab1.0", and yet it's executable name is "espresso2.3", all of which are very different.

This initial decision was made so as not to change the version information too much from the original (keeping with the authors original version information (1.0)) but adding more reasonable version information at the same time (the version number as printed by the executable).

To bring things inline with other packages, espresso should simply be repackaged to "espresso2.3.tar.bz2" with "espresso2.3" as the directory name and "espresso2.3" as the executable name.
Definition in file BooleanFunctions.hpp.