Circuit Verification using prolog

Question

i have been given functions and predicate to use to verify a 2 bit full adder circuit. This is what I have understood so far:-

a function signal(t) where t is terminal and signal takes value 1 or 0.

signal(T, V) :- V is 1; V is 0.

a function type(x) where type is a circuit element and type(x) can take value xor, and, or

type(X, T) :- T is and; T is or; T is xor.

a function out(x) denoting output at gate x and in(n, x) n is an input terminal.

out(X, O) :- type(X, and), O is I1+I2, in(1, X, I1), in(1, X, I2). 
%%and so on for other gates

for gates predicates are given as

forall X[{type(X) == OR} ----> {(out(X) =1)}-----> for some y(in(y, X) = 1)]

For these I am not sure how to convert them to prolog code and do not understand how prolog functions return something (I think the result must also be provided as a parameter).

Any Help would be very useful !

Answer 1

First, you should select a better representation for your problems. Facts are enough for this porpouse. Circuits may be represented as:

in/1 --> input signal (0 or 1). this is required to avoid infinite loops (see later).

xor/2, and/2, or/2 --> logical operations over circuits A and B. not/1 --> etc.

This way, a circuit will take this shape:

xor(and(in(In1),in(In2)),or(in(In1),not(in(In3))))

Now, let's define a predicate output/1, which computes circuit's state:

output(xor(In1,In2),1) :-
    output(In1,Out1),
    output(In2,Out2),
    Out1 \== Out2.
output(xor(In1,In2),0) :-
    output(In1,Out1),
    output(In2,Out2),
    Out1 == Out2.

output(and(In1,In2),1) :-
    output(In1,1),
    output(In2,1).
output(and(In1,In2),0) :-
    output(In1,Out1),
    output(In2,Out2),
    (Out1==0 ; Out2==0).

output(or(In1,In2),1) :-
    (output(In1,1); output(In2,1)).
output(or(In1,In2,0),0) :-
    output(In1,0),
    output(In2,0).

output(not(In),0) :-
    output(In,1).
output(not(In),1) :-
    output(In,0).
output(in(0),0).
output(in(1),1).

This predeciate is reversible on porpouse, so inputs may be left as free variables in order to obtain all outputs:

?- output(xor(and(in(In1),in(In2)),or(in(In1),not(in(In3)))),Result).
In1 = In2, In2 = In3, In3 = 0,
Result = 1 ;
In1 = In2, In2 = In3, In3 = 0,
Result = 1 ;
In1 = In3, In3 = 0,
In2 = Result, Result = 1 ;
In1 = Result, Result = 1,
In2 = 0 ;
In1 = Result, Result = 1,
In2 = In3, In3 = 0 ;
In1 = In2, In2 = 1,
Result = 0 ;
In1 = In2, In2 = 1,
In3 = Result, Result = 0 ;
false.

output(A,B) should not be confused with output(in(A),B). The first may be instantiated to any circuit (infinite loop) while the second may be instatiated to just 0 or 1.

It seems to work on recursive circuits:

?- output(or(in(Input),in(InOut)),InOut).
Input = InOut, InOut = 1 ;
InOut = 1.