yosys/passes/sat/qbfsat.cc

/*
 *  yosys -- Yosys Open SYnthesis Suite
 *
 *  Copyright (C) 2020  Alberto Gonzalez <boqwxp@airmail.cc>
 *
 *  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/register.h"
#include "kernel/celltypes.h"
#include "kernel/log.h"

USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN

struct QbfSolutionType {
	std::vector<std::string> stdout;
	bool sat;
	bool unknown; //true if neither 'sat' nor 'unsat'
	bool success; //true if exit code 0

	QbfSolutionType() : sat(false), unknown(true), success(false) {}
};

QbfSolutionType qbf_solve(RTLIL::Module *mod) {

	QbfSolutionType ret;

	//TODO: make temporary directory
	//TODO: call `prep`
	//TODO: call `write_smt2`
	//TODO: execute and capture stdout from `yosys-smtbmc`
	//TODO: remove temporary directory

	return ret;
}

void print_proof_failed()
{
	log("\n");
	log("   ______                   ___       ___       _ _            _ _ \n");
	log("  (_____ \\                 / __)     / __)     (_) |          | | |\n");
	log("   _____) )___ ___   ___ _| |__    _| |__ _____ _| | _____  __| | |\n");
	log("  |  ____/ ___) _ \\ / _ (_   __)  (_   __|____ | | || ___ |/ _  |_|\n");
	log("  | |   | |  | |_| | |_| || |       | |  / ___ | | || ____( (_| |_ \n");
	log("  |_|   |_|   \\___/ \\___/ |_|       |_|  \\_____|_|\\_)_____)\\____|_|\n");
	log("\n");
}

void print_timeout()
{
	log("\n");
	log("        _____  _  _      _____ ____  _     _____\n");
	log("       /__ __\\/ \\/ \\__/|/  __//  _ \\/ \\ /\\/__ __\\\n");
	log("         / \\  | || |\\/|||  \\  | / \\|| | ||  / \\\n");
	log("         | |  | || |  |||  /_ | \\_/|| \\_/|  | |\n");
	log("         \\_/  \\_/\\_/  \\|\\____\\\\____/\\____/  \\_/\n");
	log("\n");
}

void print_qed()
{
	log("\n");
	log("                  /$$$$$$      /$$$$$$$$     /$$$$$$$    \n");
	log("                 /$$__  $$    | $$_____/    | $$__  $$   \n");
	log("                | $$  \\ $$    | $$          | $$  \\ $$   \n");
	log("                | $$  | $$    | $$$$$       | $$  | $$   \n");
	log("                | $$  | $$    | $$__/       | $$  | $$   \n");
	log("                | $$/$$ $$    | $$          | $$  | $$   \n");
	log("                |  $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
	log("                 \\____ $$$|__/|________/|__/|_______/|__/\n");
	log("                       \\__/                              \n");
	log("\n");
}

struct QbfSatPass : public Pass {
	QbfSatPass() : Pass("qbfsat", "solve a 2QBF-SAT problem in the circuit") { }
	void help() YS_OVERRIDE
	{
		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
		log("\n");
		log("    qbfsat [options] [selection]\n");
		log("\n");
		log("This command solves a 2QBF-SAT problem defined over the currently selected module.\n");
		log("Existentially-quantified variables are declared by assigning a wire \"$anyconst\".\n");
		log("Universally-quantified variables may be explicitly declared by assigning a wire\n");
		log("\"$allconst\", but module inputs will be treated as universally-quantified variables\n");
		log("by default.\n");
		log("\n");
		log("    -timeout <seconds>\n");
		log("        Set the solver timeout to the specified number of seconds.\n");
		log("\n");
		log("    -specialize\n");
		log("        Replace all \"$anyconst\" cells with constant values determined by the solver.\n");
		log("\n");
		log("    -specialize-from-file <solution file>\n");
		log("        Do not run the solver, but instead only attempt to replace all \"$anyconst\"\n");
		log("        cells in the current module with values provided by the specified file.\n");
		log("\n");
		log("    -write-solution <solution file>\n");
		log("        Write the assignments discovered by the solver for all \"$anyconst\" cells\n");
		log("        to the specified file.");
		log("\n");
		log("\n");
	}
	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
	{
		bool timeout = false, specialize = false, specialize_from_file = false, write_solution = false;
		long timeout_sec = -1;
		std::string specialize_soln_file;
		std::string write_soln_soln_file;

		log_header(design, "Executing QBF-SAT pass (solving QBF-SAT problems in the circuit).\n");

		size_t argidx;
		for (argidx = 1; argidx < args.size(); argidx++) {
			if (args[argidx] == "-timeout") {
				timeout = true;
				if (args.size() <= argidx + 1)
					log_cmd_error("timeout not specified.\n");
				else
					timeout_sec = atol(args[++argidx].c_str());
				continue;
			}
			else if (args[argidx] == "-specialize") {
				specialize = true;
				continue;
			}
			else if (args[argidx] == "-specialize-from-file") {
				specialize_from_file = true;
				if (args.size() <= argidx + 1)
					log_cmd_error("solution file not specified.\n");
				else
					specialize_soln_file = args[++argidx];
				continue;
			}
			else if (args[argidx] == "-write-solution") {
				write_solution = true;
				if (args.size() <= argidx + 1)
					log_cmd_error("solution file not specified.\n");
				else
					write_soln_soln_file = args[++argidx];
				continue;
			}
			break;
		}
		extra_args(args, argidx, design);

		RTLIL::Module *module = NULL;
		for (auto mod : design->selected_modules()) {
			if (module)
				log_cmd_error("Only one module must be selected for the QBF-SAT pass! (selected: %s and %s)\n", log_id(module), log_id(mod));
			module = mod;
		}
		if (module == NULL)
			log_cmd_error("Can't perform QBF-SAT on an empty selection!\n");

		bool found_input = false;
		bool found_hole = false;
		bool found_1bit_output = false;
		for (auto wire : module->wires()) {
			if (wire->port_input)
				found_input = true;
			if (wire->port_output && wire->width == 1)
				found_1bit_output = true;
		}
		for (auto cell : module->cells()) {
			if (cell->type == "$allconst")
				found_input = true;
			if (cell->type == "$anyconst")
				found_hole = true;
			if (cell->type.in("$assert", "$assume"))
				found_1bit_output = true;
		}
		if (!found_input)
			log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n");
		if (!found_hole)
			log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n");
		if (!found_1bit_output)
			log_cmd_error("Did not find any single-bit outputs, assert()s, or assume()s.  Is this a miter circuit?\n");

		QbfSolutionType ret = qbf_solve(module);

		if (ret.unknown)
			log_warning("solver did not give an answer\n");
		else if (ret.sat)
			print_qed();
		else
			print_proof_failed();

		//TODO specialize etc.
	}
} QbfSatPass;

PRIVATE_NAMESPACE_END