The GSAT Chip

Tim Danner, Reuven Lax, and Andy MacKay

Abstract: The GSAT chip solves logic satisfiability problems. Given a Boolean expression (in a specific but general canonical form called 3CNF), the chip uses a randomized algorithm (GSAT) to find a truth assignment to the variables which satisfies the expression. The expression is kept in 4kB of off-chip SRAM, and the work variables (128) are kept in on-chip register space.

Contents

Contents

1  Introduction
    1.1  Attacking SAT
    1.2  How GSAT works

2  Functional Description
    2.1  Working Variables
    2.2  Expression Storage
    2.3  Randomness
    2.4  Counters
    2.5  Controller
    2.6  Pin/Signal Mappings
        2.6.1  Inputs
        2.6.2  Outputs
        2.6.3  Pin Diagram

3  Circuit Design
    3.1  Logic Diagrams
    3.2  System Timing Diagrams
    3.3  irsim Results of Entire Chip

4  PLA Description
    4.1  Input to meg

5  Circuit Layout
    5.1  Plots of Low-level Cells
    5.2  Plots of Functional Units
    5.3  Cell Heirarchy
    5.4  Floorplan
    5.5  Full Plot of Chip

6  Summary
    6.1  Division of Work by Group Members
        6.1.1  Tim Danner
        6.1.2  Reuven Lax
        6.1.3  Andy MacKay
    6.2  Comments and Suggestions on CAD tools