diff --git a/backends/json/json.cc b/backends/json/json.cc
index 52b97ef0b..59158cfa0 100644
--- a/backends/json/json.cc
+++ b/backends/json/json.cc
@@ -216,11 +216,11 @@ struct JsonWriter
 				if (!first_model)
 					f << stringf(",\n");
 				f << stringf("    \"%s\": [\n", aig.name.c_str());
-				bool first_node = true;
+				int node_idx = 0;
 				for (auto &node : aig.nodes) {
-					if (!first_node)
+					if (node_idx != 0)
 						f << stringf(",\n");
-					f << stringf("      [ ");
+					f << stringf("      /* %3d */ [ ", node_idx);
 					if (node.portbit >= 0)
 						f << stringf("\"%sport\", \"%s\", %d", node.inverter ? "n" : "",
 								log_id(node.portname), node.portbit);
@@ -231,7 +231,7 @@ struct JsonWriter
 					for (auto &op : node.outports)
 						f << stringf(", \"%s\", %d", log_id(op.first), op.second);
 					f << stringf(" ]");
-					first_node = false;
+					node_idx++;
 				}
 				f << stringf("\n    ]");
 				first_model = false;
@@ -253,7 +253,7 @@ struct JsonBackend : public Backend {
 		log("Write a JSON netlist of the current design.\n");
 		log("\n");
 		log("    -aig\n");
-		log("        also include AIG models for the different gate types\n");
+		log("        include AIG models for the different gate types\n");
 		log("\n");
 		log("\n");
 		log("The general syntax of the JSON output created by this command is as follows:\n");
@@ -274,7 +274,10 @@ struct JsonBackend : public Backend {
 		log("            ...\n");
 		log("          }\n");
 		log("        }\n");
-		log("      }\n");
+		log("      },\n");
+		log("      \"models\": {\n");
+		log("        ...\n");
+		log("      },\n");
 		log("    }\n");
 		log("\n");
 		log("Where <port_details> is:\n");
@@ -387,6 +390,60 @@ struct JsonBackend : public Backend {
 		log("      }\n");
 		log("    }\n");
 		log("\n");
+		log("The models are given as And-Inverter-Graphs (AIGs) in the following form:\n");
+		log("\n");
+		log("    \"models\": {\n");
+		log("      <model_name>: [\n");
+		log("        /*   0 */ [ <node-spec> ],\n");
+		log("        /*   1 */ [ <node-spec> ],\n");
+		log("        /*   2 */ [ <node-spec> ],\n");
+		log("        ...\n");
+		log("      ],\n");
+		log("      ...\n");
+		log("    },\n");
+		log("\n");
+		log("The following node-types may be used:\n");
+		log("\n");
+		log("    [ \"port\", <portname>, <bitindex>, <out-list> ]\n");
+		log("      - the value of the specified input port bit\n");
+		log("\n");
+		log("    [ \"nport\", <portname>, <bitindex>, <out-list> ]\n");
+		log("      - the inverted value of the specified input port bit\n");
+		log("\n");
+		log("    [ \"and\", <node-index>, <node-index>, <out-list> ]\n");
+		log("      - the ANDed value of the speciefied nodes\n");
+		log("\n");
+		log("    [ \"nand\", <node-index>, <node-index>, <out-list> ]\n");
+		log("      - the inverted ANDed value of the speciefied nodes\n");
+		log("\n");
+		log("    [ \"true\", <out-list> ]\n");
+		log("      - the constant value 1\n");
+		log("\n");
+		log("    [ \"false\", <out-list> ]\n");
+		log("      - the constant value 0\n");
+		log("\n");
+		log("All nodes appear in topological order. I.e. only nodes with smaller indices\n");
+		log("are referenced by \"and\" and \"nand\" nodes.\n");
+		log("\n");
+		log("The optional <out-list> at the end of a node specification is a list of\n");
+		log("output portname and bitindex pairs, specifying the outputs driven by this node.\n");
+		log("\n");
+		log("For example, the following is the model for a 3-input 3-output $reduce_and cell\n");
+		log("inferred by the following code:\n");
+		log("\n");
+		log("    module test(input [2:0] in, output [2:0] out);\n");
+		log("      assign in = &out;\n");
+		log("    endmodule\n");
+		log("\n");
+		log("    \"$reduce_and:3U:3\": [\n");
+		log("      /*   0 */ [ \"port\", \"A\", 0 ],\n");
+		log("      /*   1 */ [ \"port\", \"A\", 1 ],\n");
+		log("      /*   2 */ [ \"and\", 0, 1 ],\n");
+		log("      /*   3 */ [ \"port\", \"A\", 2 ],\n");
+		log("      /*   4 */ [ \"and\", 2, 3, \"Y\", 0 ],\n");
+		log("      /*   5 */ [ \"false\", \"Y\", 1, \"Y\", 2 ]\n");
+		log("    ]\n");
+		log("\n");
 		log("Future version of Yosys might add support for additional fields in the JSON\n");
 		log("format. A program processing this format must ignore all unkown fields.\n");
 		log("\n");
diff --git a/kernel/cellaigs.cc b/kernel/cellaigs.cc
index 48727c145..5b1e618f6 100644
--- a/kernel/cellaigs.cc
+++ b/kernel/cellaigs.cc
@@ -112,6 +112,14 @@ struct AigMaker
 		return node2index(node);
 	}
 
+	vector<int> inport_vec(IdString portname, int width)
+	{
+		vector<int> vec;
+		for (int i = 0; i < width; i++)
+			vec.push_back(inport(portname, i));
+		return vec;
+	}
+
 	int not_inport(IdString portname, int portbit = 0)
 	{
 		return inport(portname, portbit, true);
@@ -128,7 +136,7 @@ struct AigMaker
 	int and_gate(int A, int B, bool inverter = false)
 	{
 		if (A == B)
-			return A;
+			return inverter ? not_gate(A) : A;
 
 		const AigNode &nA = aig_indices[A];
 		const AigNode &nB = aig_indices[B];
@@ -199,11 +207,39 @@ struct AigMaker
 		return or_gate(and_gate(A, not_gate(S)), and_gate(B, S));
 	}
 
+	vector<int> adder(const vector<int> &A, const vector<int> &B, int carry, vector<int> *X = nullptr, vector<int> *CO = nullptr)
+	{
+		vector<int> Y(GetSize(A));
+		log_assert(GetSize(A) == GetSize(B));
+		for (int i = 0; i < GetSize(A); i++) {
+			Y[i] = xor_gate(xor_gate(A[i], B[i]), carry);
+			carry = or_gate(and_gate(A[i], B[i]), and_gate(or_gate(A[i], B[i]), carry));
+			if (X != nullptr)
+				X->at(i) = xor_gate(A[i], B[i]);
+			if (CO != nullptr)
+				CO->at(i) = carry;
+		}
+		return Y;
+	}
+
 	void outport(int node, IdString portname, int portbit = 0)
 	{
 		if (portbit < GetSize(cell->getPort(portname)))
 			aig->nodes.at(node).outports.push_back(pair<IdString, int>(portname, portbit));
 	}
+
+	void outport_bool(int node, IdString portname)
+	{
+		outport(node, portname);
+		for (int i = 1; i < GetSize(cell->getPort(portname)); i++)
+			outport(bool_node(false), portname, i);
+	}
+
+	void outport_vec(const vector<int> &vec, IdString portname)
+	{
+		for (int i = 0; i < GetSize(vec); i++)
+			outport(vec.at(i), portname, i);
+	}
 };
 
 Aig::Aig(Cell *cell)
@@ -214,15 +250,41 @@ Aig::Aig(Cell *cell)
 	AigMaker mk(this, cell);
 	name = cell->type.str();
 
+	string mkname_last;
+	bool mkname_a_signed = false;
+	bool mkname_b_signed = false;
+	bool mkname_is_signed = false;
+
 	cell->parameters.sort();
 	for (auto p : cell->parameters)
-		name += stringf(":%d", p.second.as_int());
+	{
+		if (p.first == "\\A_WIDTH" && mkname_a_signed) {
+			name = mkname_last + stringf(":%d%c", p.second.as_int(), mkname_is_signed ? 'S' : 'U');
+		} else if (p.first == "\\B_WIDTH" && mkname_b_signed) {
+			name = mkname_last + stringf(":%d%c", p.second.as_int(), mkname_is_signed ? 'S' : 'U');
+		} else {
+			mkname_last = name;
+			name += stringf(":%d", p.second.as_int());
+		}
 
-	if (cell->type.in("$not", "$_NOT_"))
+		mkname_a_signed = false;
+		mkname_b_signed = false;
+		mkname_is_signed = false;
+		if (p.first == "\\A_SIGNED") {
+			mkname_a_signed = true;
+			mkname_is_signed = p.second.as_bool();
+		}
+		if (p.first == "\\B_SIGNED") {
+			mkname_b_signed = true;
+			mkname_is_signed = p.second.as_bool();
+		}
+	}
+
+	if (cell->type.in("$not", "$_NOT_", "$pos", "$_BUF_"))
 	{
 		for (int i = 0; i < GetSize(cell->getPort("\\Y")); i++) {
 			int A = mk.inport("\\A", i);
-			int Y = mk.not_gate(A);
+			int Y = cell->type.in("$not", "$_NOT_") ? mk.not_gate(A) : A;
 			mk.outport(Y, "\\Y", i);
 		}
 		goto optimize;
@@ -256,6 +318,92 @@ Aig::Aig(Cell *cell)
 		goto optimize;
 	}
 
+	if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_xor", "$reduce_xnor", "$reduce_bool"))
+	{
+		int Y = mk.inport("\\A", 0);
+		for (int i = 1; i < GetSize(cell->getPort("\\A")); i++) {
+			int A = mk.inport("\\A", i);
+			if (cell->type == "$reduce_and")  Y = mk.and_gate(A, Y);
+			if (cell->type == "$reduce_or")   Y = mk.or_gate(A, Y);
+			if (cell->type == "$reduce_bool") Y = mk.or_gate(A, Y);
+			if (cell->type == "$reduce_xor")  Y = mk.xor_gate(A, Y);
+			if (cell->type == "$reduce_xnor") Y = mk.xor_gate(A, Y);
+		}
+		if (cell->type == "$reduce_xnor")
+			Y = mk.not_gate(Y);
+		mk.outport(Y, "\\Y", 0);
+		for (int i = 1; i < GetSize(cell->getPort("\\Y")); i++)
+			mk.outport(mk.bool_node(false), "\\Y", i);
+		goto optimize;
+	}
+
+	if (cell->type.in("$logic_not", "$logic_and", "$logic_or"))
+	{
+		int A = mk.inport("\\A", 0), Y = -1;
+		for (int i = 1; i < GetSize(cell->getPort("\\A")); i++)
+			A = mk.or_gate(mk.inport("\\A", i), A);
+		if (cell->type.in("$logic_and", "$logic_or")) {
+			int B = mk.inport("\\B", 0);
+			for (int i = 1; i < GetSize(cell->getPort("\\B")); i++)
+				B = mk.or_gate(mk.inport("\\B", i), B);
+			if (cell->type == "$logic_and") Y = mk.and_gate(A, B);
+			if (cell->type == "$logic_or")  Y = mk.or_gate(A, B);
+		} else {
+			if (cell->type == "$logic_not") Y = mk.not_gate(A);
+		}
+		mk.outport_bool(Y, "\\Y");
+		goto optimize;
+	}
+
+	if (cell->type.in("$add", "$sub"))
+	{
+		int width = GetSize(cell->getPort("\\Y"));
+		vector<int> A = mk.inport_vec("\\A", width);
+		vector<int> B = mk.inport_vec("\\B", width);
+		int carry = mk.bool_node(false);
+		if (cell->type == "$sub") {
+			for (auto &n : B)
+				n = mk.not_gate(n);
+			carry = mk.not_gate(carry);
+		}
+		vector<int> Y = mk.adder(A, B, carry);
+		mk.outport_vec(Y, "\\Y");
+		goto optimize;
+	}
+
+	if (cell->type == "$alu")
+	{
+		int width = GetSize(cell->getPort("\\Y"));
+		vector<int> A = mk.inport_vec("\\A", width);
+		vector<int> B = mk.inport_vec("\\B", width);
+		int carry = mk.inport("\\CI");
+		int binv = mk.inport("\\BI");
+		for (auto &n : B)
+			n = mk.xor_gate(n, binv);
+		vector<int> X(width), CO(width);
+		vector<int> Y = mk.adder(A, B, carry, &X, &CO);
+		for (int i = 0; i < width; i++)
+			X[i] = mk.xor_gate(A[i], B[i]);
+		mk.outport_vec(Y, "\\Y");
+		mk.outport_vec(X, "\\X");
+		mk.outport_vec(CO, "\\CO");
+		goto optimize;
+	}
+
+	if (cell->type.in("$eq", "$ne"))
+	{
+		int width = std::max(GetSize(cell->getPort("\\A")), GetSize(cell->getPort("\\B")));
+		vector<int> A = mk.inport_vec("\\A", width);
+		vector<int> B = mk.inport_vec("\\B", width);
+		int Y = mk.bool_node(false);
+		for (int i = 0; i < width; i++)
+			Y = mk.or_gate(Y, mk.xor_gate(A[i], B[i]));
+		if (cell->type == "$eq")
+			Y = mk.not_gate(Y);
+		mk.outport_bool(Y, "\\Y");
+		goto optimize;
+	}
+
 	if (cell->type == "$_AOI3_")
 	{
 		int A = mk.inport("\\A");