EE 709: Assignment on Testing

Krishna Kumar Singh

Roll No.: 22B3968, IIT Bombay

October 30, 2025

Submission checklist
This PDF includes: (1) a clear description of the approach to each problem, (2) the full source
code used, and (3) complete execution results for all problems.[2]

1 Problem statement and circuit

We work on the given combinational NAND circuit with primary inputs

X1, X3, X6, X2, X7

and outputs
Y 1, Y 2
, using PI order
(x1, x3, x6, x2, x7)
. Tasks: Q1 fault equivalence classes, Q2 SAT-based complete test set for

C7, C8, C11

stuck-at faults, Q3 deductive fault simulation for vector

00000

.[2]

2 Environment and tools

Experiments run in a Docker image (Ubuntu 22.04) with MiniSat on PATH. DIMACS CNF
is solved via minisat -no-pre -verb=0 <cnf> <out>, parsing models from v ... 0
lines, as documented for MiniSat.[1]

3 Question 1: Fault equivalence via exhaustive signatures

How we approached it
- A single stuck-at fault dictionary was created by simulating every fault at every net over all

25 = 32

PI vectors. For each fault, the faulty outputs

(Y 1, Y 2)

1
per vector were packed as a 64-bit signature (two bits per vector).[3] - Faults with identical
signatures across all vectors were grouped into the same equivalence class; this matches the
textbook definition: two faults are equivalent iff every test that detects one detects the other
(i.e., identical output behavior for all inputs).[3]

Why the answer follows

- Exhaustive signatures guarantee completeness because every possible input was enumerated
for this 5-PI circuit, so indistinguishability under all inputs exactly captures equivalence. Hence,
the printed classes are provably correct for the stuck-at model.[4][3]

Detailed outputs
### QUESTION 1: Fault Equivalence Classes (computed exhaustively) ###
Class 1: {X1/sa0, C7/sa1}
Class 2: {X1/sa1}
Class 3: {X2/sa0, C8/sa0}
Class 4: {X2/sa1}
Class 5: {X3/sa0}
Class 6: {X3/sa1}
Class 7: {X6/sa0}
Class 8: {X6/sa1}
Class 9: {X7/sa0, C9/sa0, C12/sa1}
Class 10: {X7/sa1}
Class 11: {C7/sa0, C10/sa0, Y1/sa1}
Class 12: {C8/sa1}
Class 13: {C9/sa1}
Class 14: {C10/sa1}
Class 15: {C11/sa0, C12/sa0, Y2/sa1}
Class 16: {C11/sa1}
Class 17: {Y1/sa0}
Class 18: {Y2/sa0}
Total: 5 multi + 13 singles = 18 unique equivalence classes

4 Question 2: SAT-based ATPG (pure SAT)

How we approached it
- For each target
T ∈ {C7, C8, C11}
and
sa ∈ {0, 1}
, we build a two-copy miter: good and faulty copies share the PIs; the driver of

is cut in the faulty copy, and a unit clause forces

to the stuck value; a detection is enforced by

(Y 1g ⊕ Y 1f ) ∨ (Y 2g ⊕ Y 2f ) = 1

2
.[5][2] - All logic is encoded as CNF using Tseitin variables: NAND, XOR, OR; fanouts are
modeled with duplicated NANDs (e.g.,
C8/C9
,
C10/C11
) rather than equality constraints to avoid over-constraining.[6] - All-SAT enumeration: invoke
MiniSat; on each SAT model, add a 5-literal blocking clause over

(X1, X3, X6, X2, X7)

that negates the found assignment; repeat until UNSAT.[7] - To keep PIs in the printed model,
preprocessing is disabled with -no-pre; model lines are parsed from v ... 0.[1]

Why the answer follows

- In a SAT miter, a satisfying assignment corresponds exactly to a test that activates and
propagates the fault to some output (the XOR-OR of outputs is set to 1). Therefore, every
SAT model yields a valid detecting vector.[5][2] - Blocking clauses ensure each subsequent solve
finds a different detecting PI assignment; terminating at UNSAT means all detecting vectors for
that fault have been enumerated. This is the standard All-SAT with blocking guarantee.[8][7] -
Because all detection lists are obtained via repeated SAT on the same miter with accumulated
blocking clauses, Q2 is purely SAT-based with no simulation fallback.[9][2]

Detailed outputs
### QUESTION 2: Programmatic Test Generation (C7, C8, C11) ###
Targets: C7, C8, C11 (sa0/sa1)

