Welcome to the CGRASP Homepage !
Introduction
What is CGRASP ? CGRASP is a circuit structure-aware version
of the satisfiability tool GRASP created at the ALGOS group of INESC. 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 here.
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
# 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.
Sources: 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