return xorshift32_state % limit;
}
-static void create_gold_module(RTLIL::Design *design, RTLIL::IdString cell_type, std::string cell_type_flags)
+static void create_gold_module(RTLIL::Design *design, RTLIL::IdString cell_type, std::string cell_type_flags, bool constmode)
{
RTLIL::Module *module = design->addModule("\\gold");
RTLIL::Cell *cell = module->addCell("\\UUT", cell_type);
RTLIL::Wire *wire;
+ if (cell_type == "$fa")
+ {
+ int width = 1 + xorshift32(8);
+
+ wire = module->addWire("\\A");
+ wire->width = width;
+ wire->port_input = true;
+ cell->setPort("\\A", wire);
+
+ wire = module->addWire("\\B");
+ wire->width = width;
+ wire->port_input = true;
+ cell->setPort("\\B", wire);
+
+ wire = module->addWire("\\C");
+ wire->width = width;
+ wire->port_input = true;
+ cell->setPort("\\C", wire);
+
+ wire = module->addWire("\\X");
+ wire->width = width;
+ wire->port_output = true;
+ cell->setPort("\\X", wire);
+
+ wire = module->addWire("\\Y");
+ wire->width = width;
+ wire->port_output = true;
+ cell->setPort("\\Y", wire);
+ }
+
+ if (cell_type == "$lcu")
+ {
+ int width = 1 + xorshift32(8);
+
+ wire = module->addWire("\\P");
+ wire->width = width;
+ wire->port_input = true;
+ cell->setPort("\\P", wire);
+
+ wire = module->addWire("\\G");
+ wire->width = width;
+ wire->port_input = true;
+ cell->setPort("\\G", wire);
+
+ wire = module->addWire("\\CI");
+ wire->port_input = true;
+ cell->setPort("\\CI", wire);
+
+ wire = module->addWire("\\CO");
+ wire->width = width;
+ wire->port_output = true;
+ cell->setPort("\\CO", wire);
+ }
+
if (cell_type == "$macc")
{
Macc macc;
for (int i = 0; i < depth; i++)
{
int size_a = xorshift32(width) + 1;
- int size_b = xorshift32(width) + 1;
+ int size_b = depth > 4 ? 0 : xorshift32(width) + 1;
if (mulbits_a + size_a*size_b <= 96 && mulbits_b + size_a + size_b <= 16 && xorshift32(2) == 1) {
mulbits_a += size_a * size_b;
}
wire = module->addWire("\\B");
- wire->width = xorshift32(xorshift32(16)+1);
+ wire->width = xorshift32(mulbits_a ? xorshift32(4)+1 : xorshift32(16)+1);
wire->port_input = true;
macc.bit_ports = wire;
cell->setPort("\\CO", wire);
}
+ if (constmode)
+ {
+ auto conn_list = cell->connections();
+ for (auto &conn : conn_list)
+ {
+ RTLIL::SigSpec sig = conn.second;
+
+ if (SIZE(sig) == 0 || sig[0].wire == nullptr || sig[0].wire->port_output)
+ continue;
+
+ int n, m;
+ switch (xorshift32(5))
+ {
+ case 0:
+ n = xorshift32(SIZE(sig) + 1);
+ for (int i = 0; i < n; i++)
+ sig[i] = xorshift32(2) == 1 ? RTLIL::S1 : RTLIL::S0;
+ break;
+ case 1:
+ n = xorshift32(SIZE(sig) + 1);
+ for (int i = n; i < SIZE(sig); i++)
+ sig[i] = xorshift32(2) == 1 ? RTLIL::S1 : RTLIL::S0;
+ break;
+ case 2:
+ n = xorshift32(SIZE(sig));
+ m = xorshift32(SIZE(sig));
+ for (int i = std::min(n, m); i < std::max(n, m); i++)
+ sig[i] = xorshift32(2) == 1 ? RTLIL::S1 : RTLIL::S0;
+ break;
+ }
+
+ cell->setPort(conn.first, sig);
+ }
+ }
+
module->fixup_ports();
cell->fixup_parameters();
cell->check();
}
-static void run_eval_test(RTLIL::Design *design, bool verbose, std::string uut_name, std::ofstream &vlog_file)
+static void run_eval_test(RTLIL::Design *design, bool verbose, bool nosat, std::string uut_name, std::ofstream &vlog_file)
{
log("Eval testing:%c", verbose ? '\n' : ' ');
SatGen satgen2(&ez2, &sigmap);
satgen2.model_undef = true;
- for (auto cell : gold_mod->cells()) {
- satgen1.importCell(cell);
- satgen2.importCell(cell);
- }
+ if (!nosat)
+ for (auto cell : gold_mod->cells()) {
+ satgen1.importCell(cell);
+ satgen2.importCell(cell);
+ }
if (vlog_file.is_open())
{
gold_ce.set(gold_wire, in_value);
gate_ce.set(gate_wire, in_value);
- if (vlog_file.is_open()) {
+ if (vlog_file.is_open() && SIZE(in_value) > 0) {
vlog_file << stringf(" %s = 'b%s;\n", log_id(gold_wire), in_value.as_string().c_str());
if (!vlog_pattern_info.empty())
vlog_pattern_info += " ";
if (verbose)
log("EVAL: %s\n", out_val.as_string().c_str());
- std::vector<int> sat1_in_sig = satgen1.importSigSpec(in_sig);
- std::vector<int> sat1_in_val = satgen1.importSigSpec(in_val);
+ if (!nosat)
+ {
+ std::vector<int> sat1_in_sig = satgen1.importSigSpec(in_sig);
+ std::vector<int> sat1_in_val = satgen1.importSigSpec(in_val);
- std::vector<int> sat1_model = satgen1.importSigSpec(out_sig);
- std::vector<bool> sat1_model_value;
+ std::vector<int> sat1_model = satgen1.importSigSpec(out_sig);
+ std::vector<bool> sat1_model_value;
- if (!ez1.solve(sat1_model, sat1_model_value, ez1.vec_eq(sat1_in_sig, sat1_in_val)))
- log_error("Evaluating sat model 1 (no undef modeling) failed!\n");
+ if (!ez1.solve(sat1_model, sat1_model_value, ez1.vec_eq(sat1_in_sig, sat1_in_val)))
+ log_error("Evaluating sat model 1 (no undef modeling) failed!\n");
- if (verbose) {
- log("SAT 1: ");
- for (int i = SIZE(out_sig)-1; i >= 0; i--)
- log("%c", sat1_model_value.at(i) ? '1' : '0');
- log("\n");
- }
+ if (verbose) {
+ log("SAT 1: ");
+ for (int i = SIZE(out_sig)-1; i >= 0; i--)
+ log("%c", sat1_model_value.at(i) ? '1' : '0');
+ log("\n");
+ }
- for (int i = 0; i < SIZE(out_sig); i++) {
- if (out_val[i] != RTLIL::S0 && out_val[i] != RTLIL::S1)
- continue;
- if (out_val[i] == RTLIL::S0 && sat1_model_value.at(i) == false)
- continue;
- if (out_val[i] == RTLIL::S1 && sat1_model_value.at(i) == true)
- continue;
- log_error("Mismatch in sat model 1 (no undef modeling) output!\n");
- }
+ for (int i = 0; i < SIZE(out_sig); i++) {
+ if (out_val[i] != RTLIL::S0 && out_val[i] != RTLIL::S1)
+ continue;
+ if (out_val[i] == RTLIL::S0 && sat1_model_value.at(i) == false)
+ continue;
+ if (out_val[i] == RTLIL::S1 && sat1_model_value.at(i) == true)
+ continue;
+ log_error("Mismatch in sat model 1 (no undef modeling) output!\n");
+ }
- std::vector<int> sat2_in_def_sig = satgen2.importDefSigSpec(in_sig);
- std::vector<int> sat2_in_def_val = satgen2.importDefSigSpec(in_val);
+ std::vector<int> sat2_in_def_sig = satgen2.importDefSigSpec(in_sig);
+ std::vector<int> sat2_in_def_val = satgen2.importDefSigSpec(in_val);
- std::vector<int> sat2_in_undef_sig = satgen2.importUndefSigSpec(in_sig);
- std::vector<int> sat2_in_undef_val = satgen2.importUndefSigSpec(in_val);
+ std::vector<int> sat2_in_undef_sig = satgen2.importUndefSigSpec(in_sig);
+ std::vector<int> sat2_in_undef_val = satgen2.importUndefSigSpec(in_val);
- std::vector<int> sat2_model_def_sig = satgen2.importDefSigSpec(out_sig);
- std::vector<int> sat2_model_undef_sig = satgen2.importUndefSigSpec(out_sig);
+ std::vector<int> sat2_model_def_sig = satgen2.importDefSigSpec(out_sig);
+ std::vector<int> sat2_model_undef_sig = satgen2.importUndefSigSpec(out_sig);
- std::vector<int> sat2_model;
- sat2_model.insert(sat2_model.end(), sat2_model_def_sig.begin(), sat2_model_def_sig.end());
- sat2_model.insert(sat2_model.end(), sat2_model_undef_sig.begin(), sat2_model_undef_sig.end());
+ std::vector<int> sat2_model;
+ sat2_model.insert(sat2_model.end(), sat2_model_def_sig.begin(), sat2_model_def_sig.end());
+ sat2_model.insert(sat2_model.end(), sat2_model_undef_sig.begin(), sat2_model_undef_sig.end());
- std::vector<bool> sat2_model_value;
+ std::vector<bool> sat2_model_value;
- if (!ez2.solve(sat2_model, sat2_model_value, ez2.vec_eq(sat2_in_def_sig, sat2_in_def_val), ez2.vec_eq(sat2_in_undef_sig, sat2_in_undef_val)))
- log_error("Evaluating sat model 2 (undef modeling) failed!\n");
+ if (!ez2.solve(sat2_model, sat2_model_value, ez2.vec_eq(sat2_in_def_sig, sat2_in_def_val), ez2.vec_eq(sat2_in_undef_sig, sat2_in_undef_val)))
+ log_error("Evaluating sat model 2 (undef modeling) failed!\n");
- if (verbose) {
- log("SAT 2: ");
- for (int i = SIZE(out_sig)-1; i >= 0; i--)
- log("%c", sat2_model_value.at(SIZE(out_sig) + i) ? 'x' : sat2_model_value.at(i) ? '1' : '0');
- log("\n");
- }
+ if (verbose) {
+ log("SAT 2: ");
+ for (int i = SIZE(out_sig)-1; i >= 0; i--)
+ log("%c", sat2_model_value.at(SIZE(out_sig) + i) ? 'x' : sat2_model_value.at(i) ? '1' : '0');
+ log("\n");
+ }
- for (int i = 0; i < SIZE(out_sig); i++) {
- if (sat2_model_value.at(SIZE(out_sig) + i)) {
- if (out_val[i] != RTLIL::S0 && out_val[i] != RTLIL::S1)
- continue;
- } else {
- if (out_val[i] == RTLIL::S0 && sat2_model_value.at(i) == false)
- continue;
- if (out_val[i] == RTLIL::S1 && sat2_model_value.at(i) == true)
- continue;
+ for (int i = 0; i < SIZE(out_sig); i++) {
+ if (sat2_model_value.at(SIZE(out_sig) + i)) {
+ if (out_val[i] != RTLIL::S0 && out_val[i] != RTLIL::S1)
+ continue;
+ } else {
+ if (out_val[i] == RTLIL::S0 && sat2_model_value.at(i) == false)
+ continue;
+ if (out_val[i] == RTLIL::S1 && sat2_model_value.at(i) == true)
+ continue;
+ }
+ log_error("Mismatch in sat model 2 (undef modeling) output!\n");
}
- log_error("Mismatch in sat model 2 (undef modeling) output!\n");
}
}
log("\n");
log(" test_cell [options] {cell-types}\n");
log("\n");
- log("Tests the internal implementation of the given cell type (for example '$mux')\n");
+ log("Tests the internal implementation of the given cell type (for example '$add')\n");
log("by comparing SAT solver, EVAL and TECHMAP implementations of the cell types..\n");
log("\n");
log("Run with 'all' instead of a cell type to run the test on all supported\n");
log(" -script {script_file}\n");
log(" instead of calling \"techmap\", call \"script {script_file}\".\n");
log("\n");
+ log(" -const\n");
+ log(" set some input bits to random constant values\n");
+ log("\n");
+ log(" -nosat\n");
+ log(" do not check SAT model or run SAT equivalence checking\n");
+ log("\n");
log(" -v\n");
log(" print additional debug information to the console\n");
log("\n");
xorshift32_state = 0;
std::ofstream vlog_file;
bool verbose = false;
+ bool constmode = false;
+ bool nosat = false;
int argidx;
for (argidx = 1; argidx < SIZE(args); argidx++)
techmap_cmd = "techmap -map +/simlib.v -max_iter 2 -autoproc";
continue;
}
+ if (args[argidx] == "-const") {
+ constmode = true;
+ continue;
+ }
+ if (args[argidx] == "-nosat") {
+ nosat = true;
+ continue;
+ }
if (args[argidx] == "-v") {
verbose = true;
continue;
cell_types["$lut"] = "*";
cell_types["$alu"] = "ABSY";
+ cell_types["$lcu"] = "*";
cell_types["$macc"] = "*";
+ cell_types["$fa"] = "*";
for (; argidx < SIZE(args); argidx++)
{
if (cell_type == "ilang")
Frontend::frontend_call(design, NULL, std::string(), "ilang " + ilang_file);
else
- create_gold_module(design, cell_type, cell_types.at(cell_type));
+ create_gold_module(design, cell_type, cell_types.at(cell_type), constmode);
Pass::call(design, stringf("copy gold gate; cd gate; %s; cd ..; opt -fast gate", techmap_cmd.c_str()));
- Pass::call(design, "miter -equiv -flatten -make_outputs -ignore_gold_x gold gate miter");
+ if (!nosat)
+ Pass::call(design, "miter -equiv -flatten -make_outputs -ignore_gold_x gold gate miter");
if (verbose)
Pass::call(design, "dump gate");
Pass::call(design, "dump gold");
- Pass::call(design, "sat -verify -enable_undef -prove trigger 0 -show-inputs -show-outputs miter");
+ if (!nosat)
+ Pass::call(design, "sat -verify -enable_undef -prove trigger 0 -show-inputs -show-outputs miter");
std::string uut_name = stringf("uut_%s_%d", cell_type.substr(1).c_str(), i);
if (vlog_file.is_open()) {
Pass::call(design, stringf("copy gold %s_expr; select %s_expr", uut_name.c_str(), uut_name.c_str()));
Backend::backend_call(design, &vlog_file, "<test_cell -vlog>", "verilog -selected -noexpr");
uut_names.push_back(uut_name);
}
- run_eval_test(design, verbose, uut_name, vlog_file);
+ run_eval_test(design, verbose, nosat, uut_name, vlog_file);
delete design;
}
projects / yosys.git / blobdiff