# Automatický generátor testovacích vektorů (ATPG) založený na testu splnitelnosti booleovské formule

## sat_aptg-1.0

Copyright © 2008 - ČVUT FEL - Jiří Červák

- Synopsis
- Options
- Examples
- File formats

### Synopsis

    sat_atpg [options] [-n] bench_file_name

### Options

#### File specification

    -n <FILE>       specifies file in .bench format
    -t <FILE>       specifies output file with patterns
    -f <FILE>       specifies input file with faults
    -F <FILE>       specifies output file with faults
    -P <FILE>       specifies output for report
    -U <FILE>       prints not covered faults
    -d <FILE/DIR>   exports cnf forms of faults to FILE (one fault solved) or DIR/*.cnf
                      (more faults to solved), no ATG is performed

#### ATPG options

    -A              for each fault computes all test vectors, no compaction
    -D <n>          for each fault computes n test vectors, no compaction
    -e <0,1,2>      expand to dont cares: 0-none (default), 1-cnf, 2-structural
    -N              dont make compaction
    -r <0,1,2>      Fault reduction: 0-only ekvivalence, 1-also dominance (default),
                      2-risky (bad coverage)
    -a              appends one line of values to report file instead of rewrite file
                      with full report
    -ch             doesnt use eqivalence but Checkpoints theorem for fault init
    -W <0,1,2,3>    vektor format: 0-no, 1-inputs, 2-outputs 3-numbered list for -A
                      or -D mode
    -s              switch to dc_solver
    -l              prints Inputs
    -V              don't use active vars

### Examples

    sat_atpg -W 1 -e 2 -t c17.bench -P C17.pat c17.bench

### File formats

Following informations were adopted from http://service.felk.cvut.cz/vlsi/prj/Atalanta-M/

#### 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)

#### Test Pattern Files

##### Simple PAT Format (-W 1) and the input test pattern file (for simulation)

Consists of test patterns only. The j'th bit of a test pattern is the value of the j'th input of the circuit (in terms of their appearance in the circuit). For example, c17 has five inputs named input1, input2, input3, input6 and input7 which appear in the order in the netlist. The first bit of a test pattern is the value for input1, the second for input2, ..., and the last for input7.

##### Example: Test Pattern File for C17 (obtained by sat_atpg -t pattern.pat -W 1 c17.bench

    00101
    10100
    01110
    01010
    10011
    01100
    x0010
    01111
    11011

#### PAT Format with output values, more vectors for each fault (-W 3)

Contains test patterns and correct CUT responses. The ordinal number of the test pattern for a particular fault preceeds the colon (:). The test vectors are numbered in a reverse order, for simpler parsing.

##### Example: Test Pattern File for C17 (obtained by sat_atpg -D 5 -t pattern.pat -W 3 c17.bench )

    2:0011x
    1:0111x
    0:0010x
    4:10000
    3:00010
    2:10010
    1:00101
    0:10100
    4:11110
    3:11111
    2:01111
    1:10111
    0:01110
    4:00011
    3:10010
    2:10001
    1:10000
    0:01010
    4:01011
    3:11011
    2:01010
    1:11010
    0:10011
    1:1000x
    0:1001x
    4:11101
    3:11100
    2:00101
    1:01101
    0:01100
    2:x0000
    1:x0100
    0:x0010
    2:1011x
    1:1111x
    0:1010x
    4:11001
    3:11011
    2:10101
    1:01101
    0:01100
    4:11111
    3:11110
    2:00111
    1:01111
    0:01110
    1:x0111
    0:x1111
    3:01110
    2:11110
    1:11111
    0:01111
    4:00010
    3:10010
    2:00100
    1:00101
    0:10100
    4:11100
    3:11000
    2:11010
    1:11001
    0:11011
    2:x1000
    1:x1010
    0:x1100
    4:0100x
    3:0101x
    2:1100x
    1:1101x
    0:0110x
    2:x0001
    1:x0011
    0:x0101
    4:0110x
    3:0101x
    2:1101x
    1:1010x
    0:1111x
    4:0011x
    3:0111x
    2:0001x
    1:1001x
    0:0010x
    4:x0001
    3:x0011
    2:x1011
    1:x0101
    0:x1100
    4:x0111
    3:x1111
    2:x0000
    1:x0010
    0:x0100

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

### The Report File Format

#### Example. The comments are not a part of the report file.

    Inputs:						5
    //primary inputs of circuit
    Outputs:					2
    //primary outputs of circuit
    Gates:						6
    //gates
    Faults:						22
    //faults generated or read
    Faults removed (dominance):			0
    //faults removed by dominance
    Faults not covered:				0
    //nontestable faults (posible redundant)
    Total vectors:					22
    //Total vectors generated
    Total vectors after compaction			22
    //Total vectors after compaction
    Average dc ratio:				0.345455
    // ratio of DC values/all values

    Total time:					0.01 s
    //total time
    Average count of clauses in CNF:		31.7273
    //average count of clauses
    Maximum of clauses in CNF:			57
    //maximum count of clauses over all faults
    Average count of variables in CNF:		15.0909
    //Average count fo variables
    Maximum of vars in CNF:				24
    //Maximum of vars
    Average count of binary clauses in CNF:		15.8182
    //count of clauses with exactly 2 literals
    Average clauses / vars ratio:			2.03425
    //ratio vars/clauses
    Maximum of clauses / vars ratio:		2.375
    //maximum ratio over all faults
    Minimum of clauses / vars ratio:		1.66667
    //minimum ratio over all faults

### DIMACS format

line startin g with c is comment. In comments the coding of variables is shown. A_10 is active var of gate 10 and f_22 is faulty var of gate 22 line p cnf 13 27 means 13 vars in 27 clauses.

    c v 13
    c 1 A_10
    c 2 1
    c 3 A_22
    c 4 10
    c 5 16
    c 6 22
    c 7 f_10
    c 8 f_22
    c 9 2
    c 10 11
    c 11 3
    c 12 6
    c 13 f_1
    p cnf 13 27
    1 0
    2 0
    3 0
    -4 -5 -6 0
    4 6 0
    5 6 0
    -7 -5 -8 0
    7 8 0
    5 8 0
    -3 6 8 0
    -3 -6 -8 0
    -9 -10 -5 0
    9 5 0
    10 5 0
    -11 -12 -10 0
    11 10 0
    12 10 0
    -2 -11 -4 0
    2 4 0
    11 4 0
    -13 0
    -1 3 0
    -1 4 7 0
    -1 -4 -7 0
    -13 -11 -7 0
    13 7 0
    11 7 0

    --------------------------------------------------------