# Some More Fun with Alloy

### david karapetyan ・3 min read

This is a continuation of Fun with Alloy Model Checker. In this episode we implement a 4 bit adder.

Alloy reminds me of Prolog and Prolog in turn reminds me of VHDL and other hardware description languages so I figured I'd take the analogy and run with it. The simplest thing one can do with the analogy is implement a 4 bit adder.

We start with several definitions of logical building blocks

```
// 0 or 1
let bits = { i: Int | 0 <= i && i <= 1 }
// Or
let bitOrTable = { i: bits, j: bits, k: sum[i + j] }
// And
let bitAndTable = { i: bits, j: bits, k: mul[i, j] }
// Not
let bitNotTable = { i: bits, j: minus[1, i] }
// Xor: https://en.wikipedia.org/wiki/Exclusive_or
let bitXorTable = {
i: bits,
j: bits,
k: bitAndTable[bitOrTable[i, j], bitNotTable[bitAndTable[i, j]]]
}
```

I'm using set comprehension notation in the above examples and if you have used python or another language with list comprehension then it should feel familiar. You should evaluate those expressions in the Alloy GUI and verify that they really are the usual tables for boolean operations.

With the boolean operations out of the way we can now spell out the definitions of the half and full adder as predicates

```
// Half adder: https://en.wikipedia.org/wiki/Adder_(electronics)#Half_adder
pred halfAdder(m: Int, n: Int, s: Int, c: Int) {
s = bitXorTable[m, n]
c = bitAndTable[m, n]
}
// https://en.wikipedia.org/wiki/Adder_(electronics)#/media/File:Full-adder_logic_diagram.svg
pred fullAdder(m: Int, n: Int, c: Int, s: Int, carry: Int) {
let xor = bitXorTable[m, n] {
s = bitXorTable[xor, c]
carry = bitOrTable[bitAndTable[m, n], bitAndTable[xor, c]]
}
}
```

I'm using predicates instead of functions but I think these could just as easily be written as functions (I'm leaving that as an exercise for the reader). Notice how it kinda looks like a wiring diagram where you can read `=`

as wiring up inputs to outputs. For the half adder the output variables are `s`

and `c`

and for the full adder the output variables are `s`

and `carry`

. Incidentally this is exactly how you'd write these predicates in Prolog.

We can't really do much with a half adder and full adder other than add together single bits so next we are going to specify a 4 bit register and instantiate 4 copies of it

```
// BitVector consists of 4 bits
abstract sig BitVector {
values: (0 + 1 + 2 + 3) -> one bits
}
// We want 4 vectors to perform a computation: 2 summands, sum, and carry
one sig A, B, C, S extends BitVector { }
```

Now we can wire up the registers for adding everything with a ripple-carry adder composed of the full adders we defined previously

```
// 4 bit adder with overflow wraparound
pred bitAddition(a: BitVector, b: BitVector, c: BitVector, s: BitVector) {
a = A
b = B
c = C
s = S
fullAdder[a.values[0], b.values[0], 0, s.values[0], c.values[0]]
fullAdder[a.values[1], b.values[1], c.values[0], s.values[1], c.values[1]]
fullAdder[a.values[2], b.values[2], c.values[1], s.values[2], c.values[2]]
fullAdder[a.values[3], b.values[3], c.values[2], s.values[3], c.values[3]]
}
```

To see the adder in action just run the predicate

```
// Run it to verify bits are being added properly
run bitAddition
```

Challenge for the reader: see if you can make an 8 bit adder from the above 4 bit adder.