1 /* -*- c++ -*-
2  *  yosys -- Yosys Open SYnthesis Suite
3  *
4  *  Copyright (C) 2020  Alberto Gonzalez <boqwxp@airmail.cc>
5  *
6  *  Permission to use, copy, modify, and/or distribute this software for any
7  *  purpose with or without fee is hereby granted, provided that the above
8  *  copyright notice and this permission notice appear in all copies.
9  *
10  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
11  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
12  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
13  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
14  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
15  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
16  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
17  *
18  */
19 
20 #ifndef QBFSAT_H
21 #define QBFSAT_H
22 
23 #include "kernel/yosys.h"
24 #include <numeric>
25 
26 YOSYS_NAMESPACE_BEGIN
27 
28 struct QbfSolveOptions {
29 	bool specialize = false, specialize_from_file = false, write_solution = false, nocleanup = false;
30 	bool dump_final_smt2 = false, assume_outputs = false, assume_neg = false, nooptimize = false;
31 	bool nobisection = false, sat = false, unsat = false, show_smtbmc = false;
32 	enum Solver{Z3, Yices, CVC4} solver = Yices;
33 	enum OptimizationLevel{O0, O1, O2} oflag = O0;
34 	dict<std::string, std::string> solver_options;
35 	int timeout = 0;
36 	std::string specialize_soln_file = "";
37 	std::string write_soln_soln_file = "";
38 	std::string dump_final_smt2_file = "";
39 	size_t argidx = 0;
40 
get_solver_nameQbfSolveOptions41 	std::string get_solver_name() const {
42 		if (solver == Solver::Z3)
43 			return "z3";
44 		else if (solver == Solver::Yices)
45 			return "yices";
46 		else if (solver == Solver::CVC4)
47 			return "cvc4";
48 
49 		log_cmd_error("unknown solver specified.\n");
50 		return "";
51 	}
52 };
53 
54 struct QbfSolutionType {
55 	std::vector<std::string> stdout_lines = {};
56 	dict<pool<std::string>, std::string> hole_to_value = {};
57 	double solver_time = 0;
58 	bool sat = false;
59 	bool unknown = true; //true if neither 'sat' nor 'unsat'
60 
get_hole_loc_idx_sigbit_mapQbfSolutionType61 	dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> get_hole_loc_idx_sigbit_map(RTLIL::Module *module) const {
62 		dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit;
63 		pool<RTLIL::SigBit> anyconst_sigbits;
64 		dict<RTLIL::SigBit, RTLIL::SigBit> anyconst_sigbit_to_wire_sigbit;
65 
66 		for (auto cell : module->cells()) {
67 			pool<std::string> cell_src = cell->get_strpool_attribute(ID::src);
68 			auto pos = hole_to_value.find(cell_src);
69 			if (pos != hole_to_value.end() && cell->type.in("$anyconst", "$anyseq")) {
70 				RTLIL::SigSpec port_y = cell->getPort(ID::Y);
71 				for (int i = GetSize(port_y) - 1; i >= 0; --i) {
72 					hole_loc_idx_to_sigbit[std::make_pair(pos->first, i)] = port_y[i];
73 					anyconst_sigbits.insert(port_y[i]);
74 				}
75 			}
76 		}
77 
78 		for (auto &conn : module->connections()) {
79 			auto lhs = conn.first;
80 			auto rhs = conn.second;
81 			for (auto i = 0; i < GetSize(rhs); ++i) {
82 				if (anyconst_sigbits[rhs[i]]) {
83 					auto pos = anyconst_sigbit_to_wire_sigbit.find(rhs[i]);
84 					if (pos != anyconst_sigbit_to_wire_sigbit.end())
85 						log_cmd_error("conflicting names for hole $anyconst sigbit %s\n", log_signal(rhs[i]));
86 					anyconst_sigbit_to_wire_sigbit[rhs[i]] = lhs[i];
87 				}
88 			}
89 		}
90 
91 		for (auto &it : hole_loc_idx_to_sigbit) {
92 			auto pos = anyconst_sigbit_to_wire_sigbit.find(it.second);
93 			if (pos != anyconst_sigbit_to_wire_sigbit.end())
94 				it.second = pos->second;
95 		}
96 
97 		return hole_loc_idx_to_sigbit;
98 	}
99 
dump_modelQbfSolutionType100 	void dump_model(RTLIL::Module *module) const {
101 		log("Satisfiable model:\n");
102 		auto hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module);
103 		for (auto &it : hole_to_value) {
104 			pool<std::string> hole_loc = it.first;
105 			std::string hole_value = it.second;
106 
107 			for (unsigned int i = 0; i < hole_value.size(); ++i) {
108 				int bit_idx = GetSize(hole_value) - 1 - i;
109 				auto it = hole_loc_idx_to_sigbit.find(std::make_pair(hole_loc, i));
110 				log_assert(it != hole_loc_idx_to_sigbit.end());
111 
112 				RTLIL::SigBit hole_sigbit = it->second;
113 				log("\t%s = 1'b%c\n", log_signal(hole_sigbit), hole_value[bit_idx]);
114 			}
115 		}
116 	}
117 
write_solutionQbfSolutionType118 	void write_solution(RTLIL::Module *module, const std::string &file) const {
119 		std::ofstream fout(file.c_str());
120 		if (!fout)
121 			log_cmd_error("could not open solution file for writing.\n");
122 
123 		//There is a question here: How exactly shall we identify holes?
124 		//There are at least two reasonable options:
125 		//1. By the source location of the $anyconst cells
126 		//2. By the name(s) of the wire(s) connected to each SigBit of the $anyconst cell->getPort(ID::Y) SigSpec.
127 		//
128 		//Option 1 has the benefit of being very precise.  There is very limited potential for confusion, as long
129 		//as the source attribute has been set.  However, if the source attribute is not set, this won't work.
130 		//More importantly, we want to have the ability to port hole assignments to other modules with compatible
131 		//hole names and widths.  Obviously in those cases source locations of the $anyconst cells will not match.
132 		//
133 		//Option 2 has the benefits previously described, but wire names can be changed automatically by
134 		//optimization or techmapping passes, especially when (ex/im)porting from BLIF for optimization with ABC.
135 		//
136 		//The approach taken here is to allow both options.  We write the assignment information for each bit of
137 		//the solution on a separate line.  Each line is of one of two forms:
138 		//
139 		//location bit name = value
140 		//location bit name [offset] = value
141 		//
142 		//where '[', ']', and '=' are literal symbols, "location" is the $anyconst cell source location attribute,
143 		//"bit" is the index of the $anyconst cell, "name" is the `wire->name` field of the SigBit corresponding
144 		//to the current bit of the $anyconst cell->getPort(ID::Y), "offset" is the `offset` field of that same
145 		//SigBit, and "value", which is either '0' or '1', represents the assignment for that bit.
146 		auto hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module);
147 		for (auto &x : hole_to_value) {
148 			std::string src_as_str = std::accumulate(x.first.begin(), x.first.end(), std::string(), [](const std::string &a, const std::string &b){return a + "|" + b;});
149 			for (auto i = 0; i < GetSize(x.second); ++i)
150 				fout << src_as_str.c_str() << " " << i << " " << log_signal(hole_loc_idx_to_sigbit[std::make_pair(x.first, i)]) << " = " << x.second[GetSize(x.second) - 1 - i] << std::endl;
151 		}
152 	}
153 
recover_solutionQbfSolutionType154 	void recover_solution() {
155 		YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED");
156 		YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
157 		YS_REGEX_TYPE unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED");
158 		YS_REGEX_TYPE timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)");
159 		YS_REGEX_TYPE timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)");
160 		YS_REGEX_TYPE unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)");
161 		YS_REGEX_TYPE unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver");
162 		YS_REGEX_TYPE memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\"");
163 		YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
164 #ifndef NDEBUG
165 		YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+");
166 		YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+");
167 #endif
168 		YS_REGEX_MATCH_TYPE m;
169 		bool sat_regex_found = false;
170 		bool unsat_regex_found = false;
171 		dict<std::string, bool> hole_value_recovered;
172 		for (const std::string &x : stdout_lines) {
173 			if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) {
174 				std::string loc = m[1].str();
175 				std::string val = m[2].str();
176 #ifndef NDEBUG
177 				log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex));
178 				log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex));
179 #endif
180 				auto locs = split_tokens(loc, "|");
181 				pool<std::string> loc_pool(locs.begin(), locs.end());
182 				hole_to_value[loc_pool] = val;
183 			}
184 			else if (YS_REGEX_NS::regex_search(x, sat_regex)) {
185 				sat_regex_found = true;
186 				sat = true;
187 				unknown = false;
188 			}
189 			else if (YS_REGEX_NS::regex_search(x, unsat_regex)) {
190 				unsat_regex_found = true;
191 				sat = false;
192 				unknown = false;
193 			}
194 			else if (YS_REGEX_NS::regex_search(x, memout_regex)) {
195 				unknown = true;
196 				log_warning("solver ran out of memory\n");
197 			}
198 			else if (YS_REGEX_NS::regex_search(x, timeout_regex)) {
199 				unknown = true;
200 				log_warning("solver timed out\n");
201 			}
202 			else if (YS_REGEX_NS::regex_search(x, timeout_regex2)) {
203 				unknown = true;
204 				log_warning("solver timed out\n");
205 			}
206 			else if (YS_REGEX_NS::regex_search(x, unknown_regex)) {
207 				unknown = true;
208 				log_warning("solver returned \"unknown\"\n");
209 			}
210 			else if (YS_REGEX_NS::regex_search(x, unsat_regex2)) {
211 				unsat_regex_found = true;
212 				sat = false;
213 				unknown = false;
214 			}
215 			else if (YS_REGEX_NS::regex_search(x, unknown_regex2)) {
216 				unknown = true;
217 			}
218 		}
219 		log_assert(!unknown && sat? sat_regex_found : true);
220 		log_assert(!unknown && !sat? unsat_regex_found : true);
221 	}
222 };
223 
print_proof_failed()224 void print_proof_failed()
225 {
226 	log("\n");
227 	log("   ______                   ___       ___       _ _            _ _ \n");
228 	log("  (_____ \\                 / __)     / __)     (_) |          | | |\n");
229 	log("   _____) )___ ___   ___ _| |__    _| |__ _____ _| | _____  __| | |\n");
230 	log("  |  ____/ ___) _ \\ / _ (_   __)  (_   __|____ | | || ___ |/ _  |_|\n");
231 	log("  | |   | |  | |_| | |_| || |       | |  / ___ | | || ____( (_| |_ \n");
232 	log("  |_|   |_|   \\___/ \\___/ |_|       |_|  \\_____|_|\\_)_____)\\____|_|\n");
233 	log("\n");
234 }
235 
print_qed()236 void print_qed()
237 {
238 	log("\n");
239 	log("                  /$$$$$$      /$$$$$$$$     /$$$$$$$    \n");
240 	log("                 /$$__  $$    | $$_____/    | $$__  $$   \n");
241 	log("                | $$  \\ $$    | $$          | $$  \\ $$   \n");
242 	log("                | $$  | $$    | $$$$$       | $$  | $$   \n");
243 	log("                | $$  | $$    | $$__/       | $$  | $$   \n");
244 	log("                | $$/$$ $$    | $$          | $$  | $$   \n");
245 	log("                |  $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
246 	log("                 \\____ $$$|__/|________/|__/|_______/|__/\n");
247 	log("                       \\__/                              \n");
248 	log("\n");
249 }
250 
251 YOSYS_NAMESPACE_END
252 
253 #endif
254