aboutsummaryrefslogtreecommitdiffstats
path: root/libs/minisat/Alg.h
blob: ddb972e772bc0775840a98e0a02cf20e344ebeeb (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
/*******************************************************************************************[Alg.h]
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007-2010, Niklas Sorensson

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/

#ifndef Minisat_Alg_h
#define Minisat_Alg_h

#include "Vec.h"

namespace Minisat {

//=================================================================================================
// Useful functions on vector-like types:

//=================================================================================================
// Removing and searching for elements:
//

template<class V, class T>
static inline void remove(V& ts, const T& t)
{
    int j = 0;
    for (; j < (int)ts.size() && ts[j] != t; j++);
    assert(j < (int)ts.size());
    for (; j < (int)ts.size()-1; j++) ts[j] = ts[j+1];
    ts.pop();
}


template<class V, class T>
static inline bool find(V& ts, const T& t)
{
    int j = 0;
    for (; j < (int)ts.size() && ts[j] != t; j++);
    return j < (int)ts.size();
}


//=================================================================================================
// Copying vectors with support for nested vector types:
//

// Base case:
template<class T>
static inline void copy(const T& from, T& to)
{
    to = from;
}

// Recursive case:
template<class T>
static inline void copy(const vec<T>& from, vec<T>& to, bool append = false)
{
    if (!append)
        to.clear();
    for (int i = 0; i < from.size(); i++){
        to.push();
        copy(from[i], to.last());
    }
}

template<class T>
static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true); }

//=================================================================================================
}

#endif
href='#n554'>554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694
/*
 *  yosys -- Yosys Open SYnthesis Suite
 *
 *  Copyright (C) 2012  Claire Xenia Wolf <claire@yosyshq.com>
 *
 *  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/cellaigs.h"
#include "kernel/log.h"
#include <string>

USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN

struct JsonWriter
{
	std::ostream &f;
	bool use_selection;
	bool aig_mode;
	bool compat_int_mode;

	Design *design;
	Module *module;

	SigMap sigmap;
	int sigidcounter;
	dict<SigBit, string> sigids;
	pool<Aig> aig_models;

	JsonWriter(std::ostream &f, bool use_selection, bool aig_mode, bool compat_int_mode) :
			f(f), use_selection(use_selection), aig_mode(aig_mode),
			compat_int_mode(compat_int_mode) { }

	string get_string(string str)
	{
		string newstr = "\"";
		for (char c : str) {
			if (c == '\\')
				newstr += "\\\\";
			else if (c == '"')
				newstr += "\\\"";
			else if (c == '\b')
				newstr += "\\b";
			else if (c == '\f')
				newstr += "\\f";
			else if (c == '\n')
				newstr += "\\n";
			else if (c == '\r')
				newstr += "\\r";
			else if (c == '\t')
				newstr += "\\t";
			else if (c < 0x20)
				newstr += stringf("\\u%04X", c);
			else
				newstr += c;
		}
		return newstr + "\"";
	}

	string get_name(IdString name)
	{
		return get_string(RTLIL::unescape_id(name));
	}

	string get_bits(SigSpec sig)
	{
		bool first = true;
		string str = "[";
		for (auto bit : sigmap(sig)) {
			str += first ? " " : ", ";
			first = false;
			if (sigids.count(bit) == 0) {
				string &s = sigids[bit];
				if (bit.wire == nullptr) {
					if (bit == State::S0) s = "\"0\"";
					else if (bit == State::S1) s = "\"1\"";
					else if (bit == State::Sz) s = "\"z\"";
					else s = "\"x\"";
				} else
					s = stringf("%d", sigidcounter++);
			}
			str += sigids[bit];
		}
		return str + " ]";
	}

	void write_parameter_value(const Const &value)
	{
		if ((value.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) != 0) {
			string str = value.decode_string();
			int state = 0;
			for (char c : str) {
				if (state == 0) {
					if (c == '0' || c == '1' || c == 'x' || c == 'z')
						state = 0;
					else if (c == ' ')
						state = 1;
					else
						state = 2;
				} else if (state == 1 && c != ' ')
					state = 2;
			}
			if (state < 2)
				str += " ";
			f << get_string(str);
		} else if (compat_int_mode && GetSize(value) <= 32 && value.is_fully_def()) {
			if ((value.flags & RTLIL::ConstFlags::CONST_FLAG_SIGNED) != 0)
				f << stringf("%d", value.as_int());
			else
				f << stringf("%u", value.as_int());
		} else {
			f << get_string(value.as_string());
		}
	}

	void write_parameters(const dict<IdString, Const> &parameters, bool for_module=false)
	{
		bool first = true;
		for (auto &param : parameters) {
			f << stringf("%s\n", first ? "" : ",");
			f << stringf("        %s%s: ", for_module ? "" : "    ", get_name(param.first).c_str());
			write_parameter_value(param.second);
			first = false;
		}
	}

	void write_module(Module *module_)
	{
		module = module_;
		log_assert(module->design == design);
		sigmap.set(module);
		sigids.clear();

		// reserve 0 and 1 to avoid confusion with "0" and "1"
		sigidcounter = 2;

		if (module->has_processes()) {
			log_error("Module %s contains processes, which are not supported by JSON backend (run `proc` first).\n", log_id(module));
		}

		f << stringf("    %s: {\n", get_name(module->name).c_str());

		f << stringf("      \"attributes\": {");
		write_parameters(module->attributes, /*for_module=*/true);
		f << stringf("\n      },\n");

		if (module->parameter_default_values.size()) {
			f << stringf("      \"parameter_default_values\": {");
			write_parameters(module->parameter_default_values, /*for_module=*/true);
			f << stringf("\n      },\n");
		}

		f << stringf("      \"ports\": {");
		bool first = true;
		for (auto n : module->ports) {
			Wire *w = module->wire(n);
			if (use_selection && !module->selected(w))
				continue;
			f << stringf("%s\n", first ? "" : ",");
			f << stringf("        %s: {\n", get_name(n).c_str());
			f << stringf("          \"direction\": \"%s\",\n", w->port_input ? w->port_output ? "inout" : "input" : "output");
			if (w->start_offset)
				f << stringf("          \"offset\": %d,\n", w->start_offset);
			if (w->upto)
				f << stringf("          \"upto\": 1,\n");
			if (w->is_signed)
				f << stringf("          \"signed\": %d,\n", w->is_signed);
			f << stringf("          \"bits\": %s\n", get_bits(w).c_str());
			f << stringf("        }");
			first = false;
		}
		f << stringf("\n      },\n");

		f << stringf("      \"cells\": {");
		first = true;
		for (auto c : module->cells()) {
			if (use_selection && !module->selected(c))
				continue;
			f << stringf("%s\n", first ? "" : ",");
			f << stringf("        %s: {\n", get_name(c->name).c_str());
			f << stringf("          \"hide_name\": %s,\n", c->name[0] == '$' ? "1" : "0");
			f << stringf("          \"type\": %s,\n", get_name(c->type).c_str());
			if (aig_mode) {
				Aig aig(c);
				if (!aig.name.empty()) {
					f << stringf("          \"model\": \"%s\",\n", aig.name.c_str());
					aig_models.insert(aig);
				}
			}
			f << stringf("          \"parameters\": {");
			write_parameters(c->parameters);
			f << stringf("\n          },\n");
			f << stringf("          \"attributes\": {");
			write_parameters(c->attributes);
			f << stringf("\n          },\n");
			if (c->known()) {
				f << stringf("          \"port_directions\": {");
				bool first2 = true;
				for (auto &conn : c->connections()) {
					string direction = "output";
					if (c->input(conn.first))
						direction = c->output(conn.first) ? "inout" : "input";
					f << stringf("%s\n", first2 ? "" : ",");
					f << stringf("            %s: \"%s\"", get_name(conn.first).c_str(), direction.c_str());
					first2 = false;
				}
				f << stringf("\n          },\n");
			}
			f << stringf("          \"connections\": {");
			bool first2 = true;
			for (auto &conn : c->connections()) {
				f << stringf("%s\n", first2 ? "" : ",");
				f << stringf("            %s: %s", get_name(conn.first).c_str(), get_bits(conn.second).c_str());
				first2 = false;
			}
			f << stringf("\n          }\n");
			f << stringf("        }");
			first = false;
		}
		f << stringf("\n      },\n");

		if (!module->memories.empty()) {
			f << stringf("      \"memories\": {");
			first = true;
			for (auto &it : module->memories) {
				if (use_selection && !module->selected(it.second))
					continue;
				f << stringf("%s\n", first ? "" : ",");
				f << stringf("        %s: {\n", get_name(it.second->name).c_str());
				f << stringf("          \"hide_name\": %s,\n", it.second->name[0] == '$' ? "1" : "0");
				f << stringf("          \"attributes\": {");
				write_parameters(it.second->attributes);
				f << stringf("\n          },\n");
				f << stringf("          \"width\": %d,\n", it.second->width);
				f << stringf("          \"start_offset\": %d,\n", it.second->start_offset);
				f << stringf("          \"size\": %d\n", it.second->size);
				f << stringf("        }");
				first = false;
			}
			f << stringf("\n      },\n");
		}

		f << stringf("      \"netnames\": {");
		first = true;
		for (auto w : module->wires()) {
			if (use_selection && !module->selected(w))
				continue;
			f << stringf("%s\n", first ? "" : ",");
			f << stringf("        %s: {\n", get_name(w->name).c_str());
			f << stringf("          \"hide_name\": %s,\n", w->name[0] == '$' ? "1" : "0");
			f << stringf("          \"bits\": %s,\n", get_bits(w).c_str());
			if (w->start_offset)
				f << stringf("          \"offset\": %d,\n", w->start_offset);
			if (w->upto)
				f << stringf("          \"upto\": 1,\n");
			if (w->is_signed)
				f << stringf("          \"signed\": %d,\n", w->is_signed);
			f << stringf("          \"attributes\": {");
			write_parameters(w->attributes);
			f << stringf("\n          }\n");
			f << stringf("        }");
			first = false;
		}
		f << stringf("\n      }\n");

		f << stringf("    }");
	}

	void write_design(Design *design_)
	{
		design = design_;
		design->sort();

		f << stringf("{\n");
		f << stringf("  \"creator\": %s,\n", get_string(yosys_version_str).c_str());
		f << stringf("  \"modules\": {\n");
		vector<Module*> modules = use_selection ? design->selected_modules() : design->modules();
		bool first_module = true;
		for (auto mod : modules) {
			if (!first_module)
				f << stringf(",\n");
			write_module(mod);
			first_module = false;
		}
		f << stringf("\n  }");
		if (!aig_models.empty()) {
			f << stringf(",\n  \"models\": {\n");
			bool first_model = true;
			for (auto &aig : aig_models) {
				if (!first_model)
					f << stringf(",\n");
				f << stringf("    \"%s\": [\n", aig.name.c_str());
				int node_idx = 0;
				for (auto &node : aig.nodes) {
					if (node_idx != 0)
						f << stringf(",\n");
					f << stringf("      /* %3d */ [ ", node_idx);
					if (node.portbit >= 0)
						f << stringf("\"%sport\", \"%s\", %d", node.inverter ? "n" : "",
								log_id(node.portname), node.portbit);
					else if (node.left_parent < 0 && node.right_parent < 0)
						f << stringf("\"%s\"", node.inverter ? "true" : "false");
					else
						f << stringf("\"%s\", %d, %d", node.inverter ? "nand" : "and", node.left_parent, node.right_parent);
					for (auto &op : node.outports)
						f << stringf(", \"%s\", %d", log_id(op.first), op.second);
					f << stringf(" ]");
					node_idx++;
				}
				f << stringf("\n    ]");
				first_model = false;
			}
			f << stringf("\n  }");
		}
		f << stringf("\n}\n");
	}
};

