/*
 *  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"
#include "kernel/consteval.h"
#include "kernel/celledges.h"
#include "kernel/macc.h"
#include <algorithm>

USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN

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 void create_gold_module(RTLIL::Design *design, RTLIL::IdString cell_type, std::string cell_type_flags, bool constmode, bool muxdiv)
{
	RTLIL::Module *module = design->addModule("\\gold");
	RTLIL::Cell *cell = module->addCell("\\UUT", cell_type);
	RTLIL::Wire *wire;

	if (cell_type.in("$mux", "$pmux"))
	{
		int width = 1 + xorshift32(8);
		int swidth = cell_type == "$mux" ? 1 : 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 * swidth;
		wire->port_input = true;
		cell->setPort("\\B", wire);

		wire = module->addWire("\\S");
		wire->width = swidth;
		wire->port_input = true;
		cell->setPort("\\S", wire);

		wire = module->addWire("\\Y");
		wire->width = width;
		wire->port_output = true;
		cell->setPort("\\Y", 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;
		int width = 1 + xorshift32(8);
		int depth = 1 + xorshift32(6);
		int mulbits_a = 0, mulbits_b = 0;

		RTLIL::Wire *wire_a = module->addWire("\\A");
		wire_a->width = 0;
		wire_a->port_input = true;

		for (int i = 0; i < depth; i++)
		{
			int size_a = 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;
				mulbits_b += size_a + size_b;
			} else
				size_b = 0;

			Macc::port_t this_port;

			wire_a->width += size_a;
			this_port.in_a = RTLIL::SigSpec(wire_a, wire_a->width - size_a, size_a);

			wire_a->width += size_b;
			this_port.in_b = RTLIL::SigSpec(wire_a, wire_a->width - size_b, size_b);

			this_port.is_signed = xorshift32(2) == 1;
			this_port.do_subtract = xorshift32(2) == 1;
			macc.ports.push_back(this_port);
		}

		wire = module->addWire("\\B");
		wire->width = xorshift32(mulbits_a ? xorshift32(4)+1 : xorshift32(16)+1);
		wire->port_input = true;
		macc.bit_ports = wire;

		wire = module->addWire("\\Y");
		wire->width = width;
		wire->port_output = true;
		cell->setPort("\\Y", wire);

		macc.to_cell(cell);
	}

	if (cell_type == "$lut")
	{
		int width = 1 + xorshift32(6);

		wire = module->addWire("\\A");
		wire->width = width;
		wire->port_input = true;
		cell->setPort("\\A", wire);

		wire = module->addWire("\\Y");
		wire->port_output = true;
		cell->setPort("\\Y", wire);

		RTLIL::SigSpec config;
		for (int i = 0; i < (1 << width); i++)
			config.append(xorshift32(2) ? State::S1 : State::S0);

		cell->setParam("\\LUT", config.as_const());
	}

	if (cell_type == "$sop")
	{
		int width = 1 + xorshift32(8);
		int depth = 1 + xorshift32(8);

		wire = module->addWire("\\A");
		wire->width = width;
		wire->port_input = true;
		cell->setPort("\\A", wire);

		wire = module->addWire("\\Y");
		wire->port_output = true;
		cell->setPort("\\Y", wire);

		RTLIL::SigSpec config;
		for (int i = 0; i < width*depth; i++)
			switch (xorshift32(3)) {
				case 0:
					config.append(State::S1);
					config.append(State::S0);
					break;
				case 1:
					config.append(State::S0);
					config.append(State::S1);
					break;
				case 2:
					config.append(State::S0);
					config.append(State::S0);
					break;
			}

		cell->setParam("\\DEPTH", depth);
		cell->setParam("\\TABLE", config.as_const());
	}

	if (cell_type_flags.find('A') != std::string::npos) {
		wire = module->addWire("\\A");
		wire->width = 1 + xorshift32(8);
		wire->port_input = true;
		cell->setPort("\\A", wire);
	}

	if (cell_type_flags.find('B') != std::string::npos) {
		wire = module->addWire("\\B");
		if (cell_type_flags.find('h') != std::string::npos)
			wire->width = 1 + xorshift32(6);
		else
			wire->width = 1 + xorshift32(8);
		wire->port_input = true;
		cell->setPort("\\B", wire);
	}

	if (cell_type_flags.find('S') != std::string::npos && xorshift32(2)) {
		if (cell_type_flags.find('A') != std::string::npos)
			cell->parameters["\\A_SIGNED"] = true;
		if (cell_type_flags.find('B') != std::string::npos)
			cell->parameters["\\B_SIGNED"] = true;
	}

	if (cell_type_flags.find('s') != std::string::npos) {
		if (cell_type_flags.find('A') != std::string::npos && xorshift32(2))
			cell->parameters["\\A_SIGNED"] = true;
		if (cell_type_flags.find('B') != std::string::npos && xorshift32(2))
			cell->parameters["\\B_SIGNED"] = true;
	}

	if (cell_type_flags.find('Y') != std::string::npos) {
		wire = module->addWire("\\Y");
		wire->width = 1 + xorshift32(8);
		wire->port_output = true;
		cell->setPort("\\Y", wire);
	}

	if (muxdiv && cell_type.in("$div", "$mod")) {
		auto b_not_zero = module->ReduceBool(NEW_ID, cell->getPort("\\B"));
		auto div_out = module->addWire(NEW_ID, GetSize(cell->getPort("\\Y")));
		module->addMux(NEW_ID, RTLIL::SigSpec(0, GetSize(div_out)), div_out, b_not_zero, cell->getPort("\\Y"));
		cell->setPort("\\Y", div_out);
	}

	if (cell_type == "$alu")
	{
		wire = module->addWire("\\CI");
		wire->port_input = true;
		cell->setPort("\\CI", wire);

		wire = module->addWire("\\BI");
		wire->port_input = true;
		cell->setPort("\\BI", wire);

		wire = module->addWire("\\X");
		wire->width = GetSize(cell->getPort("\\Y"));
		wire->port_output = true;
		cell->setPort("\\X", wire);

		wire = module->addWire("\\CO");
		wire->width = GetSize(cell->getPort("\\Y"));
		wire->port_output = true;
		cell->setPort("\\CO", wire);
	}

	if (constmode)
	{
		auto conn_list = cell->connections();
		for (auto &conn : conn_list)
		{
			RTLIL::SigSpec sig = conn.second;

			if (GetSize(sig) == 0 || sig[0].wire == nullptr || sig[0].wire->port_output)
				continue;

			int n, m;
			switch (xorshift32(5))
			{
			case 0:
				n = xorshift32(GetSize(sig) + 1);
				for (int i = 0; i < n; i++)
					sig[i] = xorshift32(2) == 1 ? State::S1 : State::S0;
				break;
			case 1:
				n = xorshift32(GetSize(sig) + 1);
				for (int i = n; i < GetSize(sig); i++)
					sig[i] = xorshift32(2) == 1 ? State::S1 : State::S0;
				break;
			case 2:
				n = xorshift32(GetSize(sig));
				m = xorshift32(GetSize(sig));
				for (int i = min(n, m); i < max(n, m); i++)
					sig[i] = xorshift32(2) == 1 ? State::S1 : State::S0;
				break;
			}

			cell->setPort(conn.first, sig);
		}
	}

	module->fixup_ports();
	cell->fixup_parameters();
	cell->check();
}

static void run_edges_test(RTLIL::Design *design, bool verbose)
{
	Module *module = *design->modules().begin();
	Cell *cell = *module->cells().begin();

	ezSatPtr ezptr;
	ezSAT &ez = *ezptr.get();

	SigMap sigmap(module);
	SatGen satgen(&ez, &sigmap);

	FwdCellEdgesDatabase edges_db(sigmap);
	if (!edges_db.add_edges_from_cell(cell))
		log_error("Creating edge database failed for this cell!\n");

	dict<SigBit, pool<SigBit>> satgen_db;

	satgen.setContext(&sigmap, "X:");
	satgen.importCell(cell);

	satgen.setContext(&sigmap, "Y:");
	satgen.importCell(cell);

	vector<tuple<SigBit, int, int>> input_db, output_db;

	for (auto &conn : cell->connections())
	{
		SigSpec bits = sigmap(conn.second);

		satgen.setContext(&sigmap, "X:");
		std::vector<int> xbits = satgen.importSigSpec(bits);

		satgen.setContext(&sigmap, "Y:");
		std::vector<int> ybits = satgen.importSigSpec(bits);

		for (int i = 0; i < GetSize(bits); i++)
			if (cell->input(conn.first))
				input_db.emplace_back(bits[i], xbits[i], ybits[i]);
			else
				output_db.emplace_back(bits[i], xbits[i], ybits[i]);
	}

	if (verbose)
		log("\nSAT solving for all edges:\n");

	for (int i = 0; i < GetSize(input_db); i++)
	{
		SigBit inbit = std::get<0>(input_db[i]);

		if (verbose)
			log("  Testing input signal %s:\n", log_signal(inbit));

		vector<int> xinbits, yinbits;
		for (int k = 0; k < GetSize(input_db); k++)
			if (k != i) {
				xinbits.push_back(std::get<1>(input_db[k]));
				yinbits.push_back(std::get<2>(input_db[k]));
			}

		int xyinbit_ok = ez.vec_eq(xinbits, yinbits);

		for (int k = 0; k < GetSize(output_db); k++)
		{
			SigBit outbit = std::get<0>(output_db[k]);
			int xoutbit = std::get<1>(output_db[k]);
			int youtbit = std::get<2>(output_db[k]);

			bool is_edge = ez.solve(xyinbit_ok, ez.XOR(xoutbit, youtbit));

			if (is_edge)
				satgen_db[inbit].insert(outbit);

			if (verbose) {
				bool is_ref_edge = edges_db.db.count(inbit) && edges_db.db.at(inbit).count(outbit);
				log("    %c %s %s\n", is_edge ? 'x' : 'o', log_signal(outbit), is_edge == is_ref_edge ? "OK" : "ERROR");
			}
		}
	}

	if (satgen_db == edges_db.db)
		log("PASS.\n");
	else
		log_error("SAT-based edge table does not match the database!\n");
}

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' : ' ');

	RTLIL::Module *gold_mod = design->module("\\gold");
	RTLIL::Module *gate_mod = design->module("\\gate");
	ConstEval gold_ce(gold_mod), gate_ce(gate_mod);

	ezSatPtr ez1, ez2;
	SigMap sigmap(gold_mod);
	SatGen satgen1(ez1.get(), &sigmap);
	SatGen satgen2(ez2.get(), &sigmap);
	satgen2.model_undef = true;

	if (!nosat)
		for (auto cell : gold_mod->cells()) {
			satgen1.importCell(cell);
			satgen2.importCell(cell);
		}

	if (vlog_file.is_open())
	{
		vlog_file << stringf("\nmodule %s;\n", uut_name.c_str());

		for (auto port : gold_mod->ports) {
			RTLIL::Wire *wire = gold_mod->wire(port);
			if (wire->port_input)
				vlog_file << stringf("  reg [%d:0] %s;\n", GetSize(wire)-1, log_id(wire));
			else
				vlog_file << stringf("  wire [%d:0] %s_expr, %s_noexpr;\n", GetSize(wire)-1, log_id(wire), log_id(wire));
		}

		vlog_file << stringf("  %s_expr uut_expr(", uut_name.c_str());
		for (int i = 0; i < GetSize(gold_mod->ports); i++)
			vlog_file << stringf("%s.%s(%s%s)", i ? ", " : "", log_id(gold_mod->ports[i]), log_id(gold_mod->ports[i]),
					gold_mod->wire(gold_mod->ports[i])->port_input ? "" : "_expr");
		vlog_file << stringf(");\n");

		vlog_file << stringf("  %s_expr uut_noexpr(", uut_name.c_str());
		for (int i = 0; i < GetSize(gold_mod->ports); i++)
			vlog_file << stringf("%s.%s(%s%s)", i ? ", " : "", log_id(gold_mod->ports[i]), log_id(gold_mod->ports[i]),
					gold_mod->wire(gold_mod->ports[i])->port_input ? "" : "_noexpr");
		vlog_file << stringf(");\n");

		vlog_file << stringf("  task run;\n");
		vlog_file << stringf("    begin\n");
		vlog_file << stringf("      $display(\"%s\");\n", uut_name.c_str());
	}

	for (int i = 0; i < 64; i++)
	{
		log(verbose ? "\n" : ".");
		gold_ce.clear();
		gate_ce.clear();

		RTLIL::SigSpec in_sig, in_val;
		RTLIL::SigSpec out_sig, out_val;
		std::string vlog_pattern_info;

		for (auto port : gold_mod->ports)
		{
			RTLIL::Wire *gold_wire = gold_mod->wire(port);
			RTLIL::Wire *gate_wire = gate_mod->wire(port);

			log_assert(gold_wire != nullptr);
			log_assert(gate_wire != nullptr);
			log_assert(gold_wire->port_input == gate_wire->port_input);
			log_assert(GetSize(gold_wire) == GetSize(gate_wire));

			if (!gold_wire->port_input)
				continue;

			RTLIL::Const in_value;
			for (int i = 0; i < GetSize(gold_wire); i++)
				in_value.bits.push_back(xorshift32(2) ? State::S1 : State::S0);

			if (xorshift32(4) == 0) {
				int inv_chance = 1 + xorshift32(8);
				for (int i = 0; i < GetSize(gold_wire); i++)
					if (xorshift32(inv_chance) == 0)
						in_value.bits[i] = RTLIL::Sx;
			}

			if (verbose)
				log("%s: %s\n", log_id(gold_wire), log_signal(in_value));

			in_sig.append(gold_wire);
			in_val.append(in_value);

			gold_ce.set(gold_wire, in_value);
			gate_ce.set(gate_wire, in_value);

			if (vlog_file.is_open() && GetSize(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 += " ";
				vlog_pattern_info += stringf("%s=%s", log_id(gold_wire), log_signal(in_value));
			}
		}

		if (vlog_file.is_open())
			vlog_file << stringf("      #1;\n");

		for (auto port : gold_mod->ports)
		{
			RTLIL::Wire *gold_wire = gold_mod->wire(port);
			RTLIL::Wire *gate_wire = gate_mod->wire(port);

			log_assert(gold_wire != nullptr);
			log_assert(gate_wire != nullptr);
			log_assert(gold_wire->port_output == gate_wire->port_output);
			log_assert(GetSize(gold_wire) == GetSize(gate_wire));

			if (!gold_wire->port_output)
				continue;

			RTLIL::SigSpec gold_outval(gold_wire);
			RTLIL::SigSpec gate_outval(gate_wire);

			if (!gold_ce.eval(gold_outval))
				log_error("Failed to eval %s in gold module.\n", log_id(gold_wire));

			if (!gate_ce.eval(gate_outval))
				log_error("Failed to eval %s in gate module.\n", log_id(gate_wire));

			bool gold_gate_mismatch = false;
			for (int i = 0; i < GetSize(gold_wire); i++) {
				if (gold_outval[i] == RTLIL::Sx)
					continue;
				if (gold_outval[i] == gate_outval[i])
					continue;
				gold_gate_mismatch = true;
				break;
			}

			if (gold_gate_mismatch)
				log_error("Mismatch in output %s: gold:%s != gate:%s\n", log_id(gate_wire), log_signal(gold_outval), log_signal(gate_outval));

			if (verbose)
				log("%s: %s\n", log_id(gold_wire), log_signal(gold_outval));

			out_sig.append(gold_wire);
			out_val.append(gold_outval);

			if (vlog_file.is_open()) {
				vlog_file << stringf("      $display(\"[%s] %s expected: %%b, expr: %%b, noexpr: %%b\", %d'b%s, %s_expr, %s_noexpr);\n",
						vlog_pattern_info.c_str(), log_id(gold_wire), GetSize(gold_outval), gold_outval.as_string().c_str(), log_id(gold_wire), log_id(gold_wire));
				vlog_file << stringf("      if (%s_expr !== %d'b%s) begin $display(\"ERROR\"); $finish; end\n", log_id(gold_wire), GetSize(gold_outval), gold_outval.as_string().c_str());
				vlog_file << stringf("      if (%s_noexpr !== %d'b%s) begin $display(\"ERROR\"); $finish; end\n", log_id(gold_wire), GetSize(gold_outval), gold_outval.as_string().c_str());
			}
		}

		if (verbose)
			log("EVAL:  %s\n", out_val.as_string().c_str());

		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;

			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 = GetSize(out_sig)-1; i >= 0; i--)
					log("%c", sat1_model_value.at(i) ? '1' : '0');
				log("\n");
			}

			for (int i = 0; i < GetSize(out_sig); i++) {
				if (out_val[i] != State::S0 && out_val[i] != State::S1)
					continue;
				if (out_val[i] == State::S0 && sat1_model_value.at(i) == false)
					continue;
				if (out_val[i] == State::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_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;
			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;

			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 = GetSize(out_sig)-1; i >= 0; i--)
					log("%c", sat2_model_value.at(GetSize(out_sig) + i) ? 'x' : sat2_model_value.at(i) ? '1' : '0');
				log("\n");
			}

			for (int i = 0; i < GetSize(out_sig); i++) {
				if (sat2_model_value.at(GetSize(out_sig) + i)) {
					if (out_val[i] != State::S0 && out_val[i] != State::S1)
						continue;
				} else {
					if (out_val[i] == State::S0 && sat2_model_value.at(i) == false)
						continue;
					if (out_val[i] == State::S1 && sat2_model_value.at(i) == true)
						continue;
				}
				log_error("Mismatch in sat model 2 (undef modeling) output!\n");
			}
		}
	}

	if (vlog_file.is_open()) {
		vlog_file << stringf("    end\n");
		vlog_file << stringf("  endtask\n");
		vlog_file << stringf("endmodule\n");
	}

	if (!verbose)
		log(" ok.\n");
}

struct TestCellPass : public Pass {
	TestCellPass() : Pass("test_cell", "automatically test the implementation of a cell type") { }
	void help() YS_OVERRIDE
	{
		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
		log("\n");
		log("    test_cell [options] {cell-types}\n");
		log("\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("cell types. Use for example 'all /$add' for all cell types except $add.\n");
		log("\n");
		log("    -n {integer}\n");
		log("        create this number of cell instances 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");
		log("    -f {ilang_file}\n");
		log("        don't generate circuits. instead load the specified ilang file.\n");
		log("\n");
		log("    -w {filename_prefix}\n");
		log("        don't test anything. just generate the circuits and write them\n");
		log("        to ilang files with the specified prefix\n");
		log("\n");
		log("    -map {filename}\n");
		log("        pass this option to techmap.\n");
		log("\n");
		log("    -simlib\n");
		log("        use \"techmap -D SIMLIB_NOCHECKS -map +/simlib.v -max_iter 2 -autoproc\"\n");
		log("\n");
		log("    -aigmap\n");
		log("        instead of calling \"techmap\", call \"aigmap\"\n");
		log("\n");
		log("    -muxdiv\n");
		log("        when creating test benches with dividers, create an additional mux\n");
		log("        to mask out the division-by-zero case\n");
		log("\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("    -noeval\n");
		log("        do not check const-eval models\n");
		log("\n");
		log("    -edges\n");
		log("        test cell edges db creator against sat-based implementation\n");
		log("\n");
		log("    -v\n");
		log("        print additional debug information to the console\n");
		log("\n");
		log("    -vlog {filename}\n");
		log("        create a Verilog test bench to test simlib and write_verilog\n");
		log("\n");
	}
	void execute(std::vector<std::string> args, RTLIL::Design*) YS_OVERRIDE
	{
		int num_iter = 100;
		std::string techmap_cmd = "techmap -assert";
		std::string ilang_file, write_prefix;
		xorshift32_state = 0;
		std::ofstream vlog_file;
		bool muxdiv = false;
		bool verbose = false;
		bool constmode = false;
		bool nosat = false;
		bool noeval = false;
		bool edges = false;

		int argidx;
		for (argidx = 1; argidx < GetSize(args); argidx++)
		{
			if (args[argidx] == "-n" && argidx+1 < GetSize(args)) {
				num_iter = atoi(args[++argidx].c_str());
				continue;
			}
			if (args[argidx] == "-s" && argidx+1 < GetSize(args)) {
				xorshift32_state = atoi(args[++argidx].c_str());
				continue;
			}
			if (args[argidx] == "-map" && argidx+1 < GetSize(args)) {
				techmap_cmd += " -map " + args[++argidx];
				continue;
			}
			if (args[argidx] == "-f" && argidx+1 < GetSize(args)) {
				ilang_file = args[++argidx];
				num_iter = 1;
				continue;
			}
			if (args[argidx] == "-w" && argidx+1 < GetSize(args)) {
				write_prefix = args[++argidx];
				continue;
			}
			if (args[argidx] == "-script" && argidx+1 < GetSize(args)) {
				techmap_cmd = "script " + args[++argidx];
				continue;
			}
			if (args[argidx] == "-simlib") {
				techmap_cmd = "techmap -D SIMLIB_NOCHECKS -map +/simlib.v -max_iter 2 -autoproc";
				continue;
			}
			if (args[argidx] == "-aigmap") {
				techmap_cmd = "aigmap";
				continue;
			}
			if (args[argidx] == "-muxdiv") {
				muxdiv = true;
				continue;
			}
			if (args[argidx] == "-const") {
				constmode = true;
				continue;
			}
			if (args[argidx] == "-nosat") {
				nosat = true;
				continue;
			}
			if (args[argidx] == "-noeval") {
				noeval = true;
				continue;
			}
			if (args[argidx] == "-edges") {
				edges = true;
				continue;
			}
			if (args[argidx] == "-v") {
				verbose = true;
				continue;
			}
			if (args[argidx] == "-vlog" && argidx+1 < GetSize(args)) {
				vlog_file.open(args[++argidx], std::ios_base::trunc);
				if (!vlog_file.is_open())
					log_cmd_error("Failed to open output file `%s'.\n", args[argidx].c_str());
				continue;
			}
			break;
		}

		if (xorshift32_state == 0) {
			xorshift32_state = time(NULL) & 0x7fffffff;
			log("Rng seed value: %d\n", int(xorshift32_state));
		}

		std::map<std::string, std::string> cell_types;
		std::vector<std::string> selected_cell_types;

		cell_types["$not"] = "ASY";
		cell_types["$pos"] = "ASY";
		cell_types["$neg"] = "ASY";

		cell_types["$and"]  = "ABSY";
		cell_types["$or"]   = "ABSY";
		cell_types["$xor"]  = "ABSY";
		cell_types["$xnor"] = "ABSY";

		cell_types["$reduce_and"]  = "ASY";
		cell_types["$reduce_or"]   = "ASY";
		cell_types["$reduce_xor"]  = "ASY";
		cell_types["$reduce_xnor"] = "ASY";
		cell_types["$reduce_bool"] = "ASY";

		cell_types["$shl"]    = "ABshY";
		cell_types["$shr"]    = "ABshY";
		cell_types["$sshl"]   = "ABshY";
		cell_types["$sshr"]   = "ABshY";
		cell_types["$shift"]  = "ABshY";
		cell_types["$shiftx"] = "ABshY";

		cell_types["$lt"]  = "ABSY";
		cell_types["$le"]  = "ABSY";
		cell_types["$eq"]  = "ABSY";
		cell_types["$ne"]  = "ABSY";
		// cell_types["$eqx"] = "ABSY";
		// cell_types["$nex"] = "ABSY";
		cell_types["$ge"]  = "ABSY";
		cell_types["$gt"]  = "ABSY";

		cell_types["$add"] = "ABSY";
		cell_types["$sub"] = "ABSY";
		cell_types["$mul"] = "ABSY";
		cell_types["$div"] = "ABSY";
		cell_types["$mod"] = "ABSY";
		// cell_types["$pow"] = "ABsY";

		cell_types["$logic_not"] = "ASY";
		cell_types["$logic_and"] = "ABSY";
		cell_types["$logic_or"]  = "ABSY";

		if (edges) {
			cell_types["$mux"] = "*";
			cell_types["$pmux"] = "*";
		}

		// cell_types["$slice"] = "A";
		// cell_types["$concat"] = "A";

		cell_types["$lut"] = "*";
		cell_types["$sop"] = "*";
		cell_types["$alu"] = "ABSY";
		cell_types["$lcu"] = "*";
		cell_types["$macc"] = "*";
		cell_types["$fa"] = "*";

		for (; argidx < GetSize(args); argidx++)
		{
			if (args[argidx].rfind("-", 0) == 0)
				log_cmd_error("Unexpected option: %s\n", args[argidx].c_str());

			if (args[argidx] == "all") {
				for (auto &it : cell_types)
					if (std::count(selected_cell_types.begin(), selected_cell_types.end(), it.first) == 0)
						selected_cell_types.push_back(it.first);
				continue;
			}

			if (args[argidx].compare(0, 1, "/") == 0) {
				std::vector<std::string> new_selected_cell_types;
				for (auto it : selected_cell_types)
					if (it != args[argidx].substr(1))
						new_selected_cell_types.push_back(it);
				new_selected_cell_types.swap(selected_cell_types);
				continue;
			}

			if (cell_types.count(args[argidx]) == 0) {
				std::string cell_type_list;
				int charcount = 100;
				for (auto &it : cell_types) {
					if (charcount > 60) {
						cell_type_list += "\n" + it.first;
						charcount = 0;
					} else
						cell_type_list += " " + it.first;
					charcount += GetSize(it.first);
				}
				log_cmd_error("The cell type `%s' is currently not supported. Try one of these:%s\n",
						args[argidx].c_str(), cell_type_list.c_str());
			}

			if (std::count(selected_cell_types.begin(), selected_cell_types.end(), args[argidx]) == 0)
				selected_cell_types.push_back(args[argidx]);
		}

		if (!ilang_file.empty()) {
			if (!selected_cell_types.empty())
				log_cmd_error("Do not specify any cell types when using -f.\n");
			selected_cell_types.push_back("ilang");
		}

		if (selected_cell_types.empty())
			log_cmd_error("No cell type to test specified.\n");

		std::vector<std::string> uut_names;

		for (auto cell_type : selected_cell_types)
			for (int i = 0; i < num_iter; i++)
			{
				RTLIL::Design *design = new RTLIL::Design;
				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), constmode, muxdiv);
				if (!write_prefix.empty()) {
					Pass::call(design, stringf("write_ilang %s_%s_%05d.il", write_prefix.c_str(), cell_type.c_str()+1, i));
				} else if (edges) {
					Pass::call(design, "dump gold");
					run_edges_test(design, verbose);
				} else {
					Pass::call(design, stringf("copy gold gate; cd gate; %s; cd ..; opt -fast gate", techmap_cmd.c_str()));
					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");
					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");
						Pass::call(design, stringf("copy gold %s_noexpr; select %s_noexpr", 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);
					}
					if (!noeval)
						run_eval_test(design, verbose, nosat, uut_name, vlog_file);
				}
				delete design;
			}

		if (vlog_file.is_open()) {
			vlog_file << "\nmodule testbench;\n";
			for (auto &uut : uut_names)
				vlog_file << stringf("  %s %s ();\n", uut.c_str(), uut.c_str());
			vlog_file << "  initial begin\n";
			for (auto &uut : uut_names)
				vlog_file << "    " << uut << ".run;\n";
			vlog_file << "  end\n";
			vlog_file << "endmodule\n";
		}
	}
} TestCellPass;

PRIVATE_NAMESPACE_END