I'm using Espresso logic minimizer to produce a minimized form of a set of boolean equations. However rather than generating logic for a programmable array logic (which is what Espresso is normally used for), I am looking to implement these on a standard microprocessor. The trouble is that Espresso produces output in conjunctive normal form, which is perfect for a PAL but non-optimal for an x86 or PPC.
For instance, Espresso ignores XOR entirely - in the below Espresso output, the subexpression (!B0&!B1&B2&!B3) | (!B0&!B1&!B2&B3) is equivalent to (!B0&!B1&(B2^B3)). This substitution does increase the gate depth / critical path of the expression, but given that I'm looking at expressions with a sufficient number of terms to completely saturate the execution resources of any CPU around it seems reasonable to trade off some gate depth for reducing the overall # of instructions. I'd also like to extend it to understand how to use instructions like ANDC or NOR which are available on some processors of interest to me.
Example of the CNF expressions I'm looking at:
O0 = (B0&!B1&!B2&B3) | (!B0&B1&B2&B3) | (!B0&!B1&B2&B3) | (B1&!B3) | (!B0 &!B2&!B3);
O1 = (B0&B1&!B2&B3) | (B0&!B1&B2&!B3) | (B0&B1&B2&!B3) | (!B0&!B1&B2&!B3) | (!B0&!B1&!B2&B3) | (!B0&!B1&B2&B3) | (!B0&!B2&!B3);
O2 = (B0&!B1&!B2&B3) | (B0&!B1&B2&!B3) | (B0&B1&B2&B3) | (!B0&B1&!B3) | (!B0&!B2&B3) | (!B0&!B1&B2&B3);
O3 = (!B0&B1&!B2&!B3) | (B0&B1&B2&B3) | (!B0&B1&B2&B3) | (B0&B1&B2&!B3) | (B0&!B1&!B2) | (!B0&!B1&B2&!B3) | (!B0&!B1&!B2&B3);
So, to make this an actual question; in order of preference:
Do you know of an option or extension of Espresso that will produce the kind of expressions I want?
Do you know of any tool for boolean logic minimization that understands (or can be taught) various gate types, rather than only producing CNF for PALs?
Do you know of an algorithm for converting from CNF expressions like the ones above to expressions using additional types of gates?
If you don't know of an algorithm for it, do you know of, or can think of, any useful heuristics in doing this?
(And, just in case you were going to suggest it - testing shows that GCC and ICC (or, I would bet, any other C compiler in existence) aren't smart enough to do the processor specific minimization for me from the CNF expressions - that would be really really nice, but examining the output of -O3 -S for both of them shows they can't even catch the cases where XOR can be used).
The most well-known algorithm for Boolean formula minimisation is the Quine-McCluskey algorithm, which yields the smallest DNF formula, but is computational expensive (necessarily, since the problem is outside PTIME, cf. The complexity of Boolean formula minimization, 2007). There's a literate Java implementation; the basic concept is crucial to Prolog, so if you have any experience with Prolog, the idea should come easily enough.
Postscript There's an IEEE-paywalled article, Extending Quine-McCluskey for exclusive-or logic synthesis, abstract:
Various forms of Boolean minimization have been used within electronic engineering degrees as a key part of the syllabus. Typically, Karnaugh maps and Quine-McCluskey methods are the principal exhaustive search techniques for digital minimization at the undergraduate level as they are easy to use and simple to understand. Despite the popularity of these methods, they are not well suited to typical digital circuits. Simple examples of such circuits are parity, adders, gray code generators, and so on. The common factor among these is the Exclusive-Or logic gate. This problem is exacerbated by the increasing importance of Exclusive-Or in modern design. This paper proposes an extension to the Quine-McCluskey method which successfully incorporates Exclusive-Or gates within the minimization process. A number of examples are given to demonstrate the effectiveness of this approach. This technique is easy to master as it can be considered to be an extension to the Quine-McCluskey method.
I had been thinking of how to extend the method before I looked this up: you should be able to synthesise applications of XOR by using an alternate version of resolution that corresponds to them. For example, for a disjunctive clause F in a CNF, which does not contain either of the atoms A, or B, from the clauses F | A | ~B and F | ~A | B, then you can replace them by F | XOR(A,B).