struct JsonBackend : public Backend {
	JsonBackend() : Backend("json", "write design to a JSON file") { }
	void help() override
	{
		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
		log("\n");
		log("    write_json [options] [filename]\n");
		log("\n");
		log("Write a JSON netlist of the current design.\n");
		log("\n");
		log("    -aig\n");
		log("        include AIG models for the different gate types\n");
		log("\n");
		log("    -compat-int\n");
		log("        emit 32-bit or smaller fully-defined parameter values directly\n");
		log("        as JSON numbers (for compatibility with old parsers)\n");
		log("\n");
		log("\n");
		log("The general syntax of the JSON output created by this command is as follows:\n");
		log("\n");
		log("    {\n");
		log("      \"creator\": \"Yosys <version info>\",\n");
		log("      \"modules\": {\n");
		log("        <module_name>: {\n");
		log("          \"attributes\": {\n");
		log("            <attribute_name>: <attribute_value>,\n");
		log("            ...\n");
		log("          },\n");
		log("          \"parameter_default_values\": {\n");
		log("            <parameter_name>: <parameter_value>,\n");
		log("            ...\n");
		log("          },\n");
		log("          \"ports\": {\n");
		log("            <port_name>: <port_details>,\n");
		log("            ...\n");
		log("          },\n");
		log("          \"cells\": {\n");
		log("            <cell_name>: <cell_details>,\n");
		log("            ...\n");
		log("          },\n");
		log("          \"memories\": {\n");
		log("            <memory_name>: <memory_details>,\n");
		log("            ...\n");
		log("          },\n");
		log("          \"netnames\": {\n");
		log("            <net_name>: <net_details>,\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");
		log("\n");
		log("    {\n");
		log("      \"direction\": <\"input\" | \"output\" | \"inout\">,\n");
		log("      \"bits\": <bit_vector>\n");
		log("      \"offset\": <the lowest bit index in use, if non-0>\n");
		log("      \"upto\": <1 if the port bit indexing is MSB-first>\n");
		log("      \"signed\": <1 if the port is signed>\n");
		log("    }\n");
		log("\n");
		log("The \"offset\" and \"upto\" fields are skipped if their value would be 0.\n");
		log("They don't affect connection semantics, and are only used to preserve original\n");
		log("HDL bit indexing.");
		log("And <cell_details> is:\n");
		log("\n");
		log("    {\n");
		log("      \"hide_name\": <1 | 0>,\n");
		log("      \"type\": <cell_type>,\n");
		log("      \"model\": <AIG model name, if -aig option used>,\n");
		log("      \"parameters\": {\n");
		log("        <parameter_name>: <parameter_value>,\n");
		log("        ...\n");
		log("      },\n");
		log("      \"attributes\": {\n");
		log("        <attribute_name>: <attribute_value>,\n");
		log("        ...\n");
		log("      },\n");
		log("      \"port_directions\": {\n");
		log("        <port_name>: <\"input\" | \"output\" | \"inout\">,\n");
		log("        ...\n");
		log("      },\n");
		log("      \"connections\": {\n");
		log("        <port_name>: <bit_vector>,\n");
		log("        ...\n");
		log("      },\n");
		log("    }\n");
		log("\n");
		log("And <memory_details> is:\n");
		log("\n");
		log("    {\n");
		log("      \"hide_name\": <1 | 0>,\n");
		log("      \"attributes\": {\n");
		log("        <attribute_name>: <attribute_value>,\n");
		log("        ...\n");
		log("      },\n");
		log("      \"width\": <memory width>\n");
		log("      \"start_offset\": <the lowest valid memory address>\n");
		log("      \"size\": <memory size>\n");
		log("    }\n");
		log("\n");
		log("And <net_details> is:\n");
		log("\n");
		log("    {\n");
		log("      \"hide_name\": <1 | 0>,\n");
		log("      \"bits\": <bit_vector>\n");
		log("      \"offset\": <the lowest bit index in use, if non-0>\n");
		log("      \"upto\": <1 if the port bit indexing is MSB-first>\n");
		log("      \"signed\": <1 if the port is signed>\n");
		log("    }\n");
		log("\n");
		log("The \"hide_name\" fields are set to 1 when the name of this cell or net is\n");
		log("automatically created and is likely not of interest for a regular user.\n");
		log("\n");
		log("The \"port_directions\" section is only included for cells for which the\n");
		log("interface is known.\n");
		log("\n");
		log("Module and cell ports and nets can be single bit wide or vectors of multiple\n");
		log("bits. Each individual signal bit is assigned a unique integer. The <bit_vector>\n");
		log("values referenced above are vectors of this integers. Signal bits that are\n");
		log("connected to a constant driver are denoted as string \"0\", \"1\", \"x\", or\n");
		log("\"z\" instead of a number.\n");
		log("\n");
		log("Bit vectors (including integers) are written as string holding the binary\n");
		log("representation of the value. Strings are written as strings, with an appended\n");
		log("blank in cases of strings of the form /[01xz]* */.\n");
		log("\n");
		log("For example the following Verilog code:\n");
		log("\n");
		log("    module test(input x, y);\n");
		log("      (* keep *) foo #(.P(42), .Q(1337))\n");
		log("          foo_inst (.A({x, y}), .B({y, x}), .C({4'd10, {4{x}}}));\n");
		log("    endmodule\n");
		log("\n");
		log("Translates to the following JSON output:\n");
		log("\n");

		log("    {\n");
		log("      \"creator\": \"Yosys 0.9+2406 (git sha1 fb1168d8, clang 9.0.1 -fPIC -Os)\",\n");
		log("      \"modules\": {\n");
		log("        \"test\": {\n");
		log("          \"attributes\": {\n");
		log("            \"cells_not_processed\": \"00000000000000000000000000000001\",\n");
		log("            \"src\": \"test.v:1.1-4.10\"\n");
		log("          },\n");
		log("          \"ports\": {\n");
		log("            \"x\": {\n");
		log("              \"direction\": \"input\",\n");
		log("              \"bits\": [ 2 ]\n");
		log("            },\n");
		log("            \"y\": {\n");
		log("              \"direction\": \"input\",\n");
		log("              \"bits\": [ 3 ]\n");
		log("            }\n");
		log("          },\n");
		log("          \"cells\": {\n");
		log("            \"foo_inst\": {\n");
		log("              \"hide_name\": 0,\n");
		log("              \"type\": \"foo\",\n");
		log("              \"parameters\": {\n");
		log("                \"P\": \"00000000000000000000000000101010\",\n");
		log("                \"Q\": \"00000000000000000000010100111001\"\n");
		log("              },\n");
		log("              \"attributes\": {\n");
		log("                \"keep\": \"00000000000000000000000000000001\",\n");
		log("                \"module_not_derived\": \"00000000000000000000000000000001\",\n");
		log("                \"src\": \"test.v:3.1-3.55\"\n");
		log("              },\n");
		log("              \"connections\": {\n");
		log("                \"A\": [ 3, 2 ],\n");
		log("                \"B\": [ 2, 3 ],\n");
		log("                \"C\": [ 2, 2, 2, 2, \"0\", \"1\", \"0\", \"1\" ]\n");
		log("              }\n");
		log("            }\n");
		log("          },\n");
		log("          \"netnames\": {\n");
		log("            \"x\": {\n");
		log("              \"hide_name\": 0,\n");
		log("              \"bits\": [ 2 ],\n");
		log("              \"attributes\": {\n");
		log("                \"src\": \"test.v:1.19-1.20\"\n");
		log("              }\n");
		log("            },\n");
		log("            \"y\": {\n");
		log("              \"hide_name\": 0,\n");
		log("              \"bits\": [ 3 ],\n");
		log("              \"attributes\": {\n");
		log("                \"src\": \"test.v:1.22-1.23\"\n");
		log("              }\n");
		log("            }\n");
		log("          }\n");
		log("        }\n");
		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 specified nodes\n");
		log("\n");
		log("    [ \"nand\", <node-index>, <node-index>, <out-list> ]\n");
		log("      - the inverted ANDed value of the specified 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 unknown fields.\n");
		log("\n");
	}
	void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
	{
		bool aig_mode = false;
		bool compat_int_mode = false;

		size_t argidx;
		for (argidx = 1; argidx < args.size(); argidx++)
		{
			if (args[argidx] == "-aig") {
				aig_mode = true;
				continue;
			}
			if (args[argidx] == "-compat-int") {
				compat_int_mode = true;
				continue;
			}
			break;
		}
		extra_args(f, filename, args, argidx);

		log_header(design, "Executing JSON backend.\n");

		JsonWriter json_writer(*f, false, aig_mode, compat_int_mode);
		json_writer.write_design(design);
	}
} JsonBackend;

