Progress on xsthammer

tests/xsthammer/.gitignore

@@ -2,3 +2,5 @@ generate
 rtl
 xst
 xst_temp
+check
+check_temp

tests/xsthammer/run-check.sh

@@ -0,0 +1,52 @@
+#!/bin/bash
+
+set -ex
+mkdir -p check
+
+rm -rf check_temp
+mkdir check_temp
+cd check_temp
+
+for job in $( ls ../rtl | sed 's,\.v$,,' )
+do
+	{
+		echo "module top(a, b, y1, y2);"
+		sed -r '/^(input|output) / !d; /output/ { s/ y;/ y1;/; p; }; s/ y1;/ y2;/;' ../rtl/$job.v
+		echo "${job}_rtl rtl_variant (.a(a), .b(b), .y(y1));"
+		echo "${job}_xst xst_variant (.a(a), .b(b), .y(y1));"
+		echo "endmodule"
+	} > ${job}_top.v
+
+	{
+		echo "read_verilog -DGLBL ../xst/$job.v"
+		echo "rename $job ${job}_xst"
+
+		echo "read_verilog ../rtl/$job.v"
+		echo "rename $job ${job}_rtl"
+
+		echo "read_verilog ${job}_top.v"
+		echo "read_verilog ../xl_cells.v"
+
+		echo "hierarchy -top top"
+		echo "flatten top"
+		echo "hierarchy -top top"
+		echo "opt_clean"
+
+		echo "write_ilang ${job}_top.il"
+	} > ${job}_top.ys
+
+	{
+		echo "read_ilang ${job}_top.il"
+		echo "sat -verify -prove y1 y2 top"
+	} > ${job}_cmp.ys
+
+	yosys ${job}_top.ys
+	if yosys -l ${job}.log ${job}_cmp.ys; then
+		mv ${job}.log ../check/${job}.log
+	else
+		mv ${job}.log ../check/${job}.err
+	fi
+
+	break;
+done
+

tests/xsthammer/xl_cells.v

@@ -0,0 +1,69 @@
+
+module GND(G);
+output G = 0;
+endmodule
+
+module INV(O, I);
+input I;
+output O = !I;
+endmodule
+
+module LUT2(O, I0, I1);
+parameter INIT = 0;
+input I0, I1;
+wire [3:0] lutdata = INIT;
+wire [1:0] idx = { I1, I0 };
+output O = lutdata[idx];
+endmodule
+
+module LUT3(O, I0, I1, I2);
+parameter INIT = 0;
+input I0, I1, I2;
+wire [7:0] lutdata = INIT;
+wire [2:0] idx = { I2, I1, I0 };
+output O = lutdata[idx];
+endmodule
+
+module LUT4(O, I0, I1, I2, I3);
+parameter INIT = 0;
+input I0, I1, I2, I3;
+wire [15:0] lutdata = INIT;
+wire [3:0] idx = { I3, I2, I1, I0 };
+output O = lutdata[idx];
+endmodule
+
+module LUT5(O, I0, I1, I2, I3, I4);
+parameter INIT = 0;
+input I0, I1, I2, I3, I4;
+wire [31:0] lutdata = INIT;
+wire [4:0] idx = { I4, I3, I2, I1, I0 };
+output O = lutdata[idx];
+endmodule
+
+module LUT6(O, I0, I1, I2, I3, I4, I5);
+parameter INIT = 0;
+input I0, I1, I2, I3, I4, I5;
+wire [63:0] lutdata = INIT;
+wire [5:0] idx = { I5, I4, I3, I2, I1, I0 };
+output O = lutdata[idx];
+endmodule
+
+module MUXCY(O, CI, DI, S);
+input CI, DI, S;
+output O = S ? CI : DI;
+endmodule
+
+module MUXF7(O, I0, I1, S);
+input I0, I1, S;
+output O = S ? I1 : I0;
+endmodule
+
+module VCC(P);
+output P = 1;
+endmodule
+
+module XORCY(O, CI, LI);
+input CI, LI;
+output O = CI ^ LI;
+endmodule
+

tests/xsthammer/xl_cells_tb.v

