--- /dev/null
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2014 Clifford Wolf <clifford@clifford.at>
+ * Copyright (C) 2014 Johann Glaser <Johann.Glaser@gmx.at>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/yosys.h"
+#include "kernel/satgen.h"
+
+static uint32_t xorshift32_state = 123456789;
+
+static uint32_t xorshift32(uint32_t limit) {
+ xorshift32_state ^= xorshift32_state << 13;
+ xorshift32_state ^= xorshift32_state >> 17;
+ xorshift32_state ^= xorshift32_state << 5;
+ return xorshift32_state % limit;
+}
+
+static RTLIL::Wire *getw(std::vector<RTLIL::Wire*> &wires, RTLIL::Wire *w)
+{
+ while (1) {
+ int idx = xorshift32(SIZE(wires));
+ if (wires[idx] != w && !wires[idx]->port_output)
+ return wires[idx];
+ }
+}
+
+static void test_abcloop()
+{
+ log("Rng seed value: %u\n", int(xorshift32_state));
+
+ RTLIL::Design *design = new RTLIL::Design;
+ RTLIL::Module *module = nullptr;
+ RTLIL::SigSpec in_sig, out_sig;
+
+ bool truthtab[16][4];
+ int create_cycles = 0;
+
+ while (1)
+ {
+ module = design->addModule("\\uut");
+ create_cycles++;
+
+ in_sig = {};
+ out_sig = {};
+
+ std::vector<RTLIL::Wire*> wires;
+
+ for (int i = 0; i < 4; i++) {
+ RTLIL::Wire *w = module->addWire(stringf("\\i%d", i));
+ w->port_input = true;
+ wires.push_back(w);
+ in_sig.append(w);
+ }
+
+ for (int i = 0; i < 4; i++) {
+ RTLIL::Wire *w = module->addWire(stringf("\\o%d", i));
+ w->port_output = true;
+ wires.push_back(w);
+ out_sig.append(w);
+ }
+
+ for (int i = 0; i < 16; i++) {
+ RTLIL::Wire *w = module->addWire(stringf("\\t%d", i));
+ wires.push_back(w);
+ }
+
+ for (auto w : wires)
+ if (!w->port_input)
+ switch (xorshift32(12))
+ {
+ case 0:
+ module->addNotGate(w->name.str() + "g", getw(wires, w), w);
+ break;
+ case 1:
+ module->addAndGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
+ break;
+ case 2:
+ module->addNandGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
+ break;
+ case 3:
+ module->addOrGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
+ break;
+ case 4:
+ module->addNorGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
+ break;
+ case 5:
+ module->addXorGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
+ break;
+ case 6:
+ module->addXnorGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
+ break;
+ case 7:
+ module->addMuxGate(w->name.str() + "g", getw(wires, w), getw(wires, w), getw(wires, w), w);
+ break;
+ case 8:
+ module->addAoi3Gate(w->name.str() + "g", getw(wires, w), getw(wires, w), getw(wires, w), w);
+ break;
+ case 9:
+ module->addOai3Gate(w->name.str() + "g", getw(wires, w), getw(wires, w), getw(wires, w), w);
+ break;
+ case 10:
+ module->addAoi4Gate(w->name.str() + "g", getw(wires, w), getw(wires, w), getw(wires, w), getw(wires, w), w);
+ break;
+ case 11:
+ module->addOai4Gate(w->name.str() + "g", getw(wires, w), getw(wires, w), getw(wires, w), getw(wires, w), w);
+ break;
+ }
+
+ module->fixup_ports();
+ Pass::call(design, "clean");
+
+ ezDefaultSAT ez;
+ SigMap sigmap(module);
+ SatGen satgen(&ez, &sigmap);
+
+ for (auto c : module->cells()) {
+ bool ok = satgen.importCell(c);
+ log_assert(ok);
+ }
+
+ std::vector<int> in_vec = satgen.importSigSpec(in_sig);
+ std::vector<int> inverse_in_vec = ez.vec_not(in_vec);
+
+ std::vector<int> out_vec = satgen.importSigSpec(out_sig);
+
+ for (int i = 0; i < 16; i++)
+ {
+ std::vector<int> assumptions;
+ for (int j = 0; j < SIZE(in_vec); j++)
+ assumptions.push_back((i & (1 << j)) ? in_vec.at(j) : inverse_in_vec.at(j));
+
+ std::vector<bool> results;
+ if (!ez.solve(out_vec, results, assumptions)) {
+ log("No stable solution for input %d found -> recreate module.\n", i);
+ goto recreate_module;
+ }
+
+ for (int j = 0; j < 4; j++)
+ truthtab[i][j] = results[j];
+
+ assumptions.push_back(ez.vec_ne(out_vec, ez.vec_const(results)));
+
+ std::vector<bool> results2;
+ if (ez.solve(out_vec, results2, assumptions)) {
+ log("Two stable solutions for input %d found -> recreate module.\n", i);
+ goto recreate_module;
+ }
+ }
+ break;
+
+ recreate_module:
+ design->remove(module);
+ }
+
+ log("Found viable UUT after %d cycles:\n", create_cycles);
+ Pass::call(design, "write_ilang");
+ Pass::call(design, "abc");
+
+ log("\n");
+ log("Pre- and post-abc truth table:\n");
+
+ ezDefaultSAT ez;
+ SigMap sigmap(module);
+ SatGen satgen(&ez, &sigmap);
+
+ for (auto c : module->cells()) {
+ bool ok = satgen.importCell(c);
+ log_assert(ok);
+ }
+
+ std::vector<int> in_vec = satgen.importSigSpec(in_sig);
+ std::vector<int> inverse_in_vec = ez.vec_not(in_vec);
+
+ std::vector<int> out_vec = satgen.importSigSpec(out_sig);
+
+ bool found_error = false;
+ bool truthtab2[16][4];
+
+ for (int i = 0; i < 16; i++)
+ {
+ std::vector<int> assumptions;
+ for (int j = 0; j < SIZE(in_vec); j++)
+ assumptions.push_back((i & (1 << j)) ? in_vec.at(j) : inverse_in_vec.at(j));
+
+ for (int j = 0; j < 4; j++)
+ truthtab2[i][j] = truthtab[i][j];
+
+ std::vector<bool> results;
+ if (!ez.solve(out_vec, results, assumptions)) {
+ log("No stable solution for input %d found.\n", i);
+ found_error = true;
+ continue;
+ }
+
+ for (int j = 0; j < 4; j++)
+ truthtab2[i][j] = results[j];
+
+ assumptions.push_back(ez.vec_ne(out_vec, ez.vec_const(results)));
+
+ std::vector<bool> results2;
+ if (ez.solve(out_vec, results2, assumptions)) {
+ log("Two stable solutions for input %d found -> recreate module.\n", i);
+ found_error = true;
+ }
+ }
+
+ for (int i = 0; i < 16; i++) {
+ log("%3d ", i);
+ for (int j = 0; j < 4; j++)
+ log("%c", truthtab[i][j] ? '1' : '0');
+ log(" ");
+ for (int j = 0; j < 4; j++)
+ log("%c", truthtab2[i][j] ? '1' : '0');
+ for (int j = 0; j < 4; j++)
+ if (truthtab[i][j] != truthtab2[i][j]) {
+ found_error = true;
+ log(" !");
+ break;
+ }
+ log("\n");
+ }
+
+ log_assert(found_error == false);
+ log("\n");
+}
+
+struct TestAbcloopPass : public Pass {
+ TestAbcloopPass() : Pass("test_abcloop", "automatically test handling of loops in abc command") { }
+ virtual void help()
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" test_abcloop [options]\n");
+ log("\n");
+ log("Test handling of logic loops in ABC.\n");
+ log("\n");
+ log(" -n {integer}\n");
+ log(" create this number of circuits and test them (default = 100).\n");
+ log("\n");
+ log(" -s {positive_integer}\n");
+ log(" use this value as rng seed value (default = unix time).\n");
+ log("\n");
+ }
+ virtual void execute(std::vector<std::string> args, RTLIL::Design*)
+ {
+ int num_iter = 100;
+ xorshift32_state = 0;
+
+ int argidx;
+ for (argidx = 1; argidx < SIZE(args); argidx++)
+ {
+ if (args[argidx] == "-n" && argidx+1 < SIZE(args)) {
+ num_iter = atoi(args[++argidx].c_str());
+ continue;
+ }
+ if (args[argidx] == "-s" && argidx+1 < SIZE(args)) {
+ xorshift32_state = atoi(args[++argidx].c_str());
+ continue;
+ }
+ break;
+ }
+
+ if (xorshift32_state == 0)
+ xorshift32_state = time(NULL) & 0x7fffffff;
+
+ for (int i = 0; i < num_iter; i++)
+ test_abcloop();
+ }
+} TestAbcloopPass;
+
projects / yosys.git / commitdiff