[Go to first, previous, next page]

2 Functional Description

To solve satisfiability problems with GSAT, a number of components are needed. We need a place to keep the working variables and the expression itself. We need a source of randomness and several moderately large counters. Finally, we need a controller which actually implements GSAT.

2.1 Working Variables

Background research revealed that an interesting SAT solver would have to be able to handle 100 variables at a bare minimum. An on-chip register file of 128 bits looked feasible, but 256 bits would be tough. We chose to go with 128, arranged as 16 one-byte (8-bit) words.

2.2 Expression Storage

Since we elected to support 128 variables, the encoding of the expression became simple. A reference to a variable takes 7 bits, and any variable reference may be complemented (B' instead of B), so that needs one bit to record, for a total of 8 bits (one byte) per variable reference. 3CNF uses three variables per clause, and an arbitrary number of clauses. This means 3 bytes per clause, but we need a way to indicate when the expression is complete. We chose to use a sentinel clause for this purpose: (a₁₂₇' + a₁₂₇' + a₁₂₇').According to the encoding scheme, this would be written as three bytes of all ones (FF, FF, FF in hexadecimal). This pattern is easy to detect and does not appreciably reduce the generality of the solver.

Complexity studies found that SAT problems are hardest when the number of clauses (recall that a clause is an OR of three variables, each of which may be complemented) is 3 to 4 times the number of variables. Much smaller than this and the satisfiability problem becomes easy - there a many solutions, any number of which can be found quickly. Much more than this ratio and the problem is overconstrained and it is straightforward to show (using software techniques not directly related to GSAT) that there is no solution at all.

Four times as many clauses as variables would be 512 clauses. That's 1536 bytes, since each clause takes three. This means that we need 12288 bits of storage for the expression, which would be an interesting challenge with a transistor budget of 5 to 6 thousand. So the expression must be kept off chip.

External SRAM chips have been used in the past. The course web page mentions that the Dallas Semiconductor DS1230 256 kilobit non-volatile SRAM was used in 1997. That appeared to meet our needs (though it is considerably larger than 12288 bits), so we designed for that chip.

We actually included 12 bits of addressing, which actually allows for 1365 clauses (including the terminator). This is somewhat more than twice what we really need (512 clauses), but in this case using 12 bits instead of 11 didn't hurt, and 12 is a nicer number than 11.

So talking to the external memory requires 12 output pins and 8 input pins, plus a 12-bit counter to iterate through the memory, and an 8-bit register to receive the data back (the DS1230 is byte-addressable and returns 8 bits at a time). Also, a three-bit shift register will be needed to detect when we've hit the terminating clause (we call this unit ``ender'').

2.3 Randomness

At each iteration of the GSAT algorithm, a variable must be selected randomly, which means 7 bits of randomness. Since an iteration of GSAT requires reading through the entire expression, randomness is consumed fairly slowly. The two major options are to implement a psuedo-random number generator on the chip or to import the randomness through a pin.

Bringing the randomness in from off-chip gives finer-grained control for testing, and simplifies the layout design, so we allocated one pin for randomness and hooked it up to an 8-bit shift register which shifts on every cycle (we use only the freshest randomness).

2.4 Counters

We need two big counters. The first is a 10-bit counter to count the clauses that are currently satisfied. You can tell whether the whole expression is satisfied without a counter (just keep and-ing the value of each clause into a 1-bit register), but the GSAT algorithm needs to be able to evaluate the efficacy of individual bit flips. It's also necessary to (optionally) save the previous value of the counter.

The second counter has 12-bits and is used to address the memory. The 10-bit counter was implemented as a PLA generated by meg. We attempted to implement the 12-bit counter the same way, but the tools choked on a system with 4096 states. Instead, we generated a 4-bit counter and connected three of them together.

2.5 Controller

The master controller is a generated PLA with 43 states, 8 inputs, and 21 outputs. The meg file used to produce it can be found in Section 4.1.

[Go to first, previous, next page]