The SEGA mapper built on the Revision 2 flash card is based
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
%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(Mask =:= Mask_new, 1),
This goal will succeed if and only if
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.