struct JsonPass : public Pass {
	JsonPass() : Pass("json", "write design in JSON format") { }
	void help() override
	{
		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
		log("\n");
		log("    json [options] [selection]\n");
		log("\n");
		log("Write a JSON netlist of all selected objects.\n");
		log("\n");
		log("    -o <filename>\n");
		log("        write to the specified file.\n");
		log("\n");
		log("    -aig\n");
		log("        also include AIG models for the different gate types\n");
		log("\n");
		log("    -compat-int\n");
		log("        emit 32-bit or smaller fully-defined parameter values directly\n");
		log("        as JSON numbers (for compatibility with old parsers)\n");
		log("\n");
		log("See 'help write_json' for a description of the JSON format used.\n");
		log("\n");
	}
	void execute(std::vector<std::string> args, RTLIL::Design *design) override
	{
		std::string filename;
		bool aig_mode = false;
		bool compat_int_mode = false;

		size_t argidx;
		for (argidx = 1; argidx < args.size(); argidx++)
		{
			if (args[argidx] == "-o" && argidx+1 < args.size()) {
				filename = args[++argidx];
				continue;
			}
			if (args[argidx] == "-aig") {
				aig_mode = true;
				continue;
			}
			if (args[argidx] == "-compat-int") {
				compat_int_mode = true;
				continue;
			}
			break;
		}
		extra_args(args, argidx, design);

		std::ostream *f;
		std::stringstream buf;

		if (!filename.empty()) {
			rewrite_filename(filename);
			std::ofstream *ff = new std::ofstream;
			ff->open(filename.c_str(), std::ofstream::trunc);
			if (ff->fail()) {
				delete ff;
				log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno));
			}
			f = ff;
		} else {
			f = &buf;
		}

		JsonWriter json_writer(*f, true, aig_mode, compat_int_mode);
		json_writer.write_design(design);

		if (!filename.empty()) {
			delete f;
		} else {
			log("%s", buf.str().c_str());
		}
	}
} JsonPass;

PRIVATE_NAMESPACE_END