// We verify for 8 bits.
//
// The basic adding block has the following form
//
//              Xi  Yi
//              |   |
//              V   V              
//            ----------
//            |        |
//   Ci  <----|        |
//            |        |
//            ----------
//                |
//                V
//               Zi
//
//


// We don't demand that Cin is 0, because most adding circuits
// allow for an ingoing carry.


%predicates
   Cin/0, Cout/0.
   C0/0, C1/0, C2/0, C3/0, C4/0, C5/0, C6/0, C7/0.
   X0/0, X1/0, X2/0, X3/0, X4/0, X5/0, X6/0, X7/0.
   Y0/0, Y1/0, Y2/0, Y3/0, Y4/0, Y5/0, Y6/0, Y7/0.
   Z0/0, Z1/0, Z2/0, Z3/0, Z4/0, Z5/0, Z6/0, Z7/0.
   B0/0, B1/0, B2/0, B3/0, B4/0, B5/0, B6/0, B7/0.

%firstorder

Z0 <-> ( X0 <-> ( Y0 <-> Cin )).
C0 <-> ( ( X0 /\ Y0 ) \/ ( X0 /\ Cin ) \/ ( Y0 /\ Cin )).

Z1 <-> ( X1 <-> ( Y1 <-> C0 )).
C1 <-> ( ( X1 /\ Y1 ) \/ ( X1 /\ C0 ) \/ ( Y1 /\ C0 )).

Z2 <-> ( X2 <-> ( Y2 <-> C1 )).
C2 <-> ( ( X2 /\ Y2 ) \/ ( X2 /\ C1 ) \/ ( Y2 /\ C1 )).

Z3 <-> ( X3 <-> ( Y3 <-> C2 )).
C3 <-> ( ( X3 /\ Y3 ) \/ ( X3 /\ C2 ) \/ ( Y3 /\ C2 )).

Z4 <-> ( X4 <-> ( Y4 <-> C3 )).
C4 <-> ( ( X4 /\ Y4 ) \/ ( X4 /\ C3 ) \/ ( Y4 /\ C3 )).

Z5 <-> ( X5 <-> ( Y5 <-> C4 )).
C5 <-> ( ( X5 /\ Y5 ) \/ ( X5 /\ C4 ) \/ ( Y5 /\ C4 )).

Z6 <-> ( X6 <-> ( Y6 <-> C5 )).
C6 <-> ( ( X6 /\ Y6 ) \/ ( X6 /\ C5 ) \/ ( Y6 /\ C5 )).

Z7 <-> ( X7 <-> ( Y7 <-> C6 )).
Cout <-> ( ( X7 /\ Y7 ) \/ ( X7 /\ C6 ) \/ ( Y7 /\ C6 )).





%predicates
A0/0, A1/0, A2/0, A3/0, A4/0, A5/0, A6/0, A7/0.
G0/0, G1/0, G2/0, G3/0, G4/0, G5/0, G6/0, G7/0.
P0/0, P1/0, P2/0, P3/0, P4/0, P5/0, P6/0, P7/0.


// Now commes the other adder:

// Each adding block creates three outputs:
// Gi : Carry generate.
// Pi : Carry propagate.
// Ai : The output.  Ai has to be XORed with the incoming carry. 


%firstorder

A0 <-> ! ( X0 <-> Y0 ).
G0 <-> ( X0 /\ Y0 ).
P0 <-> ( X0 \/ Y0 ).

A1 <-> ! ( X1 <-> Y1 ).
G1 <-> ( X1 /\ Y1 ).
P1 <-> ( X1 \/ Y1 ).

A2 <-> ! ( X2 <-> Y2 ).
G2 <-> ( X2 /\ Y2 ).
P2 <-> ( X2 \/ Y2 ).

A3 <-> ! ( X3 <-> Y3 ).
G3 <-> ( X3 /\ Y3 ).
P3 <-> ( X3 \/ Y3 ).

A4 <-> ! ( X4 <-> Y4 ).
G4 <-> ( X4 /\ Y4 ).
P4 <-> ( X4 \/ Y4 ).

A5 <-> ! ( X5 <-> Y5 ).
G5 <-> ( X5 /\ Y5 ).
P5 <-> ( X5 \/ Y5 ).

A6 <-> ! ( X6 <-> Y6 ).
G6 <-> ( X6 /\ Y6 ).
P6 <-> ( X6 \/ Y6 ).

A7 <-> ! ( X7 <-> Y7 ).
G7 <-> ( X7 /\ Y7 ).
P7 <-> ( X7 \/ Y7 ).


B0 <-> ( A0 <-> ! Cin ).
B1 <-> ( A1 <-> ! ( G0 \/ ( Cin /\ P0 ))).
B2 <-> ( A2 <-> ! ( G1 \/ ( G0 /\ P1 ) \/ ( Cin /\ P0 /\ P1 ))).
B3 <-> ( A3 <-> ! ( G2 \/ ( G1 /\ P2 ) \/ ( G0 /\ P1 /\ P2 ) \/ 
                    ( Cin /\ P0 /\ P1 /\ P2 ))).
B4 <-> ( A4 <-> ! ( G3 \/ ( G2 /\ P3 ) \/ ( G1 /\ P2 /\ P3 ) \/
                  ( G0 /\ P1 /\ P2 /\ P3 ) \/
                  ( Cin /\ P0 /\ P1 /\ P2 /\ P3 ))).
B5 <-> ( A5 <-> ! ( G4 \/ ( G3 /\ P4 ) \/ ( G2 /\ P3 /\ P4 ) \/
                    ( G1 /\ P2 /\ P3 /\ P4 ) \/ 
                    ( G0 /\ P1 /\ P2 /\ P3 /\ P4 ) \/
                    ( Cin /\ P0 /\ P1 /\ P2 /\ P3 /\ P4 ))).
B6 <-> ( A6 <-> ! ( G5 \/ ( G4 /\ P5 ) \/ ( G3 /\ P4 /\ P5 ) \/
                    ( G2 /\ P3 /\ P4 /\ P5 ) \/
                    ( G1 /\ P2 /\ P3 /\ P4 /\ P5 ) \/
                    ( G0 /\ P1 /\ P2 /\ P3 /\ P4 /\ P5 ) \/
                    ( Cin /\ P0 /\ P1 /\ P2 /\ P3 /\ P4 /\ P5 ))).

B7 <-> ( A7 <-> ! ( G6 \/ ( G5 /\ P6 ) \/ ( G4 /\ P5 /\ P6 ) \/
                    ( G3 /\ P4 /\ P5 /\ P6 ) \/
                    ( G2 /\ P3 /\ P4 /\ P5 /\ P6 ) \/
                    ( G1 /\ P2 /\ P3 /\ P4 /\ P5 /\ P6 ) \/
                    ( G0 /\ P1 /\ P2 /\ P3 /\ P4 /\ P5 /\ P6 ) \/
                    ( Cin /\ P0 /\ P1 /\ P2 /\ P3 /\ P4 /\ P5 /\ P6 ))).
           

! ( ( Z0 <-> B0 ) /\ ( Z1 <-> B1 ) /\ ( Z2 <-> B2 ) /\ ( Z3 <-> B3 ) /\
    ( Z4 <-> B4 ) /\ ( Z5 <-> B5 ) /\ ( Z6 <-> B6 ) /\ ( Z7 <-> B7 )).