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


// We don't demand that C0 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

// Specification of ripple adder.

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
Din/0, Dout/0.

A0/0, A1/0, A2/0, A3/0, A4/0, A5/0, A6/0, A7/0.
B0/0, B1/0, B2/0, B3/0, B4/0, B5/0, B6/0, B7/0.
D0/0, D1/0, D2/0, D3/0, D4/0, D5/0, D6/0, D7/0.
E0/0, E1/0, E2/0, E3/0, E4/0, E5/0, E6/0, E7/0.


//     Subtraction block: 
//
//              Ai  Bi
//              |   |
//              V   V
//            ----------
//            |        |
//   Di  <----|        |<-----D(i-1)
//            |        |
//            ----------
//                |
//                V
//               Ei
//
//


%firstorder

E0 <-> ( A0 <-> ( B0 <-> Din )).
D0 <-> (( ! A0 /\ ( B0 \/ Din )) \/ ( A0 /\ B0 /\ Din )).

E1 <-> ( A1 <-> ( B1 <-> D0 )).
D1 <-> (( ! A1 /\ ( B1 \/ D0 )) \/ ( A1 /\ B1 /\ D0 )).

E2 <-> ( A2 <-> ( B2 <-> D1 )).
D2 <-> (( ! A2 /\ ( B2 \/ D1 )) \/ ( A2 /\ B2 /\ D1 )).

E3 <-> ( A3 <-> ( B3 <-> D2 )).
D3 <-> (( ! A3 /\ ( B3 \/ D2 )) \/ ( A3 /\ B3 /\ D2 )).

E4 <-> ( A4 <-> ( B4 <-> D3 )).
D4 <-> (( ! A4 /\ ( B4 \/ D3 )) \/ ( A4 /\ B4 /\ D3 )).

E5 <-> ( A5 <-> ( B5 <-> D4 )).
D5 <-> (( ! A5 /\ ( B5 \/ D4 )) \/ ( A5 /\ B5 /\ D4 )).

E6 <-> ( A6 <-> ( B6 <-> D5 )).
D6 <-> (( ! A6 /\ ( B6 \/ D5 )) \/ ( A6 /\ B6 /\ D5 )).

E7 <-> ( A7 <-> ( B7 <-> D6 )).
Dout <-> (( ! A7 /\ ( B7 \/ D6 )) \/ ( A7 /\ B7 /\ D6 )).


// This is the two-complement relation: 

X0 <-> A0.
X1 <-> A1.
X2 <-> A2.
X3 <-> A3.
X4 <-> A4.
X5 <-> A5.
X6 <-> A6.
X7 <-> A7.

Y0 <-> ! B0.
Y1 <-> ! B1.
Y2 <-> ! B2.
Y3 <-> ! B3.
Y4 <-> ! B4.
Y5 <-> ! B5.
Y6 <-> ! B6.
Y7 <-> ! B7.

Cin <-> ! Din.


! ( ( Z0 <-> E0 ) /\ ( Z1 <-> E1 ) /\ ( Z2 <-> E2 ) /\ ( Z3 <-> E3 ) /\
    ( Z4 <-> E4 ) /\ ( Z5 <-> E5 ) /\ ( Z6 <-> E6 ) /\ ( Z7 <-> E7 ) /\
    ( Cout <-> ! Dout )).