aboutsummaryrefslogtreecommitdiffstats
path: root/kernel/macc.h
blob: 371f6737d32995b112b063f7688d20b83312b25e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
/*
 *  yosys -- Yosys Open SYnthesis Suite
 *
 *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
 *
 *  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.
 *
 */

#ifndef MACC_H
#define MACC_H

#include "kernel/yosys.h"

YOSYS_NAMESPACE_BEGIN

struct Macc
{
	struct port_t {
		RTLIL::SigSpec in_a, in_b;
		bool is_signed, do_subtract;
	};

	std::vector<port_t> ports;
	RTLIL::SigSpec bit_ports;

	void optimize(int width)
	{
		std::vector<port_t> new_ports;
		RTLIL::SigSpec new_bit_ports;
		RTLIL::Const off(0, width);

		for (auto &port : ports)
		{
			if (GetSize(port.in_a) == 0 && GetSize(port.in_b) == 0)
				continue;

			if (GetSize(port.in_a) < GetSize(port.in_b))
				std::swap(port.in_a, port.in_b);

			if (GetSize(port.in_a) == 1 && GetSize(port.in_b) == 0 && !port.is_signed && !port.do_subtract) {
				bit_ports.append(port.in_a);
				continue;
			}

			if (port.in_a.is_fully_const() && port.in_b.is_fully_const()) {
				RTLIL::Const v = port.in_a.as_const();
				if (GetSize(port.in_b))
					v = const_mul(v, port.in_b.as_const(), port.is_signed, port.is_signed, width);
				if (port.do_subtract)
					off = const_sub(off, v, port.is_signed, port.is_signed, width);
				else
					off = const_add(off, v, port.is_signed, port.is_signed, width);
				continue;
			}

			if (port.is_signed) {
				while (GetSize(port.in_a) > 1 && port.in_a[GetSize(port.in_a)-1] == port.in_a[GetSize(port.in_a)-2])
					port.in_a.remove(GetSize(port.in_a)-1);
				while (GetSize(port.in_b) > 1 && port.in_b[GetSize(port.in_b)-1] == port.in_b[GetSize(port.in_b)-2])
					port.in_b.remove(GetSize(port.in_b)-1);
			} else {
				while (GetSize(port.in_a) > 1 && port.in_a[GetSize(port.in_a)-1] == State::S0)
					port.in_a.remove(GetSize(port.in_a)-1);
				while (GetSize(port.in_b) > 1 && port.in_b[GetSize(port.in_b)-1] == State::S0)
					port.in_b.remove(GetSize(port.in_b)-1);
			}

			new_ports.push_back(port);
		}

		for (auto &bit : bit_ports)
			if (bit == State::S1)
				off = const_add(off, RTLIL::Const(1, width), false, false, width);
			else if (bit != State::S0)
				new_bit_ports.append(bit);

		if (off.as_bool()) {
			port_t port;
			port.in_a = off;
			port.is_signed = false;
			port.do_subtract = false;
			new_ports.push_back(port);
		}

		new_ports.swap(ports);
		bit_ports = new_bit_ports;
	}

	void from_cell(RTLIL::Cell *cell)
	{
		RTLIL::SigSpec port_a = cell->getPort(ID::A);

		ports.clear();
		bit_ports = cell->getPort(ID::B);

		std::vector<RTLIL::State> config_bits = cell->getParam(ID(CONFIG)).bits;
		int config_cursor = 0;

#ifndef NDEBUG
		int config_width = cell->getParam(ID(CONFIG_WIDTH)).as_int();
		log_assert(GetSize(config_bits) >= config_width);
#endif

		int num_bits = 0;
		if (config_bits[config_cursor++] == State::S1) num_bits |= 1;
		if (config_bits[config_cursor++] == State::S1) num_bits |= 2;
		if (config_bits[config_cursor++] == State::S1) num_bits |= 4;
		if (config_bits[config_cursor++] == State::S1) num_bits |= 8;

		int port_a_cursor = 0;
		while (port_a_cursor < GetSize(port_a))
		{
			log_assert(config_cursor + 2 + 2*num_bits <= config_width);

			port_t this_port;
			this_port.is_signed = config_bits[config_cursor++] == State::S1;
			this_port.do_subtract = config_bits[config_cursor++] == State::S1;

			int size_a = 0;
			for (int i = 0; i < num_bits; i++)
				if (config_bits[config_cursor++] == State::S1)
					size_a |= 1 << i;

			this_port.in_a = port_a.extract(port_a_cursor, size_a);
			port_a_cursor += size_a;

			int size_b = 0;
			for (int i = 0; i < num_bits; i++)
				if (config_bits[config_cursor++] == State::S1)
					size_b |= 1 << i;

			this_port.in_b = port_a.extract(port_a_cursor, size_b);
			port_a_cursor += size_b;

			if (size_a || size_b)
				ports.push_back(this_port);
		}

		log_assert(config_cursor == config_width);
		log_assert(port_a_cursor == GetSize(port_a));
	}

	void to_cell(RTLIL::Cell *cell) const
	{
		RTLIL::SigSpec port_a;
		std::vector<RTLIL::State> config_bits;
		int max_size = 0, num_bits = 0;

		for (auto &port : ports) {
			max_size = max(max_size, GetSize(port.in_a));
			max_size = max(max_size, GetSize(port.in_b));
		}

		while (max_size)
			num_bits++, max_size /= 2;

		log_assert(num_bits < 16);
		config_bits.push_back(num_bits & 1 ? State::S1 : State::S0);
		config_bits.push_back(num_bits & 2 ? State::S1 : State::S0);
		config_bits.push_back(num_bits & 4 ? State::S1 : State::S0);
		config_bits.push_back(num_bits & 8 ? State::S1 : State::S0);

		for (auto &port : ports)
		{
			if (GetSize(port.in_a) == 0)
				continue;

			config_bits.push_back(port.is_signed ? State::S1 : State::S0);
			config_bits.push_back(port.do_subtract ? State::S1 : State::S0);

			int size_a = GetSize(port.in_a);
			for (int i = 0; i < num_bits; i++)
				config_bits.push_back(size_a & (1 << i) ? State::S1 : State::S0);

			int size_b = GetSize(port.in_b);
			for (int i = 0; i < num_bits; i++)
				config_bits.push_back(size_b & (1 << i) ? State::S1 : State::S0);

			port_a.append(port.in_a);
			port_a.append(port.in_b);
		}

		cell->setPort(ID::A, port_a);
		cell->setPort(ID::B, bit_ports);
		cell->setParam(ID(CONFIG), config_bits);
		cell->setParam(ID(CONFIG_WIDTH), GetSize(config_bits));
		cell->setParam(ID(A_WIDTH), GetSize(port_a));
		cell->setParam(ID(B_WIDTH), GetSize(bit_ports));
	}

