diff --git a/flash_minipro.sh b/flash_minipro.sh new file mode 100755 index 0000000..ad59121 --- /dev/null +++ b/flash_minipro.sh @@ -0,0 +1,34 @@ +#!/bin/bash + +set -e + +# Check args +if [[ $# -ne 2 ]]; then + echo "USAGE: $0 " + exit 1 +fi + +# Program GAL +minipro -p "$2" -w "$1" + +# Read GAL +READBACK=/tmp/gal_tmp +minipro -p "$2" -r "$READBACK.jed" + +# Fix JEDEC for jedutil +truncate -s -7 "$READBACK.jed" +printf "*\r\n\x03" >> "$READBACK.jed" +od -t u1 -An -w1 -v "$READBACK.jed" | awk '{s+=$1; if(s > 65535) s = and(65535, s)} END {printf("%04X\r\n", s)}' >> "$READBACK.jed" + +# Convert to binary and compare +jedutil -convert "$READBACK.jed" "$READBACK.bin" +jedutil -convert "$1" "${1%.jed}.bin" + +if cmp -s "$READBACK.bin" "${1%.jed}.bin"; then + echo "VERIFICATION OK!" +else + echo "VERIFICATION FAILED!" +fi + +# Clean up +rm "$READBACK.jed" "$READBACK.bin" "${1%.jed}.bin" diff --git a/models/GAL16V8_reg.hex b/models/GAL16V8_reg.hex deleted file mode 100644 index 1178309..0000000 --- a/models/GAL16V8_reg.hex +++ /dev/null @@ -1,279 +0,0 @@ -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 index 6c7be31..487dc85 100644 --- a/models/GAL16V8_reg.v +++ b/models/GAL16V8_reg.v @@ -1,9 +1,9 @@ `default_nettype none module GAL16V8_reg ( - input wire clk, - input wire [7:0] in, - input wire oe_n, - inout wire [7:0] io + input wire clk, // Pin 1 + input wire [7:0] in, // Pin {9, 8, 7, 6, 5, 4, 3, 2} + input wire oe_n, // Pin 11 + inout wire [7:0] io // Pin {12, 13, 14, 15, 16, 17, 18, 19} ); // Read in binary JEDEC file reg [7:0] jed_bin_file [0:278]; @@ -63,7 +63,7 @@ module GAL16V8_reg ( .NUM_PRODUCTS(1), .NUM_INPUTS(16) ) one_sop_inst ( - .sop_fuses(sop_fuses[i][255:224]), + .sop_fuses(sop_fuses[i][31:0]), .ptd_fuses(ptd_fuses[i][0]), .in(interleaved), .out(one_sop_out) @@ -74,7 +74,7 @@ module GAL16V8_reg ( .NUM_PRODUCTS(7), .NUM_INPUTS(16) ) sop_inst ( - .sop_fuses(sop_fuses[i][223:0]), + .sop_fuses(sop_fuses[i][255:32]), .ptd_fuses(ptd_fuses[i][7:1]), .in(interleaved), .out(sop_out) @@ -168,7 +168,7 @@ module olmc ( reg_out <= out; end - assign feedback = ac1_fuse ? !reg_out : out; + assign feedback = ac1_fuse ? !out : !reg_out; assign io = ac1_fuse ? (one_sop ? !out : 1'bz) : // Combinational (oe_n ? 1'bz : !reg_out); // Registered diff --git a/models/GAL16V8_reg_tb.v b/models/GAL16V8_reg_tb.v index b7dfb60..06b841e 100644 --- a/models/GAL16V8_reg_tb.v +++ b/models/GAL16V8_reg_tb.v @@ -19,16 +19,16 @@ initial begin $dumpfile("dump.vcd"); $dumpvars(0, GAL16V8_reg_tb); #3; - in = 8'b0000_1100; + in = 8'b0000_0000; oe_n = 0; #10; - in = 8'b0000_1001; + in = 8'b0000_0001; #10; - in = 8'b0000_0110; + in = 8'b0000_0010; #10; in = 8'b0000_0011; #10; - in = 8'b0000_1100; + in = 8'b0000_1101; #30; oe_n = 1; #10; diff --git a/models/prove_equiv.tcl b/models/prove_equiv.tcl index ccef4cc..837ff6e 100755 --- a/models/prove_equiv.tcl +++ b/models/prove_equiv.tcl @@ -1,14 +1,74 @@ #!/usr/bin/env -S yosys -c yosys -import -read_verilog original.v +# Parse arguments +if { $argc < 3 } { + puts "USAGE: $argv0 -- ..." + exit +} + +set jedec_file [lindex $argv 0] +set pcf_file [lindex $argv 1] +set verilog_files [lrange $argv 2 end] + +# Convert JEDEC file to hex for Verilog model +exec jedutil -convert $jedec_file GAL16V8_reg.bin +exec xxd -ps -c 1 GAL16V8_reg.bin GAL16V8_reg.hex + +# Read and synthesize original Verilog +read_verilog $verilog_files +hierarchy -auto-top flatten synth +splitnets -ports +yosys rename -top __original +select -module __original +# Process PCF file and rename ports +set used [list] +set pin_mapping [dict create 1 "clk" 2 "in\[0\]" 3 "in\[1\]" 4 "in\[2\]" 5 "in\[3\]" 6 "in\[4\]" 7 "in\[5\]" 8 "in\[6\]" 9 "in\[7\]" 11 "oe_n" 12 "io\[7\]" 13 "io\[6\]" 14 "io\[5\]" 15 "io\[4\]" 16 "io\[3\]" 17 "io\[2\]" 18 "io\[1\]" 19 "io\[0\]"] + +set pcf_fp [open $pcf_file r] +foreach line [split [read $pcf_fp] "\n"] { + puts $line + if {[regexp {set_io\s+(.*)\s+([0-9]+)} $line -> net pin]} { + # Rename nets to match GAL model + yosys rename $net __[dict get $pin_mapping $pin] + + # Mark as used + lappend used [dict get $pin_mapping $pin] + } +} + +select -clear +design -stash __original + +# Read and synthesize GAL model read_verilog wrapper.v GAL16V8_reg.v flatten synth +splitnets -ports +select -module __wrapper -equiv_make original wrapper equiv +# Delete extra "unused" ports +foreach pin_name [dict values $pin_mapping] { + if {[lsearch -exact $used $pin_name] >= 0} { + puts "$pin_name is used" + } elseif {$pin_name == "oe_n"} { + puts "$pin_name is not used" + # Enable registered outputs if net unused + connect -set __oe_n '0 + delete -port __$pin_name + } else { + puts "$pin_name is not used" + delete -port __$pin_name + } +} +select -clear + +# Make and check equivalence circuit +design -copy-from __original -as __original A:top + +equiv_make __original __wrapper equiv equiv_induct equiv equiv_status -assert equiv diff --git a/models/wrapper.v b/models/wrapper.v index 9fde3e9..8a80e93 100644 --- a/models/wrapper.v +++ b/models/wrapper.v @@ -1,22 +1,16 @@ -module wrapper ( - input wire clk, - input wire [5:0] in, - output wire [4:0] out +`default_nettype none +module __wrapper ( + input wire __clk, // Pin 1 + input wire [7:0] __in, // Pin {9, 8, 7, 6, 5, 4, 3, 2} + input wire __oe_n, // Pin 11 + inout wire [7:0] __io // Pin {12, 13, 14, 15, 16, 17, 18, 19} ); -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) + .clk(__clk), + .in(__in), + .oe_n(__oe_n), + .io(__io) ); endmodule diff --git a/testcases/big_xor.pcf b/testcases/big_xor.pcf index 3e70be3..b48ccdb 100644 --- a/testcases/big_xor.pcf +++ b/testcases/big_xor.pcf @@ -1,4 +1,3 @@ -set_io clk 1 set_io A[0] 2 set_io A[1] 3 set_io A[2] 4