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".