	bool eval(RTLIL::Const &result) const
	{
		for (auto &bit : result.bits)
			bit = State::S0;

		for (auto &port : ports)
		{
			if (!port.in_a.is_fully_const() || !port.in_b.is_fully_const())
				return false;

			RTLIL::Const summand;
			if (GetSize(port.in_b) == 0)
				summand = const_pos(port.in_a.as_const(), port.in_b.as_const(), port.is_signed, port.is_signed, GetSize(result));
			else
				summand = const_mul(port.in_a.as_const(), port.in_b.as_const(), port.is_signed, port.is_signed, GetSize(result));

			if (port.do_subtract)
				result = const_sub(result, summand, port.is_signed, port.is_signed, GetSize(result));
			else
				result = const_add(result, summand, port.is_signed, port.is_signed, GetSize(result));
		}

		for (auto bit : bit_ports) {
			if (bit.wire)
				return false;
			result = const_add(result, bit.data, false, false, GetSize(result));
		}

		return true;
	}

	Macc(RTLIL::Cell *cell = nullptr)
	{
		if (cell != nullptr)
			from_cell(cell);
	}
};

YOSYS_NAMESPACE_END

#endif
ht: bold } /* Keyword.Declaration */ .highlight .kn { color: #008800; font-weight: bold } /* Keyword.Namespace */ .highlight .kp { color: #008800 } /* Keyword.Pseudo */ .highlight .kr { color: #008800; font-weight: bold } /* Keyword.Reserved */ .highlight .kt { color: #888888; font-weight: bold } /* Keyword.Type */ .highlight .m { color: #0000DD; font-weight: bold } /* Literal.Number */ .highlight .s { color: #dd2200; background-color: #fff0f0 } /* Literal.String */ .highlight .na { color: #336699 } /* Name.Attribute */ .highlight .nb { color: #003388 } /* Name.Builtin */ .highlight .nc { color: #bb0066; font-weight: bold } /* Name.Class */ .highlight .no { color: #003366; font-weight: bold } /* Name.Constant */ .highlight .nd { color: #555555 } /* Name.Decorator */ .highlight .ne { color: #bb0066; font-weight: bold } /* Name.Exception */ .highlight .nf { color: #0066bb; font-weight: bold } /* Name.Function */ .highlight .nl { color: #336699; font-style: italic } /* Name.Label */ .highlight .nn { color: #bb0066; font-weight: bold } /* Name.Namespace */ .highlight .py { color: #336699; font-weight: bold } /* Name.Property */ .highlight .nt { color: #bb0066; font-weight: bold } /* Name.Tag */ .highlight .nv { color: #336699 } /* Name.Variable */ .highlight .ow { color: #008800 } /* Operator.Word */ .highlight .w { color: #bbbbbb } /* Text.Whitespace */ .highlight .mb { color: #0000DD; font-weight: bold } /* Literal.Number.Bin */ .highlight .mf { color: #0000DD; font-weight: bold } /* Literal.Number.Float */ .highlight .mh { color: #0000DD; font-weight: bold } /* Literal.Number.Hex */ .highlight .mi { color: #0000DD; font-weight: bold } /* Literal.Number.Integer */ .highlight .mo { color: #0000DD; font-weight: bold } /* Literal.Number.Oct */ .highlight .sa { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Affix */ .highlight .sb { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Backtick */ .highlight .sc { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Char */ .highlight .dl { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Delimiter */ .highlight .sd { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Doc */ .highlight .s2 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Double */ .highlight .se { color: #0044dd; background-color: #fff0f0 } /* Literal.String.Escape */ .highlight .sh { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Heredoc */ .highlight .si { color: #3333bb; background-color: #fff0f0 } /* Literal.String.Interpol */ .highlight .sx { color: #22bb22; background-color: #f0fff0 } /* Literal.String.Other */ .highlight .sr { color: #008800; background-color: #fff0ff } /* Literal.String.Regex */ .highlight .s1 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Single */ .highlight .ss { color: #aa6600; background-color: #fff0f0 } /* Literal.String.Symbol */ .highlight .bp { color: #003388 } /* Name.Builtin.Pseudo */ .highlight .fm { color: #0066bb; font-weight: bold } /* Name.Function.Magic */ .highlight .vc { color: #336699 } /* Name.Variable.Class */ .highlight .vg { color: #dd7700 } /* Name.Variable.Global */ .highlight .vi { color: #3333bb } /* Name.Variable.Instance */ .highlight .vm { color: #336699 } /* Name.Variable.Magic */ .highlight .il { color: #0000DD; font-weight: bold } /* Literal.Number.Integer.Long */
/*
 *  yosys -- Yosys Open SYnthesis Suite
 *
 *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
 *
 *  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/rtlil.h"
#include "kernel/register.h"
#include "kernel/sigtools.h"
#include "kernel/celltypes.h"
#include "kernel/log.h"
#include <string>

USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN

struct Smt2Worker
{
	CellTypes ct;
	SigMap sigmap;
	RTLIL::Module *module;
	bool bvmode, memmode, wiresmode, verbose, statebv, statedt, forallmode;
	dict<IdString, int> &mod_stbv_width;
	int idcounter = 0, statebv_width = 0;

	std::vector<std::string> decls, trans, hier, dtmembers;
	std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
	std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
	pool<Cell*> recursive_cells, registers;

	pool<SigBit> clock_posedge, clock_negedge;
	vector<string> ex_state_eq, ex_input_eq;

	std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
	std::map<Cell*, int> memarrays;
	std::map<int, int> bvsizes;
	dict<IdString, char*> ids;

	const char *get_id(IdString n)
	{
		if (ids.count(n) == 0) {
			std::string str = log_id(n);
			for (int i = 0; i < GetSize(str); i++) {
				if (str[i] == '\\')
					str[i] = '/';
			}
			ids[n] = strdup(str.c_str());
		}
		return ids[n];
	}

	template<typename T>
	const char *get_id(T *obj) {
		return get_id(obj->name);
	}

	void makebits(std::string name, int width = 0, std::string comment = std::string())
	{
		std::string decl_str;

		if (statebv)
		{
			if (width == 0) {
				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);
				statebv_width += 1;
			} else {
				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);
				statebv_width += width;
			}
		}
		else if (statedt)
		{
			if (width == 0) {
				decl_str = stringf("  (|%s| Bool)", name.c_str());
			} else {
				decl_str = stringf("  (|%s| (_ BitVec %d))", name.c_str(), width);
			}
		}
		else
		{
			if (width == 0) {
				decl_str = stringf("(declare-fun |%s| (|%s_s|) Bool)", name.c_str(), get_id(module));
			} else {
				decl_str = stringf("(declare-fun |%s| (|%s_s|) (_ BitVec %d))", name.c_str(), get_id(module), width);
			}
		}

		if (!comment.empty())
			decl_str += " ; " + comment;

		if (statedt)
			dtmembers.push_back(decl_str + "\n");
		else
			decls.push_back(decl_str + "\n");
	}

	Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, bool forallmode,
			dict<IdString, int> &mod_stbv_width, dict<IdString, dict<IdString, pair<bool, bool>>> &mod_clk_cache) :
			ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode),
			verbose(verbose), statebv(statebv), statedt(statedt), forallmode(forallmode), mod_stbv_width(mod_stbv_width)
	{
		pool<SigBit> noclock;

		makebits(stringf("%s_is", get_id(module)));

		for (auto cell : module->cells())
		for (auto &conn : cell->connections())
		{
			if (GetSize(conn.second) == 0)
				continue;

			bool is_input = ct.cell_input(cell->type, conn.first);
			bool is_output = ct.cell_output(cell->type, conn.first);

			if (is_output && !is_input)
				for (auto bit : sigmap(conn.second)) {
					if (bit_driver.count(bit))
						log_error("Found multiple drivers for %s.\n", log_signal(bit));
					bit_driver[bit] = cell;
				}
			else if (is_output || !is_input)
				log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n",
						log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type));

			if (cell->type.in("$mem") && conn.first.in("\\RD_CLK", "\\WR_CLK"))
			{
				SigSpec clk = sigmap(conn.second);
				for (int i = 0; i < GetSize(clk); i++)
				{
					if (clk[i].wire == nullptr)
						continue;

					if (cell->getParam(conn.first == "\\RD_CLK" ? "\\RD_CLK_ENABLE" : "\\WR_CLK_ENABLE")[i] != State::S1)
						continue;

					if (cell->getParam(conn.first == "\\RD_CLK" ? "\\RD_CLK_POLARITY" : "\\WR_CLK_POLARITY")[i] == State::S1)
						clock_posedge.insert(clk[i]);
					else
						clock_negedge.insert(clk[i]);
				}
			}
			else
			if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_") && conn.first.in("\\CLK", "\\C"))
			{
				bool posedge = (cell->type == "$_DFF_N_") || (cell->type == "$dff" && cell->getParam("\\CLK_POLARITY").as_bool());
				for (auto bit : sigmap(conn.second)) {
					if (posedge)
						clock_posedge.insert(bit);
					else
						clock_negedge.insert(bit);
				}
			}
			else
			if (mod_clk_cache.count(cell->type) && mod_clk_cache.at(cell->type).count(conn.first))
			{
				for (auto bit : sigmap(conn.second)) {
					if (mod_clk_cache.at(cell->type).at(conn.first).first)
						clock_posedge.insert(bit);
					if (mod_clk_cache.at(cell->type).at(conn.first).second)
						clock_negedge.insert(bit);
				}
			}
			else
			{
				for (auto bit : sigmap(conn.second))
					noclock.insert(bit);
			}
		}

		for (auto bit : noclock) {
			clock_posedge.erase(bit);
			clock_negedge.erase(bit);
		}

		for (auto wire : module->wires())
		{
			if (!wire->port_input || GetSize(wire) != 1)
				continue;
			SigBit bit = sigmap(wire);
			if (clock_posedge.count(bit))
				mod_clk_cache[module->name][wire->name].first = true;
			if (clock_negedge.count(bit))
				mod_clk_cache[module->name][wire->name].second = true;
		}
	}

	~Smt2Worker()
	{
		for (auto &it : ids)
			free(it.second);
		ids.clear();
	}

	const char *get_id(Module *m)
	{
		return get_id(m->name);
	}

	const char *get_id(Cell *c)
	{
		return get_id(c->name);
	}

	const char *get_id(Wire *w)
	{
		return get_id(w->name);
	}

	void register_bool(RTLIL::SigBit bit, int id)
	{
		if (verbose) log("%*s-> register_bool: %s %d\n", 2+2*GetSize(recursive_cells), "",
				log_signal(bit), id);

		sigmap.apply(bit);
		log_assert(fcache.count(bit) == 0);
		fcache[bit] = std::pair<int, int>(id, -1);
	}

	void register_bv(RTLIL::SigSpec sig, int id)
	{
		if (verbose) log("%*s-> register_bv: %s %d\n", 2+2*GetSize(recursive_cells), "",
				log_signal(sig), id);

		log_assert(bvmode);
		sigmap.apply(sig);

		log_assert(bvsizes.count(id) == 0);
		bvsizes[id] = GetSize(sig);

		for (int i = 0; i < GetSize(sig); i++) {
			log_assert(fcache.count(sig[i]) == 0);
			fcache[sig[i]] = std::pair<int, int>(id, i);
		}
	}

	void register_boolvec(RTLIL::SigSpec sig, int id)
	{
		if (verbose) log("%*s-> register_boolvec: %s %d\n", 2+2*GetSize(recursive_cells), "",
				log_signal(sig), id);

		log_assert(bvmode);
		sigmap.apply(sig);
		register_bool(sig[0], id);

		for (int i = 1; i < GetSize(sig); i++)
			sigmap.add(sig[i], RTLIL::State::S0);
	}

	std::string get_bool(RTLIL::SigBit bit, const char *state_name = "state")
	{
		sigmap.apply(bit);

		if (bit.wire == nullptr)
			return bit == RTLIL::State::S1 ? "true" : "false";

		if (bit_driver.count(bit))
			export_cell(bit_driver.at(bit));
		sigmap.apply(bit);

		if (fcache.count(bit) == 0) {
			if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "",
					log_signal(bit));
			makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(bit));
			register_bool(bit, idcounter++);
		}

		auto f = fcache.at(bit);
		if (f.second >= 0)
			return stringf("(= ((_ extract %d %d) (|%s#%d| %s)) #b1)", f.second, f.second, get_id(module), f.first, state_name);
		return stringf("(|%s#%d| %s)", get_id(module), f.first, state_name);
	}

	std::string get_bool(RTLIL::SigSpec sig, const char *state_name = "state")
	{
		return get_bool(sig.as_bit(), state_name);
	}

	std::string get_bv(RTLIL::SigSpec sig, const char *state_name = "state")
	{
		log_assert(bvmode);
		sigmap.apply(sig);

		std::vector<std::string> subexpr;

		SigSpec orig_sig;
		while (orig_sig != sig) {
			for (auto bit : sig)
				if (bit_driver.count(bit))
					export_cell(bit_driver.at(bit));
			orig_sig = sig;
			sigmap.apply(sig);
		}

		for (int i = 0, j = 1; i < GetSize(sig); i += j, j = 1)
		{
			if (sig[i].wire == nullptr) {
				while (i+j < GetSize(sig) && sig[i+j].wire == nullptr) j++;
				subexpr.push_back("#b");
				for (int k = i+j-1; k >= i; k--)
					subexpr.back() += sig[k] == RTLIL::State::S1 ? "1" : "0";
				continue;
			}

			if (fcache.count(sig[i]) && fcache.at(sig[i]).second == -1) {
				subexpr.push_back(stringf("(ite %s #b1 #b0)", get_bool(sig[i], state_name).c_str()));
				continue;
			}

			if (fcache.count(sig[i])) {
				auto t1 = fcache.at(sig[i]);
				while (i+j < GetSize(sig)) {
					if (fcache.count(sig[i+j]) == 0)
						break;
					auto t2 = fcache.at(sig[i+j]);
					if (t1.first != t2.first)
						break;
					if (t1.second+j != t2.second)
						break;
					j++;
				}
				if (t1.second == 0 && j == bvsizes.at(t1.first))
					subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), t1.first, state_name));
				else
					subexpr.push_back(stringf("((_ extract %d %d) (|%s#%d| %s))",
							t1.second + j - 1, t1.second, get_id(module), t1.first, state_name));
				continue;
			}

			std::set<RTLIL::SigBit> seen_bits = { sig[i] };
			while (i+j < GetSize(sig) && sig[i+j].wire && !fcache.count(sig[i+j]) && !seen_bits.count(sig[i+j]))
				seen_bits.insert(sig[i+j]), j++;

			if (verbose) log("%*s-> external bv: %s\n", 2+2*GetSize(recursive_cells), "",
					log_signal(sig.extract(i, j)));
			for (auto bit : sig.extract(i, j))
				log_assert(bit_driver.count(bit) == 0);
			makebits(stringf("%s#%d", get_id(module), idcounter), j, log_signal(sig.extract(i, j)));
			subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), idcounter, state_name));
			register_bv(sig.extract(i, j), idcounter++);
		}

		if (GetSize(subexpr) > 1) {
			std::string expr = "", end_str = "";
			for (int i = GetSize(subexpr)-1; i >= 0; i--) {
				if (i > 0) expr += " (concat", end_str += ")";
				expr += " " + subexpr[i];
			}
			return expr.substr(1) + end_str;
		} else {
			log_assert(GetSize(subexpr) == 1);
			return subexpr[0];
		}
	}

	void export_gate(RTLIL::Cell *cell, std::string expr)
	{
		RTLIL::SigBit bit = sigmap(cell->getPort("\\Y").as_bit());
		std::string processed_expr;

		for (char ch : expr) {
			if (ch == 'A') processed_expr += get_bool(cell->getPort("\\A"));
			else if (ch == 'B') processed_expr += get_bool(cell->getPort("\\B"));
			else if (ch == 'C') processed_expr += get_bool(cell->getPort("\\C"));
			else if (ch == 'D') processed_expr += get_bool(cell->getPort("\\D"));
			else if (ch == 'S') processed_expr += get_bool(cell->getPort("\\S"));
			else processed_expr += ch;
		}

		if (verbose)
			log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));

		decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
				get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(bit)));
		register_bool(bit, idcounter++);
		recursive_cells.erase(cell);
	}

	void export_bvop(RTLIL::Cell *cell, std::string expr, char type = 0)
	{
		RTLIL::SigSpec sig_a, sig_b;
		RTLIL::SigSpec sig_y = sigmap(cell->getPort("\\Y"));
		bool is_signed = cell->getParam("\\A_SIGNED").as_bool();
		int width = GetSize(sig_y);

		if (type == 's' || type == 'd' || type == 'b') {
			width = max(width, GetSize(cell->getPort("\\A")));
			if (cell->hasPort("\\B"))
				width = max(width, GetSize(cell->getPort("\\B")));
		}

		if (cell->hasPort("\\A")) {
			sig_a = cell->getPort("\\A");
			sig_a.extend_u0(width, is_signed);
		}

		if (cell->hasPort("\\B")) {
			sig_b = cell->getPort("\\B");
			sig_b.extend_u0(width, is_signed && !(type == 's'));
		}

		std::string processed_expr;

		for (char ch : expr) {
			if (ch == 'A') processed_expr += get_bv(sig_a);
			else if (ch == 'B') processed_expr += get_bv(sig_b);
			else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
			else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
			else processed_expr += ch;
		}

		if (width != GetSize(sig_y) && type != 'b')
			processed_expr = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, processed_expr.c_str());

		if (verbose)
			log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));

		if (type == 'b') {
			decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
					get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(sig_y)));
			register_boolvec(sig_y, idcounter++);
		} else {
			decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
					get_id(module), idcounter, get_id(module), GetSize(sig_y), processed_expr.c_str(), log_signal(sig_y)));
			register_bv(sig_y, idcounter++);
		}

		recursive_cells.erase(cell);
	}

	void export_reduce(RTLIL::Cell *cell, std::string expr, bool identity_val)
	{
		RTLIL::SigSpec sig_y = sigmap(cell->getPort("\\Y"));
		std::string processed_expr;

		for (char ch : expr)
			if (ch == 'A' || ch == 'B') {
				RTLIL::SigSpec sig = sigmap(cell->getPort(stringf("\\%c", ch)));
				for (auto bit : sig)
					processed_expr += " " + get_bool(bit);
				if (GetSize(sig) == 1)
					processed_expr += identity_val ? " true" : " false";
			} else
				processed_expr += ch;

		if (verbose)
			log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));

		decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
				get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(sig_y)));
		register_boolvec(sig_y, idcounter++);
		recursive_cells.erase(cell);
	}

	void export_cell(RTLIL::Cell *cell)
	{
		if (verbose)
			log("%*s=> export_cell %s (%s) [%s]\n", 2+2*GetSize(recursive_cells), "",
					log_id(cell), log_id(cell->type), exported_cells.count(cell) ? "old" : "new");

		if (recursive_cells.count(cell))
			log_error("Found logic loop in module %s! See cell %s.\n", get_id(module), get_id(cell));

		if (exported_cells.count(cell))
			return;

		exported_cells.insert(cell);
		recursive_cells.insert(cell);

		if (cell->type == "$initstate")
		{
			SigBit bit = sigmap(cell->getPort("\\Y").as_bit());
			decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (|%s_is| state)) ; %s\n",
					get_id(module), idcounter, get_id(module), get_id(module), log_signal(bit)));
			register_bool(bit, idcounter++);
			recursive_cells.erase(cell);
			return;
		}

		if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
		{
			registers.insert(cell);
			makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort("\\Q")));
			register_bool(cell->getPort("\\Q"), idcounter++);
			recursive_cells.erase(cell);
			return;
		}

		if (cell->type == "$_BUF_") return export_gate(cell, "A");
		if (cell->type == "$_NOT_") return export_gate(cell, "(not A)");
		if (cell->type == "$_AND_") return export_gate(cell, "(and A B)");
		if (cell->type == "$_NAND_") return export_gate(cell, "(not (and A B))");
		if (cell->type == "$_OR_") return export_gate(cell, "(or A B)");
		if (cell->type == "$_NOR_") return export_gate(cell, "(not (or A B))");
		if (cell->type == "$_XOR_") return export_gate(cell, "(xor A B)");
		if (cell->type == "$_XNOR_") return export_gate(cell, "(not (xor A B))");
		if (cell->type == "$_ANDNOT_") return export_gate(cell, "(and A (not B))");
		if (cell->type == "$_ORNOT_") return export_gate(cell, "(or A (not B))");
		if (cell->type == "$_MUX_") return export_gate(cell, "(ite S B A)");
		if (cell->type == "$_AOI3_") return export_gate(cell, "(not (or (and A B) C))");
		if (cell->type == "$_OAI3_") return export_gate(cell, "(not (and (or A B) C))");
		if (cell->type == "$_AOI4_") return export_gate(cell, "(not (or (and A B) (and C D)))");
		if (cell->type == "$_OAI4_") return export_gate(cell, "(not (and (or A B) (or C D)))");

		// FIXME: $lut

		if (bvmode)
		{
			if (cell->type.in("$ff", "$dff"))
			{
				registers.insert(cell);
				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q")));
				register_bv(cell->getPort("\\Q"), idcounter++);
				recursive_cells.erase(cell);
				return;
			}

			if (cell->type.in("$anyconst", "$anyseq", "$allconst", "$allseq"))
			{
				registers.insert(cell);
				string infostr = cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell);
				if (cell->attributes.count("\\reg"))
					infostr += " " + cell->attributes.at("\\reg").decode_string();
				decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort("\\Y")), infostr.c_str()));
				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y")));
				if (cell->type == "$anyseq")
					ex_input_eq.push_back(stringf("  (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter));
				register_bv(cell->getPort("\\Y"), idcounter++);
				recursive_cells.erase(cell);
				return;
			}

			if (cell->type == "$and") return export_bvop(cell, "(bvand A B)");
			if (cell->type == "$or") return export_bvop(cell, "(bvor A B)");
			if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)");
			if (cell->type == "$xnor") return export_bvop(cell, "(bvxnor A B)");

			if (cell->type == "$shl") return export_bvop(cell, "(bvshl A B)", 's');
			if (cell->type == "$shr") return export_bvop(cell, "(bvlshr A B)", 's');
			if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", 's');
			if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", 's');

			if (cell->type.in("$shift", "$shiftx")) {
				if (cell->getParam("\\B_SIGNED").as_bool()) {
					/* FIXME */
				} else {
					return export_bvop(cell, "(bvlshr A B)", 's');
				}
			}

			if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)", 'b');
			if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)", 'b');
			if (cell->type == "$ge") return export_bvop(cell, "(bvUge A B)", 'b');
			if (cell->type == "$gt") return export_bvop(cell, "(bvUgt A B)", 'b');

			if (cell->type == "$ne") return export_bvop(cell, "(distinct A B)", 'b');
			if (cell->type == "$nex") return export_bvop(cell, "(distinct A B)", 'b');
			if (cell->type == "$eq") return export_bvop(cell, "(= A B)", 'b');
			if (cell->type == "$eqx") return export_bvop(cell, "(= A B)", 'b');

			if (cell->type == "$not") return export_bvop(cell, "(bvnot A)");
			if (cell->type == "$pos") return export_bvop(cell, "A");
			if (cell->type == "$neg") return export_bvop(cell, "(bvneg A)");

			if (cell->type == "$add") return export_bvop(cell, "(bvadd A B)");
			if (cell->type == "$sub") return export_bvop(cell, "(bvsub A B)");
			if (cell->type == "$mul") return export_bvop(cell, "(bvmul A B)");
			if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)", 'd');
			if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)", 'd');

			if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool") &&
					2*GetSize(cell->getPort("\\A").chunks()) < GetSize(cell->getPort("\\A"))) {
				bool is_and = cell->type == "$reduce_and";
				string bits(GetSize(cell->getPort("\\A")), is_and ? '1' : '0');
				return export_bvop(cell, stringf("(%s A #b%s)", is_and ? "=" : "distinct", bits.c_str()), 'b');
			}

			if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true);
			if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false);
			if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false);
			if (cell->type == "$reduce_xnor") return export_reduce(cell, "(not (xor A))", false);
			if (cell->type == "$reduce_bool") return export_reduce(cell, "(or A)", false);

			if (cell->type == "$logic_not") return export_reduce(cell, "(not (or A))", false);
			if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))", false);
			if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)", false);

			if (cell->type == "$mux" || cell->type == "$pmux")
			{
				int width = GetSize(cell->getPort("\\Y"));
				std::string processed_expr = get_bv(cell->getPort("\\A"));

				RTLIL::SigSpec sig_b = cell->getPort("\\B");
				RTLIL::SigSpec sig_s = cell->getPort("\\S");
				get_bv(sig_b);
				get_bv(sig_s);

				for (int i = 0; i < GetSize(sig_s); i++)
					processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(),
							get_bv(sig_b.extract(i*width, width)).c_str(), processed_expr.c_str());

				if (verbose)
					log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));

				RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y"));
				decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
						get_id(module), idcounter, get_id(module), width, processed_expr.c_str(), log_signal(sig)));
				register_bv(sig, idcounter++);
				recursive_cells.erase(cell);
				return;
			}

			// FIXME: $slice $concat
		}

		if (memmode && cell->type == "$mem")
		{
			int arrayid = idcounter++;
			memarrays[cell] = arrayid;

			int abits = cell->getParam("\\ABITS").as_int();
			int width = cell->getParam("\\WIDTH").as_int();
			int rd_ports = cell->getParam("\\RD_PORTS").as_int();
			int wr_ports = cell->getParam("\\WR_PORTS").as_int();

			bool async_read = false;
			if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_ones()) {
				if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_zero())
					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));
				async_read = true;
			}

			decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(cell), abits, width, rd_ports, wr_ports, async_read ? "async" : "sync"));

			string memstate;
			if (async_read) {
				memstate = stringf("%s#%d#final", get_id(module), arrayid);
			} else {
				memstate = stringf("%s#%d#0", get_id(module), arrayid);
			}

			if (statebv)
			{
				int mem_size = cell->getParam("\\SIZE").as_int();
				int mem_offset = cell->getParam("\\OFFSET").as_int();

				makebits(memstate, width*mem_size, get_id(cell));
				decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s| state))\n",
						get_id(module), get_id(cell), get_id(module), width*mem_size, memstate.c_str()));

				for (int i = 0; i < rd_ports; i++)
				{
					SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits);
					SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
					std::string addr = get_bv(addr_sig);

					if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
						log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
								"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));

					decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
							get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));

					std::string read_expr = "#b";
					for (int k = 0; k < width; k++)
						read_expr += "0";

					for (int k = 0; k < mem_size; k++)
						read_expr = stringf("(ite (= (|%s_m:R%dA %s| state) #b%s) ((_ extract %d %d) (|%s| state))\n  %s)",
								get_id(module), i, get_id(cell), Const(k+mem_offset, abits).as_string().c_str(),
								width*(k+1)-1, width*k, memstate.c_str(), read_expr.c_str());

					decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d)\n  %s) ; %s\n",
							get_id(module), idcounter, get_id(module), width, read_expr.c_str(), log_signal(data_sig)));

					decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n",
							get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter));

					register_bv(data_sig, idcounter++);
				}
			}
			else
			{
				if (statedt)
					dtmembers.push_back(stringf("  (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
							memstate.c_str(), abits, width, get_id(cell)));
				else
					decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
							memstate.c_str(), get_id(module), abits, width, get_id(cell)));

				decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s| state))\n",
						get_id(module), get_id(cell), get_id(module), abits, width, memstate.c_str()));

				for (int i = 0; i < rd_ports; i++)
				{
					SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits);
					SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
					std::string addr = get_bv(addr_sig);

					if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
						log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
								"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));

					decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
							get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));

					decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s| state) (|%s_m:R%dA %s| state))) ; %s\n",
							get_id(module), idcounter, get_id(module), width, memstate.c_str(), get_id(module), i, get_id(cell), log_signal(data_sig)));

					decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n",
							get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter));

					register_bv(data_sig, idcounter++);
				}
			}

			registers.insert(cell);
			recursive_cells.erase(cell);
			return;
		}

		Module *m = module->design->module(cell->type);

		if (m != nullptr)
		{
			decls.push_back(stringf("; yosys-smt2-cell %s %s\n", get_id(cell->type), get_id(cell->name)));
			string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));

			for (auto &conn : cell->connections())
			{
				if (GetSize(conn.second) == 0)
					continue;

				Wire *w = m->wire(conn.first);
				SigSpec sig = sigmap(conn.second);

				if (w->port_output && !w->port_input) {
					if (GetSize(w) > 1) {
						if (bvmode) {
							makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(w), log_signal(sig));
							register_bv(sig, idcounter++);
						} else {
							for (int i = 0; i < GetSize(w); i++) {
								makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(sig[i]));
								register_bool(sig[i], idcounter++);
							}
						}
					} else {
						makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(sig));
						register_bool(sig, idcounter++);
					}
				}
			}

			if (statebv)
				makebits(stringf("%s_h %s", get_id(module), get_id(cell->name)), mod_stbv_width.at(cell->type));
			else if (statedt)
				dtmembers.push_back(stringf("  (|%s_h %s| |%s_s|)\n",
						get_id(module), get_id(cell->name), get_id(cell->type)));
			else
				decls.push_back(stringf("(declare-fun |%s_h %s| (|%s_s|) |%s_s|)\n",
						get_id(module), get_id(cell->name), get_id(module), get_id(cell->type)));

			hiercells.insert(cell);
			hiercells_queue.insert(cell);
			recursive_cells.erase(cell);
			return;
		}

		log_error("Unsupported cell type %s for cell %s.%s.\n",
				log_id(cell->type), log_id(module), log_id(cell));
	}

	void run()
	{
		if (verbose) log("=> export logic driving outputs\n");

		pool<SigBit> reg_bits;
		for (auto cell : module->cells())
			if (cell->type.in("$ff", "$dff", "$_FF_", "$_DFF_P_", "$_DFF_N_")) {
				// not using sigmap -- we want the net directly at the dff output
				for (auto bit : cell->getPort("\\Q"))
					reg_bits.insert(bit);
			}

		for (auto wire : module->wires()) {
			bool is_register = false;
			for (auto bit : SigSpec(wire))
				if (reg_bits.count(bit))
					is_register = true;
			if (wire->port_id || is_register || wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) {
				RTLIL::SigSpec sig = sigmap(wire);
				if (wire->port_input)
					decls.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width));
				if (wire->port_output)
					decls.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width));
				if (is_register)
					decls.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
				if (wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\'))
					decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
				if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
					decls.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
							clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
				if (bvmode && GetSize(sig) > 1) {
					decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
							get_id(module), get_id(wire), get_id(module), GetSize(sig), get_bv(sig).c_str()));
					if (wire->port_input)
						ex_input_eq.push_back(stringf("  (= (|%s_n %s| state) (|%s_n %s| other_state))",
								get_id(module), get_id(wire), get_id(module), get_id(wire)));
				} else {
					for (int i = 0; i < GetSize(sig); i++)
						if (GetSize(sig) > 1) {
							decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
									get_id(module), get_id(wire), i, get_id(module), get_bool(sig[i]).c_str()));
							if (wire->port_input)
								ex_input_eq.push_back(stringf("  (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))",
										get_id(module), get_id(wire), i, get_id(module), get_id(wire), i));
						} else {
							decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
									get_id(module), get_id(wire), get_id(module), get_bool(sig[i]).c_str()));
							if (wire->port_input)
								ex_input_eq.push_back(stringf("  (= (|%s_n %s| state) (|%s_n %s| other_state))",
										get_id(module), get_id(wire), get_id(module), get_id(wire)));
						}
				}
			}
		}

		if (verbose) log("=> export logic associated with the initial state\n");

		vector<string> init_list;
		for (auto wire : module->wires())
			if (wire->attributes.count("\\init")) {
				RTLIL::SigSpec sig = sigmap(wire);
				Const val = wire->attributes.at("\\init");
				val.bits.resize(GetSize(sig), State::Sx);
				if (bvmode && GetSize(sig) > 1) {
					Const mask(State::S1, GetSize(sig));
					bool use_mask = false;
					for (int i = 0; i < GetSize(sig); i++)
						if (val[i] != State::S0 && val[i] != State::S1) {
							val[i] = State::S0;
							mask[i] = State::S0;
							use_mask = true;
						}
					if (use_mask)
						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)));
					else
						init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), get_id(wire)));
				} else {
					for (int i = 0; i < GetSize(sig); i++)
						if (val[i] == State::S0 || val[i] == State::S1)
							init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val[i] == State::S1 ? "true" : "false", get_id(wire)));
				}
			}

		if (verbose) log("=> export logic driving asserts\n");

		int assert_id = 0, assume_id = 0, cover_id = 0;
		vector<string> assert_list, assume_list, cover_list;

		for (auto cell : module->cells())
		{
			if (cell->type.in("$assert", "$assume", "$cover"))
			{
				int &id = cell->type == "$assert" ? assert_id :
						cell->type == "$assume" ? assume_id :
						cell->type == "$cover" ? cover_id : *(int*)nullptr;

				char postfix = cell->type == "$assert" ? 'a' :
						cell->type == "$assume" ? 'u' :
						cell->type == "$cover" ? 'c' : 0;

				string name_a = get_bool(cell->getPort("\\A"));
				string name_en = get_bool(cell->getPort("\\EN"));
				decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id,
						cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));

				if (cell->type == "$cover")
					decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
							get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
				else
					decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
							get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));

				if (cell->type == "$assert")
					assert_list.push_back(stringf("(|%s_a %d| state)", get_id(module), id));
				else if (cell->type == "$assume")
					assume_list.push_back(stringf("(|%s_u %d| state)", get_id(module), id));

				id++;
			}
		}

		if (verbose) log("=> export logic driving hierarchical cells\n");

		for (auto cell : module->cells())
			if (module->design->module(cell->type) != nullptr)
				export_cell(cell);

		while (!hiercells_queue.empty())
		{
			std::set<RTLIL::Cell*> queue;
			queue.swap(hiercells_queue);

			for (auto cell : queue)
			{
				string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));
				Module *m = module->design->module(cell->type);
				log_assert(m != nullptr);

				hier.push_back(stringf("  (= (|%s_is| state) (|%s_is| %s))\n",
						get_id(module), get_id(cell->type), cell_state.c_str()));

				for (auto &conn : cell->connections())
				{
					if (GetSize(conn.second) == 0)
						continue;

					Wire *w = m->wire(conn.first);
					SigSpec sig = sigmap(conn.second);

					if (bvmode || GetSize(w) == 1) {
						hier.push_back(stringf("  (= %s (|%s_n %s| %s)) ; %s.%s\n", (GetSize(w) > 1 ? get_bv(sig) : get_bool(sig)).c_str(),
								get_id(cell->type), get_id(w), cell_state.c_str(), get_id(cell->type), get_id(w)));
					} else {
						for (int i = 0; i < GetSize(w); i++)
							hier.push_back(stringf("  (= %s (|%s_n %s %d| %s)) ; %s.%s[%d]\n", get_bool(sig[i]).c_str(),
									get_id(cell->type), get_id(w), i, cell_state.c_str(), get_id(cell->type), get_id(w), i));
					}
				}
			}
		}

		for (int iter = 1; !registers.empty(); iter++)
		{
			pool<Cell*> this_regs;
			this_regs.swap(registers);

			if (verbose) log("=> export logic driving registers [iteration %d]\n", iter);

			for (auto cell : this_regs)
			{
				if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
				{
					std::string expr_d = get_bool(cell->getPort("\\D"));
					std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
					ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort("\\Q")).c_str(), get_bool(cell->getPort("\\Q"), "other_state").c_str()));
				}

				if (cell->type.in("$ff", "$dff"))
				{
					std::string expr_d = get_bv(cell->getPort("\\D"));
					std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
					ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort("\\Q")).c_str(), get_bv(cell->getPort("\\Q"), "other_state").c_str()));
				}

				if (cell->type.in("$anyconst", "$allconst"))
				{
					std::string expr_d = get_bv(cell->getPort("\\Y"));
					std::string expr_q = get_bv(cell->getPort("\\Y"), "next_state");
					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Y"))));
					if (cell->type == "$anyconst")
						ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort("\\Y")).c_str(), get_bv(cell->getPort("\\Y"), "other_state").c_str()));
				}

				if (cell->type == "$mem")
				{
					int arrayid = memarrays.at(cell);

					int abits = cell->getParam("\\ABITS").as_int();
					int width = cell->getParam("\\WIDTH").as_int();
					int wr_ports = cell->getParam("\\WR_PORTS").as_int();

					bool async_read = false;
					string initial_memstate, final_memstate;

					if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_ones()) {
						log_assert(cell->getParam("\\WR_CLK_ENABLE").is_fully_zero());
						async_read = true;
						initial_memstate = stringf("%s#%d#0", get_id(module), arrayid);
						final_memstate = stringf("%s#%d#final", get_id(module), arrayid);
					}

					if (statebv)
					{
						int mem_size = cell->getParam("\\SIZE").as_int();
						int mem_offset = cell->getParam("\\OFFSET").as_int();

						if (async_read) {
							makebits(final_memstate, width*mem_size, get_id(cell));
						}

						for (int i = 0; i < wr_ports; i++)
						{
							SigSpec addr_sig = cell->getPort("\\WR_ADDR").extract(abits*i, abits);
							SigSpec data_sig = cell->getPort("\\WR_DATA").extract(width*i, width);
							SigSpec mask_sig = cell->getPort("\\WR_EN").extract(width*i, width);

							std::string addr = get_bv(addr_sig);
							std::string data = get_bv(data_sig);
							std::string mask = get_bv(mask_sig);

							decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
									get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
							addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell));

							decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
									get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig)));
							data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell));

							decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
									get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig)));
							mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell));

							std::string data_expr;

							for (int k = mem_size-1; k >= 0; k--) {
								std::string new_data = stringf("(bvor (bvand %s %s) (bvand ((_ extract %d %d) (|%s#%d#%d| state)) (bvnot %s)))",
										data.c_str(), mask.c_str(), width*(k+1)-1, width*k, get_id(module), arrayid, i, mask.c_str());
								data_expr += stringf("\n  (ite (= %s #b%s) %s ((_ extract %d %d) (|%s#%d#%d| state)))",
										addr.c_str(), Const(k+mem_offset, abits).as_string().c_str(), new_data.c_str(),
										width*(k+1)-1, width*k, get_id(module), arrayid, i);
							}

							decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (_ BitVec %d) (concat%s)) ; %s\n",
									get_id(module), arrayid, i+1, get_id(module), width*mem_size, data_expr.c_str(), get_id(cell)));
						}
					}
					else
					{
						if (async_read) {
							if (statedt)
								dtmembers.push_back(stringf("  (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
										initial_memstate.c_str(), abits, width, get_id(cell)));
							else
								decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
										initial_memstate.c_str(), get_id(module), abits, width, get_id(cell)));
						}

						for (int i = 0; i < wr_ports; i++)
						{
							SigSpec addr_sig = cell->getPort("\\WR_ADDR").extract(abits*i, abits);
							SigSpec data_sig = cell->getPort("\\WR_DATA").extract(width*i, width);
							SigSpec mask_sig = cell->getPort("\\WR_EN").extract(width*i, width);

							std::string addr = get_bv(addr_sig);
							std::string data = get_bv(data_sig);
							std::string mask = get_bv(mask_sig);

							decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
									get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
							addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell));

							decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
									get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig)));
							data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell));

							decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
									get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig)));
							mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell));

							data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
									data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str());

							decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) "
									"(store (|%s#%d#%d| state) %s %s)) ; %s\n",
									get_id(module), arrayid, i+1, get_id(module), abits, width,
									get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(cell)));
						}
					}

					std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, wr_ports);
					std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid);
					trans.push_back(stringf("  (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell)));
					ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid));

					if (async_read)
						hier.push_back(stringf("  (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(cell)));

					Const init_data = cell->getParam("\\INIT");
					int memsize = cell->getParam("\\SIZE").as_int();

					for (int i = 0; i < memsize; i++)
					{
						if (i*width >= GetSize(init_data))
							break;

						Const initword = init_data.extract(i*width, width, State::Sx);
						bool gen_init_constr = false;

						for (auto bit : initword.bits)
							if (bit == State::S0 || bit == State::S1)
								gen_init_constr = true;

						if (gen_init_constr)
						{
							if (statebv)
								/* FIXME */;
							else
								init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
										get_id(module), arrayid, Const(i, abits).as_string().c_str(),
										initword.as_string().c_str(), get_id(cell), i));
						}
					}
				}
			}
		}

		if (verbose) log("=> finalizing SMT2 representation of %s.\n", log_id(module));

		for (auto c : hiercells) {
			assert_list.push_back(stringf("(|%s_a| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name)));
			assume_list.push_back(stringf("(|%s_u| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name)));
			init_list.push_back(stringf("(|%s_i| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name)));
			hier.push_back(stringf("  (|%s_h| (|%s_h %s| state))\n", get_id(c->type), get_id(module), get_id(c->name)));
			trans.push_back(stringf("  (|%s_t| (|%s_h %s| state) (|%s_h %s| next_state))\n",
					get_id(c->type), get_id(module), get_id(c->name), get_id(module), get_id(c->name)));
			ex_state_eq.push_back(stringf("(|%s_ex_state_eq| (|%s_h %s| state) (|%s_h %s| other_state))\n",
					get_id(c->type), get_id(module), get_id(c->name), get_id(module), get_id(c->name)));
		}

		if (forallmode)
		{
			string expr = ex_state_eq.empty() ? "true" : "(and";
			if (!ex_state_eq.empty()) {
				if (GetSize(ex_state_eq) == 1) {
					expr = "\n  " + ex_state_eq.front() + "\n";
				} else {
					for (auto &str : ex_state_eq)
						expr += stringf("\n  %s", str.c_str());
					expr += "\n)";
				}
			}
			decls.push_back(stringf("(define-fun |%s_ex_state_eq| ((state |%s_s|) (other_state |%s_s|)) Bool %s)\n",
				get_id(module), get_id(module), get_id(module), expr.c_str()));

			expr = ex_input_eq.empty() ? "true" : "(and";
			if (!ex_input_eq.empty()) {
				if (GetSize(ex_input_eq) == 1) {
					expr = "\n  " + ex_input_eq.front() + "\n";
				} else {
					for (auto &str : ex_input_eq)
						expr += stringf("\n  %s", str.c_str());
					expr += "\n)";
				}
			}
			decls.push_back(stringf("(define-fun |%s_ex_input_eq| ((state |%s_s|) (other_state |%s_s|)) Bool %s)\n",
				get_id(module), get_id(module), get_id(module), expr.c_str()));
		}

		string assert_expr = assert_list.empty() ? "true" : "(and";
		if (!assert_list.empty()) {
			if (GetSize(assert_list) == 1) {
				assert_expr = "\n  " + assert_list.front() + "\n";