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.