4 bit Adder in Alloy and TypeScript

Introduction

While learning Alloy I took a small detour to implement a 4 bit adder because I wanted a fun exercise to help with the learning process. Today I revisited that exercise and started wondering what it would be like to re-implement the adder in a regular programming language instead of Alloy's specification language.

I'll first outline the Alloy model and then convert the specification into an implementation in TypeScript.

4 bit Adder in Alloy

From a high level the specification is pretty simple and just defines several basic relations on bits which are then inductively used in other relations and predicates to build the 4 bit adder.

The basic components of the specification are the definitions of bits and primitive boolean operations

let bits = { i: Int | 0 <= i && i <= 1 }
let bitOrTable = { i: bits, j: bits, k: sum[i + j] }
let bitAndTable = { i: bits, j: bits, k: mul[i, j] }
let bitNotTable = { i: bits, j: minus[1, i] }
let bitXorTable = {
  i: bits,
  j: bits,
  k: bitAndTable[bitOrTable[i, j], bitNotTable[bitAndTable[i, j]]]
}

Using the above relations we next define some components that we can use to define a 4 bit adder (1 bit half/full-adder)

pred halfAdder(m: Int, n: Int, s: Int, c: Int) {
  s = bitXorTable[m, n]
  c = bitAndTable[m, n]
}
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 think my intention was to use the half adder to define a full adder but as you can see I just implemented the full adder from basic gates instead of half adders. I don't remember why I opted for this route instead of using the half adders.

Before we can implement the 4 bit adder we need to define the 4 bit vectors that we want to use to implement it

abstract sig BitVector {
  values: (0 + 1 + 2 + 3) -> one bits
}
one sig A, B, C, S extends BitVector { }

I don't remember where I picked up the trick for encoding a vector as a relation with integer components and in general I suspect it is not the best approach but works well enough in this case.

The final definition of the 4 bit adder is almost anticlimactic because it is a bunch of copies of the full adder in ripple carry order

pred bitAddition(a: BitVector, b: BitVector, c: BitVector, s: BitVector) {
  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]]
}
run {
  bitAddition[A, B, C, S]
}

When I was learning Alloy putting this together was pretty challenging but looking back now all the pieces make sense and showcase a whole bunch of useful Alloy syntax. Every Alloy tutorial should definitely have a few exercises like this one where the learners have to implement basic boolean operations on bit vectors.

Translation into TypeScript

I'm going to start from the bottom and move upwards because all the predicates and relations are functional, i.e. for every input there is a unique output.

The implementaiton isn't anything special and an almost literal translation gives us this

type BitVector = [number, number, number, number];

function fullAdder(m: number, n: number, c: number): [number, number] {
  const xor = m ^ n;
  const s = xor ^ c;
  const carry  = (m & n) | (xor & c);
  return [s, carry];
}

function bitAddition(a: BitVector, b: BitVector): [BitVector, BitVector] {
  const carries: BitVector = [0, 0, 0, 0];
  carries[-1] = 0; // Hack used below
  const sums: BitVector = [0, 0, 0, 0];
  for (let i = 0; i++; i <= 3) {
    const f = fullAdder(a[i], b[i], carries[i - 1]); // Hack used here
    sums[i] = f[0];
    carries[i] = f[1];
  }
  return [sums, carries];
}

I will leave tests and validation as an exercise for the reader. As a bonus challenge see if you can use the model generation capabilities of Alloy to automatically generate the test cases. If you manage to do this then let me know. Another challenge is to extend both the model and the code to an 8 bit adder.

$ ./keygen.sh 6428f5771007cf005037d47c9aeac9bfcc8925f9  -