From d07b32ade5f7d3d95792160e40617121e5ef2402 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 10 Jun 2013 12:37:05 +0200 Subject: [PATCH] Progress on xsthammer --- tests/xsthammer/.gitignore | 2 + tests/xsthammer/run-check.sh | 52 ++++++++++++++++++++ tests/xsthammer/xl_cells.v | 69 +++++++++++++++++++++++++++ tests/xsthammer/xl_cells_tb.v | 87 ++++++++++++++++++++++++++++++++++ tests/xsthammer/xl_cells_tb.ys | 58 +++++++++++++++++++++++ 5 files changed, 268 insertions(+) create mode 100644 tests/xsthammer/run-check.sh create mode 100644 tests/xsthammer/xl_cells.v create mode 100644 tests/xsthammer/xl_cells_tb.v create mode 100644 tests/xsthammer/xl_cells_tb.ys diff --git a/tests/xsthammer/.gitignore b/tests/xsthammer/.gitignore index bdaf6b320..98d60704b 100644 --- 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 index 000000000..dd080d02d --- /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 index 000000000..6a3fa7996 --- /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 index 000000000..6226698a3 --- /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 index 000000000..9ceab558d --- /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 + -- 2.30.2