yosys/passes/sat/miter.cc

/*
 *  yosys -- Yosys Open SYnthesis Suite
 *
 *  Copyright (C) 2012  Claire Xenia Wolf <claire@yosyshq.com>
 *
 *  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/log_help.h"

USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN

void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL::Design *design)
{
	bool flag_ignore_gold_x = false;
	bool flag_make_outputs = false;
	bool flag_make_outcmp = false;
	bool flag_make_assert = false;
	bool flag_make_cover = false;
	bool flag_flatten = false;
	bool flag_cross = false;

	log_header(design, "Executing MITER pass (creating miter circuit).\n");

	size_t argidx;
	for (argidx = 2; argidx < args.size(); argidx++)
	{
		if (args[argidx] == "-ignore_gold_x") {
			flag_ignore_gold_x = true;
			continue;
		}
		if (args[argidx] == "-make_outputs") {
			flag_make_outputs = true;
			continue;
		}
		if (args[argidx] == "-make_outcmp") {
			flag_make_outcmp = true;
			continue;
		}
		if (args[argidx] == "-make_assert") {
			flag_make_assert = true;
			continue;
		}
		if (args[argidx] == "-make_cover") {
			flag_make_cover = true;
			continue;
		}
		if (args[argidx] == "-flatten") {
			flag_flatten = true;
			continue;
		}
		if (args[argidx] == "-cross") {
			flag_cross = true;
			continue;
		}
		break;
	}
	if (argidx+3 != args.size() || args[argidx].compare(0, 1, "-") == 0)
		that->cmd_error(args, argidx, "command argument error");

	RTLIL::IdString gold_name = RTLIL::escape_id(args[argidx++]);
	RTLIL::IdString gate_name = RTLIL::escape_id(args[argidx++]);
	RTLIL::IdString miter_name = RTLIL::escape_id(args[argidx++]);

	if (design->module(gold_name) == nullptr)
		log_cmd_error("Can't find gold module %s!\n", gold_name);
	if (design->module(gate_name) == nullptr)
		log_cmd_error("Can't find gate module %s!\n", gate_name);
	if (design->module(miter_name) != nullptr)
		log_cmd_error("There is already a module %s!\n", miter_name);

	RTLIL::Module *gold_module = design->module(gold_name);
	RTLIL::Module *gate_module = design->module(gate_name);
	pool<Wire*> gold_cross_ports;

	for (auto gold_wire : gold_module->wires()) {
		if (gold_wire->port_id == 0)
			continue;
		RTLIL::Wire *gate_wire = gate_module->wire(gold_wire->name);
		if (gate_wire == nullptr)
			goto match_gold_port_error;
		if (gold_wire->width != gate_wire->width)
			goto match_gold_port_error;
		if (flag_cross && !gold_wire->port_input && gold_wire->port_output &&
				gate_wire->port_input && !gate_wire->port_output) {
			gold_cross_ports.insert(gold_wire);
			continue;
		}
		if (gold_wire->port_input != gate_wire->port_input)
			goto match_gold_port_error;
		if (gold_wire->port_output != gate_wire->port_output)
			goto match_gold_port_error;
		continue;
	match_gold_port_error:
		log_cmd_error("No matching port in gate module was found for %s!\n", gold_wire->name);
	}

	for (auto gate_wire : gate_module->wires()) {
		if (gate_wire->port_id == 0)
			continue;
		RTLIL::Wire *gold_wire = gold_module->wire(gate_wire->name);
		if (gold_wire == nullptr)
			goto match_gate_port_error;
		if (gate_wire->width != gold_wire->width)
			goto match_gate_port_error;
		if (flag_cross && !gold_wire->port_input && gold_wire->port_output &&
				gate_wire->port_input && !gate_wire->port_output)
			continue;
		if (gate_wire->port_input != gold_wire->port_input)
			goto match_gate_port_error;
		if (gate_wire->port_output != gold_wire->port_output)
			goto match_gate_port_error;
		continue;
	match_gate_port_error:
		log_cmd_error("No matching port in gold module was found for %s!\n", gate_wire->name);
	}

	log("Creating miter cell \"%s\" with gold cell \"%s\" and gate cell \"%s\".\n", RTLIL::id2cstr(miter_name), RTLIL::id2cstr(gold_name), RTLIL::id2cstr(gate_name));

	RTLIL::Module *miter_module = new RTLIL::Module;
	miter_module->name = miter_name;
	design->add(miter_module);

	RTLIL::Cell *gold_cell = miter_module->addCell(ID(gold), gold_name);
	RTLIL::Cell *gate_cell = miter_module->addCell(ID(gate), gate_name);

	RTLIL::SigSpec all_conditions;

	for (auto gold_wire : gold_module->wires())
	{
		if (gold_cross_ports.count(gold_wire))
		{
			SigSpec w = miter_module->addWire("\\cross_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width);
			gold_cell->setPort(gold_wire->name, w);
			if (flag_ignore_gold_x) {
				RTLIL::SigSpec w_x = miter_module->addWire(NEW_ID, GetSize(w));
				for (int i = 0; i < GetSize(w); i++)
					miter_module->addEqx(NEW_ID, w[i], State::Sx, w_x[i]);
				RTLIL::SigSpec w_any = miter_module->And(NEW_ID, miter_module->Anyseq(NEW_ID, GetSize(w)), w_x);
				RTLIL::SigSpec w_masked = miter_module->And(NEW_ID, w, miter_module->Not(NEW_ID, w_x));
				w = miter_module->And(NEW_ID, w_any, w_masked);
			}
			gate_cell->setPort(gold_wire->name, w);
			continue;
		}

		if (gold_wire->port_input)
		{
			RTLIL::Wire *w = miter_module->addWire("\\in_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width);
			w->port_input = true;

			gold_cell->setPort(gold_wire->name, w);
			gate_cell->setPort(gold_wire->name, w);
		}

		if (gold_wire->port_output)
		{
			RTLIL::Wire *w_gold = miter_module->addWire("\\gold_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width);
			w_gold->port_output = flag_make_outputs;

			RTLIL::Wire *w_gate = miter_module->addWire("\\gate_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width);
			w_gate->port_output = flag_make_outputs;

			gold_cell->setPort(gold_wire->name, w_gold);
			gate_cell->setPort(gold_wire->name, w_gate);

			RTLIL::SigSpec this_condition;

			if (flag_ignore_gold_x)
			{
				RTLIL::SigSpec gold_x = miter_module->addWire(NEW_ID, w_gold->width);
				for (int i = 0; i < w_gold->width; i++) {
					RTLIL::Cell *eqx_cell = miter_module->addCell(NEW_ID, ID($eqx));
					eqx_cell->parameters[ID::A_WIDTH] = 1;
					eqx_cell->parameters[ID::B_WIDTH] = 1;
					eqx_cell->parameters[ID::Y_WIDTH] = 1;
					eqx_cell->parameters[ID::A_SIGNED] = 0;
					eqx_cell->parameters[ID::B_SIGNED] = 0;
					eqx_cell->setPort(ID::A, RTLIL::SigSpec(w_gold, i));
					eqx_cell->setPort(ID::B, RTLIL::State::Sx);
					eqx_cell->setPort(ID::Y, gold_x.extract(i, 1));
				}

				RTLIL::SigSpec gold_masked = miter_module->addWire(NEW_ID, w_gold->width);
				RTLIL::SigSpec gate_masked = miter_module->addWire(NEW_ID, w_gate->width);

				RTLIL::Cell *or_gold_cell = miter_module->addCell(NEW_ID, ID($or));
				or_gold_cell->parameters[ID::A_WIDTH] = w_gold->width;
				or_gold_cell->parameters[ID::B_WIDTH] = w_gold->width;
				or_gold_cell->parameters[ID::Y_WIDTH] = w_gold->width;
				or_gold_cell->parameters[ID::A_SIGNED] = 0;
				or_gold_cell->parameters[ID::B_SIGNED] = 0;
				or_gold_cell->setPort(ID::A, w_gold);
				or_gold_cell->setPort(ID::B, gold_x);
				or_gold_cell->setPort(ID::Y, gold_masked);

				RTLIL::Cell *or_gate_cell = miter_module->addCell(NEW_ID, ID($or));
				or_gate_cell->parameters[ID::A_WIDTH] = w_gate->width;
				or_gate_cell->parameters[ID::B_WIDTH] = w_gate->width;
				or_gate_cell->parameters[ID::Y_WIDTH] = w_gate->width;
				or_gate_cell->parameters[ID::A_SIGNED] = 0;
				or_gate_cell->parameters[ID::B_SIGNED] = 0;
				or_gate_cell->setPort(ID::A, w_gate);
				or_gate_cell->setPort(ID::B, gold_x);
				or_gate_cell->setPort(ID::Y, gate_masked);

				RTLIL::Cell *eq_cell = miter_module->addCell(NEW_ID, ID($eqx));
				eq_cell->parameters[ID::A_WIDTH] = w_gold->width;
				eq_cell->parameters[ID::B_WIDTH] = w_gate->width;
				eq_cell->parameters[ID::Y_WIDTH] = 1;
				eq_cell->parameters[ID::A_SIGNED] = 0;
				eq_cell->parameters[ID::B_SIGNED] = 0;
				eq_cell->setPort(ID::A, gold_masked);
				eq_cell->setPort(ID::B, gate_masked);
				eq_cell->setPort(ID::Y, miter_module->addWire(NEW_ID));
				this_condition = eq_cell->getPort(ID::Y);
			}
			else
			{
				RTLIL::Cell *eq_cell = miter_module->addCell(NEW_ID, ID($eqx));
				eq_cell->parameters[ID::A_WIDTH] = w_gold->width;
				eq_cell->parameters[ID::B_WIDTH] = w_gate->width;
				eq_cell->parameters[ID::Y_WIDTH] = 1;
				eq_cell->parameters[ID::A_SIGNED] = 0;
				eq_cell->parameters[ID::B_SIGNED] = 0;
				eq_cell->setPort(ID::A, w_gold);
				eq_cell->setPort(ID::B, w_gate);
				eq_cell->setPort(ID::Y, miter_module->addWire(NEW_ID));
				this_condition = eq_cell->getPort(ID::Y);
			}

			if (flag_make_outcmp)
			{
				RTLIL::Wire *w_cmp = miter_module->addWire("\\cmp_" + RTLIL::unescape_id(gold_wire->name));
				w_cmp->port_output = true;
				miter_module->connect(RTLIL::SigSig(w_cmp, this_condition));
			}

			if (flag_make_cover)
			{
				auto cover_condition = miter_module->Not(NEW_ID, this_condition);
				miter_module->addCover("\\cover_" + RTLIL::unescape_id(gold_wire->name), cover_condition, State::S1);
			}

			all_conditions.append(this_condition);
		}
	}

	if (all_conditions.size() != 1) {
		RTLIL::Cell *reduce_cell = miter_module->addCell(NEW_ID, ID($reduce_and));
		reduce_cell->parameters[ID::A_WIDTH] = all_conditions.size();
		reduce_cell->parameters[ID::Y_WIDTH] = 1;
		reduce_cell->parameters[ID::A_SIGNED] = 0;
		reduce_cell->setPort(ID::A, all_conditions);
		reduce_cell->setPort(ID::Y, miter_module->addWire(NEW_ID));
		all_conditions = reduce_cell->getPort(ID::Y);
	}

	if (flag_make_assert) {
		RTLIL::Cell *assert_cell = miter_module->addCell(NEW_ID, ID($assert));
		assert_cell->setPort(ID::A, all_conditions);
		assert_cell->setPort(ID::EN, State::S1);
	}

	RTLIL::Wire *w_trigger = miter_module->addWire(ID(trigger));
	w_trigger->port_output = true;

	RTLIL::Cell *not_cell = miter_module->addCell(NEW_ID, ID($not));
	not_cell->parameters[ID::A_WIDTH] = all_conditions.size();
	not_cell->parameters[ID::A_WIDTH] = all_conditions.size();
	not_cell->parameters[ID::Y_WIDTH] = w_trigger->width;
	not_cell->parameters[ID::A_SIGNED] = 0;
	not_cell->setPort(ID::A, all_conditions);
	not_cell->setPort(ID::Y, w_trigger);

	miter_module->fixup_ports();

	if (flag_flatten) {
		log_push();
		Pass::call_on_module(design, miter_module, "flatten -wb; opt_expr -keepdc -undriven;;");
		log_pop();
	}
}

void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL::Design *design)
{
	bool flag_make_outputs = false;
	bool flag_flatten = false;

	log_header(design, "Executing MITER pass (creating miter circuit).\n");

	size_t argidx;
	for (argidx = 2; argidx < args.size(); argidx++)
	{
		if (args[argidx] == "-make_outputs") {
			flag_make_outputs = true;
			continue;
		}
		if (args[argidx] == "-flatten") {
			flag_flatten = true;
			continue;
		}
		break;
	}
	if ((argidx+1 != args.size() && argidx+2 != args.size()) || args[argidx].compare(0, 1, "-") == 0)
		that->cmd_error(args, argidx, "command argument error");

	IdString module_name = RTLIL::escape_id(args[argidx++]);
	IdString miter_name = argidx < args.size() ? RTLIL::escape_id(args[argidx++]) : "";

	if (design->module(module_name) == nullptr)
		log_cmd_error("Can't find module %s!\n", module_name);
	if (!miter_name.empty() && design->module(miter_name) != nullptr)
		log_cmd_error("There is already a module %s!\n", miter_name);

	Module *module = design->module(module_name);

	if (!miter_name.empty()) {
		module = module->clone();
		module->name = miter_name;
		design->add(module);
	}

	if (!flag_make_outputs)
		for (auto wire : module->wires())
			wire->port_output = false;

	Wire *trigger = module->addWire(ID(trigger));
	trigger->port_output = true;
	module->fixup_ports();

	if (flag_flatten) {
		log_push();
		Pass::call_on_module(design, module, "flatten -wb;;");
		log_pop();
	}

	SigSpec assert_signals, assume_signals;
	vector<Cell*> cell_list = module->cells();
	for (auto cell : cell_list)
	{
		if (!cell->type.in(ID($assert), ID($assume)))
			continue;

		SigBit is_active = module->Nex(NEW_ID, cell->getPort(ID::A), State::S1);
		SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort(ID::EN), State::S1);

		if (cell->type == ID($assert)) {
			assert_signals.append(module->And(NEW_ID, is_active, is_enabled));
		} else {
			assume_signals.append(module->And(NEW_ID, is_active, is_enabled));
		}

		module->remove(cell);
	}

	if (assume_signals.empty())
	{
		module->addReduceOr(NEW_ID, assert_signals, trigger);
	}
	else
	{
		Wire *assume_q = module->addWire(NEW_ID);
		assume_q->attributes[ID::init] = State::S0;
		assume_signals.append(assume_q);

		SigSpec assume_nok = module->ReduceOr(NEW_ID, assume_signals);
		SigSpec assume_ok = module->Not(NEW_ID, assume_nok);
		module->addFf(NEW_ID, assume_nok, assume_q);

		SigSpec assert_fail = module->ReduceOr(NEW_ID, assert_signals);
		module->addAnd(NEW_ID, assert_fail, assume_ok, trigger);
	}

	if (flag_flatten) {
		log_push();
		Pass::call_on_module(design, module, "opt_expr -keepdc -undriven;;");
		log_pop();
	}
}

struct MiterPass : public Pass {
	MiterPass() : Pass("miter", "automatically create a miter circuit") { }
	bool formatted_help() override {
		auto *help = PrettyHelp::get_current();
		help->set_group("formal");
		return false;
	}
	void help() override
	{
		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
		log("\n");
		log("    miter -equiv [options] gold_name gate_name miter_name\n");
		log("\n");
		log("Creates a miter circuit for equivalence checking. The gold- and gate- modules\n");
		log("must have the same interfaces. The miter circuit will have all inputs of the\n");
		log("two source modules, prefixed with 'in_'. The miter circuit has a 'trigger'\n");
		log("output that goes high if an output mismatch between the two source modules is\n");
		log("detected.\n");
		log("\n");
		log("    -ignore_gold_x\n");
		log("        a undef (x) bit in the gold module output will match any value in\n");
		log("        the gate module output.\n");
		log("\n");
		log("    -make_outputs\n");
		log("        also route the gold- and gate-outputs to 'gold_*' and 'gate_*' outputs\n");
		log("        on the miter circuit.\n");
		log("\n");
		log("    -make_outcmp\n");
		log("        also create a cmp_* output for each gold/gate output pair.\n");
		log("\n");
		log("    -make_assert\n");
		log("        also create an 'assert' cell that checks if trigger is always low.\n");
		log("\n");
		log("    -make_cover\n");
		log("        also create a 'cover' cell for each gold/gate output pair.\n");
		log("\n");
		log("    -flatten\n");
		log("        call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
		log("\n");
		log("\n");
		log("    -cross\n");
		log("        allow output ports on the gold module to match input ports on the\n");
		log("        gate module. This is useful when the gold module contains additional\n");
		log("        logic to drive some of the gate module inputs.\n");
		log("\n");
		log("\n");
		log("    miter -assert [options] module [miter_name]\n");
		log("\n");
		log("Creates a miter circuit for property checking. All input ports are kept,\n");
		log("output ports are discarded. An additional output 'trigger' is created that\n");
		log("goes high when an assert is violated. Without a miter_name, the existing\n");
		log("module is modified.\n");
		log("\n");
		log("    -make_outputs\n");
		log("        keep module output ports.\n");
		log("\n");
		log("    -flatten\n");
		log("        call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
		log("\n");
	}
	void execute(std::vector<std::string> args, RTLIL::Design *design) override
	{
		if (args.size() > 1 && args[1] == "-equiv") {
			create_miter_equiv(this, args, design);
			return;
		}

		if (args.size() > 1 && args[1] == "-assert") {
			create_miter_assert(this, args, design);
			return;
		}

		log_cmd_error("Missing mode parameter!\n");
	}
} MiterPass;

PRIVATE_NAMESPACE_END