summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2013-06-11 19:49:35 +0200
committerClifford Wolf <clifford@clifford.at>2013-06-11 19:49:35 +0200
commit4b311b7b99f55ee4bfe43447067b177fb2f90a82 (patch)
tree193d4d97230bd7665846293a4229312d2227b0e6
parent8ce99fa6863a8e43b889a11c13e45f317fff11b3 (diff)
Further improved and extended xsthammer
-rw-r--r--frontends/verilog/lexer.l1
-rw-r--r--tests/xsthammer/.gitignore1
-rw-r--r--tests/xsthammer/Makefile28
-rw-r--r--tests/xsthammer/README13
-rw-r--r--tests/xsthammer/generate.cc89
-rw-r--r--tests/xsthammer/run-check.sh100
-rw-r--r--tests/xsthammer/run-xst.sh133
7 files changed, 227 insertions, 138 deletions
diff --git a/frontends/verilog/lexer.l b/frontends/verilog/lexer.l
index f899191b..783b790b 100644
--- a/frontends/verilog/lexer.l
+++ b/frontends/verilog/lexer.l
@@ -234,6 +234,7 @@ supply1 { return TOK_SUPPLY1; }
">=" { return OP_GE; }
"===" { return OP_EQ; }
+"!==" { return OP_NE; }
/* "~&" { return OP_NAND; } */
/* "~|" { return OP_NOR; } */
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 <job_id>" >&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 <job_id>" >&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