Previous: CLPB Example 3, Up: CLPB Examples [Contents][Index]
The predicate fault/3
below describes a 1-bit adder
consisting of five gates, with at most one faulty gate. If one of the
variables Fi
is equal to 1, then the corresponding gate is
faulty, and its output signal is undefined (i.e. the constraint
representing the gate is relaxed).
Assuming that we have found some incorrect output from a circuit, we
are interesting in finding the faulty gate. Two instances of incorrect
output are listed in fault_ex/2
:
fault([F1,F2,F3,F4,F5], [X,Y,Cin], [Sum,Cout]) :- sat( card([0-1],[F1,F2,F3,F4,F5]) * (F1 + (U1 =:= X * Cin)) * (F2 + (U2 =:= Y * U3)) * (F3 + (Cout =:= U1 + U2)) * (F4 + (U3 =:= X # Cin)) * (F5 + (Sum =:= Y # U3)) ). fault_ex(1, Faults) :- fault(Faults, [1,1,0], [1,0]). fault_ex(2, Faults) :- fault(Faults, [1,0,1], [0,0]).
To find the faulty gates, we run the query
| ?- fault_ex(I,L), labeling(L). I = 1, L = [0,0,0,1,0] ? ; I = 2, L = [1,0,0,0,0] ? ; I = 2, L = [0,0,1,0,0] ? ; no
Thus for input data [1,1,0]
, gate 4 must be faulty.
For input data [1,0,1]
, either gate 1 or gate 3 must be faulty.
To get a symbolic representation of the outputs in terms of the input, we run the query
| ?- fault([0,0,0,0,0], [x,y,cin], [Sum,Cout]). sat(Cout=:=x*cin#x*y#y*cin), sat(Sum=:=cin#x#y)
which shows that the sum and carry out signals indeed compute the intended functions if no gate is faulty.