C7/sa0: 00000 00001 00100 00101 01000 01001 01100 01101 01110 01111 10000 10001
C7/sa1: 11000 11001 11100 11101 11110 11111
C8/sa0: 00010 00011 00110 00111 01010 01011 10010 10011 10110 10111 11010
C8/sa1: 01110 01111 11110 11111
C11/sa0: 00000 00100 01000 01100 01101 01110 01111 10000 10100 11000 11100 11101
C11/sa1: 00010 00110 01010 10010 10110 11010

Minimal complete test set (3 vectors):

1. 01110 (detects: C7/sa0 C8/sa1 C11/sa0 )
2. 00010 (detects: C8/sa0 C11/sa1 )
3. 11000 (detects: C7/sa1 C11/sa0 )

5 Question 3: Deductive fault simulation (vector 00000)

How we approached it
- Deductive simulation attaches an L-list to each net, containing exactly those single stuck-at
faults that would invert that net under the current input. L-lists are initialized at PIs and
propagated through gates using local rules for NAND fan-ins and controlling/non-controlling
values.[10][4] - For
(x1, x3, x6, x2, x7) = (0, 0, 0, 0, 0)
, L-lists are computed once in a single forward pass, then

L(Y 1)

3
,
L(Y 2)
, and their union are reported.[11]

Why the answer follows

- Deductive simulation reasons symbolically about all single faults in one pass; a fault appears
in
L(Y k)
iff it would change
Yk
relative to the fault-free value under the chosen input. Thus the union of

L(Y 1)

and
L(Y 2)
is exactly the set of faults detected by vector

00000

.[12][4]

Detailed outputs
### QUESTION 3: Deductive Fault Simulation ###
Input: X1=0, X3=0, X6=0, X2=0, X7=0

Fault-free: Y1=0, Y2=0

Detected faults (evaluated dynamically):

X2/sa1 (Y1=1, Y2=1)
X7/sa1 (Y1=0, Y2=1)
C7/sa0 (Y1=1, Y2=0)
C10/sa0 (Y1=1, Y2=0)
C11/sa0 (Y1=0, Y2=1)
C12/sa0 (Y1=0, Y2=1)
Y1/sa1 (Y1=1, Y2=0)
Y2/sa1 (Y1=0, Y2=1)

Total: 8 DISTINCT faults

--- Deductive L-list trace (full) for vector 00000 ---

L(Y1): C7/sa0 X2/sa1 C10/sa0 Y1/sa1
L(Y2): X2/sa1 C11/sa0 X7/sa1 C12/sa0 Y2/sa1
Detected (deductive union): C7/sa0 X2/sa1 C10/sa0 Y1/sa1 C11/sa0 X7/sa1 C12/sa0

4
 6 Reproducibility and usage
• Build: gcc -O0 -g -std=c99 -o final correct correct ee709 final.c in
a container with MiniSat on PATH.[1]

• Run: ./final correct to print Q3, then Q2 lists and minimal cover, then Q1 classes.[1]

• The program writes one CNF and one model file per Q2 target and deletes them after
enumeration.[1]

7 Quick start and reproducibility

Quick start (Docker)
• Build the image (pinned base): docker build -t ee709t estg enm sat.

• Start an interactive shell with the project mounted at /app: docker

run -it --rm -v "(pwd)” : /appee709t estg enm sat

• Inside the container, verify MiniSat is on PATH and usable: which

minisat minisat --help | head -5 Expected: /usr/local/bin/minisat
and a usage banner showing minisat [options] <input-file> <result-output-fil

• Compile and run the program: gcc -O0 -g -o finalc orrectcorrecte e709f inal.c−
std = c99

Dockerfile
The Dockerfile used for all results:
1 FROM ubuntu:22.04
2

3 Prevent interactive prompts

