riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Progress in xsthammer: working proof for cell models

This commit is contained in:
Clifford Wolf 2013-06-10 13:57:10 +02:00
parent 59dd02baa2
commit a6370ce857
3 changed files with 51 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
tests/xsthammer/run-check.sh
View File

@ -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

45
tests/xsthammer/xl_cells_tb.v
View File

@ -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

33
tests/xsthammer/xl_cells_tb.ys
View File

@ -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