Rim Semiconductor Company (fka RSMI)

[dilt1]

A little info from digging a bit this morning on a Dr. Greaves search.....

http://www.cl.cam.ac.uk/~djg/wwwhpr/dslogic.html

Some of the highlights from the link:

The recent development in the size of problems that may be tackled with SAT solvers now enables problems of 100K variables to be readily solved. This is a useful size both for hardware and for software synthesis, provided the problem and the possible solutions can be phrased as logic functions.

There are many ways of using a SAT solver to generate hardware designs, but one of the most simple is to postulate a pseudo-FPGA architecture and allow the SAT solver to program it. In the basic case, the problem to be solved is phrased as a formal logic function and the behaviour of the FPGA given a given programming is expressed similarly. Then a bi-equivalence equation can be solved by a SAT solver to generate solutions. Un-used gates in the FPGA are then removed using standard identities to trim the solution for ASIC or other flows. Finally, we can select from a number of solutions either by refining the query or selecting from the generated solutions using cost evaluations (e.g. lines of code or gate count).

Note that the info is current, dated January 2003