1 /*
2  *  yosys -- Yosys Open SYnthesis Suite
3  *
4  *  Copyright (C) 2012  Claire Xenia Wolf <claire@yosyshq.com>
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 #include "kernel/rtlil.h"
21 #include "kernel/register.h"
22 #include "kernel/sigtools.h"
23 #include "kernel/celltypes.h"
24 #include "kernel/log.h"
25 #include "kernel/mem.h"
26 #include <string>
27 
28 USING_YOSYS_NAMESPACE
29 PRIVATE_NAMESPACE_BEGIN
30 
31 struct Smt2Worker
32 {
33 	CellTypes ct;
34 	SigMap sigmap;
35 	RTLIL::Module *module;
36 	bool bvmode, memmode, wiresmode, verbose, statebv, statedt, forallmode;
37 	dict<IdString, int> &mod_stbv_width;
38 	int idcounter = 0, statebv_width = 0;
39 
40 	std::vector<std::string> decls, trans, hier, dtmembers;
41 	std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
42 	std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
43 	pool<Cell*> recursive_cells, registers;
44 	std::vector<Mem> memories;
45 	dict<Cell*, Mem*> mem_cells;
46 	std::set<Mem*> memory_queue;
47 
48 	pool<SigBit> clock_posedge, clock_negedge;
49 	vector<string> ex_state_eq, ex_input_eq;
50 
51 	std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
52 	std::map<Mem*, int> memarrays;
53 	std::map<int, int> bvsizes;
54 	dict<IdString, char*> ids;
55 
get_idSmt2Worker56 	const char *get_id(IdString n)
57 	{
58 		if (ids.count(n) == 0) {
59 			std::string str = log_id(n);
60 			for (int i = 0; i < GetSize(str); i++) {
61 				if (str[i] == '\\')
62 					str[i] = '/';
63 			}
64 			ids[n] = strdup(str.c_str());
65 		}
66 		return ids[n];
67 	}
68 
69 	template<typename T>
get_idSmt2Worker70 	const char *get_id(T *obj) {
71 		return get_id(obj->name);
72 	}
73 
makebitsSmt2Worker74 	void makebits(std::string name, int width = 0, std::string comment = std::string())
75 	{
76 		std::string decl_str;
77 
78 		if (statebv)
79 		{
80 			if (width == 0) {
81 				decl_str = stringf("(define-fun |%s| ((state |%s_s|)) Bool (= ((_ extract %d %d) state) #b1))", name.c_str(), get_id(module), statebv_width, statebv_width);
82 				statebv_width += 1;
83 			} else {
84 				decl_str = stringf("(define-fun |%s| ((state |%s_s|)) (_ BitVec %d) ((_ extract %d %d) state))", name.c_str(), get_id(module), width, statebv_width+width-1, statebv_width);
85 				statebv_width += width;
86 			}
87 		}
88 		else if (statedt)
89 		{
90 			if (width == 0) {
91 				decl_str = stringf("  (|%s| Bool)", name.c_str());
92 			} else {
93 				decl_str = stringf("  (|%s| (_ BitVec %d))", name.c_str(), width);
94 			}
95 		}
96 		else
97 		{
98 			if (width == 0) {
99 				decl_str = stringf("(declare-fun |%s| (|%s_s|) Bool)", name.c_str(), get_id(module));
100 			} else {
101 				decl_str = stringf("(declare-fun |%s| (|%s_s|) (_ BitVec %d))", name.c_str(), get_id(module), width);
102 			}
103 		}
104 
105 		if (!comment.empty())
106 			decl_str += " ; " + comment;
107 
108 		if (statedt)
109 			dtmembers.push_back(decl_str + "\n");
110 		else
111 			decls.push_back(decl_str + "\n");
112 	}
113 
Smt2WorkerSmt2Worker114 	Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, bool forallmode,
115 			dict<IdString, int> &mod_stbv_width, dict<IdString, dict<IdString, pair<bool, bool>>> &mod_clk_cache) :
116 			ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode),
117 			verbose(verbose), statebv(statebv), statedt(statedt), forallmode(forallmode), mod_stbv_width(mod_stbv_width)
118 	{
119 		pool<SigBit> noclock;
120 
121 		makebits(stringf("%s_is", get_id(module)));
122 
123 		dict<IdString, Mem*> mem_dict;
124 		memories = Mem::get_all_memories(module);
125 		for (auto &mem : memories)
126 		{
127 			mem.narrow();
128 			mem_dict[mem.memid] = &mem;
129 			for (auto &port : mem.wr_ports)
130 			{
131 				if (port.clk_enable) {
132 					SigSpec clk = sigmap(port.clk);
133 					for (int i = 0; i < GetSize(clk); i++)
134 					{
135 						if (clk[i].wire == nullptr)
136 							continue;
137 						if (port.clk_polarity)
138 							clock_posedge.insert(clk[i]);
139 						else
140 							clock_negedge.insert(clk[i]);
141 					}
142 				}
143 				for (auto bit : sigmap(port.en))
144 					noclock.insert(bit);
145 				for (auto bit : sigmap(port.addr))
146 					noclock.insert(bit);
147 				for (auto bit : sigmap(port.data))
148 					noclock.insert(bit);
149 			}
150 			for (auto &port : mem.rd_ports)
151 			{
152 				if (port.clk_enable) {
153 					SigSpec clk = sigmap(port.clk);
154 					for (int i = 0; i < GetSize(clk); i++)
155 					{
156 						if (clk[i].wire == nullptr)
157 							continue;
158 						if (port.clk_polarity)
159 							clock_posedge.insert(clk[i]);
160 						else
161 							clock_negedge.insert(clk[i]);
162 					}
163 				}
164 				for (auto bit : sigmap(port.en))
165 					noclock.insert(bit);
166 				for (auto bit : sigmap(port.addr))
167 					noclock.insert(bit);
168 				for (auto bit : sigmap(port.data))
169 					noclock.insert(bit);
170 				Cell *driver = port.cell ? port.cell : mem.cell;
171 				for (auto bit : sigmap(port.data)) {
172 					if (bit_driver.count(bit))
173 						log_error("Found multiple drivers for %s.\n", log_signal(bit));
174 					bit_driver[bit] = driver;
175 				}
176 			}
177 		}
178 
179 		for (auto cell : module->cells())
180 		for (auto &conn : cell->connections())
181 		{
182 			if (GetSize(conn.second) == 0)
183 				continue;
184 
185 			// Handled above.
186 			if (cell->is_mem_cell()) {
187 				mem_cells[cell] = mem_dict[cell->parameters.at(ID::MEMID).decode_string()];
188 				continue;
189 			}
190 
191 			bool is_input = ct.cell_input(cell->type, conn.first);
192 			bool is_output = ct.cell_output(cell->type, conn.first);
193 
194 			if (is_output && !is_input)
195 				for (auto bit : sigmap(conn.second)) {
196 					if (bit_driver.count(bit))
197 						log_error("Found multiple drivers for %s.\n", log_signal(bit));
198 					bit_driver[bit] = cell;
199 				}
200 			else if (is_output || !is_input)
201 				log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n",
202 						log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type));
203 
204 			if (cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)) && conn.first.in(ID::CLK, ID::C))
205 			{
206 				bool posedge = (cell->type == ID($_DFF_N_)) || (cell->type == ID($dff) && cell->getParam(ID::CLK_POLARITY).as_bool());
207 				for (auto bit : sigmap(conn.second)) {
208 					if (posedge)
209 						clock_posedge.insert(bit);
210 					else
211 						clock_negedge.insert(bit);
212 				}
213 			}
214 			else
215 			if (mod_clk_cache.count(cell->type) && mod_clk_cache.at(cell->type).count(conn.first))
216 			{
217 				for (auto bit : sigmap(conn.second)) {
218 					if (mod_clk_cache.at(cell->type).at(conn.first).first)
219 						clock_posedge.insert(bit);
220 					if (mod_clk_cache.at(cell->type).at(conn.first).second)
221 						clock_negedge.insert(bit);
222 				}
223 			}
224 			else
225 			{
226 				for (auto bit : sigmap(conn.second))
227 					noclock.insert(bit);
228 			}
229 		}
230 
231 		for (auto bit : noclock) {
232 			clock_posedge.erase(bit);
233 			clock_negedge.erase(bit);
234 		}
235 
236 		for (auto wire : module->wires())
237 		{
238 			if (!wire->port_input || GetSize(wire) != 1)
239 				continue;
240 			SigBit bit = sigmap(wire);
241 			if (clock_posedge.count(bit))
242 				mod_clk_cache[module->name][wire->name].first = true;
243 			if (clock_negedge.count(bit))
244 				mod_clk_cache[module->name][wire->name].second = true;
245 		}
246 	}
247 
~Smt2WorkerSmt2Worker248 	~Smt2Worker()
249 	{
250 		for (auto &it : ids)
251 			free(it.second);
252 		ids.clear();
253 	}
254 
get_idSmt2Worker255 	const char *get_id(Module *m)
256 	{
257 		return get_id(m->name);
258 	}
259 
get_idSmt2Worker260 	const char *get_id(Cell *c)
261 	{
262 		return get_id(c->name);
263 	}
264 
get_idSmt2Worker265 	const char *get_id(Wire *w)
266 	{
267 		return get_id(w->name);
268 	}
269 
register_boolSmt2Worker270 	void register_bool(RTLIL::SigBit bit, int id)
271 	{
272 		if (verbose) log("%*s-> register_bool: %s %d\n", 2+2*GetSize(recursive_cells), "",
273 				log_signal(bit), id);
274 
275 		sigmap.apply(bit);
276 		log_assert(fcache.count(bit) == 0);
277 		fcache[bit] = std::pair<int, int>(id, -1);
278 	}
279 
register_bvSmt2Worker280 	void register_bv(RTLIL::SigSpec sig, int id)
281 	{
282 		if (verbose) log("%*s-> register_bv: %s %d\n", 2+2*GetSize(recursive_cells), "",
283 				log_signal(sig), id);
284 
285 		log_assert(bvmode);
286 		sigmap.apply(sig);
287 
288 		log_assert(bvsizes.count(id) == 0);
289 		bvsizes[id] = GetSize(sig);
290 
291 		for (int i = 0; i < GetSize(sig); i++) {
292 			log_assert(fcache.count(sig[i]) == 0);
293 			fcache[sig[i]] = std::pair<int, int>(id, i);
294 		}
295 	}
296 
register_boolvecSmt2Worker297 	void register_boolvec(RTLIL::SigSpec sig, int id)
298 	{
299 		if (verbose) log("%*s-> register_boolvec: %s %d\n", 2+2*GetSize(recursive_cells), "",
300 				log_signal(sig), id);
301 
302 		log_assert(bvmode);
303 		sigmap.apply(sig);
304 		register_bool(sig[0], id);
305 
306 		for (int i = 1; i < GetSize(sig); i++)
307 			sigmap.add(sig[i], RTLIL::State::S0);
308 	}
309 
get_boolSmt2Worker310 	std::string get_bool(RTLIL::SigBit bit, const char *state_name = "state")
311 	{
312 		sigmap.apply(bit);
313 
314 		if (bit.wire == nullptr)
315 			return bit == RTLIL::State::S1 ? "true" : "false";
316 
317 		if (bit_driver.count(bit))
318 			export_cell(bit_driver.at(bit));
319 		sigmap.apply(bit);
320 
321 		if (fcache.count(bit) == 0) {
322 			if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "",
323 					log_signal(bit));
324 			makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(bit));
325 			register_bool(bit, idcounter++);
326 		}
327 
328 		auto f = fcache.at(bit);
329 		if (f.second >= 0)
330 			return stringf("(= ((_ extract %d %d) (|%s#%d| %s)) #b1)", f.second, f.second, get_id(module), f.first, state_name);
331 		return stringf("(|%s#%d| %s)", get_id(module), f.first, state_name);
332 	}
333 
get_boolSmt2Worker334 	std::string get_bool(RTLIL::SigSpec sig, const char *state_name = "state")
335 	{
336 		return get_bool(sig.as_bit(), state_name);
337 	}
338 
get_bvSmt2Worker339 	std::string get_bv(RTLIL::SigSpec sig, const char *state_name = "state")
340 	{
341 		log_assert(bvmode);
342 		sigmap.apply(sig);
343 
344 		std::vector<std::string> subexpr;
345 
346 		SigSpec orig_sig;
347 		while (orig_sig != sig) {
348 			for (auto bit : sig)
349 				if (bit_driver.count(bit))
350 					export_cell(bit_driver.at(bit));
351 			orig_sig = sig;
352 			sigmap.apply(sig);
353 		}
354 
355 		for (int i = 0, j = 1; i < GetSize(sig); i += j, j = 1)
356 		{
357 			if (sig[i].wire == nullptr) {
358 				while (i+j < GetSize(sig) && sig[i+j].wire == nullptr) j++;
359 				subexpr.push_back("#b");
360 				for (int k = i+j-1; k >= i; k--)
361 					subexpr.back() += sig[k] == RTLIL::State::S1 ? "1" : "0";
362 				continue;
363 			}
364 
365 			if (fcache.count(sig[i]) && fcache.at(sig[i]).second == -1) {
366 				subexpr.push_back(stringf("(ite %s #b1 #b0)", get_bool(sig[i], state_name).c_str()));
367 				continue;
368 			}
369 
370 			if (fcache.count(sig[i])) {
371 				auto t1 = fcache.at(sig[i]);
372 				while (i+j < GetSize(sig)) {
373 					if (fcache.count(sig[i+j]) == 0)
374 						break;
375 					auto t2 = fcache.at(sig[i+j]);
376 					if (t1.first != t2.first)
377 						break;
378 					if (t1.second+j != t2.second)
379 						break;
380 					j++;
381 				}
382 				if (t1.second == 0 && j == bvsizes.at(t1.first))
383 					subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), t1.first, state_name));
384 				else
385 					subexpr.push_back(stringf("((_ extract %d %d) (|%s#%d| %s))",
386 							t1.second + j - 1, t1.second, get_id(module), t1.first, state_name));
387 				continue;
388 			}
389 
390 			std::set<RTLIL::SigBit> seen_bits = { sig[i] };
391 			while (i+j < GetSize(sig) && sig[i+j].wire && !fcache.count(sig[i+j]) && !seen_bits.count(sig[i+j]))
392 				seen_bits.insert(sig[i+j]), j++;
393 
394 			if (verbose) log("%*s-> external bv: %s\n", 2+2*GetSize(recursive_cells), "",
395 					log_signal(sig.extract(i, j)));
396 			for (auto bit : sig.extract(i, j))
397 				log_assert(bit_driver.count(bit) == 0);
398 			makebits(stringf("%s#%d", get_id(module), idcounter), j, log_signal(sig.extract(i, j)));
399 			subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), idcounter, state_name));
400 			register_bv(sig.extract(i, j), idcounter++);
401 		}
402 
403 		if (GetSize(subexpr) > 1) {
404 			std::string expr = "", end_str = "";
405 			for (int i = GetSize(subexpr)-1; i >= 0; i--) {
406 				if (i > 0) expr += " (concat", end_str += ")";
407 				expr += " " + subexpr[i];
408 			}
409 			return expr.substr(1) + end_str;
410 		} else {
411 			log_assert(GetSize(subexpr) == 1);
412 			return subexpr[0];
413 		}
414 	}
415 
export_gateSmt2Worker416 	void export_gate(RTLIL::Cell *cell, std::string expr)
417 	{
418 		RTLIL::SigBit bit = sigmap(cell->getPort(ID::Y).as_bit());
419 		std::string processed_expr;
420 
421 		for (char ch : expr) {
422 			if (ch == 'A') processed_expr += get_bool(cell->getPort(ID::A));
423 			else if (ch == 'B') processed_expr += get_bool(cell->getPort(ID::B));
424 			else if (ch == 'C') processed_expr += get_bool(cell->getPort(ID::C));
425 			else if (ch == 'D') processed_expr += get_bool(cell->getPort(ID::D));
426 			else if (ch == 'S') processed_expr += get_bool(cell->getPort(ID::S));
427 			else processed_expr += ch;
428 		}
429 
430 		if (verbose)
431 			log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
432 
433 		decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
434 				get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(bit)));
435 		register_bool(bit, idcounter++);
436 		recursive_cells.erase(cell);
437 	}
438 
export_bvopSmt2Worker439 	void export_bvop(RTLIL::Cell *cell, std::string expr, char type = 0)
440 	{
441 		RTLIL::SigSpec sig_a, sig_b;
442 		RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y));
443 		bool is_signed = cell->getParam(ID::A_SIGNED).as_bool();
444 		int width = GetSize(sig_y);
445 
446 		if (type == 's' || type == 'd' || type == 'b') {
447 			width = max(width, GetSize(cell->getPort(ID::A)));
448 			if (cell->hasPort(ID::B))
449 				width = max(width, GetSize(cell->getPort(ID::B)));
450 		}
451 
452 		if (cell->hasPort(ID::A)) {
453 			sig_a = cell->getPort(ID::A);
454 			sig_a.extend_u0(width, is_signed);
455 		}
456 
457 		if (cell->hasPort(ID::B)) {
458 			sig_b = cell->getPort(ID::B);
459 			sig_b.extend_u0(width, is_signed && !(type == 's'));
460 		}
461 
462 		std::string processed_expr;
463 
464 		for (char ch : expr) {
465 			if (ch == 'A') processed_expr += get_bv(sig_a);
466 			else if (ch == 'B') processed_expr += get_bv(sig_b);
467 			else if (ch == 'P') processed_expr += get_bv(cell->getPort(ID::B));
468 			else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
469 			else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
470 			else processed_expr += ch;
471 		}
472 
473 		if (width != GetSize(sig_y) && type != 'b')
474 			processed_expr = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, processed_expr.c_str());
475 
476 		if (verbose)
477 			log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
478 
479 		if (type == 'b') {
480 			decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
481 					get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(sig_y)));
482 			register_boolvec(sig_y, idcounter++);
483 		} else {
484 			decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
485 					get_id(module), idcounter, get_id(module), GetSize(sig_y), processed_expr.c_str(), log_signal(sig_y)));
486 			register_bv(sig_y, idcounter++);
487 		}
488 
489 		recursive_cells.erase(cell);
490 	}
491 
export_reduceSmt2Worker492 	void export_reduce(RTLIL::Cell *cell, std::string expr, bool identity_val)
493 	{
494 		RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y));
495 		std::string processed_expr;
496 
497 		for (char ch : expr)
498 			if (ch == 'A' || ch == 'B') {
499 				RTLIL::SigSpec sig = sigmap(cell->getPort(stringf("\\%c", ch)));
500 				for (auto bit : sig)
501 					processed_expr += " " + get_bool(bit);
502 				if (GetSize(sig) == 1)
503 					processed_expr += identity_val ? " true" : " false";
504 			} else
505 				processed_expr += ch;
506 
507 		if (verbose)
508 			log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
509 
510 		decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
511 				get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(sig_y)));
512 		register_boolvec(sig_y, idcounter++);
513 		recursive_cells.erase(cell);
514 	}
515 
export_cellSmt2Worker516 	void export_cell(RTLIL::Cell *cell)
517 	{
518 		if (verbose)
519 			log("%*s=> export_cell %s (%s) [%s]\n", 2+2*GetSize(recursive_cells), "",
520 					log_id(cell), log_id(cell->type), exported_cells.count(cell) ? "old" : "new");
521 
522 		if (recursive_cells.count(cell))
523 			log_error("Found logic loop in module %s! See cell %s.\n", get_id(module), get_id(cell));
524 
525 		if (exported_cells.count(cell))
526 			return;
527 
528 		exported_cells.insert(cell);
529 		recursive_cells.insert(cell);
530 
531 		if (cell->type == ID($initstate))
532 		{
533 			SigBit bit = sigmap(cell->getPort(ID::Y).as_bit());
534 			decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (|%s_is| state)) ; %s\n",
535 					get_id(module), idcounter, get_id(module), get_id(module), log_signal(bit)));
536 			register_bool(bit, idcounter++);
537 			recursive_cells.erase(cell);
538 			return;
539 		}
540 
541 		if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_)))
542 		{
543 			registers.insert(cell);
544 			makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort(ID::Q)));
545 			register_bool(cell->getPort(ID::Q), idcounter++);
546 			recursive_cells.erase(cell);
547 			return;
548 		}
549 
550 		if (cell->type == ID($_BUF_)) return export_gate(cell, "A");
551 		if (cell->type == ID($_NOT_)) return export_gate(cell, "(not A)");
552 		if (cell->type == ID($_AND_)) return export_gate(cell, "(and A B)");
553 		if (cell->type == ID($_NAND_)) return export_gate(cell, "(not (and A B))");
554 		if (cell->type == ID($_OR_)) return export_gate(cell, "(or A B)");
555 		if (cell->type == ID($_NOR_)) return export_gate(cell, "(not (or A B))");
556 		if (cell->type == ID($_XOR_)) return export_gate(cell, "(xor A B)");
557 		if (cell->type == ID($_XNOR_)) return export_gate(cell, "(not (xor A B))");
558 		if (cell->type == ID($_ANDNOT_)) return export_gate(cell, "(and A (not B))");
559 		if (cell->type == ID($_ORNOT_)) return export_gate(cell, "(or A (not B))");
560 		if (cell->type == ID($_MUX_)) return export_gate(cell, "(ite S B A)");
561 		if (cell->type == ID($_NMUX_)) return export_gate(cell, "(not (ite S B A))");
562 		if (cell->type == ID($_AOI3_)) return export_gate(cell, "(not (or (and A B) C))");
563 		if (cell->type == ID($_OAI3_)) return export_gate(cell, "(not (and (or A B) C))");
564 		if (cell->type == ID($_AOI4_)) return export_gate(cell, "(not (or (and A B) (and C D)))");
565 		if (cell->type == ID($_OAI4_)) return export_gate(cell, "(not (and (or A B) (or C D)))");
566 
567 		// FIXME: $lut
568 
569 		if (bvmode)
570 		{
571 			if (cell->type.in(ID($ff), ID($dff)))
572 			{
573 				registers.insert(cell);
574 				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q)));
575 				register_bv(cell->getPort(ID::Q), idcounter++);
576 				recursive_cells.erase(cell);
577 				return;
578 			}
579 
580 			if (cell->type.in(ID($anyconst), ID($anyseq), ID($allconst), ID($allseq)))
581 			{
582 				registers.insert(cell);
583 				string infostr = cell->attributes.count(ID::src) ? cell->attributes.at(ID::src).decode_string().c_str() : get_id(cell);
584 				if (cell->attributes.count(ID::reg))
585 					infostr += " " + cell->attributes.at(ID::reg).decode_string();
586 				decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort(ID::Y)), infostr.c_str()));
587 				if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::maximize)){
588 					decls.push_back(stringf("; yosys-smt2-maximize %s#%d\n", get_id(module), idcounter));
589 					log("Wire %s is maximized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str());
590 				}
591 				else if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::minimize)){
592 					decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter));
593 					log("Wire %s is minimized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str());
594 				}
595 				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Y)), log_signal(cell->getPort(ID::Y)));
596 				if (cell->type == ID($anyseq))
597 					ex_input_eq.push_back(stringf("  (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter));
598 				register_bv(cell->getPort(ID::Y), idcounter++);
599 				recursive_cells.erase(cell);
600 				return;
601 			}
602 
603 			if (cell->type == ID($and)) return export_bvop(cell, "(bvand A B)");
604 			if (cell->type == ID($or)) return export_bvop(cell, "(bvor A B)");
605 			if (cell->type == ID($xor)) return export_bvop(cell, "(bvxor A B)");
606 			if (cell->type == ID($xnor)) return export_bvop(cell, "(bvxnor A B)");
607 
608 			if (cell->type == ID($shl)) return export_bvop(cell, "(bvshl A B)", 's');
609 			if (cell->type == ID($shr)) return export_bvop(cell, "(bvlshr A B)", 's');
610 			if (cell->type == ID($sshl)) return export_bvop(cell, "(bvshl A B)", 's');
611 			if (cell->type == ID($sshr)) return export_bvop(cell, "(bvLshr A B)", 's');
612 
613 			if (cell->type.in(ID($shift), ID($shiftx))) {
614 				if (cell->getParam(ID::B_SIGNED).as_bool()) {
615 					return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) "
616 							"(bvlshr A B) (bvlshr A (bvneg B)))",
617 							GetSize(cell->getPort(ID::B)), 0), 's');
618 				} else {
619 					return export_bvop(cell, "(bvlshr A B)", 's');
620 				}
621 			}
622 
623 			if (cell->type == ID($lt)) return export_bvop(cell, "(bvUlt A B)", 'b');
624 			if (cell->type == ID($le)) return export_bvop(cell, "(bvUle A B)", 'b');
625 			if (cell->type == ID($ge)) return export_bvop(cell, "(bvUge A B)", 'b');
626 			if (cell->type == ID($gt)) return export_bvop(cell, "(bvUgt A B)", 'b');
627 
628 			if (cell->type == ID($ne)) return export_bvop(cell, "(distinct A B)", 'b');
629 			if (cell->type == ID($nex)) return export_bvop(cell, "(distinct A B)", 'b');
630 			if (cell->type == ID($eq)) return export_bvop(cell, "(= A B)", 'b');
631 			if (cell->type == ID($eqx)) return export_bvop(cell, "(= A B)", 'b');
632 
633 			if (cell->type == ID($not)) return export_bvop(cell, "(bvnot A)");
634 			if (cell->type == ID($pos)) return export_bvop(cell, "A");
635 			if (cell->type == ID($neg)) return export_bvop(cell, "(bvneg A)");
636 
637 			if (cell->type == ID($add)) return export_bvop(cell, "(bvadd A B)");
638 			if (cell->type == ID($sub)) return export_bvop(cell, "(bvsub A B)");
639 			if (cell->type == ID($mul)) return export_bvop(cell, "(bvmul A B)");
640 			if (cell->type == ID($div)) return export_bvop(cell, "(bvUdiv A B)", 'd');
641 			// "rem" = truncating modulo
642 			if (cell->type == ID($mod)) return export_bvop(cell, "(bvUrem A B)", 'd');
643 			// "mod" = flooring modulo
644 			if (cell->type == ID($modfloor)) {
645 				// bvumod doesn't exist because it's the same as bvurem
646 				if (cell->getParam(ID::A_SIGNED).as_bool()) {
647 					return export_bvop(cell, "(bvsmod A B)", 'd');
648 				} else {
649 					return export_bvop(cell, "(bvurem A B)", 'd');
650 				}
651 			}
652 
653 			if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool)) &&
654 					2*GetSize(cell->getPort(ID::A).chunks()) < GetSize(cell->getPort(ID::A))) {
655 				bool is_and = cell->type == ID($reduce_and);
656 				string bits(GetSize(cell->getPort(ID::A)), is_and ? '1' : '0');
657 				return export_bvop(cell, stringf("(%s A #b%s)", is_and ? "=" : "distinct", bits.c_str()), 'b');
658 			}
659 
660 			if (cell->type == ID($reduce_and)) return export_reduce(cell, "(and A)", true);
661 			if (cell->type == ID($reduce_or)) return export_reduce(cell, "(or A)", false);
662 			if (cell->type == ID($reduce_xor)) return export_reduce(cell, "(xor A)", false);
663 			if (cell->type == ID($reduce_xnor)) return export_reduce(cell, "(not (xor A))", false);
664 			if (cell->type == ID($reduce_bool)) return export_reduce(cell, "(or A)", false);
665 
666 			if (cell->type == ID($logic_not)) return export_reduce(cell, "(not (or A))", false);
667 			if (cell->type == ID($logic_and)) return export_reduce(cell, "(and (or A) (or B))", false);
668 			if (cell->type == ID($logic_or)) return export_reduce(cell, "(or A B)", false);
669 
670 			if (cell->type.in(ID($mux), ID($pmux)))
671 			{
672 				int width = GetSize(cell->getPort(ID::Y));
673 				std::string processed_expr = get_bv(cell->getPort(ID::A));
674 
675 				RTLIL::SigSpec sig_b = cell->getPort(ID::B);
676 				RTLIL::SigSpec sig_s = cell->getPort(ID::S);
677 				get_bv(sig_b);
678 				get_bv(sig_s);
679 
680 				for (int i = 0; i < GetSize(sig_s); i++)
681 					processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(),
682 							get_bv(sig_b.extract(i*width, width)).c_str(), processed_expr.c_str());
683 
684 				if (verbose)
685 					log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
686 
687 				RTLIL::SigSpec sig = sigmap(cell->getPort(ID::Y));
688 				decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
689 						get_id(module), idcounter, get_id(module), width, processed_expr.c_str(), log_signal(sig)));
690 				register_bv(sig, idcounter++);
691 				recursive_cells.erase(cell);
692 				return;
693 			}
694 
695 			// FIXME: $slice $concat
696 		}
697 
698 		if (memmode && cell->is_mem_cell())
699 		{
700 			Mem *mem = mem_cells[cell];
701 
702 			if (memarrays.count(mem)) {
703 				recursive_cells.erase(cell);
704 				return;
705 			}
706 
707 			int arrayid = idcounter++;
708 			memarrays[mem] = arrayid;
709 
710 			int abits = ceil_log2(mem->size);
711 
712 			bool has_sync_wr = false;
713 			bool has_async_wr = false;
714 			for (auto &port : mem->wr_ports) {
715 				if (port.clk_enable)
716 					has_sync_wr = true;
717 				else
718 					has_async_wr = true;
719 			}
720 			if (has_async_wr && has_sync_wr)
721 				log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module));
722 
723 			decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(mem->memid), abits, mem->width, GetSize(mem->rd_ports), GetSize(mem->wr_ports), has_async_wr ? "async" : "sync"));
724 
725 			string memstate;
726 			if (has_async_wr) {
727 				memstate = stringf("%s#%d#final", get_id(module), arrayid);
728 			} else {
729 				memstate = stringf("%s#%d#0", get_id(module), arrayid);
730 			}
731 
732 			if (statebv)
733 			{
734 				makebits(memstate, mem->width*mem->size, get_id(mem->memid));
735 				decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s| state))\n",
736 						get_id(module), get_id(mem->memid), get_id(module), mem->width*mem->size, memstate.c_str()));
737 
738 				for (int i = 0; i < GetSize(mem->rd_ports); i++)
739 				{
740 					auto &port = mem->rd_ports[i];
741 					SigSpec addr_sig = port.addr;
742 					addr_sig.extend_u0(abits);
743 					std::string addr = get_bv(addr_sig);
744 
745 					if (port.clk_enable)
746 						log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
747 								"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(port.data), log_id(mem->memid), log_id(module));
748 
749 					decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
750 							get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
751 
752 					std::string read_expr = "#b";
753 					for (int k = 0; k < mem->width; k++)
754 						read_expr += "0";
755 
756 					for (int k = 0; k < mem->size; k++)
757 						read_expr = stringf("(ite (= (|%s_m:R%dA %s| state) #b%s) ((_ extract %d %d) (|%s| state))\n  %s)",
758 								get_id(module), i, get_id(mem->memid), Const(k+mem->start_offset, abits).as_string().c_str(),
759 								mem->width*(k+1)-1, mem->width*k, memstate.c_str(), read_expr.c_str());
760 
761 					decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d)\n  %s) ; %s\n",
762 							get_id(module), idcounter, get_id(module), mem->width, read_expr.c_str(), log_signal(port.data)));
763 
764 					decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n",
765 							get_id(module), i, get_id(mem->memid), get_id(module), mem->width, get_id(module), idcounter));
766 
767 					register_bv(port.data, idcounter++);
768 				}
769 			}
770 			else
771 			{
772 				if (statedt)
773 					dtmembers.push_back(stringf("  (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
774 							memstate.c_str(), abits, mem->width, get_id(mem->memid)));
775 				else
776 					decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
777 							memstate.c_str(), get_id(module), abits, mem->width, get_id(mem->memid)));
778 
779 				decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s| state))\n",
780 						get_id(module), get_id(mem->memid), get_id(module), abits, mem->width, memstate.c_str()));
781 
782 				for (int i = 0; i < GetSize(mem->rd_ports); i++)
783 				{
784 					auto &port = mem->rd_ports[i];
785 					SigSpec addr_sig = port.addr;
786 					addr_sig.extend_u0(abits);
787 					std::string addr = get_bv(addr_sig);
788 
789 					if (port.clk_enable)
790 						log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
791 								"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(port.data), log_id(mem->memid), log_id(module));
792 
793 					decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
794 							get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
795 
796 					decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s| state) (|%s_m:R%dA %s| state))) ; %s\n",
797 							get_id(module), idcounter, get_id(module), mem->width, memstate.c_str(), get_id(module), i, get_id(mem->memid), log_signal(port.data)));
798 
799 					decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n",
800 							get_id(module), i, get_id(mem->memid), get_id(module), mem->width, get_id(module), idcounter));
801 
802 					register_bv(port.data, idcounter++);
803 				}
804 			}
805 
806 			memory_queue.insert(mem);
807 			recursive_cells.erase(cell);
808 			return;
809 		}
810 
811 		Module *m = module->design->module(cell->type);
812 
813 		if (m != nullptr)
814 		{
815 			decls.push_back(stringf("; yosys-smt2-cell %s %s\n", get_id(cell->type), get_id(cell->name)));
816 			string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));
817 
818 			for (auto &conn : cell->connections())
819 			{
820 				if (GetSize(conn.second) == 0)
821 					continue;
822 
823 				Wire *w = m->wire(conn.first);
824 				SigSpec sig = sigmap(conn.second);
825 
826 				if (w->port_output && !w->port_input) {
827 					if (GetSize(w) > 1) {
828 						if (bvmode) {
829 							makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(w), log_signal(sig));
830 							register_bv(sig, idcounter++);
831 						} else {
832 							for (int i = 0; i < GetSize(w); i++) {
833 								makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(sig[i]));
834 								register_bool(sig[i], idcounter++);
835 							}
836 						}
837 					} else {
838 						makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(sig));
839 						register_bool(sig, idcounter++);
840 					}
841 				}
842 			}
843 
844 			if (statebv)
845 				makebits(stringf("%s_h %s", get_id(module), get_id(cell->name)), mod_stbv_width.at(cell->type));
846 			else if (statedt)
847 				dtmembers.push_back(stringf("  (|%s_h %s| |%s_s|)\n",
848 						get_id(module), get_id(cell->name), get_id(cell->type)));
849 			else
850 				decls.push_back(stringf("(declare-fun |%s_h %s| (|%s_s|) |%s_s|)\n",
851 						get_id(module), get_id(cell->name), get_id(module), get_id(cell->type)));
852 
853 			hiercells.insert(cell);
854 			hiercells_queue.insert(cell);
855 			recursive_cells.erase(cell);
856 			return;
857 		}
858 
859 		if (cell->type.in(ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)) || cell->type.str().substr(0, 6) == "$_SDFF" || (cell->type.str().substr(0, 6) == "$_DFFE" && cell->type.str().size() == 10)) {
860 			log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smt2`.\n",
861 					log_id(cell->type), log_id(module), log_id(cell));
862 		}
863 		if (cell->type.in(ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF" || cell->type.str().substr(0, 7) == "$_ALDFF") {
864 			log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smt2`.\n",
865 					log_id(cell->type), log_id(module), log_id(cell));
866 		}
867 		if (cell->type.in(ID($sr), ID($dlatch), ID($adlatch), ID($dlatchsr)) || cell->type.str().substr(0, 8) == "$_DLATCH" || cell->type.str().substr(0, 5) == "$_SR_") {
868 			log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_smt2`.\n",
869 					log_id(cell->type), log_id(module), log_id(cell));
870 		}
871 		log_error("Unsupported cell type %s for cell %s.%s.\n",
872 				log_id(cell->type), log_id(module), log_id(cell));
873 	}
874 
runSmt2Worker875 	void run()
876 	{
877 		if (verbose) log("=> export logic driving outputs\n");
878 
879 		pool<SigBit> reg_bits;
880 		for (auto cell : module->cells())
881 			if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) {
882 				// not using sigmap -- we want the net directly at the dff output
883 				for (auto bit : cell->getPort(ID::Q))
884 					reg_bits.insert(bit);
885 			}
886 
887 		for (auto wire : module->wires()) {
888 			bool is_register = false;
889 			for (auto bit : SigSpec(wire))
890 				if (reg_bits.count(bit))
891 					is_register = true;
892 			if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) {
893 				RTLIL::SigSpec sig = sigmap(wire);
894 				std::vector<std::string> comments;
895 				if (wire->port_input)
896 					comments.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width));
897 				if (wire->port_output)
898 					comments.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width));
899 				if (is_register)
900 					comments.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
901 				if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic()))
902 					comments.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
903 				if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
904 					comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
905 							clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
906 				if (bvmode && GetSize(sig) > 1) {
907 					std::string sig_bv = get_bv(sig);
908 					if (!comments.empty())
909 						decls.insert(decls.end(), comments.begin(), comments.end());
910 					decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
911 							get_id(module), get_id(wire), get_id(module), GetSize(sig), sig_bv.c_str()));
912 					if (wire->port_input)
913 						ex_input_eq.push_back(stringf("  (= (|%s_n %s| state) (|%s_n %s| other_state))",
914 								get_id(module), get_id(wire), get_id(module), get_id(wire)));
915 				} else {
916 					std::vector<std::string> sig_bool;
917 					for (int i = 0; i < GetSize(sig); i++) {
918 						sig_bool.push_back(get_bool(sig[i]));
919 					}
920 					if (!comments.empty())
921 						decls.insert(decls.end(), comments.begin(), comments.end());
922 					for (int i = 0; i < GetSize(sig); i++) {
923 						if (GetSize(sig) > 1) {
924 							decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
925 									get_id(module), get_id(wire), i, get_id(module), sig_bool[i].c_str()));
926 							if (wire->port_input)
927 								ex_input_eq.push_back(stringf("  (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))",
928 										get_id(module), get_id(wire), i, get_id(module), get_id(wire), i));
929 						} else {
930 							decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
931 									get_id(module), get_id(wire), get_id(module), sig_bool[i].c_str()));
932 							if (wire->port_input)
933 								ex_input_eq.push_back(stringf("  (= (|%s_n %s| state) (|%s_n %s| other_state))",
934 										get_id(module), get_id(wire), get_id(module), get_id(wire)));
935 						}
936 					}
937 				}
938 			}
939 		}
940 
941 		if (verbose) log("=> export logic associated with the initial state\n");
942 
943 		vector<string> init_list;
944 		for (auto wire : module->wires())
945 			if (wire->attributes.count(ID::init)) {
946 				RTLIL::SigSpec sig = sigmap(wire);
947 				Const val = wire->attributes.at(ID::init);
948 				val.bits.resize(GetSize(sig), State::Sx);
949 				if (bvmode && GetSize(sig) > 1) {
950 					Const mask(State::S1, GetSize(sig));
951 					bool use_mask = false;
952 					for (int i = 0; i < GetSize(sig); i++)
953 						if (val[i] != State::S0 && val[i] != State::S1) {
954 							val[i] = State::S0;
955 							mask[i] = State::S0;
956 							use_mask = true;
957 						}
958 					if (use_mask)
959 						init_list.push_back(stringf("(= (bvand %s #b%s) #b%s) ; %s", get_bv(sig).c_str(), mask.as_string().c_str(), val.as_string().c_str(), get_id(wire)));
960 					else
961 						init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), get_id(wire)));
962 				} else {
963 					for (int i = 0; i < GetSize(sig); i++)
964 						if (val[i] == State::S0 || val[i] == State::S1)
965 							init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val[i] == State::S1 ? "true" : "false", get_id(wire)));
966 				}
967 			}
968 
969 		if (verbose) log("=> export logic driving asserts\n");
970 
971 		int assert_id = 0, assume_id = 0, cover_id = 0;
972 		vector<string> assert_list, assume_list, cover_list;
973 
974 		for (auto cell : module->cells())
975 		{
976 			if (cell->type.in(ID($assert), ID($assume), ID($cover)))
977 			{
978 				int &id = cell->type == ID($assert) ? assert_id :
979 						cell->type == ID($assume) ? assume_id :
980 						cell->type == ID($cover) ? cover_id : *(int*)nullptr;
981 
982 				char postfix = cell->type == ID($assert) ? 'a' :
983 						cell->type == ID($assume) ? 'u' :
984 						cell->type == ID($cover) ? 'c' : 0;
985 
986 				string name_a = get_bool(cell->getPort(ID::A));
987 				string name_en = get_bool(cell->getPort(ID::EN));
988 				string infostr = (cell->name[0] == '$' && cell->attributes.count(ID::src)) ? cell->attributes.at(ID::src).decode_string() : get_id(cell);
989 				decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str()));
990 
991 				if (cell->type == ID($cover))
992 					decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
993 							get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
994 				else
995 					decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
996 							get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
997 
998 				if (cell->type == ID($assert))
999 					assert_list.push_back(stringf("(|%s_a %d| state)", get_id(module), id));
1000 				else if (cell->type == ID($assume))
1001 					assume_list.push_back(stringf("(|%s_u %d| state)", get_id(module), id));
1002 
1003 				id++;
1004 			}
1005 		}
1006 
1007 		if (verbose) log("=> export logic driving hierarchical cells\n");
1008 
1009 		for (auto cell : module->cells())
1010 			if (module->design->module(cell->type) != nullptr)
1011 				export_cell(cell);
1012 
1013 		while (!hiercells_queue.empty())
1014 		{
1015 			std::set<RTLIL::Cell*> queue;
1016 			queue.swap(hiercells_queue);
1017 
1018 			for (auto cell : queue)
1019 			{
1020 				string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));
1021 				Module *m = module->design->module(cell->type);
1022 				log_assert(m != nullptr);
1023 
1024 				hier.push_back(stringf("  (= (|%s_is| state) (|%s_is| %s))\n",
1025 						get_id(module), get_id(cell->type), cell_state.c_str()));
1026 
1027 				for (auto &conn : cell->connections())
1028 				{
1029 					if (GetSize(conn.second) == 0)
1030 						continue;
1031 
1032 					Wire *w = m->wire(conn.first);
1033 					SigSpec sig = sigmap(conn.second);
1034 
1035 					if (bvmode || GetSize(w) == 1) {
1036 						hier.push_back(stringf("  (= %s (|%s_n %s| %s)) ; %s.%s\n", (GetSize(w) > 1 ? get_bv(sig) : get_bool(sig)).c_str(),
1037 								get_id(cell->type), get_id(w), cell_state.c_str(), get_id(cell->type), get_id(w)));
1038 					} else {
1039 						for (int i = 0; i < GetSize(w); i++)
1040 							hier.push_back(stringf("  (= %s (|%s_n %s %d| %s)) ; %s.%s[%d]\n", get_bool(sig[i]).c_str(),
1041 									get_id(cell->type), get_id(w), i, cell_state.c_str(), get_id(cell->type), get_id(w), i));
1042 					}
1043 				}
1044 			}
1045 		}
1046 
1047 		for (int iter = 1; !registers.empty() || !memory_queue.empty(); iter++)
1048 		{
1049 			pool<Cell*> this_regs;
1050 			this_regs.swap(registers);
1051 
1052 			if (verbose) log("=> export logic driving registers [iteration %d]\n", iter);
1053 
1054 			for (auto cell : this_regs)
1055 			{
1056 				if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_)))
1057 				{
1058 					std::string expr_d = get_bool(cell->getPort(ID::D));
1059 					std::string expr_q = get_bool(cell->getPort(ID::Q), "next_state");
1060 					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort(ID::Q))));
1061 					ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort(ID::Q)).c_str(), get_bool(cell->getPort(ID::Q), "other_state").c_str()));
1062 				}
1063 
1064 				if (cell->type.in(ID($ff), ID($dff)))
1065 				{
1066 					std::string expr_d = get_bv(cell->getPort(ID::D));
1067 					std::string expr_q = get_bv(cell->getPort(ID::Q), "next_state");
1068 					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort(ID::Q))));
1069 					ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Q)).c_str(), get_bv(cell->getPort(ID::Q), "other_state").c_str()));
1070 				}
1071 
1072 				if (cell->type.in(ID($anyconst), ID($allconst)))
1073 				{
1074 					std::string expr_d = get_bv(cell->getPort(ID::Y));
1075 					std::string expr_q = get_bv(cell->getPort(ID::Y), "next_state");
1076 					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort(ID::Y))));
1077 					if (cell->type == ID($anyconst))
1078 						ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Y)).c_str(), get_bv(cell->getPort(ID::Y), "other_state").c_str()));
1079 				}
1080 			}
1081 
1082 			std::set<Mem*> this_mems;
1083 			this_mems.swap(memory_queue);
1084 
1085 			for (auto mem : this_mems)
1086 			{
1087 				int arrayid = memarrays.at(mem);
1088 
1089 				int abits = ceil_log2(mem->size);;
1090 
1091 				bool has_sync_wr = false;
1092 				bool has_async_wr = false;
1093 				for (auto &port : mem->wr_ports) {
1094 					if (port.clk_enable)
1095 						has_sync_wr = true;
1096 					else
1097 						has_async_wr = true;
1098 				}
1099 
1100 				string initial_memstate, final_memstate;
1101 
1102 				if (has_async_wr) {
1103 					log_assert(!has_sync_wr);
1104 					initial_memstate = stringf("%s#%d#0", get_id(module), arrayid);
1105 					final_memstate = stringf("%s#%d#final", get_id(module), arrayid);
1106 				}
1107 
1108 				if (statebv)
1109 				{
1110 					if (has_async_wr) {
1111 						makebits(final_memstate, mem->width*mem->size, get_id(mem->memid));
1112 					}
1113 
1114 					for (int i = 0; i < GetSize(mem->wr_ports); i++)
1115 					{
1116 						auto &port = mem->wr_ports[i];
1117 						SigSpec addr_sig = port.addr;
1118 						addr_sig.extend_u0(abits);
1119 
1120 						std::string addr = get_bv(addr_sig);
1121 						std::string data = get_bv(port.data);
1122 						std::string mask = get_bv(port.en);
1123 
1124 						decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
1125 								get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
1126 						addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(mem->memid));
1127 
1128 						decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
1129 								get_id(module), i, get_id(mem->memid), get_id(module), mem->width, data.c_str(), log_signal(port.data)));
1130 						data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(mem->memid));
1131 
1132 						decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
1133 								get_id(module), i, get_id(mem->memid), get_id(module), mem->width, mask.c_str(), log_signal(port.en)));
1134 						mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid));
1135 
1136 						std::string data_expr;
1137 
1138 						for (int k = mem->size-1; k >= 0; k--) {
1139 							std::string new_data = stringf("(bvor (bvand %s %s) (bvand ((_ extract %d %d) (|%s#%d#%d| state)) (bvnot %s)))",
1140 									data.c_str(), mask.c_str(), mem->width*(k+1)-1, mem->width*k, get_id(module), arrayid, i, mask.c_str());
1141 							data_expr += stringf("\n  (ite (= %s #b%s) %s ((_ extract %d %d) (|%s#%d#%d| state)))",
1142 									addr.c_str(), Const(k+mem->start_offset, abits).as_string().c_str(), new_data.c_str(),
1143 									mem->width*(k+1)-1, mem->width*k, get_id(module), arrayid, i);
1144 						}
1145 
1146 						decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (_ BitVec %d) (concat%s)) ; %s\n",
1147 								get_id(module), arrayid, i+1, get_id(module), mem->width*mem->size, data_expr.c_str(), get_id(mem->memid)));
1148 					}
1149 				}
1150 				else
1151 				{
1152 					if (has_async_wr) {
1153 						if (statedt)
1154 							dtmembers.push_back(stringf("  (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
1155 									initial_memstate.c_str(), abits, mem->width, get_id(mem->memid)));
1156 						else
1157 							decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
1158 									initial_memstate.c_str(), get_id(module), abits, mem->width, get_id(mem->memid)));
1159 					}
1160 
1161 					for (int i = 0; i < GetSize(mem->wr_ports); i++)
1162 					{
1163 						auto &port = mem->wr_ports[i];
1164 						SigSpec addr_sig = port.addr;
1165 						addr_sig.extend_u0(abits);
1166 
1167 						std::string addr = get_bv(addr_sig);
1168 						std::string data = get_bv(port.data);
1169 						std::string mask = get_bv(port.en);
1170 
1171 						decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
1172 								get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
1173 						addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(mem->memid));
1174 
1175 						decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
1176 								get_id(module), i, get_id(mem->memid), get_id(module), mem->width, data.c_str(), log_signal(port.data)));
1177 						data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(mem->memid));
1178 
1179 						decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
1180 								get_id(module), i, get_id(mem->memid), get_id(module), mem->width, mask.c_str(), log_signal(port.en)));
1181 						mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid));
1182 
1183 						data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
1184 								data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str());
1185 
1186 						decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) "
1187 								"(store (|%s#%d#%d| state) %s %s)) ; %s\n",
1188 								get_id(module), arrayid, i+1, get_id(module), abits, mem->width,
1189 								get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid)));
1190 					}
1191 				}
1192 
1193 				std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, GetSize(mem->wr_ports));
1194 				std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid);
1195 				trans.push_back(stringf("  (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(mem->memid)));
1196 				ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid));
1197 
1198 				if (has_async_wr)
1199 					hier.push_back(stringf("  (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(mem->memid)));
1200 
1201 				Const init_data = mem->get_init_data();
1202 
1203 				for (int i = 0; i < mem->size; i++)
1204 				{
1205 					if (i*mem->width >= GetSize(init_data))
1206 						break;
1207 
1208 					Const initword = init_data.extract(i*mem->width, mem->width, State::Sx);
1209 					Const initmask = initword;
1210 					bool gen_init_constr = false;
1211 
1212 					for (int k = 0; k < GetSize(initword); k++) {
1213 						if (initword[k] == State::S0 || initword[k] == State::S1) {
1214 							gen_init_constr = true;
1215 							initmask[k] = State::S1;
1216 						} else {
1217 							initmask[k] = State::S0;
1218 							initword[k] = State::S0;
1219 						}
1220 					}
1221 
1222 					if (gen_init_constr)
1223 					{
1224 						if (statebv)
1225 							/* FIXME */;
1226 						else
1227 							init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]",
1228 									get_id(module), arrayid, Const(i, abits).as_string().c_str(),
1229 									initmask.as_string().c_str(), initword.as_string().c_str(), get_id(mem->memid), i));
1230 					}
1231 				}
1232 			}
1233 		}
1234 
1235 		if (verbose) log("=> finalizing SMT2 representation of %s.\n", log_id(module));
1236 
1237 		for (auto c : hiercells) {
1238 			assert_list.push_back(stringf("(|%s_a| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name)));
1239 			assume_list.push_back(stringf("(|%s_u| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name)));
1240 			init_list.push_back(stringf("(|%s_i| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name)));
1241 			hier.push_back(stringf("  (|%s_h| (|%s_h %s| state))\n", get_id(c->type), get_id(module), get_id(c->name)));
1242 			trans.push_back(stringf("  (|%s_t| (|%s_h %s| state) (|%s_h %s| next_state))\n",
1243 					get_id(c->type), get_id(module), get_id(c->name), get_id(module), get_id(c->name)));
1244 			ex_state_eq.push_back(stringf("(|%s_ex_state_eq| (|%s_h %s| state) (|%s_h %s| other_state))\n",
1245 					get_id(c->type), get_id(module), get_id(c->name), get_id(module), get_id(c->name)));
1246 		}
1247 
1248 		if (forallmode)
1249 		{
1250 			string expr = ex_state_eq.empty() ? "true" : "(and";
1251 			if (!ex_state_eq.empty()) {
1252 				if (GetSize(ex_state_eq) == 1) {
1253 					expr = "\n  " + ex_state_eq.front() + "\n";
1254 				} else {
1255 					for (auto &str : ex_state_eq)
1256 						expr += stringf("\n  %s", str.c_str());
1257 					expr += "\n)";
1258 				}
1259 			}
1260 			decls.push_back(stringf("(define-fun |%s_ex_state_eq| ((state |%s_s|) (other_state |%s_s|)) Bool %s)\n",
1261 				get_id(module), get_id(module), get_id(module), expr.c_str()));
1262 
1263 			expr = ex_input_eq.empty() ? "true" : "(and";
1264 			if (!ex_input_eq.empty()) {
1265 				if (GetSize(ex_input_eq) == 1) {
1266 					expr = "\n  " + ex_input_eq.front() + "\n";
1267 				} else {
1268 					for (auto &str : ex_input_eq)
1269 						expr += stringf("\n  %s", str.c_str());
1270 					expr += "\n)";
1271 				}
1272 			}
1273 			decls.push_back(stringf("(define-fun |%s_ex_input_eq| ((state |%s_s|) (other_state |%s_s|)) Bool %s)\n",
1274 				get_id(module), get_id(module), get_id(module), expr.c_str()));
1275 		}
1276 
1277 		string assert_expr = assert_list.empty() ? "true" : "(and";
1278 		if (!assert_list.empty()) {
1279 			if (GetSize(assert_list) == 1) {
1280 				assert_expr = "\n  " + assert_list.front() + "\n";
1281 			} else {
1282 				for (auto &str : assert_list)
1283 					assert_expr += stringf("\n  %s", str.c_str());
1284 				assert_expr += "\n)";
1285 			}
1286 		}
1287 		decls.push_back(stringf("(define-fun |%s_a| ((state |%s_s|)) Bool %s)\n",
1288 				get_id(module), get_id(module), assert_expr.c_str()));
1289 
1290 		string assume_expr = assume_list.empty() ? "true" : "(and";
1291 		if (!assume_list.empty()) {
1292 			if (GetSize(assume_list) == 1) {
1293 				assume_expr = "\n  " + assume_list.front() + "\n";
1294 			} else {
1295 				for (auto &str : assume_list)
1296 					assume_expr += stringf("\n  %s", str.c_str());
1297 				assume_expr += "\n)";
1298 			}
1299 		}
1300 		decls.push_back(stringf("(define-fun |%s_u| ((state |%s_s|)) Bool %s)\n",
1301 				get_id(module), get_id(module), assume_expr.c_str()));
1302 
1303 		string init_expr = init_list.empty() ? "true" : "(and";
1304 		if (!init_list.empty()) {
1305 			if (GetSize(init_list) == 1) {
1306 				init_expr = "\n  " + init_list.front() + "\n";
1307 			} else {
1308 				for (auto &str : init_list)
1309 					init_expr += stringf("\n  %s", str.c_str());
1310 				init_expr += "\n)";
1311 			}
1312 		}
1313 		decls.push_back(stringf("(define-fun |%s_i| ((state |%s_s|)) Bool %s)\n",
1314 				get_id(module), get_id(module), init_expr.c_str()));
1315 	}
1316 
writeSmt2Worker1317 	void write(std::ostream &f)
1318 	{
1319 		f << stringf("; yosys-smt2-module %s\n", get_id(module));
1320 
1321 		if (statebv) {
1322 			f << stringf("(define-sort |%s_s| () (_ BitVec %d))\n", get_id(module), statebv_width);
1323 			mod_stbv_width[module->name] = statebv_width;
1324 		} else
1325 		if (statedt) {
1326 			f << stringf("(declare-datatype |%s_s| ((|%s_mk|\n", get_id(module), get_id(module));
1327 			for (auto it : dtmembers)
1328 				f << it;
1329 			f << stringf(")))\n");
1330 		} else
1331 			f << stringf("(declare-sort |%s_s| 0)\n", get_id(module));
1332 
1333 		for (auto it : decls)
1334 			f << it;
1335 
1336 		f << stringf("(define-fun |%s_h| ((state |%s_s|)) Bool ", get_id(module), get_id(module));
1337 		if (GetSize(hier) > 1) {
1338 			f << "(and\n";
1339 			for (auto it : hier)
1340 				f << it;
1341 			f << "))\n";
1342 		} else
1343 		if (GetSize(hier) == 1)
1344 			f << "\n" + hier.front() + ")\n";
1345 		else
1346 			f << "true)\n";
1347 
1348 		f << stringf("(define-fun |%s_t| ((state |%s_s|) (next_state |%s_s|)) Bool ", get_id(module), get_id(module), get_id(module));
1349 		if (GetSize(trans) > 1) {
1350 			f << "(and\n";
1351 			for (auto it : trans)
1352 				f << it;
1353 			f << "))";
1354 		} else
1355 		if (GetSize(trans) == 1)
1356 			f << "\n" + trans.front() + ")";
1357 		else
1358 			f << "true)";
1359 		f << stringf(" ; end of module %s\n", get_id(module));
1360 	}
1361 };
1362 
1363 struct Smt2Backend : public Backend {
Smt2BackendSmt2Backend1364 	Smt2Backend() : Backend("smt2", "write design to SMT-LIBv2 file") { }
helpSmt2Backend1365 	void help() override
1366 	{
1367 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1368 		log("\n");
1369 		log("    write_smt2 [options] [filename]\n");
1370 		log("\n");
1371 		log("Write a SMT-LIBv2 [1] description of the current design. For a module with name\n");
1372 		log("'<mod>' this will declare the sort '<mod>_s' (state of the module) and will\n");
1373 		log("define and declare functions operating on that state.\n");
1374 		log("\n");
1375 		log("The following SMT2 functions are generated for a module with name '<mod>'.\n");
1376 		log("Some declarations/definitions are printed with a special comment. A prover\n");
1377 		log("using the SMT2 files can use those comments to collect all relevant metadata\n");
1378 		log("about the design.\n");
1379 		log("\n");
1380 		log("    ; yosys-smt2-module <mod>\n");
1381 		log("    (declare-sort |<mod>_s| 0)\n");
1382 		log("        The sort representing a state of module <mod>.\n");
1383 		log("\n");
1384 		log("    (define-fun |<mod>_h| ((state |<mod>_s|)) Bool (...))\n");
1385 		log("        This function must be asserted for each state to establish the\n");
1386 		log("        design hierarchy.\n");
1387 		log("\n");
1388 		log("    ; yosys-smt2-input <wirename> <width>\n");
1389 		log("    ; yosys-smt2-output <wirename> <width>\n");
1390 		log("    ; yosys-smt2-register <wirename> <width>\n");
1391 		log("    ; yosys-smt2-wire <wirename> <width>\n");
1392 		log("    (define-fun |<mod>_n <wirename>| (|<mod>_s|) (_ BitVec <width>))\n");
1393 		log("    (define-fun |<mod>_n <wirename>| (|<mod>_s|) Bool)\n");
1394 		log("        For each port, register, and wire with the 'keep' attribute set an\n");
1395 		log("        accessor function is generated. Single-bit wires are returned as Bool,\n");
1396 		log("        multi-bit wires as BitVec.\n");
1397 		log("\n");
1398 		log("    ; yosys-smt2-cell <submod> <instancename>\n");
1399 		log("    (declare-fun |<mod>_h <instancename>| (|<mod>_s|) |<submod>_s|)\n");
1400 		log("        There is a function like that for each hierarchical instance. It\n");
1401 		log("        returns the sort that represents the state of the sub-module that\n");
1402 		log("        implements the instance.\n");
1403 		log("\n");
1404 		log("    (declare-fun |<mod>_is| (|<mod>_s|) Bool)\n");
1405 		log("        This function must be asserted 'true' for initial states, and 'false'\n");
1406 		log("        otherwise.\n");
1407 		log("\n");
1408 		log("    (define-fun |<mod>_i| ((state |<mod>_s|)) Bool (...))\n");
1409 		log("        This function must be asserted 'true' for initial states. For\n");
1410 		log("        non-initial states it must be left unconstrained.\n");
1411 		log("\n");
1412 		log("    (define-fun |<mod>_t| ((state |<mod>_s|) (next_state |<mod>_s|)) Bool (...))\n");
1413 		log("        This function evaluates to 'true' if the states 'state' and\n");
1414 		log("        'next_state' form a valid state transition.\n");
1415 		log("\n");
1416 		log("    (define-fun |<mod>_a| ((state |<mod>_s|)) Bool (...))\n");
1417 		log("        This function evaluates to 'true' if all assertions hold in the state.\n");
1418 		log("\n");
1419 		log("    (define-fun |<mod>_u| ((state |<mod>_s|)) Bool (...))\n");
1420 		log("        This function evaluates to 'true' if all assumptions hold in the state.\n");
1421 		log("\n");
1422 		log("    ; yosys-smt2-assert <id> <filename:linenum>\n");
1423 		log("    (define-fun |<mod>_a <id>| ((state |<mod>_s|)) Bool (...))\n");
1424 		log("        Each $assert cell is converted into one of this functions. The function\n");
1425 		log("        evaluates to 'true' if the assert statement holds in the state.\n");
1426 		log("\n");
1427 		log("    ; yosys-smt2-assume <id> <filename:linenum>\n");
1428 		log("    (define-fun |<mod>_u <id>| ((state |<mod>_s|)) Bool (...))\n");
1429 		log("        Each $assume cell is converted into one of this functions. The function\n");
1430 		log("        evaluates to 'true' if the assume statement holds in the state.\n");
1431 		log("\n");
1432 		log("    ; yosys-smt2-cover <id> <filename:linenum>\n");
1433 		log("    (define-fun |<mod>_c <id>| ((state |<mod>_s|)) Bool (...))\n");
1434 		log("        Each $cover cell is converted into one of this functions. The function\n");
1435 		log("        evaluates to 'true' if the cover statement is activated in the state.\n");
1436 		log("\n");
1437 		log("Options:\n");
1438 		log("\n");
1439 		log("    -verbose\n");
1440 		log("        this will print the recursive walk used to export the modules.\n");
1441 		log("\n");
1442 		log("    -stbv\n");
1443 		log("        Use a BitVec sort to represent a state instead of an uninterpreted\n");
1444 		log("        sort. As a side-effect this will prevent use of arrays to model\n");
1445 		log("        memories.\n");
1446 		log("\n");
1447 		log("    -stdt\n");
1448 		log("        Use SMT-LIB 2.6 style datatypes to represent a state instead of an\n");
1449 		log("        uninterpreted sort.\n");
1450 		log("\n");
1451 		log("    -nobv\n");
1452 		log("        disable support for BitVec (FixedSizeBitVectors theory). without this\n");
1453 		log("        option multi-bit wires are represented using the BitVec sort and\n");
1454 		log("        support for coarse grain cells (incl. arithmetic) is enabled.\n");
1455 		log("\n");
1456 		log("    -nomem\n");
1457 		log("        disable support for memories (via ArraysEx theory). this option is\n");
1458 		log("        implied by -nobv. only $mem cells without merged registers in\n");
1459 		log("        read ports are supported. call \"memory\" with -nordff to make sure\n");
1460 		log("        that no registers are merged into $mem read ports. '<mod>_m' functions\n");
1461 		log("        will be generated for accessing the arrays that are used to represent\n");
1462 		log("        memories.\n");
1463 		log("\n");
1464 		log("    -wires\n");
1465 		log("        create '<mod>_n' functions for all public wires. by default only ports,\n");
1466 		log("        registers, and wires with the 'keep' attribute are exported.\n");
1467 		log("\n");
1468 		log("    -tpl <template_file>\n");
1469 		log("        use the given template file. the line containing only the token '%%%%'\n");
1470 		log("        is replaced with the regular output of this command.\n");
1471 		log("\n");
1472 		log("    -solver-option <option> <value>\n");
1473 		log("        emit a `; yosys-smt2-solver-option` directive for yosys-smtbmc to write\n");
1474 		log("        the given option as a `(set-option ...)` command in the SMT-LIBv2.\n");
1475 		log("\n");
1476 		log("[1] For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David\n");
1477 		log("R. Cok's tutorial: https://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf\n");
1478 		log("\n");
1479 		log("---------------------------------------------------------------------------\n");
1480 		log("\n");
1481 		log("Example:\n");
1482 		log("\n");
1483 		log("Consider the following module (test.v). We want to prove that the output can\n");
1484 		log("never transition from a non-zero value to a zero value.\n");
1485 		log("\n");
1486 		log("        module test(input clk, output reg [3:0] y);\n");
1487 		log("          always @(posedge clk)\n");
1488 		log("            y <= (y << 1) | ^y;\n");
1489 		log("        endmodule\n");
1490 		log("\n");
1491 		log("For this proof we create the following template (test.tpl).\n");
1492 		log("\n");
1493 		log("        ; we need QF_UFBV for this proof\n");
1494 		log("        (set-logic QF_UFBV)\n");
1495 		log("\n");
1496 		log("        ; insert the auto-generated code here\n");
1497 		log("        %%%%\n");
1498 		log("\n");
1499 		log("        ; declare two state variables s1 and s2\n");
1500 		log("        (declare-fun s1 () test_s)\n");
1501 		log("        (declare-fun s2 () test_s)\n");
1502 		log("\n");
1503 		log("        ; state s2 is the successor of state s1\n");
1504 		log("        (assert (test_t s1 s2))\n");
1505 		log("\n");
1506 		log("        ; we are looking for a model with y non-zero in s1\n");
1507 		log("        (assert (distinct (|test_n y| s1) #b0000))\n");
1508 		log("\n");
1509 		log("        ; we are looking for a model with y zero in s2\n");
1510 		log("        (assert (= (|test_n y| s2) #b0000))\n");
1511 		log("\n");
1512 		log("        ; is there such a model?\n");
1513 		log("        (check-sat)\n");
1514 		log("\n");
1515 		log("The following yosys script will create a 'test.smt2' file for our proof:\n");
1516 		log("\n");
1517 		log("        read_verilog test.v\n");
1518 		log("        hierarchy -check; proc; opt; check -assert\n");
1519 		log("        write_smt2 -bv -tpl test.tpl test.smt2\n");
1520 		log("\n");
1521 		log("Running 'cvc4 test.smt2' will print 'unsat' because y can never transition\n");
1522 		log("from non-zero to zero in the test design.\n");
1523 		log("\n");
1524 	}
executeSmt2Backend1525 	void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
1526 	{
1527 		std::ifstream template_f;
1528 		bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false;
1529 		bool forallmode = false;
1530 		dict<std::string, std::string> solver_options;
1531 
1532 		log_header(design, "Executing SMT2 backend.\n");
1533 
1534 		size_t argidx;
1535 		for (argidx = 1; argidx < args.size(); argidx++)
1536 		{
1537 			if (args[argidx] == "-tpl" && argidx+1 < args.size()) {
1538 				template_f.open(args[++argidx]);
1539 				if (template_f.fail())
1540 					log_error("Can't open template file `%s'.\n", args[argidx].c_str());
1541 				continue;
1542 			}
1543 			if (args[argidx] == "-bv" || args[argidx] == "-mem") {
1544 				log_warning("Options -bv and -mem are now the default. Support for -bv and -mem will be removed in the future.\n");
1545 				continue;
1546 			}
1547 			if (args[argidx] == "-stbv") {
1548 				statebv = true;
1549 				statedt = false;
1550 				continue;
1551 			}
1552 			if (args[argidx] == "-stdt") {
1553 				statebv = false;
1554 				statedt = true;
1555 				continue;
1556 			}
1557 			if (args[argidx] == "-nobv") {
1558 				bvmode = false;
1559 				memmode = false;
1560 				continue;
1561 			}
1562 			if (args[argidx] == "-nomem") {
1563 				memmode = false;
1564 				continue;
1565 			}
1566 			if (args[argidx] == "-wires") {
1567 				wiresmode = true;
1568 				continue;
1569 			}
1570 			if (args[argidx] == "-verbose") {
1571 				verbose = true;
1572 				continue;
1573 			}
1574 			if (args[argidx] == "-solver-option" && argidx+2 < args.size()) {
1575 				solver_options.emplace(args[argidx+1], args[argidx+2]);
1576 				argidx += 2;
1577 				continue;
1578 			}
1579 			break;
1580 		}
1581 		extra_args(f, filename, args, argidx);
1582 
1583 		if (template_f.is_open()) {
1584 			std::string line;
1585 			while (std::getline(template_f, line)) {
1586 				int indent = 0;
1587 				while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t'))
1588 					indent++;
1589 				if (line.compare(indent, 2, "%%") == 0)
1590 					break;
1591 				*f << line << std::endl;
1592 			}
1593 		}
1594 
1595 		*f << stringf("; SMT-LIBv2 description generated by %s\n", yosys_version_str);
1596 
1597 		if (!bvmode)
1598 			*f << stringf("; yosys-smt2-nobv\n");
1599 
1600 		if (!memmode)
1601 			*f << stringf("; yosys-smt2-nomem\n");
1602 
1603 		if (statebv)
1604 			*f << stringf("; yosys-smt2-stbv\n");
1605 
1606 		if (statedt)
1607 			*f << stringf("; yosys-smt2-stdt\n");
1608 
1609 		for (auto &it : solver_options)
1610 			*f << stringf("; yosys-smt2-solver-option %s %s\n", it.first.c_str(), it.second.c_str());
1611 
1612 		std::vector<RTLIL::Module*> sorted_modules;
1613 
1614 		// extract module dependencies
1615 		std::map<RTLIL::Module*, std::set<RTLIL::Module*>> module_deps;
1616 		for (auto mod : design->modules()) {
1617 			module_deps[mod] = std::set<RTLIL::Module*>();
1618 			for (auto cell : mod->cells())
1619 				if (design->has(cell->type))
1620 					module_deps[mod].insert(design->module(cell->type));
1621 		}
1622 
1623 		// simple good-enough topological sort
1624 		// (O(n*m) on n elements and depth m)
1625 		while (module_deps.size() > 0) {
1626 			size_t sorted_modules_idx = sorted_modules.size();
1627 			for (auto &it : module_deps) {
1628 				for (auto &dep : it.second)
1629 					if (module_deps.count(dep) > 0)
1630 						goto not_ready_yet;
1631 				// log("Next in topological sort: %s\n", log_id(it.first->name));
1632 				sorted_modules.push_back(it.first);
1633 			not_ready_yet:;
1634 			}
1635 			if (sorted_modules_idx == sorted_modules.size())
1636 				log_error("Cyclic dependency between modules found! Cycle includes module %s.\n", log_id(module_deps.begin()->first->name));
1637 			while (sorted_modules_idx < sorted_modules.size())
1638 				module_deps.erase(sorted_modules.at(sorted_modules_idx++));
1639 		}
1640 
1641 		dict<IdString, int> mod_stbv_width;
1642 		dict<IdString, dict<IdString, pair<bool, bool>>> mod_clk_cache;
1643 		Module *topmod = design->top_module();
1644 		std::string topmod_id;
1645 
1646 		for (auto module : sorted_modules)
1647 			for (auto cell : module->cells())
1648 				if (cell->type.in(ID($allconst), ID($allseq)))
1649 					goto found_forall;
1650 		if (0) {
1651 	found_forall:
1652 			forallmode = true;
1653 			*f << stringf("; yosys-smt2-forall\n");
1654 			if (!statebv && !statedt)
1655 				log_error("Forall-exists problems are only supported in -stbv or -stdt mode.\n");
1656 		}
1657 
1658 		for (auto module : sorted_modules)
1659 		{
1660 			if (module->get_blackbox_attribute() || module->has_processes_warn())
1661 				continue;
1662 
1663 			log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
1664 
1665 			Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, forallmode, mod_stbv_width, mod_clk_cache);
1666 			worker.run();
1667 			worker.write(*f);
1668 
1669 			if (module == topmod)
1670 				topmod_id = worker.get_id(module);
1671 		}
1672 
1673 		if (topmod)
1674 			*f << stringf("; yosys-smt2-topmod %s\n", topmod_id.c_str());
1675 
1676 		*f << stringf("; end of yosys output\n");
1677 
1678 		if (template_f.is_open()) {
1679 			std::string line;
1680 			while (std::getline(template_f, line))
1681 				*f << line << std::endl;
1682 		}
1683 	}
1684 } Smt2Backend;
1685 
1686 PRIVATE_NAMESPACE_END
1687