From a6370ce857bdb547804a9c5905a6dc4ffa433ee6 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 10 Jun 2013 13:57:10 +0200 Subject: [PATCH] Progress in xsthammer: working proof for cell models --- tests/xsthammer/run-check.sh | 7 +++--- tests/xsthammer/xl_cells_tb.v | 45 ++++++++++++++++++++++------------ tests/xsthammer/xl_cells_tb.ys | 33 +++++++++++++------------ 3 files changed, 51 insertions(+), 34 deletions(-) diff --git a/tests/xsthammer/run-check.sh b/tests/xsthammer/run-check.sh index dd080d02d..de7c33b4b 100644 --- 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 6226698a3..a7472e4f1 100644 --- 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 9ceab558d..616f1b278 100644 --- 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 -- 2.30.2