yosys/passes/sat/fminit.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"
#include "kernel/sigtools.h"

USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN

struct FminitPass : public Pass {
	FminitPass() : Pass("fminit", "set init values/sequences for formal") { }
	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("    fminit [options] <selection>\n");
		log("\n");
		log("This pass creates init constraints (for example for reset sequences) in a formal\n");
		log("model.\n");
		log("\n");
		log("    -seq <signal> <sequence>\n");
		log("        Set sequence using comma-separated list of values, use 'z for\n");
		log("        unconstrained bits. The last value is used for the remainder of the\n");
		log("        trace.\n");
		log("\n");
		log("    -set <signal> <value>\n");
		log("        Add constant value constraint\n");
		log("\n");
		log("    -posedge <signal>\n");
		log("    -negedge <signal>\n");
		log("        Set clock for init sequences\n");
		log("\n");
	}
	void execute(std::vector<std::string> args, RTLIL::Design *design) override
	{
		vector<pair<string, vector<string>>> initdata;
		vector<pair<string, string>> setdata;
		string clocksignal;
		bool clockedge;

		log_header(design, "Executing FMINIT pass.\n");

		size_t argidx;
		for (argidx = 1; argidx < args.size(); argidx++)
		{
			// if (args[argidx] == "-o" && argidx+1 < args.size()) {
			// 	filename = args[++argidx];
			// 	continue;
			// }
			if (args[argidx] == "-seq" && argidx+2 < args.size()) {
				string lhs = args[++argidx];
				string rhs = args[++argidx];
				initdata.push_back(make_pair(lhs, split_tokens(rhs, ",")));
				continue;
			}
			if (args[argidx] == "-set" && argidx+2 < args.size()) {
				string lhs = args[++argidx];
				string rhs = args[++argidx];
				setdata.push_back(make_pair(lhs, rhs));
				continue;
			}
			if (args[argidx] == "-posedge" && argidx+1 < args.size()) {
				clocksignal = args[++argidx];
				clockedge = true;
				continue;
			}
			if (args[argidx] == "-negedge" && argidx+1 < args.size()) {
				clocksignal = args[++argidx];
				clockedge = true;
				continue;
			}
			break;
		}
		extra_args(args, argidx, design);

		Module *module = nullptr;

		for (auto mod : design->selected_modules()) {
			if (module != nullptr)
				log_error("'fminit' requires exactly one module to be selected.\n");
			module = mod;
		}

		if (module == nullptr)
			log_error("'fminit' requires exactly one module to be selected.\n");

		SigSpec clksig;
		if (!clocksignal.empty()) {
			if (!SigSpec::parse(clksig, module, clocksignal))
				log_error("Error parsing expression '%s'.\n", clocksignal);
		}

		for (auto &it : setdata)
		{
			SigSpec lhs, rhs;

			if (!SigSpec::parse(lhs, module, it.first))
				log_error("Error parsing expression '%s'.\n", it.first);

			if (!SigSpec::parse_rhs(lhs, rhs, module, it.second))
				log_error("Error parsing expression '%s'.\n", it.second);

			SigSpec final_lhs, final_rhs;

			for (int i = 0; i < GetSize(rhs); i++)
				if (rhs[i] != State::Sz) {
					final_lhs.append(lhs[i]);
					final_rhs.append(rhs[i]);
				}

			if (!final_lhs.empty()) {
				SigSpec eq = module->Eq(NEW_ID, final_lhs, final_rhs);
				module->addAssume(NEW_ID, eq, State::S1);
			}
		}

		vector<SigSpec> ctrlsig;
		vector<SigSpec> ctrlsig_latched;

		for (auto &it : initdata)
		{
			SigSpec lhs, rhs;

			if (!SigSpec::parse(lhs, module, it.first))
				log_error("Error parsing expression '%s'.\n", it.first);

			for (int i = 0; i < GetSize(it.second); i++)
			{
				if (i >= GetSize(ctrlsig))
				{
					SigSpec insig = i > 0 ? ctrlsig.at(i-1) : State::S0;

					Wire *outwire = module->addWire(NEW_ID);
					outwire->attributes[ID::init] = i > 0 ? State::S0 : State::S1;

					if (clksig.empty())
						module->addFf(NEW_ID, insig, outwire);
					else
						module->addDff(NEW_ID, clksig, insig, outwire, clockedge);

					ctrlsig.push_back(outwire);
					ctrlsig_latched.push_back(SigSpec());
				}

				if (i+1 == GetSize(it.second) && ctrlsig_latched[i].empty())
				{
					Wire *ffwire = module->addWire(NEW_ID);
					ffwire->attributes[ID::init] = State::S0;
					SigSpec outsig = module->Or(NEW_ID, ffwire, ctrlsig[i]);

					if (clksig.empty())
						module->addFf(NEW_ID, outsig, ffwire);
					else
						module->addDff(NEW_ID, clksig, outsig, ffwire, clockedge);

					ctrlsig_latched[i] = outsig;
				}

				SigSpec ctrl = i+1 == GetSize(it.second) ? ctrlsig_latched[i] : ctrlsig[i];

				SigSpec final_lhs, final_rhs;

				if (!SigSpec::parse_rhs(lhs, rhs, module, it.second[i]))
					log_error("Error parsing expression '%s'.\n", it.second[i]);

				for (int i = 0; i < GetSize(rhs); i++)
					if (rhs[i] != State::Sz) {
						final_lhs.append(lhs[i]);
						final_rhs.append(rhs[i]);
					}

				if (!final_lhs.empty()) {
					SigSpec eq = module->Eq(NEW_ID, final_lhs, final_rhs);
					module->addAssume(NEW_ID, eq, ctrl);
				}
			}
		}
	}
} FminitPass;

PRIVATE_NAMESPACE_END