## [Z3][SMT][Python][EE] Fault check of digital circuit: minimizing test set

Donald Knuth's TAOCP section 7.2.2.2 has the following exercise.

Given the circuit:

Find a way to check, if it was soldered correclty, with no wires stuck at ground (always 0) or current (always 1). You can just enumerate all possible inputs (5) and this will be a table of correct inputs/outputs, 32 pairs. But you want to make fault check as fast as possible and minimize test set.

This is almost a problem I've been writing about: "Making smallest possible test suite using Z3": https://yurichev.com/writings/SAT_SMT_by_example.pdf#page=250&zoom=auto,-266,710 (page 250).

We want such a test set, so that all gates' outputs will output 0 and 1, at least once. And the test set should be as small, as possible.

The source code is very close to my previous example...

from z3 import *

# 5 inputs, so 1<<5=32 posible combinations:
TOTAL_TESTS=1<<5

# number of gates and/or gates' outputs:
OUTPUTS_TOTAL=15

OUT_Z1, OUT_Z2, OUT_Z3, OUT_Z4, OUT_Z5, OUT_A2, OUT_A3, OUT_B1, OUT_B2, OUT_B3, OUT_C1, OUT_C2, OUT_P, OUT_Q, OUT_S = range(OUTPUTS_TOTAL)

out_false_if={}
out_true_if={}

# enumerate all possible inputs
for i in range(1<<5):
x1=i&1
x2=(i>>1)&1
y1=(i>>2)&1
y2=(i>>3)&1
y3=(i>>4)&1

outs={}

# simulate the circuit:
outs[OUT_Z1]=y1&x1
outs[OUT_B1]=y1&x2
outs[OUT_A2]=x1&y2
outs[OUT_B2]=y2&x2
outs[OUT_A3]=x1&y3
outs[OUT_B3]=y3&x2

outs[OUT_P]=outs[OUT_A3] & outs[OUT_B2]
outs[OUT_S]=outs[OUT_A3] ^ outs[OUT_B2]
outs[OUT_C1]=outs[OUT_A2] & outs[OUT_B1]
outs[OUT_Z2]=outs[OUT_A2] ^ outs[OUT_B1]

outs[OUT_Q]=outs[OUT_S] & outs[OUT_C1]
outs[OUT_Z3]=outs[OUT_S] ^ outs[OUT_C1]

outs[OUT_C2]=outs[OUT_P] | outs[OUT_Q]

outs[OUT_Z5]=outs[OUT_B3] & outs[OUT_C2]
outs[OUT_Z4]=outs[OUT_B3] ^ outs[OUT_C2]

inputs=(y3, y2, y1, x2, x1)
print "inputs:", inputs, "outputs of all gates:", outs

for o in range(OUTPUTS_TOTAL):
if outs[o]==0:
if o not in out_false_if:
out_false_if[o]=[]
out_false_if[o].append(i)
else:
if o not in out_true_if:
out_true_if[o]=[]
out_true_if[o].append(i)

for o in range(OUTPUTS_TOTAL):
print "output #%d" % o
print "    false if:", out_false_if[o]
print "    true if:", out_true_if[o]

s=Solver()

# if the test will be picked or not:
tests=[Int('test_%d' % (t)) for t in range(TOTAL_TESTS)]

# this is optimization problem:
opt = Optimize()

# a test may be picked (1) or not (0):
for t in tests:

# this generates expression like (tests[0]==1 OR tests[1]==1 OR tests[X]==1):
for o in range(OUTPUTS_TOTAL):

# minimize number of tests:
opt.minimize(Sum(*tests))

print (opt.check())
m=opt.model()

for i in range(TOTAL_TESTS):
t=m[tests[i]].as_long()
if t==1:
print format(i, '05b')