4 ARG DEBIAN_FRONTEND=noninteractive
5
6 Install build tools + cmake + git + zlib
7 RUN apt-get update && apt-get install -y
8 build-essential
9 gcc
10 g++
11 make
12 cmake
13 git
14 zlib1g-dev
15 ca-certificates
16 && rm -rf /var/lib/apt/lists/*
17
18 === BUILD MODERN MINISAT (C++11 clean) ===
19 RUN cd /tmp &&
20 git clone [Link] &&
21 cd minisat &&
22 mkdir -p build && cd build &&
23 cmake .. &&
24 make &&
25 cp minisat /usr/local/bin/minisat &&
26 chmod +x /usr/local/bin/minisat &&

5
27 rm -rf /tmp/minisat
28
29 Verify
30 RUN minisat --help | head -3
31
32 WORKDIR /app
33 COPY . .
34
35 CMD ["/bin/bash"]

8 Appendix A: Full source code

1 #include <stdio.h>
2 #include <stdbool.h>
3 #include <string.h>
4 #include <stdint.h>
5
6
7 #include <stdlib.h> // system, strtol, labs, snprintf
8 #include <ctype.h> // isdigit
9 #include <string.h> // strcat, memset
10

11 // PI var constants (for blocking literals)

12 #define X1v 1
13 #define X3v 2
14 #define X6v 3
15 #define X2v 4
16 #define X7v 5
17
18 // CNF helpers
19 static void fprint_clause(FILE* f, const int* lits, int n){
20 for(int i = 0; i < n; i++) fprintf(f, "%d ", lits[i]);
21 fprintf(f, "0\n");
22 }
23
24 static void cnf_nand(FILE* f, int a, int b, int o){
25 int c1[2] = {a, o}; fprint_clause(f, c1, 2); // a | o
26 int c2[2] = {b, o}; fprint_clause(f, c2, 2); // b | o
27 int c3[3] = {-a, -b, -o}; fprint_clause(f, c3, 3); // ˜a | ˜b | ˜o
28 }
29
30 static void cnf_eq(FILE* f, int z, int x){
31 int c1[2] = {-z, x}; fprint_clause(f, c1, 2);
32 int c2[2] = {z, -x}; fprint_clause(f, c2, 2);
33 }
34

35 static void cnf_xor(FILE* f, int a, int b, int d){

36 int c1[3] = {-d, -a, -b}; fprint_clause(f, c1, 3);
37 int c2[3] = {-d, a, b}; fprint_clause(f, c2, 3);
38 int c3[3] = {d, -a, b}; fprint_clause(f, c3, 3);
39 int c4[3] = {d, a, -b}; fprint_clause(f, c4, 3);
40 }
41
42 static void cnf_or(FILE* f, int a, int b, int z){
43 int c1[2] = {-a, z}; fprint_clause(f, c1, 2);
44 int c2[2] = {-b, z}; fprint_clause(f, c2, 2);

6
45 int c3[3] = {-z, a, b}; fprint_clause(f, c3, 3);
46 }
47

48 // Updated: Miter writer with full fanout NANDs (no EQs), driver cut in
faulty copy, dynamic clause count
49 static int write_miter_cnf(const char* tgt_net, int sa, const char*
cnf_path, const int blocks[][5], int nblocks){
50 int VX1=1, VX3=2, VX6=3, VX2=4, VX7=5;
51 int C7g=6, C8g=7, C9g=8, C10g=9, C11g=10, C12g=11, Y1g=12, Y2g=13;
52 int C7f=14, C8f=15, C9f=16, C10f=17, C11f=18, C12f=19, Y1f=20, Y2f=21;
53 int D1=22, D2=23, DIFF=24; int nvars=24;
54
55 FILE* f = fopen(cnf_path, "w"); if(!f) return -1;
56 // Placeholder header; rewrite later with accurate m
57 fprintf(f, "p cnf %d %d\n", nvars, 0);
58 long hdr_pos = ftell(f); int m = 0; // Track clauses
59
60 // Good copy: Full fanout with duplicated NANDs (C9=NAND(X3,X6), C11=
NAND(C8,X2))
61 cnf_nand(f, VX1, VX3, C7g); m += 3;
62 cnf_nand(f, VX3, VX6, C8g); m += 3;
63 cnf_nand(f, VX3, VX6, C9g); m += 3; // Duplicate for fanout (no EQ)
64 cnf_nand(f, C8g, VX2, C10g); m += 3;
65 cnf_nand(f, C8g, VX2, C11g); m += 3; // Duplicate for fanout (no EQ)
66 cnf_nand(f, C9g, VX7, C12g); m += 3;
67 cnf_nand(f, C7g, C10g, Y1g); m += 3;
68 cnf_nand(f, C11g, C12g, Y2g); m += 3;
69
70 // Faulty copy: Cut driver NAND for target (skip emit, just force unit
later)
71 int cutC7 = (strcmp(tgt_net, "C7") == 0);
72 int cutC8 = (strcmp(tgt_net, "C8") == 0);
73 int cutC11 = (strcmp(tgt_net, "C11") == 0);
74
75 if(!cutC7){ cnf_nand(f, VX1, VX3, C7f); m += 3; }
76 if(!cutC8){ cnf_nand(f, VX3, VX6, C8f); m += 3; }
77 cnf_nand(f, VX3, VX6, C9f); m += 3; // C9f always full (not target)
78 cnf_nand(f, C8f, VX2, C10f); m += 3;
79 if(!cutC11){ cnf_nand(f, C8f, VX2, C11f); m += 3; }
80 cnf_nand(f, C9f, VX7, C12f); m += 3;
81 cnf_nand(f, C7f, C10f, Y1f); m += 3;
82 cnf_nand(f, C11f, C12f, Y2f); m += 3;
83
84 // Stuck-at unit on target net in faulty copy (sa=0: -v=0; sa=1: +v=1)
85 int v_stuck = cutC7 ? C7f : (cutC8 ? C8f : C11f);
86 int unit_fault[1] = {sa ? v_stuck : -v_stuck}; fprint_clause(f,
unit_fault, 1); m += 1;
87
88 // Miter: Force output difference (Y1g XOR Y1f OR Y2g XOR Y2f =1)
89 cnf_xor(f, Y1g, Y1f, D1); m += 4;
90 cnf_xor(f, Y2g, Y2f, D2); m += 4;
91 cnf_or(f, D1, D2, DIFF); m += 3;
92 int unit_diff[1] = {DIFF}; fprint_clause(f, unit_diff, 1); m += 1;
93
94 // Blocking clauses (5-lit each)
95 for(int b = 0; b < nblocks; b++){ fprint_clause(f, blocks[b], 5); m +=
1; }
96

7
 97 // Rewrite header with accurate clause count
98 long end_pos = ftell(f); fseek(f, 0, SEEK_SET);
99 fprintf(f, "p cnf %d %d\n", nvars, m); fseek(f, end_pos, SEEK_SET);
100 fclose(f); return 0;
101 }
102
103 // Updated: Solver call with -no-pre -verb=0; improved parsing (handles ’v’
prefix, spaces)
104 static int solve_miter_get_pis(const char* cnf_path, const char* out_path,
int* x1, int* x3, int* x6, int* x2, int* x7){
105 char cmd[256]; snprintf(cmd, sizeof(cmd), "minisat -no-pre -verb=0 %s %
s", cnf_path, out_path);
106 int rc = system(cmd); if(rc != 0) return -1; // Non-zero rc indicates
error
107

108 FILE* f = fopen(out_path, "r"); if(!f) return -1;

109 char line[8192]; if(!fgets(line, sizeof(line), f)) { fclose(f); return
0; }
110 if(strncmp(line, "SAT", 3) != 0 && strncmp(line, "SATISFIABLE", 11) !=
0) { fclose(f); return 0; }
111

112 int pi_vals[6] = {0}; int got_pi = 0;

113 while(fgets(line, sizeof(line), f)){
114 char* p = line;
115 while(*p){
116 // Skip spaces/tabs
117 while(*p == ’ ’ || *p == ’\t’) p++;
118 if(*p == ’v’ || *p == ’V’) { p++; continue; } // Skip ’v’
prefix
119 char* endp = p; long v = strtol(p, &endp, 10);
120 if(endp == p) break; // No number
121 p = endp;
122 if(v == 0){ // End of model
123 *x1 = pi_vals[1]; *x3 = pi_vals[2]; *x6 = pi_vals[3]; *x2 =
pi_vals[4]; *x7 = pi_vals[5];
124 fclose(f); return got_pi ? 1 : -1;
125 }
126 int var_id = labs((int)v); if(var_id >= 1 && var_id <= 5){
127 pi_vals[var_id] = (v > 0) ? 1 : 0; got_pi = 1;
128 }
129 }
130 }
131 fclose(f); return 0;
132 }
133
134
135 /* ===== Helpers for deductive L-lists (Q3) ===== */
136 typedef struct { const char* net; int sa; } FaultRec;
137 typedef struct { FaultRec f[256]; int n; } LList;
138

