Progress on xsthammer

diff --git a/tests/xsthammer/.gitignore b/tests/xsthammer/.gitignore
index bdaf6b32055d01df00990aa665b72e85e7035e49..98d60704bbe3c0361af0f5b2f6a08d550abc2e27 100644 (file)
--- a/tests/xsthammer/.gitignore
+++ b/tests/xsthammer/.gitignore
@@ -2,3 +2,5 @@ generate
 rtl
 xst
 xst_temp
+check
+check_temp

diff --git a/tests/xsthammer/run-check.sh b/tests/xsthammer/run-check.sh
new file mode 100644 (file)
index 0000000..dd080d0
--- /dev/null
+++ b/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
+

diff --git a/tests/xsthammer/xl_cells.v b/tests/xsthammer/xl_cells.v
new file mode 100644 (file)
index 0000000..6a3fa79
--- /dev/null
+++ b/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
+

diff --git a/tests/xsthammer/xl_cells_tb.v b/tests/xsthammer/xl_cells_tb.v
new file mode 100644 (file)
index 0000000..6226698
--- /dev/null
+++ b/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
+

diff --git a/tests/xsthammer/xl_cells_tb.ys b/tests/xsthammer/xl_cells_tb.ys
new file mode 100644 (file)
index 0000000..9ceab55
--- /dev/null
+++ b/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
+