diff --git a/models/GAL16V8_reg.hex b/models/GAL16V8_reg.hex
new file mode 100644
index 0000000..1178309
--- /dev/null
+++ b/models/GAL16V8_reg.hex
@@ -0,0 +1,279 @@
+00
+00
+08
+92
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+fe
+ff
+ff
+ff
+ef
+ff
+ff
+ff
+ff
+fe
+ff
+ff
+ff
+ef
+ff
+ff
+ff
+ff
+fe
+ff
+ff
+ff
+ef
+ff
+00
+00
+00
+00
+00
+00
+00
+00
+ee
+ee
+ee
+ff
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+ff
+ff
+de
+ff
+ff
+ff
+ed
+ff
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+ff
+fe
+ff
+ff
+ff
+ef
+ff
+ff
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+ee
+ff
+ff
+ff
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+00
+f0
+c2
+f6
+b6
+46
+2a
+a6
+ce
+2e
+00
+ff
+ff
+ff
+ff
+ff
+ff
+ff
+ff
+02
diff --git a/models/GAL16V8_reg.v b/models/GAL16V8_reg.v
new file mode 100644
index 0000000..6c7be31
--- /dev/null
+++ b/models/GAL16V8_reg.v
@@ -0,0 +1,175 @@
+`default_nettype none
+module GAL16V8_reg (
+	input wire       clk,
+	input wire [7:0] in,
+	input wire       oe_n,
+	inout wire [7:0] io
+);
+	// Read in binary JEDEC file
+	reg [7:0] jed_bin_file [0:278];
+	initial $readmemh("GAL16V8_reg.hex", jed_bin_file);
+
+	// Linearize to a fuse map
+	wire [2193:0] fuses;
+	genvar i, j;
+	generate
+		for (i = 0; i < 274; i = i + 1) begin
+			for (j = 0; j < 8; j = j + 1) begin
+				assign fuses[8*i + j] = jed_bin_file[i + 4][j];
+			end
+		end
+		// Last couple bits
+		for (j = 0; j < 2; j = j + 1) begin
+			assign fuses[8*274 + j] = jed_bin_file[274 + 4][j];
+		end
+	endgenerate
+
+	// Extract useful fuses
+	wire syn_fuse, ac0_fuse;
+	assign syn_fuse = fuses[2192];
+	assign ac0_fuse = fuses[2193];
+
+	wire [7:0] xor_fuses;
+	assign xor_fuses = fuses[2055:2048];
+
+	wire [7:0] ac1_fuses;
+	assign ac1_fuses = fuses[2127:2120];
+
+	wire [255:0] sop_fuses [0:7];
+	wire [7:0] ptd_fuses [0:7];
+	generate
+		for (i = 0; i < 8; i = i + 1) begin
+			assign sop_fuses[i] = fuses[256*i +: 256];
+			assign ptd_fuses[i] = fuses[2128 + 8*i +: 8];
+		end
+	endgenerate
+
+	// Interleave in and feedback for SOP inputs
+	wire [7:0] feedback;
+	wire [15:0] interleaved;
+	generate
+		for (i = 0; i < 8; i = i + 1) begin
+			assign interleaved[2*i +: 2] = {feedback[i], in[i]};
+		end
+	endgenerate
+
+	// Generate GAL elements
+	generate
+		for (i = 0; i < 8; i = i + 1) begin
+			wire one_sop_out, sop_out;
+
+			// 1SOP
+			sop #(
+				.NUM_PRODUCTS(1),
+				.NUM_INPUTS(16)
+			) one_sop_inst (
+				.sop_fuses(sop_fuses[i][255:224]),
+				.ptd_fuses(ptd_fuses[i][0]),
+				.in(interleaved),
+				.out(one_sop_out)
+			);
+
+			// SOP
+			sop #(
+				.NUM_PRODUCTS(7),
+				.NUM_INPUTS(16)
+			) sop_inst (
+				.sop_fuses(sop_fuses[i][223:0]),
+				.ptd_fuses(ptd_fuses[i][7:1]),
+				.in(interleaved),
+				.out(sop_out)
+			);
+
+			// OLMC
+			olmc olmc_inst (
+				.xor_fuse(xor_fuses[i]),
+				.ac1_fuse(ac1_fuses[i]),
+				.sop(sop_out),
+				.one_sop(one_sop_out),
+				.clk(clk),
+				.oe_n(oe_n),
+				.io(io[i]),
+				.feedback(feedback[i])
+			);
+		end
+	endgenerate
+
+	// Simulation printing
+	initial begin
+		#1;
+		$display("SYN: %d, AC0: %d", syn_fuse, ac0_fuse);
+		$display("XOR: %b, AC1: %b", xor_fuses, ac1_fuses);
+		$display("Fuses: %x", fuses);
+
+		$display("sop0 %x", sop_fuses[0]);
+		$display("ptd0 %x", ptd_fuses[0]);
+
+		$display("sop1 %x", sop_fuses[1]);
+		$display("ptd1 %x", ptd_fuses[1]);
+		$display("sop2 %x", sop_fuses[2]);
+		$display("ptd2 %x", ptd_fuses[2]);
+		$display("sop3 %x", sop_fuses[3]);
+		$display("ptd3 %x", ptd_fuses[3]);
+		$display("sop4 %x", sop_fuses[4]);
+		$display("ptd4 %x", ptd_fuses[4]);
+		$display("sop5 %x", sop_fuses[5]);
+		$display("ptd5 %x", ptd_fuses[5]);
+		$display("sop6 %x", sop_fuses[6]);
+		$display("ptd6 %x", ptd_fuses[6]);
+		$display("sop7 %x", sop_fuses[7]);
+		$display("ptd7 %x", ptd_fuses[7]);
+	end
+endmodule
+
+module sop #(
+	parameter NUM_PRODUCTS = 7,
+	parameter NUM_INPUTS = 16
+)(
+	input  wire [2*NUM_INPUTS*NUM_PRODUCTS-1:0] sop_fuses,
+	input  wire [NUM_PRODUCTS-1:0] ptd_fuses,
+	input  wire [NUM_INPUTS-1:0] in,
+	output reg  out
+);
+	integer i, j;
+	reg match;
+
+	always @ (*) begin
+		out = 0;
+		for (i = 0; i < NUM_PRODUCTS; i = i + 1) begin
+			match = 1;
+			for (j = 0; j < NUM_INPUTS; j = j + 1) begin
+				if (!sop_fuses[2*NUM_INPUTS*i + 2*j + 0] && !in[j]) match = 0;
+				if (!sop_fuses[2*NUM_INPUTS*i + 2*j + 1] &&  in[j]) match = 0;
+			end
+			if (match && ptd_fuses[i]) out = 1;
+		end
+	end
+endmodule
+
+module olmc (
+	input wire xor_fuse,
+	input wire ac1_fuse,
+
+	input wire sop,
+	input wire one_sop,
+
+	input wire clk,
+	input wire oe_n,
+
+	inout  wire io,
+	output wire feedback
+);
+	// Internal combined SOP output with optional inversion
+	wire out;
+	assign out = (ac1_fuse ? sop : (sop || one_sop)) ^ xor_fuse;
+
+	reg reg_out;
+	always @ (posedge clk) begin
+		reg_out <= out;
+	end
+
+	assign feedback = ac1_fuse ? !reg_out : out;
+
+	assign io = ac1_fuse ? (one_sop ? !out : 1'bz) : // Combinational
+		(oe_n ? 1'bz : !reg_out); // Registered
+endmodule
diff --git a/models/GAL16V8_reg_tb.v b/models/GAL16V8_reg_tb.v
new file mode 100644
index 0000000..b7dfb60
--- /dev/null
+++ b/models/GAL16V8_reg_tb.v
@@ -0,0 +1,38 @@
+
+module GAL16V8_reg_tb(
+	output reg        clk = 0,
+	output reg  [7:0] in,
+	output reg        oe_n,
+	inout  wire [7:0] io
+);
+
+GAL16V8_reg GAL16V8_reg_inst (
+	.clk(clk),
+	.in(in),
+	.oe_n(oe_n),
+	.io(io)
+);
+
+always #5 clk = !clk;
+
+initial begin
+	$dumpfile("dump.vcd");
+	$dumpvars(0, GAL16V8_reg_tb);
+	#3;
+	in = 8'b0000_1100;
+	oe_n = 0;
+	#10;
+	in = 8'b0000_1001;
+	#10;
+	in = 8'b0000_0110;
+	#10;
+	in = 8'b0000_0011;
+	#10;
+	in = 8'b0000_1100;
+	#30;
+	oe_n = 1;
+	#10;
+	$finish;
+end
+
+endmodule
diff --git a/models/original.v b/models/original.v
new file mode 100644
index 0000000..30fe28a
--- /dev/null
+++ b/models/original.v
@@ -0,0 +1,15 @@
+module original (
+	input wire clk,
+	input wire [5:0] in,
+	output reg [4:0] out
+);
+
+always @(posedge clk) begin
+	out[0] <= in[0] && in[1];
+	out[1] <= in[2] || in[3];
+	out[2] <= in[4] && !in[5] || !in[4] && in[5];
+	out[3] <= in[0] && in[1] && in[2] && in[3] && in[4] && in[5];
+	out[4] <= !(in[0] || in[1] || in[2] || in[3] || in[4] || in[5]);
+end
+
+endmodule
diff --git a/models/prove_equiv.tcl b/models/prove_equiv.tcl
new file mode 100755
index 0000000..ccef4cc
--- /dev/null
+++ b/models/prove_equiv.tcl
@@ -0,0 +1,14 @@
+#!/usr/bin/env -S yosys -c
+yosys -import
+
+read_verilog original.v
+flatten
+synth
+
+read_verilog wrapper.v GAL16V8_reg.v
+flatten
+synth
+
+equiv_make original wrapper equiv
+equiv_induct equiv
+equiv_status -assert equiv
diff --git a/models/wrapper.v b/models/wrapper.v
new file mode 100644
index 0000000..9fde3e9
--- /dev/null
+++ b/models/wrapper.v
@@ -0,0 +1,22 @@
+module wrapper (
+	input wire clk,
+	input wire [5:0] in,
+	output wire [4:0] out
+);
+
+wire [7:0] in_int;
+wire [7:0] io_int;
+wire oe_n;
+
+assign oe_n = 0;
+assign in_int = {3'b0, in};
+assign out = {io_int[3], io_int[4], io_int[5], io_int[6], io_int[7]};
+
+GAL16V8_reg GAL16V8_reg_inst (
+	.clk(clk),
+	.in(in_int),
+	.oe_n(oe_n),
+	.io(io_int)
+);
+
+endmodule