The output:
inputs: (0, 0, 0, 0, 0) outputs of all gates: {0: 0, 1: 0, 2: 0, 3: 0, 4: 0, 5: 0, 6: 0, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (0, 0, 0, 0, 1) outputs of all gates: {0: 0, 1: 0, 2: 0, 3: 0, 4: 0, 5: 0, 6: 0, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (0, 0, 0, 1, 0) outputs of all gates: {0: 0, 1: 0, 2: 0, 3: 0, 4: 0, 5: 0, 6: 0, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (0, 0, 0, 1, 1) outputs of all gates: {0: 0, 1: 0, 2: 0, 3: 0, 4: 0, 5: 0, 6: 0, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (0, 0, 1, 0, 0) outputs of all gates: {0: 0, 1: 0, 2: 0, 3: 0, 4: 0, 5: 0, 6: 0, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (0, 0, 1, 0, 1) outputs of all gates: {0: 1, 1: 0, 2: 0, 3: 0, 4: 0, 5: 0, 6: 0, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (0, 0, 1, 1, 0) outputs of all gates: {0: 0, 1: 1, 2: 0, 3: 0, 4: 0, 5: 0, 6: 0, 7: 1, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (0, 0, 1, 1, 1) outputs of all gates: {0: 1, 1: 1, 2: 0, 3: 0, 4: 0, 5: 0, 6: 0, 7: 1, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (0, 1, 0, 0, 0) outputs of all gates: {0: 0, 1: 0, 2: 0, 3: 0, 4: 0, 5: 0, 6: 0, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (0, 1, 0, 0, 1) outputs of all gates: {0: 0, 1: 1, 2: 0, 3: 0, 4: 0, 5: 1, 6: 0, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (0, 1, 0, 1, 0) outputs of all gates: {0: 0, 1: 0, 2: 1, 3: 0, 4: 0, 5: 0, 6: 0, 7: 0, 8: 1, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 1}
inputs: (0, 1, 0, 1, 1) outputs of all gates: {0: 0, 1: 1, 2: 1, 3: 0, 4: 0, 5: 1, 6: 0, 7: 0, 8: 1, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 1}
inputs: (0, 1, 1, 0, 0) outputs of all gates: {0: 0, 1: 0, 2: 0, 3: 0, 4: 0, 5: 0, 6: 0, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (0, 1, 1, 0, 1) outputs of all gates: {0: 1, 1: 1, 2: 0, 3: 0, 4: 0, 5: 1, 6: 0, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (0, 1, 1, 1, 0) outputs of all gates: {0: 0, 1: 1, 2: 1, 3: 0, 4: 0, 5: 0, 6: 0, 7: 1, 8: 1, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 1}
inputs: (0, 1, 1, 1, 1) outputs of all gates: {0: 1, 1: 0, 2: 0, 3: 1, 4: 0, 5: 1, 6: 0, 7: 1, 8: 1, 9: 0, 10: 1, 11: 1, 12: 0, 13: 1, 14: 1}
inputs: (1, 0, 0, 0, 0) outputs of all gates: {0: 0, 1: 0, 2: 0, 3: 0, 4: 0, 5: 0, 6: 0, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (1, 0, 0, 0, 1) outputs of all gates: {0: 0, 1: 0, 2: 1, 3: 0, 4: 0, 5: 0, 6: 1, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 1}
inputs: (1, 0, 0, 1, 0) outputs of all gates: {0: 0, 1: 0, 2: 0, 3: 1, 4: 0, 5: 0, 6: 0, 7: 0, 8: 0, 9: 1, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (1, 0, 0, 1, 1) outputs of all gates: {0: 0, 1: 0, 2: 1, 3: 1, 4: 0, 5: 0, 6: 1, 7: 0, 8: 0, 9: 1, 10: 0, 11: 0, 12: 0, 13: 0, 14: 1}
inputs: (1, 0, 1, 0, 0) outputs of all gates: {0: 0, 1: 0, 2: 0, 3: 0, 4: 0, 5: 0, 6: 0, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (1, 0, 1, 0, 1) outputs of all gates: {0: 1, 1: 0, 2: 1, 3: 0, 4: 0, 5: 0, 6: 1, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 1}
inputs: (1, 0, 1, 1, 0) outputs of all gates: {0: 0, 1: 1, 2: 0, 3: 1, 4: 0, 5: 0, 6: 0, 7: 1, 8: 0, 9: 1, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (1, 0, 1, 1, 1) outputs of all gates: {0: 1, 1: 1, 2: 1, 3: 1, 4: 0, 5: 0, 6: 1, 7: 1, 8: 0, 9: 1, 10: 0, 11: 0, 12: 0, 13: 0, 14: 1}
inputs: (1, 1, 0, 0, 0) outputs of all gates: {0: 0, 1: 0, 2: 0, 3: 0, 4: 0, 5: 0, 6: 0, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (1, 1, 0, 0, 1) outputs of all gates: {0: 0, 1: 1, 2: 1, 3: 0, 4: 0, 5: 1, 6: 1, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 1}
inputs: (1, 1, 0, 1, 0) outputs of all gates: {0: 0, 1: 0, 2: 1, 3: 1, 4: 0, 5: 0, 6: 0, 7: 0, 8: 1, 9: 1, 10: 0, 11: 0, 12: 0, 13: 0, 14: 1}
inputs: (1, 1, 0, 1, 1) outputs of all gates: {0: 0, 1: 1, 2: 0, 3: 0, 4: 1, 5: 1, 6: 1, 7: 0, 8: 1, 9: 1, 10: 0, 11: 1, 12: 1, 13: 0, 14: 0}
inputs: (1, 1, 1, 0, 0) outputs of all gates: {0: 0, 1: 0, 2: 0, 3: 0, 4: 0, 5: 0, 6: 0, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 0}
inputs: (1, 1, 1, 0, 1) outputs of all gates: {0: 1, 1: 1, 2: 1, 3: 0, 4: 0, 5: 1, 6: 1, 7: 0, 8: 0, 9: 0, 10: 0, 11: 0, 12: 0, 13: 0, 14: 1}
inputs: (1, 1, 1, 1, 0) outputs of all gates: {0: 0, 1: 1, 2: 1, 3: 1, 4: 0, 5: 0, 6: 0, 7: 1, 8: 1, 9: 1, 10: 0, 11: 0, 12: 0, 13: 0, 14: 1}
inputs: (1, 1, 1, 1, 1) outputs of all gates: {0: 1, 1: 0, 2: 1, 3: 0, 4: 1, 5: 1, 6: 1, 7: 1, 8: 1, 9: 1, 10: 1, 11: 1, 12: 1, 13: 0, 14: 0}
output #0
false if: [0, 1, 2, 3, 4, 6, 8, 9, 10, 11, 12, 14, 16, 17, 18, 19, 20, 22, 24, 25, 26, 27, 28, 30]
true if: [5, 7, 13, 15, 21, 23, 29, 31]
output #1
false if: [0, 1, 2, 3, 4, 5, 8, 10, 12, 15, 16, 17, 18, 19, 20, 21, 24, 26, 28, 31]
true if: [6, 7, 9, 11, 13, 14, 22, 23, 25, 27, 29, 30]
output #2
false if: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 12, 13, 15, 16, 18, 20, 22, 24, 27, 28]
true if: [10, 11, 14, 17, 19, 21, 23, 25, 26, 29, 30, 31]
output #3
false if: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 16, 17, 20, 21, 24, 25, 27, 28, 29, 31]
true if: [15, 18, 19, 22, 23, 26, 30]
output #4
false if: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 28, 29, 30]
true if: [27, 31]
output #5
false if: [0, 1, 2, 3, 4, 5, 6, 7, 8, 10, 12, 14, 16, 17, 18, 19, 20, 21, 22, 23, 24, 26, 28, 30]
true if: [9, 11, 13, 15, 25, 27, 29, 31]
output #6
false if: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 18, 20, 22, 24, 26, 28, 30]
true if: [17, 19, 21, 23, 25, 27, 29, 31]
output #7
false if: [0, 1, 2, 3, 4, 5, 8, 9, 10, 11, 12, 13, 16, 17, 18, 19, 20, 21, 24, 25, 26, 27, 28, 29]
true if: [6, 7, 14, 15, 22, 23, 30, 31]
output #8
false if: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 12, 13, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 28, 29]
true if: [10, 11, 14, 15, 26, 27, 30, 31]
output #9
false if: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 20, 21, 24, 25, 28, 29]
true if: [18, 19, 22, 23, 26, 27, 30, 31]
output #10
false if: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30]
true if: [15, 31]
output #11
false if: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 28, 29, 30]
true if: [15, 27, 31]
output #12
false if: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 28, 29, 30]
true if: [27, 31]
output #13
false if: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31]
true if: [15]
output #14
false if: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 12, 13, 16, 18, 20, 22, 24, 27, 28, 31]
true if: [10, 11, 14, 15, 17, 19, 21, 23, 25, 26, 29, 30]
sat
01111
10001
11011



This is it, you can test this circuit using just 3 test vectors: 01111, 10001 and 11011.

However, Donald Knuth's test set is bigger: 5 test vectors, but his algorithm also checks "fanout" gates (one input, multiple outputs), which also may be faulty. I've omitted this for simplification.