mirror of https://github.com/YosysHQ/yosys.git
Added "test_abcloop" command
This commit is contained in:
Clifford Wolf
parent
00964f2f61
commit
a7758ef953
|
|
@ -1,4 +1,5 @@
|
||||||
|
|
||||||
OBJS += passes/tests/test_autotb.o
|
OBJS += passes/tests/test_autotb.o
|
||||||
OBJS += passes/tests/test_cell.o
|
OBJS += passes/tests/test_cell.o
|
||||||
|
OBJS += passes/tests/test_abcloop.o
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,285 @@
|
||||||
|
/*
|
||||||
|
* 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;
|
||||||
|
|
||||||
Loading…
Reference in New Issue