From 4b311b7b99f55ee4bfe43447067b177fb2f90a82 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 11 Jun 2013 19:49:35 +0200 Subject: Further improved and extended xsthammer --- tests/xsthammer/.gitignore | 1 + tests/xsthammer/Makefile | 28 +++++++++ tests/xsthammer/README | 13 +---- tests/xsthammer/generate.cc | 89 +++++++++++++++++++++++++---- tests/xsthammer/run-check.sh | 100 ++++++++++++++++---------------- tests/xsthammer/run-xst.sh | 133 ++++++++++++++++++++++--------------------- 6 files changed, 226 insertions(+), 138 deletions(-) create mode 100644 tests/xsthammer/Makefile (limited to 'tests') diff --git a/tests/xsthammer/.gitignore b/tests/xsthammer/.gitignore index 98d60704..207ebd40 100644 --- a/tests/xsthammer/.gitignore +++ b/tests/xsthammer/.gitignore @@ -1,4 +1,5 @@ generate +generate.lst rtl xst xst_temp diff --git a/tests/xsthammer/Makefile b/tests/xsthammer/Makefile new file mode 100644 index 00000000..ab7aebdc --- /dev/null +++ b/tests/xsthammer/Makefile @@ -0,0 +1,28 @@ + +include generate.lst + +test: $(TARGETS) + +check/%.log: rtl/%.v xst/%.v + bash run-check.sh $(notdir $(basename $<)) + +xst/%.v: rtl/%.v + bash run-xst.sh $(notdir $(basename $<)) + +generate.lst: generate.cc + clang -Wall -o generate generate.cc -lstdc++ + ./generate + { echo -n "TARGETS := "; ls rtl/ | sed 's,\.v$$,.log,; s,^,check/,;' | tr '\n' ' '; } > generate.lst + +check_xl_cells: + ../../yosys xl_cells_tb.ys + +clean: + rm -rf generate generate.lst check_temp xst_temp + +mrproper: clean + rm -rf rtl xst check + +.PHONY: test check_xl_cells clean mrproper +.PRECIOUS: check/%.log xst/%.v rtl/%.v generate.lst + diff --git a/tests/xsthammer/README b/tests/xsthammer/README index 10756dd4..3f1b198d 100644 --- a/tests/xsthammer/README +++ b/tests/xsthammer/README @@ -9,15 +9,6 @@ to synthesize them with Yosys and Xilinx XST and perform formal equivialence checks using the Yosys SAT-based equivialence checker. This will hopefully reveal some bugs in both applications.. ;-) - -Generating the Test Cases: - clang -Wall -o generate generate.cc -lstdc++ - ./generate - -Running XST Synthesis: - bash run-xst.sh - rm -rf xst_temp - -Running Yosys Synthesis and Check: - TBD +Simply run 'make' to generate all test cases and run all the tests. +(Use 'make -j N' to use N parallel cores.) diff --git a/tests/xsthammer/generate.cc b/tests/xsthammer/generate.cc index 9f236c34..b1ec9508 100644 --- a/tests/xsthammer/generate.cc +++ b/tests/xsthammer/generate.cc @@ -13,19 +13,47 @@ const char *arg_types[][2] = { { "{dir} signed [5:0] {name}", "{name}" } // 05 }; -const char *ops[] = { +// See Table 5-1 (page 42) in IEEE Std 1364-2005 +// for a list of all Verilog oprators. + +const char *binary_ops[] = { "+", // 00 "-", // 01 "*", // 02 - "&&", // 03 - "||", // 04 - "&", // 05 +// "/", +// "%", +// "**", + ">", // 03 + ">=", // 04 + "<", // 05 + "<=", // 06 + "&&", // 07 + "||", // 08 + "==", // 09 + "!=", // 10 + "===", // 11 + "!==", // 12 + "&", // 13 + "|", // 14 + "^", // 15 + "^~", // 16 + "<<", // 17 + ">>", // 18 + "<<<", // 19 + ">>>", // 20 +}; + +const char *unary_ops[] = { + "+", // 00 + "-", // 01 + "!", // 02 + "~", // 03 + "&", // 04 + "~&", // 05 "|", // 06 - "^", // 07 - "<<", // 08 - ">>", // 09 - "<<<", // 10 - ">>>", // 11 + "~|", // 07 + "^", // 08 + "~^", // 09 }; void strsubst(std::string &str, const std::string &match, const std::string &replace) @@ -38,10 +66,13 @@ void strsubst(std::string &str, const std::string &match, const std::string &rep int main() { mkdir("rtl", 0777); + + // generate test cases for binary operators + for (int ai = 0; ai < sizeof(arg_types)/sizeof(arg_types[0]); ai++) for (int bi = 0; bi < sizeof(arg_types)/sizeof(arg_types[0]); bi++) for (int yi = 0; yi < sizeof(arg_types)/sizeof(arg_types[0]); yi++) - for (int oi = 0; oi < sizeof(ops)/sizeof(ops[0]); oi++) + for (int oi = 0; oi < sizeof(binary_ops)/sizeof(binary_ops[0]); oi++) { std::string a_decl = arg_types[ai][0]; strsubst(a_decl, "{dir}", "input"); @@ -76,10 +107,46 @@ int main() fprintf(f, "%s;\n", b_decl.c_str()); fprintf(f, "%s;\n", y_decl.c_str()); fprintf(f, "assign %s = %s %s %s;\n", y_ref.c_str(), - a_ref.c_str(), ops[oi], b_ref.c_str()); + a_ref.c_str(), binary_ops[oi], b_ref.c_str()); fprintf(f, "endmodule\n"); fclose(f); } + + // generate test cases for unary operators + + for (int ai = 0; ai < sizeof(arg_types)/sizeof(arg_types[0]); ai++) + for (int yi = 0; yi < sizeof(arg_types)/sizeof(arg_types[0]); yi++) + for (int oi = 0; oi < sizeof(unary_ops)/sizeof(unary_ops[0]); oi++) + { + std::string a_decl = arg_types[ai][0]; + strsubst(a_decl, "{dir}", "input"); + strsubst(a_decl, "{name}", "a"); + + std::string y_decl = arg_types[yi][0]; + strsubst(y_decl, "{dir}", "output"); + strsubst(y_decl, "{name}", "y"); + + std::string a_ref = arg_types[ai][1]; + strsubst(a_ref, "{dir}", "input"); + strsubst(a_ref, "{name}", "a"); + + std::string y_ref = arg_types[yi][1]; + strsubst(y_ref, "{dir}", "output"); + strsubst(y_ref, "{name}", "y"); + + char buffer[1024]; + snprintf(buffer, 1024, "rtl/unary_ops_%02d%02d%02d.v", ai, yi, oi); + + FILE *f = fopen(buffer, "w"); + fprintf(f, "module unary_ops_%02d%02d%02d(a, b, y);\n", ai, yi, oi); + fprintf(f, "%s;\n", a_decl.c_str()); + fprintf(f, "%s;\n", y_decl.c_str()); + fprintf(f, "assign %s = %s %s;\n", y_ref.c_str(), + unary_ops[oi], a_ref.c_str()); + fprintf(f, "endmodule\n"); + fclose(f); + } + return 0; } diff --git a/tests/xsthammer/run-check.sh b/tests/xsthammer/run-check.sh index 6604f6e0..6a77e236 100644 --- a/tests/xsthammer/run-check.sh +++ b/tests/xsthammer/run-check.sh @@ -1,65 +1,65 @@ #!/bin/bash -set -e -mkdir -p check +if [ $# -eq 0 ]; then + echo "Usage: $0 " >&2 + exit 1 +fi -rm -rf check_temp -mkdir check_temp +job="$1" +set -- + +set -e +mkdir -p check check_temp cd check_temp -if [ $# -eq 0 ]; then - set -- $( ls ../rtl | sed 's,\.v$,,' ) -fi +{ + echo "module ${job}_top(a, b, y_rtl, y_xst);" + sed -r '/^(input|output) / !d; /output/ { s/ y;/ y_rtl;/; p; }; s/ y_rtl;/ y_xst;/;' ../rtl/$job.v + echo "${job}_rtl rtl_variant (.a(a), .b(b), .y(y_rtl));" + echo "${job}_xst xst_variant (.a(a), .b(b), .y(y_xst));" + echo "endmodule" +} > ${job}_top.v -for job -do +for mode in nomap techmap; do { - echo "module ${job}_top(a, b, y_rtl, y_xst);" - sed -r '/^(input|output) / !d; /output/ { s/ y;/ y_rtl;/; p; }; s/ y_rtl;/ y_xst;/;' ../rtl/$job.v - echo "${job}_rtl rtl_variant (.a(a), .b(b), .y(y_rtl));" - echo "${job}_xst xst_variant (.a(a), .b(b), .y(y_xst));" - echo "endmodule" - } > ${job}_top.v + echo "read_verilog -DGLBL ../xst/$job.v" + echo "rename $job ${job}_xst" - for mode in nomap techmap; do - { - echo "read_verilog -DGLBL ../xst/$job.v" - echo "rename $job ${job}_xst" + echo "read_verilog ../rtl/$job.v" + echo "rename $job ${job}_rtl" + if [ $mode = techmap ]; then + echo "techmap ${job}_rtl" + fi - echo "read_verilog ../rtl/$job.v" - echo "rename $job ${job}_rtl" - if [ $mode = techmap ]; then - echo "techmap ${job}_rtl" - fi + echo "read_verilog ${job}_top.v" + echo "read_verilog ../xl_cells.v" - echo "read_verilog ${job}_top.v" - echo "read_verilog ../xl_cells.v" + echo "hierarchy -top ${job}_top" + echo "flatten ${job}_top" + echo "hierarchy -top ${job}_top" + echo "opt_clean" - echo "hierarchy -top ${job}_top" - echo "flatten ${job}_top" - echo "hierarchy -top ${job}_top" - echo "opt_clean" + echo "rename ${job}_top ${job}_top_${mode}" + echo "write_ilang ${job}_top_${mode}.il" + } > ${job}_top_${mode}.ys + ../../../yosys -q ${job}_top_${mode}.ys +done - echo "rename ${job}_top ${job}_top_${mode}" - echo "write_ilang ${job}_top_${mode}.il" - } > ${job}_top_${mode}.ys - ../../../yosys -q ${job}_top_${mode}.ys - done +{ + echo "read_ilang ${job}_top_nomap.il" + echo "read_ilang ${job}_top_techmap.il" + echo "sat -verify -show a,b,y_rtl,y_xst -prove y_rtl y_xst ${job}_top_nomap" + echo "sat -verify -show a,b,y_rtl,y_xst -prove y_rtl y_xst ${job}_top_techmap" +} > ${job}_cmp.ys - { - echo "read_ilang ${job}_top_nomap.il" - echo "read_ilang ${job}_top_techmap.il" - echo "sat -verify -show a,b,y_rtl,y_xst -prove y_rtl y_xst ${job}_top_nomap" - echo "sat -verify -show a,b,y_rtl,y_xst -prove y_rtl y_xst ${job}_top_techmap" - } > ${job}_cmp.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 + exit 1 +fi - 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 - # break - fi -done +exit 0 diff --git a/tests/xsthammer/run-xst.sh b/tests/xsthammer/run-xst.sh index 879ce75c..21670707 100644 --- a/tests/xsthammer/run-xst.sh +++ b/tests/xsthammer/run-xst.sh @@ -1,75 +1,76 @@ #!/bin/bash +if [ $# -eq 0 ]; then + echo "Usage: $0 " >&2 + exit 1 +fi + +job="$1" +set -- + set -e -mkdir -p xst -. /opt/Xilinx/14.2/ISE_DS/settings64.sh +mkdir -p xst xst_temp/$job +cd xst_temp/$job -rm -rf xst_temp -mkdir xst_temp -cd xst_temp +cat > $job.xst <<- EOT + run + -ifn $job.prj + -ifmt mixed + -ofn $job + -ofmt NGC + -p xc6vlx75t-2-ff784 + -top $job + -opt_mode Speed + -opt_level 1 + -power NO + -iuc NO + -keep_hierarchy NO + -rtlview Yes + -glob_opt AllClockNets + -read_cores YES + -write_timing_constraints NO + -cross_clock_analysis NO + -hierarchy_separator / + -bus_delimiter <> + -case maintain + -slice_utilization_ratio 100 + -bram_utilization_ratio 100 + -dsp_utilization_ratio 100 + -fsm_extract YES -fsm_encoding Auto + -safe_implementation No + -fsm_style lut + -ram_extract Yes + -ram_style Auto + -rom_extract Yes + -shreg_extract YES + -rom_style Auto + -auto_bram_packing NO + -resource_sharing YES + -async_to_sync NO + -use_dsp48 auto + -iobuf NO + -max_fanout 100000 + -bufg 32 + -register_duplication YES + -register_balancing No + -optimize_primitives NO + -use_clock_enable Auto + -use_sync_set Auto + -use_sync_reset Auto + -iob auto + -equivalent_register_removal YES + -slice_utilization_ratio_maxmargin 5 +EOT -if [ $# -eq 0 ]; then - set -- $( ls ../rtl | sed 's,\.v$,,' ) -fi +cat > $job.prj <<- EOT + verilog work "../../rtl/$job.v" +EOT -for job -do - cat > $job.xst <<- EOT - run - -ifn $job.prj - -ifmt mixed - -ofn $job - -ofmt NGC - -p xc6vlx75t-2-ff784 - -top $job - -opt_mode Speed - -opt_level 1 - -power NO - -iuc NO - -keep_hierarchy NO - -rtlview Yes - -glob_opt AllClockNets - -read_cores YES - -write_timing_constraints NO - -cross_clock_analysis NO - -hierarchy_separator / - -bus_delimiter <> - -case maintain - -slice_utilization_ratio 100 - -bram_utilization_ratio 100 - -dsp_utilization_ratio 100 - -fsm_extract YES -fsm_encoding Auto - -safe_implementation No - -fsm_style lut - -ram_extract Yes - -ram_style Auto - -rom_extract Yes - -shreg_extract YES - -rom_style Auto - -auto_bram_packing NO - -resource_sharing YES - -async_to_sync NO - -use_dsp48 auto - -iobuf NO - -max_fanout 100000 - -bufg 32 - -register_duplication YES - -register_balancing No - -optimize_primitives NO - -use_clock_enable Auto - -use_sync_set Auto - -use_sync_reset Auto - -iob auto - -equivalent_register_removal YES - -slice_utilization_ratio_maxmargin 5 - EOT +. /opt/Xilinx/14.2/ISE_DS/settings64.sh - cat > $job.prj <<- EOT - verilog work "../rtl/$job.v" - EOT +xst -ifn $job.xst +netgen -w -ofmt verilog $job.ngc $job +cp $job.v ../../xst/$job.v - xst -ifn $job.xst - netgen -w -ofmt verilog $job.ngc $job - cp $job.v ../xst/$job.v -done +exit 0 -- cgit v1.2.3