Node:Example 4, Previous:Example 3, Up:CLPB Examples

Example 4

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, 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 interms 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.