Added first xsthammer scripts
authorClifford Wolf <clifford@clifford.at>
Sun, 9 Jun 2013 23:40:20 +0000 (01:40 +0200)
committerClifford Wolf <clifford@clifford.at>
Sun, 9 Jun 2013 23:40:20 +0000 (01:40 +0200)
tests/xsthammer/.gitignore [new file with mode: 0644]
tests/xsthammer/README [new file with mode: 0644]
tests/xsthammer/generate.cc [new file with mode: 0644]
tests/xsthammer/run-xst.sh [new file with mode: 0644]

diff --git a/tests/xsthammer/.gitignore b/tests/xsthammer/.gitignore
new file mode 100644 (file)
index 0000000..bdaf6b3
--- /dev/null
@@ -0,0 +1,4 @@
+generate
+rtl
+xst
+xst_temp
diff --git a/tests/xsthammer/README b/tests/xsthammer/README
new file mode 100644 (file)
index 0000000..10756dd
--- /dev/null
@@ -0,0 +1,23 @@
+
+       ================================
+       This is work under construction!
+       ================================
+
+
+This is going to be a collection of auto-generated test cases. The goal is
+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
+
diff --git a/tests/xsthammer/generate.cc b/tests/xsthammer/generate.cc
new file mode 100644 (file)
index 0000000..2e50398
--- /dev/null
@@ -0,0 +1,85 @@
+
+#include <sys/stat.h>
+#include <sys/types.h>
+#include <stdio.h>
+#include <string>
+
+const char *arg_types[][2] = {
+       { "{dir} [3:0] {name}", "{name}" },
+       { "{dir} [4:0] {name}", "{name}" },
+       { "{dir} [5:0] {name}", "{name}" },
+       { "{dir} signed [3:0] {name}", "{name}" },
+       { "{dir} signed [4:0] {name}", "{name}" },
+       { "{dir} signed [5:0] {name}", "{name}" }
+};
+
+const char *ops[] = {
+       "+",
+       "-",
+       "*",
+       "&&",
+       "||",
+       "&",
+       "|",
+       "^",
+       "<<",
+       ">>",
+       "<<<",
+       ">>>",
+};
+
+void strsubst(std::string &str, const std::string &match, const std::string &replace)
+{
+       size_t pos;
+       while ((pos = str.find(match)) != std::string::npos)
+               str.replace(pos, match.size(), replace);
+}
+
+int main()
+{
+       mkdir("rtl", 0777);
+       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++)
+       {
+               std::string a_decl = arg_types[ai][0];
+               strsubst(a_decl, "{dir}", "input");
+               strsubst(a_decl, "{name}", "a");
+
+               std::string b_decl = arg_types[bi][0];
+               strsubst(b_decl, "{dir}", "input");
+               strsubst(b_decl, "{name}", "b");
+
+               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 b_ref = arg_types[bi][1];
+               strsubst(b_ref, "{dir}", "input");
+               strsubst(b_ref, "{name}", "b");
+
+               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/binary_ops_%02d%02d%02d%02d.v", ai, bi, yi, oi);
+
+               FILE *f = fopen(buffer, "w");
+               fprintf(f, "module binary_ops_%02d%02d%02d%02d(a, b, y);\n", ai, bi, yi, oi);
+               fprintf(f, "%s;\n", a_decl.c_str());
+               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());
+               fprintf(f, "endmodule\n");
+               fclose(f);
+       }
+       return 0;
+}
+
diff --git a/tests/xsthammer/run-xst.sh b/tests/xsthammer/run-xst.sh
new file mode 100644 (file)
index 0000000..bcd12ea
--- /dev/null
@@ -0,0 +1,71 @@
+#!/bin/bash
+
+set -ex
+mkdir -p xst
+. /opt/Xilinx/14.2/ISE_DS/settings64.sh
+
+rm -rf xst_temp
+mkdir xst_temp
+cd xst_temp
+
+for job in $( ls ../rtl | sed 's,\.v$,,' )
+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
+
+       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
+done
+