SAT-Compress algorithm - Manual

Copyright (C) 2012, CTU Prague, Jiri Balcarek, Petr Fiser, Jan Schmidt

***********************************************************************

SAT-Compress algorithm - test patterns compression algorithm based on overlapping of the test patterns (stuck-at fault model).

File specification

Note that at least bench file must be specified for SAT-Compress v 1.1 and moreover file for compressed bitstream must be specified for SAT-Compress v1.0.

-n fn Name of the .bench file (v 1.0 + v 1.1).
-t fn Specifies output file for the compressed output stream (v 1.0 only).

SAT-Compress options

-DC enables searching for don't care bits in test patterns (implicitly set false, v 1.0 only)
-S choose sort heuristic to be applied on fault list (v 1.0 only)
n = 0 - sort disabled (default)
n = 1 - sort heuristic MAX-MIN
n = 2 - sort heuristic MIN-MAX
-W specify first fault to be processed (initial seed, implicitly set 0, v 1.0 only)
-rr remove redundant faults - set false (implicitly set true, v 1.1 only)
-pi reduce Care Bit count - set true (implicitly set false, v 1.1 only)
-ps use presimulation - set true (implicitly set false, v 1.0 + v 1.1)
-atpg use clasic ATPG mode - set true (implicitly set false, v 1.1 only)
-rep print report - set true (implicitly set false, v 1.1 only)
-sim turn simulation off - set false (implicitly set true, v 1.1 only)
-ffp print CNF for fault free circuit and quit (implicitly set false, v 1.1 only)
-exp enable export of CNFs to the directory which is set by next parameter (v 1.1 only)
-uf enable UNSAT filtr based on resolution table (implicitly set false, v 1.1 only)
-df enable dynamic resolutions in UNSAT filtr (implicitly set false, v 1.1 only)
-scnf enable store cnf in memory instead of on-fly generation (implicitly set false, v 1.1 only)
-scnfr enable store reduced cnfs in memory (implicitly set false, v 1.1 only)
-expFlt export atalanta fault list to the specified file (implicitly set false, v 1.1 only)
-start set start fault (initial seed, implicitly se 0, v 1.1 only)

Command line examples

SAT-Compress v 1.1

 satcompress -n c17.bench
Run compression of test patterns for c17 benchmark circuit (default mode). 
 satcompress -n c17.bench -atpg
Run standard SAT-ATPG for c17 benchmark circuit. Test patterns are stored in c17.bench.tst. Stats are written in file statssolver.csv. 
 satcompress -n c17.bench -pi -ps
Run compression of test patterns for c17 benchmark circuit with CNF presimulation and don't care reduction. 
 satcompress -n c17.bench -uf
Run compression of test patterns for c17 benchmark circuit with static UNSAT filter enabled. 
 satcompress -n c17.bench -uf -df
Run compression of test patterns for c17 benchmark circuit with static and dynamic UNSAT filter enabled.

SAT-Compress v 1.0

 satcompress -n c17.bench -t compressed_bitstream.pat
Run compression of test patterns for c17 benchmark circuit and stores compressed bitstream to file(default mode). 
 satcompress -n c17.bench -t compressed_bitstream.pat -PS
Run compression of test patterns for c17 benchmark circuit with CNF presimulation and stores compressed bitstream to file. 
 satcompress -n c17.bench -t compressed_bitstream.pat -PS -DC
Run compression of test patterns for c17 benchmark circuit with CNF presimulation and don't care bit reduction. Stores compressed bitstream to file. 
 satcompress -n c17.bench -t compressed_bitstream.pat -PS -DC -W 3
Run compression of test patterns for c17 benchmark circuit with CNF presimulation and don't care bit reduction. Starts with third fault in the fault list. Stores compressed bitstream to file. 
 satcompress -n c17.bench -t compressed_bitstream.pat -PS -DC -W 3 -S 1
Run compression of test patterns for c17 benchmark circuit with CNF presimulation and don't care bit reduction. Use sort heuristic MAX-MIN on the fault list. Starts with third fault in the fault list. Stores compressed bitstream to file.

File Formats

BENCH Format

The input netlist format for atalanta is ISCAS89 netlist format except for the following two cases. The first line should be # followed by the name of the circuit. The lines beginning with # excluding the first line are comment lines and ignored. These comment lines may be put into any part of the netlist. It should be noted that the order of gates appearing in the netlist is not significant. The name of gates can be a string of alpha-numeric characters (0-9, A-Z, a-z, _, [, or ]).

Supported Gates
-------------------------------------------------------
   syntax                   gate type
-------------------------------------------------------
   INPUT                    primary input
   OUTPUT                   primary output
   AND                      and gate
   NAND                     nand gate
   OR                       or gate
   NOR                      nor gate
   XOR                      2 input exclusive-or gate
   BUFF or BUF              buffer
   NOT                      inverter
-------------------------------------------------------
* Gate types can be also written in lower case.
EXAMPLE: ISCAS89 NETLIST FORMAT (c17.bench) 
# c17
# 5 inputs
# 2 outputs
# 0 inverters
# 6 gates ( 6 NANDs )

INPUT(1)
INPUT(2)
INPUT(3)
INPUT(6)
INPUT(7)

OUTPUT(22)
OUTPUT(23)

10 = NAND(1, 3)
11 = NAND(3, 6)
16 = NAND(2, 11)
19 = NAND(11, 7)
22 = NAND(10, 16)
23 = NAND(16, 19)

Fault List Format

        ------ EXAMPLE: A FAULT LIST FILE ----------------------
        gate_A->gate_B /1
        gate_A->gate_B /0
        gate_A /1
        gate_B /1
        --------------------------------------------------------
In the above example, gate_A and gate_B are the name of gates. The first line, "gate_A->gate_B /1" describes the stuck-at 1 fault on the gate_B input line, which is connected to gate_A. Similarly, the second line, "gate_A->gate_B /0" describes the stuck-at 0 fault on the gate B input which is connected to gate_A. The third and fourth lines describe the stuck-at 1 faults on the gate_A output and the gate_B output, respectively.