ALGOS Logo

What is CGRASP ? CGRASP is a circuit structure-aware version of the satisfiability tool GRASP created at the ALGOS group of INESC-ID. It is intended to be used in solving satisfiability problems derived from combinational logic circuits (ATPG, CEC, CDC, etc).

Where can I get CGRASP ? You can get the source code from below.

What is the input format of CGRASP ? CGRASP accepts as input file an extended version of the ISCAS'85 format. This version contains the same netlist as in the ISCAS'85 format plus the support for ITE (if-then-else) gates and clause information.  Each clause is added as a comment and can only be understood by CGRASP. The following example file illustrate a possible input file.


# Example file

# I/O ports
INPUT (a)
INPUT (b)
INPUT (c)
OUTPUT (z)

# combinational circuit
x = NAND (a, b)
y = ITE (a, b, x)
z = OR (y, x)

# clauses
#@ z -y a


In the previous example file, we specify a problem in which we have a combinational circuit with primary inputs a, b, and c and a primary output z, containing three gates: a NAND gate, an ITE (if-the-else) gate and an OR gate. Besides the circuit we add a CNF clause (z+y'+a). For this example, CGRASP will try to find one set of assignments for the variables in order to satisfy the clause and to obtain consistent assignments to the nodes values.

Source code & Binaries

Source code: cgrasp.tar.gz
Binaries: cgrasp-linux-rh5.2.gz[Linux RedHat 5.2], cgrasp-linux-rh6.2.gz[Linux RedHat 6.2], cgrasp-solaris5.gz[Solaris 5], cgrasp-solaris7.gz [Solaris 7]

History

[LGS - Fri Oct  8 18:20:33 WEST 1999] CGRASP basic version
[LGS - Wed Oct 13 19:48:26 WEST 1999] temporarily removed sources & binaries
[LGS - Mon Oct 18 21:28:40 WEST 1999] new corrected version added
[LGS - Thu Jul 6 18:21:53 WEST 2000] added support for larger files


Any comments regarding this page or CGRASP can be sent to "lgs(at)inesc-id.pt".