Progress in xsthammer: working proof for cell models

diff --git a/tests/xsthammer/run-check.sh b/tests/xsthammer/run-check.sh
index dd080d02df95575dc96c82ac07164f9e64384106..de7c33b4b4625b45e0ae6eb3ff982ab30a43ee1c 100644 (file)
--- a/tests/xsthammer/run-check.sh
+++ b/tests/xsthammer/run-check.sh
@@ -13,7 +13,7 @@ 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 "${job}_xst xst_variant (.a(a), .b(b), .y(y2));"
                echo "endmodule"
        } > ${job}_top.v
 
@@ -41,12 +41,13 @@ do
        } > ${job}_cmp.ys
 
        yosys ${job}_top.ys
+
        if yosys -l ${job}.log ${job}_cmp.ys; then
                mv ${job}.log ../check/${job}.log
+               rm -f ../check/${job}.err
        else
                mv ${job}.log ../check/${job}.err
+               rm -f ../check/${job}.log
        fi
-
-       break;
 done
 

diff --git a/tests/xsthammer/xl_cells_tb.v b/tests/xsthammer/xl_cells_tb.v
index 6226698a37bd01cb9300f70109dc51fbb06ff49e..a7472e4f19c90927c313338cf5e07a46c52a9db1 100644 (file)
--- a/tests/xsthammer/xl_cells_tb.v
+++ b/tests/xsthammer/xl_cells_tb.v
@@ -16,41 +16,56 @@ 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));
+wire [3:0] MY_O, XL_O;
+genvar i;
+generate for (i=0; i<4; i=i+1) begin:V
+       MY_LUT2 #(.INIT(i)) MY(.O(MY_O[i]), .I0(I0), .I1(I1));
+       XL_LUT2 #(.INIT(i)) XL(.O(XL_O[i]), .I0(I0), .I1(I1));
+end endgenerate
 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));
+wire [7:0] MY_O, XL_O;
+genvar i;
+generate for (i=0; i<8; i=i+1) begin:V
+       MY_LUT3 #(.INIT(i)) MY(.O(MY_O[i]), .I0(I0), .I1(I1), .I2(I2));
+       XL_LUT3 #(.INIT(i)) XL(.O(XL_O[i]), .I0(I0), .I1(I1), .I2(I2));
+end endgenerate
 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));
+wire [15:0] MY_O, XL_O;
+genvar i;
+generate for (i=0; i<16; i=i+1) begin:V
+       MY_LUT4 #(.INIT(i)) MY(.O(MY_O[i]), .I0(I0), .I1(I1), .I2(I2), .I3(I3));
+       XL_LUT4 #(.INIT(i)) XL(.O(XL_O[i]), .I0(I0), .I1(I1), .I2(I2), .I3(I3));
+end endgenerate
 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));
+wire [31:0] MY_O, XL_O;
+genvar i;
+generate for (i=0; i<32; i=i+1) begin:V
+       MY_LUT5 #(.INIT(i)) MY(.O(MY_O[i]), .I0(I0), .I1(I1), .I2(I2), .I3(I3), .I4(I4));
+       XL_LUT5 #(.INIT(i)) XL(.O(XL_O[i]), .I0(I0), .I1(I1), .I2(I2), .I3(I3), .I4(I4));
+end endgenerate
 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));
+wire [63:0] MY_O, XL_O;
+genvar i;
+generate for (i=0; i<64; i=i+1) begin:V
+       MY_LUT6 #(.INIT(i)) MY(.O(MY_O[i]), .I0(I0), .I1(I1), .I2(I2), .I3(I3), .I4(I4), .I5(I5));
+       XL_LUT6 #(.INIT(i)) XL(.O(XL_O[i]), .I0(I0), .I1(I1), .I2(I2), .I3(I3), .I4(I4), .I5(I5));
+end endgenerate
 output ok = MY_O == XL_O;
 endmodule
 

diff --git a/tests/xsthammer/xl_cells_tb.ys b/tests/xsthammer/xl_cells_tb.ys
index 9ceab558d947442662ea8026511e146e146c2ac5..616f1b27848b8ed7d3aafef670c9a4ba8116afe6 100644 (file)
--- a/tests/xsthammer/xl_cells_tb.ys
+++ b/tests/xsthammer/xl_cells_tb.ys
@@ -18,11 +18,11 @@ 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/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
@@ -30,27 +30,28 @@ 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 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
 
+hierarchy
 proc
-flatten
+flatten TB_*
 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_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