# Validating the logical equivalence of circuits with Prolog

The SEGA mapper built on the Revision 2 flash card is based
around two `ATF16V8B`

programmable logic ICs, these ICs are way past their
prime and quickly becoming hard to develop to (outdated tools) hard to flash
(no hardware support) and generally a nuisance to use. For that reason I’ve
decided to redo the logic side of the mapper with discrete `74xx`

series logic
ICs but to do so I would need to validate that the old `ATF16V8B`

and the new
discrete circuits are equivalent. Enter Prolog.

Prolog is a programming language that makes working with logical expressions rather easily, and since 2016, SWI-Prolog has implemented constraint logic manipulation. With this tool I can convert the PLD logical expressions:

```
SLOT1_ADDR = (!A0) & A1 & A2 & A3 & A4 & A5 & A6 & A7 & A8 & A9 & A10 & A11 & A12 & A13 & A14 & A15 ;
SLOT2_ADDR = A0 & A1 & A2 & A3 & A4 & A5 & A6 & A7 & A8 & A9 & A10 & A11 & A12 & A13 & A14 & A15 ;
```

Into a prolog expression (Note `[A2, A15]`

are `AND`

separately from `A0`

`A1`

)

```
%Mask is the logical-nand of address bits [A2, A15]
Mask = (
A2 * A3 * A4 * A5 * A6 * A7 *
A8 * A9 * A10 * A11 * A12 * A13 * A14 * A15
),
Slot1_address = Mask * ~A0 * A1,
Slot2_address = Mask * A0 * A1,
```

Given these expressions we can make another set, mimicking the implementation using discrete logic gates. For example, the Mask expression implemented using 8-input NAND gates and inverters would be:

```
% - 2x 8-input NAND gate (74HC30)
% - 1x Inverter (from 74HC04)
%
% 6 +---+
% [A2,A7] -------/----------------| |
% True (Vcc) ---------------------| & |o----> NMask_new
% +--| |
% 8 +---+ +---+ | +---+
% [A8,A15] -/-| & |o---| 1 |o--+
% +---+ +---+
%
NMask_new = (
%Outer nand (8-input)
~(
A2 *
A3 *
A4 *
A5 *
A6 *
A7 *
1 *
(
%Inverter
~(
%Inner nand (8-input)
~(
A8 *
A9 *
A10 *
A11 *
A12 *
A13 *
A14 *
A15
)
)
)
)
),
%Inverter
Mask_new = ~NMask_new,
```

And then let Prolog test the equality of these circuits using `taut()`

from
the `clpb`

module:

```
taut(Mask =:= Mask_new, 1),
```

This goal will succeed if and only if `Mask`

and `Mask_new`

are equivalent over
all the variables on both expressions.

For complex combinatorial circuits, this approach to validation scales better than other options I’ve tested.