@@ -0,0 +1,87 @@
+
+module TB_GND(ok);
+wire MY_G, XL_G;
+MY_GND MY(.G(MY_G));
+XL_GND XL(.G(XL_G));
+output ok = MY_G == XL_G;
+endmodule
+
+module TB_INV(ok, I);
+input I;
+wire MY_O, XL_O;
+MY_INV MY(.O(MY_O), .I(I));
+XL_INV XL(.O(XL_O), .I(I));
+output ok = MY_O == XL_O;
+endmodule
+
+module TB_LUT2(ok, I0, I1);
+input I0, I1;
+wire MY_O, XL_O;
+MY_LUT2 #(.INIT(1234567)) MY(.O(MY_O), .I0(I0), .I1(I1));
+XL_LUT2 #(.INIT(1234567)) XL(.O(XL_O), .I0(I0), .I1(I1));
+output ok = MY_O == XL_O;
+endmodule
+
+module TB_LUT3(ok, I0, I1, I2);
+input I0, I1, I2;
+wire MY_O, XL_O;
+MY_LUT3 #(.INIT(1234567)) MY(.O(MY_O), .I0(I0), .I1(I1), .I2(I2));
+XL_LUT3 #(.INIT(1234567)) XL(.O(XL_O), .I0(I0), .I1(I1), .I2(I2));
+output ok = MY_O == XL_O;
+endmodule
+
+module TB_LUT4(ok, I0, I1, I2, I3);
+input I0, I1, I2, I3;
+wire MY_O, XL_O;
+MY_LUT4 #(.INIT(1234567)) MY(.O(MY_O), .I0(I0), .I1(I1), .I2(I2), .I3(I3));
+XL_LUT4 #(.INIT(1234567)) XL(.O(XL_O), .I0(I0), .I1(I1), .I2(I2), .I3(I3));
+output ok = MY_O == XL_O;
+endmodule
+
+module TB_LUT5(ok, I0, I1, I2, I3, I4);
+input I0, I1, I2, I3, I4;
+wire MY_O, XL_O;
+MY_LUT5 #(.INIT(1234567)) MY(.O(MY_O), .I0(I0), .I1(I1), .I2(I2), .I3(I3), .I4(I4));
+XL_LUT5 #(.INIT(1234567)) XL(.O(XL_O), .I0(I0), .I1(I1), .I2(I2), .I3(I3), .I4(I4));
+output ok = MY_O == XL_O;
+endmodule
+
+module TB_LUT6(ok, I0, I1, I2, I3, I4, I5);
+input I0, I1, I2, I3, I4, I5;
+wire MY_O, XL_O;
+MY_LUT6 #(.INIT(1234567)) MY(.O(MY_O), .I0(I0), .I1(I1), .I2(I2), .I3(I3), .I4(I4), .I5(I5));
+XL_LUT6 #(.INIT(1234567)) XL(.O(XL_O), .I0(I0), .I1(I1), .I2(I2), .I3(I3), .I4(I4), .I5(I5));
+output ok = MY_O == XL_O;
+endmodule
+
+module TB_MUXCY(ok, CI, DI, S);
+input CI, DI, S;
+wire MY_O, XL_O;
+MY_MUXCY MY(.O(MY_O), .CI(CI), .DI(DI), .S(S));
+XL_MUXCY XL(.O(XL_O), .CI(CI), .DI(DI), .S(S));
+output ok = MY_O == XL_O;
+endmodule
+
+module TB_MUXF7(ok, I0, I1, S);
+input I0, I1, S;
+wire MY_O, XL_O;
+MY_MUXF7 MY(.O(MY_O), .I0(I0), .I1(I1), .S(S));
+XL_MUXF7 XL(.O(XL_O), .I0(I0), .I1(I1), .S(S));
+output ok = MY_O == XL_O;
+endmodule
+
+module TB_VCC(ok);
+wire MY_P, XL_P;
+MY_VCC MY(.P(MY_P));
+XL_VCC XL(.P(XL_P));
+output ok = MY_P == XL_P;
+endmodule
+
+module TB_XORCY(ok, CI, LI);
+input CI, LI;
+wire MY_O, XL_O;
+MY_XORCY MY(.O(MY_O), .CI(CI), .LI(LI));
+XL_XORCY XL(.O(XL_O), .CI(CI), .LI(LI));
+output ok = MY_O == XL_O;
+endmodule
+

tests/xsthammer/xl_cells_tb.ys

@@ -0,0 +1,58 @@
+
+# Verify xilinx cell models
+
+read_verilog xl_cells.v
+read_verilog xl_cells_tb.v
+
+rename GND   MY_GND
+rename INV   MY_INV
+rename LUT2  MY_LUT2
+rename LUT3  MY_LUT3
+rename LUT4  MY_LUT4
+rename LUT5  MY_LUT5
+rename LUT6  MY_LUT6
+rename MUXCY MY_MUXCY
+rename MUXF7 MY_MUXF7
+rename VCC   MY_VCC
+rename XORCY MY_XORCY
+
+read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/GND.v
+read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/INV.v
+# read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/LUT2.v
+# read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/LUT3.v
+# read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/LUT4.v
+# read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/LUT5.v
+# read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/LUT6.v
+read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/MUXCY.v
+read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/MUXF7.v
+read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/VCC.v
+read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/XORCY.v
+
+rename GND   XL_GND
+rename INV   XL_INV
+# rename LUT2  XL_LUT2
+# rename LUT3  XL_LUT3
+# rename LUT4  XL_LUT4
+# rename LUT5  XL_LUT5
+# rename LUT6  XL_LUT6
+rename MUXCY XL_MUXCY
+rename MUXF7 XL_MUXF7
+rename VCC   XL_VCC
+rename XORCY XL_XORCY
+
+proc
+flatten
+opt_clean
+
+sat -verify -prove ok 1'b1 TB_GND
+sat -verify -prove ok 1'b1 TB_INV
+# sat -verify -prove ok 1'b1 TB_LUT2
+# sat -verify -prove ok 1'b1 TB_LUT3
+# sat -verify -prove ok 1'b1 TB_LUT4
+# sat -verify -prove ok 1'b1 TB_LUT5
+# sat -verify -prove ok 1'b1 TB_LUT6
+sat -verify -prove ok 1'b1 TB_MUXCY
+sat -verify -prove ok 1'b1 TB_MUXF7
+sat -verify -prove ok 1'b1 TB_VCC
+sat -verify -prove ok 1'b1 TB_XORCY
+