139 static void Ladd(LList* L, const char* net, int sa){

140 if (L->n < 256) { L->f[L->n].net = net; L->f[L->n].sa = sa; L->n++; }
141 }
142 static int Leq(const FaultRec* a, const FaultRec* b){
143 return a->sa==b->sa && strcmp(a->net,b->net)==0;
144 }
145 static void Luniq(LList* L){
146 for(int i=0;i<L->n;i++){

8
147 for(int j=i+1;j<L->n;){
148 if(Leq(&L->f[i],&L->f[j])){ for(int k=j;k<L->n-1;k++) L->f[k]=L
->f[k+1]; L->n--; }
149 else j++;
150 }
151 }
152 }
153 static void Lmerge(LList* Z, const LList* A, const LList* B){
154 Z->n = 0;
155 for(int i=0;i<A->n;i++) Ladd(Z,A->f[i].net,A->f[i].sa);
156 for(int i=0;i<B->n;i++) Ladd(Z,B->f[i].net,B->f[i].sa);
157 Luniq(Z);
158 }
159 static void Lprint(const char* name, const LList* L){
160 printf("%s: ", name);
161 for (int i=0;i<L->n;i++) printf("%s/sa%d ", L->f[i].net, L->f[i].sa);
162 printf("\n");
163 }
164 static int nand2(int a, int b){ return !(a && b); }
165 static int apply_fault_to_net(int val, const FaultRec* f, const char* net){
166 return (strcmp(f->net, net)==0) ? f->sa : val;
167 }
168
169 /* ============================================== */
170
171 /* NOTE: PI order used everywhere in this file: (x1, x3, x6, x2, x7) */
172 void eval_clean(int x1, int x3, int x6, int x2, int x7, int *y1, int *y2) {
173 int c1 = x1, c2 = x3, c3 = x3, c4 = x6, c6 = x7;
174
175 // G1 -> C7
176 int g1 = !(c1 && c2);
177 int c7 = g1;
178
179 // G2 -> C8, C9
180 int g2 = !(c3 && c4);
181 int c8 = g2, c9 = g2;
182
183 // G3 -> C10, C11
184 int g3 = !(c8 && x2);
185 int c10 = g3;
186 int c11 = g3;
187
188 // G4 -> C12
189 int g4 = !(c9 && c6);
190 int c12 = g4;
191
192 // G5 -> Y1
193 int g5 = !(c7 && c10);
194
195 // G6 -> Y2
196 int g6 = !(c11 && c12);
197
198 *y1 = g5; *y2 = g6;
199 }
200
201 void eval_faulty(int x1, int x3, int x6, int x2, int x7,
202 const char *fault_net, int stuck_val,
203 int *y1, int *y2) {

9
204
205 if (strcmp(fault_net, "X1") == 0) x1 = stuck_val;
206 if (strcmp(fault_net, "X3") == 0) x3 = stuck_val;
207 if (strcmp(fault_net, "X6") == 0) x6 = stuck_val;
208 if (strcmp(fault_net, "X2") == 0) x2 = stuck_val;
209 if (strcmp(fault_net, "X7") == 0) x7 = stuck_val;
210
211 int g1 = !(((strcmp(fault_net, "X1") == 0) ? stuck_val : x1) &&
212 ((strcmp(fault_net, "X3") == 0) ? stuck_val : x3));
213 int c7 = (strcmp(fault_net, "C7") == 0) ? stuck_val : g1;
214
215 int g2 = !(((strcmp(fault_net, "X3") == 0) ? stuck_val : x3) &&
216 ((strcmp(fault_net, "X6") == 0) ? stuck_val : x6));
217 int c8 = (strcmp(fault_net, "C8") == 0) ? stuck_val : g2;
218 int c9 = (strcmp(fault_net, "C9") == 0) ? stuck_val : g2;
219
220 int g3 = !(((strcmp(fault_net, "C8") == 0) ? stuck_val : c8) &&
221 ((strcmp(fault_net, "X2") == 0) ? stuck_val : x2));
222 int c10 = (strcmp(fault_net, "C10") == 0) ? stuck_val : g3;
223 int c11 = (strcmp(fault_net, "C11") == 0) ? stuck_val : g3;
224

225 int g4 = !(((strcmp(fault_net, "C9") == 0) ? stuck_val : c9) &&

226 ((strcmp(fault_net, "X7") == 0) ? stuck_val : x7));
227 int c12 = (strcmp(fault_net, "C12") == 0) ? stuck_val : g4;
228
229 int g5 = !(((strcmp(fault_net, "C7") == 0) ? stuck_val : c7) &&
230 ((strcmp(fault_net, "C10") == 0) ? stuck_val : c10));
231 int y1v = (strcmp(fault_net, "Y1") == 0) ? stuck_val : g5;
232
233 int g6 = !(((strcmp(fault_net, "C11") == 0) ? stuck_val : c11) &&
234 ((strcmp(fault_net, "C12") == 0) ? stuck_val : c12));
235 int y2v = (strcmp(fault_net, "Y2") == 0) ? stuck_val : g6;
236
237 *y1 = y1v; *y2 = y2v;
238 }
239
240 /* ===== Q1 helpers: exhaustive signature-based equivalence ===== */
241 typedef struct {
242 const char* net;
243 int sa; // 0 or 1
244 uint64_t sig; // pack Y1/Y2 across 32 vectors, two bits per vector
245 } FaultSig;
246
247 typedef struct {
248 uint64_t sig;
249 int idxs[128];
250 int n;
251 } SigGroup;
252
253 /* Map a 5-bit vector index to PIs using the p r o j e c t s PI order (x1,x3,x6
,x2,x7) */
254 static inline void vec_to_pis(int v, int* x1, int* x3, int* x6, int* x2,
int* x7){
255 // bits: b4 b3 b2 b1 b0; choose a consistent mapping for enumeration
256 *x1 = (v>>4)&1;
257 *x3 = (v>>3)&1;
258 *x6 = (v>>2)&1;
259 *x2 = (v>>1)&1;

10
260 *x7 = (v>>0)&1;
261 }
262 static inline uint64_t pack_out(uint64_t sig, int vec_idx, int y1, int y2){
263 // store 2 bits per vector as [y1,y2] at positions (2*vec_idx+1, 2*
vec_idx)
264 uint64_t bits = ((uint64_t)(y1&1) << (2*vec_idx+1)) | ((uint64_t)(y2&1)
<< (2*vec_idx));
265 return sig | bits;
266 }
267
268 /* ===== MAIN ===== */
269 int main() {
270 printf("
================================================================================\
n");
271 printf("EE 709 ASSIGNMENT - TEST GENERATION \n");
272 printf("
================================================================================\
n\n");
273
274 // ===================== QUESTION 3 =====================
275 printf("### QUESTION 3: Deductive Fault Simulation ###\n");
276 printf("Input: X1=0, X3=0, X6=0, X2=0, X7=0\n\n");
277
278 int y1_clean, y2_clean;
279 eval_clean(0,0,0,0,0,&y1_clean,&y2_clean);
280 printf("Fault-free: Y1=%d, Y2=%d\n\n", y1_clean, y2_clean);
281
282 const char *nets[] = {"X1","X2","X3","X6","X7","C7","C8","C9","C10","
C11","C12","Y1","Y2"};
283 int num_nets = 13;
284

285 printf("Detected faults (evaluated dynamically):\n");

286 int count = 0;
287 for (int i=0;i<num_nets;i++){
288 for (int sa=0; sa<=1; sa++){
289 int fy1, fy2;
290 eval_faulty(0,0,0,0,0, nets[i], sa, &fy1, &fy2);
291 if (fy1!=y1_clean || fy2!=y2_clean){
292 printf(" %s/sa%d (Y1=%d, Y2=%d)\n", nets[i], sa, fy1, fy2)
;
293 count++;
294 }
295 }
296 }
297 printf("\nTotal: %d DISTINCT faults\n", count);
298
299 // Full deductive L-list trace that propagates PI faults (single-pass
NAND-based)
300 printf("\n--- Deductive L-list trace (full) for vector 00000 ---\n");
301 int X1=0,X3=0,X6=0,X2=0,X7=0;
302 int C7= !(X1&&X3);
303 int C8= !(X3&&X6), C9=C8;
304 int C10= !(C8&&X2);
305 // int C11=C10;
306 int C12= !(C9&&X7);
307
308 LList LX1={0},LX3={0},LX6={0},LX2={0},LX7={0};

11
309 if(X1==0) Ladd(&LX1,"X1",1); else Ladd(&LX1,"X1",0);
310 if(X3==0) Ladd(&LX3,"X3",1); else Ladd(&LX3,"X3",0);
311 if(X6==0) Ladd(&LX6,"X6",1); else Ladd(&LX6,"X6",0);
312 if(X2==0) Ladd(&LX2,"X2",1); else Ladd(&LX2,"X2",0);
313 if(X7==0) Ladd(&LX7,"X7",1); else Ladd(&LX7,"X7",0);
314
315 // G1: C7 = NAND(X1,X3)
316 LList LC7={0};
317 LList candC7={0}; Lmerge(&candC7,&LX1,&LX3);
318 for (int i = 0; i < candC7.n; i++){
319 int a = apply_fault_to_net(X1,&candC7.f[i],"X1");
320 int b = apply_fault_to_net(X3,&candC7.f[i],"X3");
321 if (nand2(a,b)!=C7) Ladd(&LC7,candC7.f[i].net,candC7.f[i].sa);
322 }
323 Ladd(&LC7,"C7",0);
324
325 // G2: C8=C9 = NAND(X3,X6)
326 LList LC8={0}, LC9={0};
327 LList candC8={0}; Lmerge(&candC8,&LX3,&LX6);
328 for (int i = 0; i < candC8.n; i++){
329 int a = apply_fault_to_net(X3,&candC8.f[i],"X3");
330 int b = apply_fault_to_net(X6,&candC8.f[i],"X6");
331 if (nand2(a,b)!=C8){ Ladd(&LC8,candC8.f[i].net,candC8.f[i].sa);
Ladd(&LC9,candC8.f[i].net,candC8.f[i].sa); }
332 }
333 Ladd(&LC8,"C8",0); Ladd(&LC9,"C9",0);
334
335 // G3: C10=C11 = NAND(C8,X2)
336 LList LC10={0}, LC11={0};
337 LList candC10={0}; Lmerge(&candC10,&LC8,&LX2);
338 for (int i = 0; i < candC10.n; i++){
339 int a = apply_fault_to_net(C8,&candC10.f[i],"C8");
340 int b = apply_fault_to_net(X2,&candC10.f[i],"X2");
341 if (nand2(a,b)!=C10){ Ladd(&LC10,candC10.f[i].net,candC10.f[i].sa);
Ladd(&LC11,candC10.f[i].net,candC10.f[i].sa); }
342 }
343 Ladd(&LC10,"C10",0); Ladd(&LC11,"C11",0);
344

345 // G4: C12 = NAND(C9,X7)

346 LList LC12={0};
347 LList candC12={0}; Lmerge(&candC12,&LC9,&LX7);
348 for (int i = 0; i < candC12.n; i++){
349 int a = apply_fault_to_net(C9,&candC12.f[i],"C9");
350 int b = apply_fault_to_net(X7,&candC12.f[i],"X7");
351 if (nand2(a,b)!=C12) Ladd(&LC12,candC12.f[i].net,candC12.f[i].sa);
352 }
353 Ladd(&LC12,"C12",0);
354
355 // G5/G6: POs
356 LList LY1={0}; Lmerge(&LY1,&LC7,&LC10); Ladd(&LY1,"Y1",1);
357 LList LY2={0}; Lmerge(&LY2,&LC11,&LC12); Ladd(&LY2,"Y2",1);
358 Luniq(&LY1); Luniq(&LY2);
359
360 Lprint("L(Y1)", &LY1);
361 Lprint("L(Y2)", &LY2);
362 LList LDET={0}; Lmerge(&LDET,&LY1,&LY2);
363 Lprint("Detected (deductive union)", &LDET);
364

12
365
366 // ===================== QUESTION 2 (Pure SAT-based Enumeration)
=====================
367 printf("\n
================================================================================\
n");
368 printf("### QUESTION 2: Programmatic Test Generation (C7, C8, C11) ###\n");
369 printf("Targets: C7, C8, C11 (sa0/sa1)\n\n");
370

371 #define T 6
372 const char* tnets[] = {"C7","C7","C8","C8","C11","C11"};
373 int tsa[] = {0,1,0,1,0,1};
374
375 int cover[T][32] = {0};
376 char dets[T][1024]; memset(dets, 0, sizeof(dets));
377
378 int ndet[T] = {0};
379 for(int t = 0; t < T; t++){
380 int blocks[64][5]; int nblocks = 0;
381 char cnf_base[64], out_path[64];
382 snprintf(cnf_base, sizeof(cnf_base), "miter_%s_sa%[Link]", tnets[t], tsa
[t]);
383 snprintf(out_path, sizeof(out_path), "miter_%s_sa%[Link]", tnets[t], tsa
[t]);
384
385 while(1){
386 if(write_miter_cnf(tnets[t], tsa[t], cnf_base, blocks, nblocks) !=
0) break;
387 int x1, x3, x6, x2, x7; int sat = solve_miter_get_pis(cnf_base,
out_path, &x1, &x3, &x6, &x2, &x7);
388 if(sat <= 0) break;
389

390 int v = (x1 << 4) | (x3 << 3) | (x6 << 2) | (x2 << 1) | x7;
391 char vec[8]; sprintf(vec, "%d%d%d%d%d", x1, x3, x6, x2, x7);
392 strcat(dets[t], vec); strcat(dets[t], " ");
393 cover[t][v] = 1; ndet[t]++;
394
395 // Blocking literal negation
396 blocks[nblocks][0] = x1 ? -X1v : X1v;
397 blocks[nblocks][1] = x3 ? -X3v : X3v;
398 blocks[nblocks][2] = x6 ? -X6v : X6v;
399 blocks[nblocks][3] = x2 ? -X2v : X2v;
400 blocks[nblocks][4] = x7 ? -X7v : X7v;
401 nblocks++;
402 if(nblocks >= 32) break;
403 }
404
405 printf("SAT enumerated %d vectors for %s/sa%d\n", ndet[t], tnets[t],
tsa[t]);
406 }
407
408 // Print full sorted lists
409 for(int t = 0; t < T; t++){
410 printf("%s/sa%d: ", tnets[t], tsa[t]);
411 char sorted_dets[1024] = "";
412 for(int v = 0; v < 32; v++) if(cover[t][v]){
413 char vec[8]; sprintf(vec, "%d%d%d%d%d", (v>>4)&1, (v>>3)&1, (v>>2)
&1, (v>>1)&1, v&1);

13
414 strcat(sorted_dets, vec); strcat(sorted_dets, " ");
415 }
416 printf("%s\n", sorted_dets);
417 }
418
419 // Greedy cover (low-index tie-break)
420 int covered[T] = {0}; int nc = 0; int chosen[32]; int remaining = T;
421 while(remaining > 0){
422 int best_v = -1, best_gain = -1;
423 for(int v = 0; v < 32; v++){
424 int gain = 0; for(int tt = 0; tt < T; tt++) if(!covered[tt] &&
cover[tt][v]) gain++;
425 if(gain > best_gain || (gain == best_gain && (best_v == -1 || v <
best_v))){ best_gain = gain; best_v = v; }
426 }
427 if(best_v < 0 || best_gain <= 0) break;
428 for(int tt = 0; tt < T; tt++) if(!covered[tt] && cover[tt][best_v]){
covered[tt] = 1; remaining--; }
429 chosen[nc++] = best_v;
430 }
431

432 printf("\nMinimal complete test set (%d vectors):\n", nc);

433 for(int i = 0; i < nc; i++){
434 int v = chosen[i]; int x1 = (v>>4)&1, x3 = (v>>3)&1, x6 = (v>>2)&1, x2
= (v>>1)&1, x7 = v&1;
435 char vec[8]; sprintf(vec, "%d%d%d%d%d", x1, x3, x6, x2, x7);
436 printf(" %2d. %s (detects:", i+1, vec); // Fixed: %2d for proper
numbering
437 for(int tt = 0; tt < T; tt++) if(cover[tt][v]) printf(" %s/sa%d", tnets
[tt], tsa[tt]);
438 printf(" )\n");
439 }
440
441 // Cleanup temp files
442 for(int t = 0; t < T; t++){
443 char cnf[64], outf[64];
444 snprintf(cnf, sizeof(cnf), "miter_%s_sa%[Link]", tnets[t], tsa[t]);
445 snprintf(outf, sizeof(outf), "miter_%s_sa%[Link]", tnets[t], tsa[t]);
446 remove(cnf); remove(outf);
447 }
448
449
450 // ===================== QUESTION 1 =====================
451 printf("\n
================================================================================\
n");
452 printf("### QUESTION 1: Fault Equivalence Classes (computed
exhaustively) ###\n\n");
453
454 // Build the complete fault list consistent with simulation
455 FaultSig faults[64]; int nf=0;
456 for (int i=0;i<num_nets;i++){
457 for (int sa=0; sa<=1; sa++){
458 faults[nf].net = nets[i];
459 faults[nf].sa = sa;
460 faults[nf].sig = 0ULL;
461 nf++;
462 }

14
463 }
464
465 // Compute signatures over all 32 vectors
466 for (int f=0; f<nf; f++){
467 uint64_t sig = 0ULL;
468 for (int v=0; v<32; v++){
469 int x1,x3,x6,x2,x7; vec_to_pis(v,&x1,&x3,&x6,&x2,&x7);
470 int y1g,y2g,y1f,y2f;
471 eval_clean(x1,x3,x6,x2,x7,&y1g,&y2g);
472 eval_faulty(x1,x3,x6,x2,x7, faults[f].net, faults[f].sa, &y1f,
&y2f);
473 // Record faulty outputs only (fault dictionary signature)
474 sig = pack_out(sig, v, y1f, y2f);
475 }
476 faults[f].sig = sig;
477 }
478
479 // Group by identical signatures
480 SigGroup groups[64]; int ng=0;
481 for (int f=0; f<nf; f++){
482 int found=-1;
483 for (int g=0; g<ng; g++){
484 if (groups[g].sig == faults[f].sig){ found=g; break; }
485 }
486 if (found<0){
487 groups[ng].sig = faults[f].sig;
488 groups[ng].n = 0;
489 groups[ng].idxs[groups[ng].n++] = f;
490 ng++;
491 } else {
492 groups[found].idxs[ groups[found].n++ ] = f;
493 }
494 }
495
496 // Print groups as equivalence classes
497 int class_id = 1;
498 int multi = 0, singles = 0;
499 for (int g = 0; g < ng; g++) {
500 printf("Class %d: {", class_id++);
501 for (int k = 0; k < groups[g].n; k++) {
502 int fi = groups[g].idxs[k];
503 printf("%s/sa%d", faults[fi].net, faults[fi].sa);
504 if (k + 1 < groups[g].n) printf(", ");
505 }
506 printf("}\n");
507 if (groups[g].n > 1) multi++; else singles++;
508 }
509
510 printf("\nTotal: %d multi + %d singles = %d unique equivalence classes\n",
511 multi, singles, ng);
512
513
514
515 printf("\n
================================================================================\
n");
516 printf("FINAL NOTE Q2 & Q3 verified; Q1 computed exhaustively across 32
patterns\n");

15
517 printf("
================================================================================\
n");
518
519
520 return 0;
521 }

16