diff --git a/backends/aiger2/Makefile.inc b/backends/aiger2/Makefile.inc new file mode 100644 index 000000000..494b8d6c6 --- /dev/null +++ b/backends/aiger2/Makefile.inc @@ -0,0 +1 @@ +OBJS += backends/aiger2/aiger.o diff --git a/backends/aiger2/aiger.cc b/backends/aiger2/aiger.cc new file mode 100644 index 000000000..3fc6ccdba --- /dev/null +++ b/backends/aiger2/aiger.cc @@ -0,0 +1,1471 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) Martin Povišer + * + * 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. + * + */ + +// TODOs: +// - gracefully handling inout ports (an error message probably) +// - undriven wires +// - zero-width operands + +#include "kernel/register.h" +#include "kernel/celltypes.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +#define BITWISE_OPS ID($buf), ID($not), ID($mux), ID($and), ID($or), ID($xor), ID($xnor), ID($fa), \ + ID($bwmux) + +#define REDUCE_OPS ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_xnor), ID($reduce_bool) + +#define LOGIC_OPS ID($logic_and), ID($logic_or), ID($logic_not) + +#define GATE_OPS ID($_BUF_), ID($_NOT_), ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), \ + ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_), ID($_MUX_), ID($_NMUX_), \ + ID($_AOI3_), ID($_OAI3_), ID($_AOI4_), ID($_OAI4_) + +#define CMP_OPS ID($eq), ID($ne), ID($lt), ID($le), ID($ge), ID($gt) + +// TODO +//#define ARITH_OPS ID($add), ID($sub), ID($neg) + +#define KNOWN_OPS BITWISE_OPS, REDUCE_OPS, LOGIC_OPS, GATE_OPS, ID($pos), CMP_OPS, \ + ID($pmux), ID($bmux) /*, ARITH_OPS*/ + +template +struct Index { + struct HierCursor; + struct ModuleInfo { + Module *module; + int len; + dict windices; + dict suboffsets; + pool found_blackboxes; + + bool indexing = false; + bool indexed = false; + }; + + dict modules; + + int index_wires(ModuleInfo &info, RTLIL::Module *m) + { + int sum = 0; + for (auto w : m->wires()) { + info.windices[w] = sum; + sum += w->width; + } + return sum; + } + + bool flatten = false; + bool inline_whiteboxes = false; + bool allow_blackboxes = false; + + int index_module(RTLIL::Module *m) + { + ModuleInfo &info = modules[m]; + + if (info.indexed) + return info.len; + + if (info.indexing && !info.indexed) + log_error("Hierarchy error\n"); + + info.module = m; + int pos = index_wires(info, m); + + for (auto cell : m->cells()) { + if (cell->type.in(KNOWN_OPS) || cell->type.in(ID($scopeinfo), ID($specify2), ID($specify3))) + continue; + + Module *submodule = m->design->module(cell->type); + + if (submodule && flatten && + !submodule->get_bool_attribute(ID::keep_hierarchy) && + !submodule->get_blackbox_attribute(inline_whiteboxes)) { + info.suboffsets[cell] = pos; + pos += index_module(submodule); + } else { + if (allow_blackboxes) { + info.found_blackboxes.insert(cell); + } else { + if (!submodule || submodule->get_blackbox_attribute()) + log_error("Unsupported cell type: %s (%s in %s)\n", + log_id(cell->type), log_id(cell), log_id(m)); + } + } + } + + info.len = pos; + return info.len; + } + + Design *design; + Module *top; + ModuleInfo *top_minfo; + std::vector lits; + + Index() + { + } + + void setup(RTLIL::Module *top) + { + design = top->design; + this->top = top; + + modules.reserve(top->design->modules().size()); + int nlits = index_module(top); + log_debug("allocating for %d literals\n", nlits); + lits.resize(nlits, Writer::EMPTY_LIT); + top_minfo = &modules.at(top); + } + + bool const_folding = true; + bool strashing = false; + dict, Lit> cache; + + Lit AND(Lit a, Lit b) + { + if (const_folding) { + if (a == CFALSE || b == CFALSE) + return CFALSE; + if (a == CTRUE) + return b; + if (b == CTRUE) + return a; + } + + if (!strashing) { + return (static_cast(this))->emit_gate(a, b); + } else { + if (a < b) std::swap(a, b); + auto pair = std::make_pair(a, b); + + if (!cache.count(pair)) { + Lit nl = (static_cast(this))->emit_gate(a, b); + cache[pair] = nl; + return nl; + } else { + return cache.at(pair); + } + } + } + + Lit NOT(Lit lit) + { + return Writer::negate(lit); + } + + Lit OR(Lit a, Lit b) + { + return NOT(AND(NOT(a), NOT(b))); + } + + Lit MUX(Lit a, Lit b, Lit s) + { + if (const_folding) { + if (a == b) + return a; + if (s == CFALSE) + return a; + if (s == CTRUE) + return b; + } + + return OR(AND(a, NOT(s)), AND(b, s)); + } + + Lit XOR(Lit a, Lit b) + { + return OR(AND(a, NOT(b)), AND(NOT(a), b)); + } + + Lit XNOR(Lit a, Lit b) + { + return NOT(OR(AND(a, NOT(b)), AND(NOT(a), b))); + } + + Lit CARRY(Lit a, Lit b, Lit c) + { + if (const_folding) { + if (c == CTRUE) { + return OR(a, b); + } else if (c == CFALSE) { + return AND(a, b); + } + } + return OR(AND(a, b), AND(c, OR(a, b))); + } + + Lit REDUCE(std::vector lits, bool op_xor=false) + { + std::vector next; + while (lits.size() > 1) { + next.clear(); + for (int i = 0; i < (int) lits.size(); i += 2) { + if (i + 1 >= (int) lits.size()) { + next.push_back(lits[i]); + } else { + Lit a = lits[i], b = lits[i + 1]; + next.push_back(op_xor ? XOR(a, b) : AND(a, b)); + } + } + next.swap(lits); + } + + if (lits.empty()) + return op_xor ? CFALSE : CTRUE; + else + return lits.front(); + } + + Lit impl_op(HierCursor &cursor, Cell *cell, IdString oport, int obit) + { + if (cell->type.in(REDUCE_OPS, LOGIC_OPS, CMP_OPS) && obit != 0) { + return CFALSE; + } else if (cell->type.in(CMP_OPS)) { + SigSpec aport = cell->getPort(ID::A); + bool asigned = cell->getParam(ID::A_SIGNED).as_bool(); + SigSpec bport = cell->getPort(ID::B); + bool bsigned = cell->getParam(ID::B_SIGNED).as_bool(); + + int width = std::max(aport.size(), bport.size()) + 1; + aport.extend_u0(width, asigned); + bport.extend_u0(width, bsigned); + + if (cell->type.in(ID($eq), ID($ne))) { + int carry = CTRUE; + for (int i = 0; i < width; i++) { + Lit a = visit(cursor, aport[i]); + Lit b = visit(cursor, bport[i]); + carry = AND(carry, XNOR(a, b)); + } + return (cell->type == ID($eq)) ? carry : /* $ne */ NOT(carry); + } else if (cell->type.in(ID($lt), ID($le), ID($gt), ID($ge))) { + if (cell->type.in(ID($gt), ID($ge))) + std::swap(aport, bport); + int carry = cell->type.in(ID($le), ID($ge)) ? CFALSE : CTRUE; + Lit a, b; + // TODO: this might not be the most economic structure; revisit at a later date + for (int i = 0; i < width; i++) { + a = visit(cursor, aport[i]); + b = visit(cursor, bport[i]); + if (i != width - 1) + carry = CARRY(a, NOT(b), carry); + } + return XOR(carry, XNOR(a, b)); + } else { + log_abort(); + } + } else if (cell->type.in(REDUCE_OPS, ID($logic_not))) { + SigSpec inport = cell->getPort(ID::A); + + std::vector lits; + for (int i = 0; i < inport.size(); i++) { + Lit lit = visit(cursor, inport[i]); + if (cell->type.in(ID($reduce_and), ID($reduce_xor), ID($reduce_xnor))) { + lits.push_back(lit); + } else if (cell->type.in(ID($reduce_or), ID($reduce_bool), ID($logic_not))) { + lits.push_back(NOT(lit)); + } else { + log_abort(); + } + } + + Lit acc = REDUCE(lits, cell->type.in(ID($reduce_xor), ID($reduce_xnor))); + + if (!cell->type.in(ID($reduce_xnor), ID($reduce_or), ID($reduce_bool))) + return acc; + else + return NOT(acc); + } else if (cell->type.in(ID($logic_and), ID($logic_or))) { + SigSpec aport = cell->getPort(ID::A); + SigSpec bport = cell->getPort(ID::B); + + log_assert(aport.size() > 0 && bport.size() > 0); // TODO + + Lit a = visit(cursor, aport[0]); + for (int i = 1; i < aport.size(); i++) { + Lit l = visit(cursor, aport[i]); + a = OR(a, l); + } + + Lit b = visit(cursor, bport[0]); + for (int i = 1; i < bport.size(); i++) { + Lit l = visit(cursor, bport[i]); + b = OR(b, l); + } + + if (cell->type == ID($logic_and)) + return AND(a, b); + else if (cell->type == ID($logic_or)) + return OR(a, b); + else + log_abort(); + } else if (cell->type.in(BITWISE_OPS, GATE_OPS, ID($pos))) { + SigSpec aport = cell->getPort(ID::A); + Lit a; + if (obit < aport.size()) { + a = visit(cursor, aport[obit]); + } else { + if (cell->getParam(ID::A_SIGNED).as_bool()) + a = visit(cursor, aport.msb()); + else + a = CFALSE; + } + + if (cell->type.in(ID($buf), ID($pos), ID($_BUF_))) { + return a; + } else if (cell->type.in(ID($not), ID($_NOT_))) { + return NOT(a); + } else { + SigSpec bport = cell->getPort(ID::B); + Lit b; + if (obit < bport.size()) { + b = visit(cursor, bport[obit]); + } else { + if (cell->getParam(ID::B_SIGNED).as_bool()) + b = visit(cursor, bport.msb()); + else + b = CFALSE; + } + + if (cell->type.in(ID($and), ID($_AND_))) { + return AND(a, b); + } else if (cell->type.in(ID($_NAND_))) { + return NOT(AND(a, b)); + } else if (cell->type.in(ID($or), ID($_OR_))) { + return OR(a, b); + } else if (cell->type.in(ID($_NOR_))) { + return NOT(OR(a, b)); + } else if (cell->type.in(ID($xor), ID($_XOR_))) { + return XOR(a, b); + } else if (cell->type.in(ID($xnor), ID($_XNOR_))) { + return NOT(XOR(a, b)); + } else if (cell->type.in(ID($_ANDNOT_))) { + return AND(a, NOT(b)); + } else if (cell->type.in(ID($_ORNOT_))) { + return OR(a, NOT(b)); + } else if (cell->type.in(ID($mux), ID($_MUX_))) { + Lit s = visit(cursor, cell->getPort(ID::S)); + return MUX(a, b, s); + } else if (cell->type.in(ID($bwmux))) { + Lit s = visit(cursor, cell->getPort(ID::S)[obit]); + return MUX(a, b, s); + } else if (cell->type.in(ID($_NMUX_))) { + Lit s = visit(cursor, cell->getPort(ID::S)[obit]); + return NOT(MUX(a, b, s)); + } else if (cell->type.in(ID($fa))) { + Lit c = visit(cursor, cell->getPort(ID::C)[obit]); + Lit ab = XOR(a, b); + if (oport == ID::Y) { + return XOR(ab, c); + } else /* oport == ID::X */ { + return OR(AND(a, b), AND(c, ab)); + } + } else if (cell->type.in(ID($_AOI3_), ID($_OAI3_), ID($_AOI4_), ID($_OAI4_))) { + Lit c, d; + + c = visit(cursor, cell->getPort(ID::C)[obit]); + if (/* 4 input types */ cell->type.in(ID($_AOI4_), ID($_OAI4_))) + d = visit(cursor, cell->getPort(ID::D)[obit]); + else + d = cell->type == ID($_AOI3_) ? 1 : 0; + + if (/* aoi */ cell->type.in(ID($_AOI3_), ID($_AOI4_))) + return NOT(OR(AND(a, b), AND(c, d))); + else + return NOT(AND(OR(a, b), OR(c, d))); + } else { + log_abort(); + } + } + } else if (cell->type == ID($pmux)) { + SigSpec aport = cell->getPort(ID::A); + SigSpec bport = cell->getPort(ID::B); + SigSpec sport = cell->getPort(ID::S); + int width = aport.size(); + + Lit a = visit(cursor, aport[obit]); + + std::vector bar, sels; + for (int i = 0; i < sport.size(); i++) { + Lit s = visit(cursor, sport[i]); + Lit b = visit(cursor, bport[width * i + obit]); + bar.push_back(NOT(AND(s, b))); + sels.push_back(NOT(s)); + } + + return OR(AND(REDUCE(sels), a), NOT(REDUCE(bar))); + } else if (cell->type == ID($bmux)) { + SigSpec aport = cell->getPort(ID::A); + SigSpec sport = cell->getPort(ID::S); + int width = cell->getParam(ID::WIDTH).as_int(); + + std::vector data; + for (int i = obit; i < aport.size(); i += width) + data.push_back(visit(cursor, aport[i])); + + std::vector next; + for (int i = 0; i < sport.size(); i++) { + Lit s = visit(cursor, sport[i]); + next.clear(); + for (int j = 0; j < (int) data.size(); j += 2) + next.push_back(MUX(data[j], data[j + 1], s)); + data.swap(next); + } + log_assert(data.size() == 1); + return data[0]; + } else { + log_abort(); + } + } + + struct HierCursor { + typedef std::pair Level; + std::vector levels; + int instance_offset = 0; + + HierCursor() + { + } + + ModuleInfo &leaf_minfo(Index &index) + { + if (levels.empty()) + return *index.top_minfo; + else + return levels.back().first; + } + + Module *leaf_module(Index &index) + { + return leaf_minfo(index).module; + } + + int bitwire_index(Index &index, SigBit bit) + { + log_assert(bit.wire != nullptr); + return instance_offset + leaf_minfo(index).windices[bit.wire] + bit.offset; + } + + Cell *exit(Index &index) + { + log_assert(!levels.empty()); + Cell *instance = levels.back().second; + + levels.pop_back(); + instance_offset -= leaf_minfo(index).suboffsets.at(instance); + + // return the instance we just exited + return instance; + } + + Module *enter(Index &index, Cell *cell) + { + Design *design = index.design; + auto &minfo = leaf_minfo(index); + log_assert(minfo.suboffsets.count(cell)); + Module *def = design->module(cell->type); + log_assert(def); + levels.push_back(Level(index.modules.at(def), cell)); + instance_offset += minfo.suboffsets.at(cell); + + // return the module definition we just entered + return def; + } + + bool is_top() + { + return levels.empty(); + } + + std::string path() + { + std::string ret; + bool first = true; + for (auto pair : levels) { + if (!first) + ret += "."; + if (!pair.second) + ret += RTLIL::unescape_id(pair.first.module->name); + else + ret += RTLIL::unescape_id(pair.second->name); + first = false; + } + return ret; + } + + int hash() const + { + int hash = 0; + for (auto pair : levels) + hash += (uintptr_t) pair.second; + return hash; + } + + bool operator==(const HierCursor &other) const + { + if (levels.size() != other.levels.size()) + return false; + + for (int i = 0; i < levels.size(); i++) + if (levels[i].second != other.levels[i].second) + return false; + + return true; + } + }; + + bool visit_hook(int, HierCursor&, SigBit) + { + return false; + } + + Lit visit(HierCursor &cursor, SigBit bit) + { + if (!bit.wire) { + if (bit == State::S1) + return CTRUE; + else if (bit == State::S0) + return CFALSE; + else if (bit == State::Sx) + return CFALSE; + else + log_error("Unhandled state %s\n", log_signal(bit)); + } + + int idx = cursor.bitwire_index(*this, bit); + if (lits[idx] != Writer::EMPTY_LIT) { + // literal already assigned + return lits[idx]; + } + + // provide means for the derived class to override + // the visit behavior + if ((static_cast(this))->visit_hook(idx, cursor, bit)) { + return lits[idx]; + } + + Lit ret; + if (!bit.wire->port_input) { + // an output of a cell + Cell *driver = bit.wire->driverCell(); + + if (driver->type.in(KNOWN_OPS)) { + ret = impl_op(cursor, driver, bit.wire->driverPort(), bit.offset); + } else { + Module *def = cursor.enter(*this, driver); + { + IdString portname = bit.wire->driverPort(); + Wire *w = def->wire(portname); + if (!w) + log_error("Output port %s on instance %s of %s doesn't exist\n", + log_id(portname), log_id(driver), log_id(def)); + if (bit.offset >= w->width) + log_error("Bit position %d of output port %s on instance %s of %s is out of range (port has width %d)\n", + bit.offset, log_id(portname), log_id(driver), log_id(def), w->width); + ret = visit(cursor, SigBit(w, bit.offset)); + } + cursor.exit(*this); + } + } else { + // a module input: we cannot be the top module, otherwise + // the branch for pre-existing literals would have been taken + log_assert(!cursor.is_top()); + + // step into the upper module + Cell *instance = cursor.exit(*this); + { + IdString portname = bit.wire->name; + if (!instance->hasPort(portname)) + log_error("Input port %s on instance %s of %s unconnected\n", + log_id(portname), log_id(instance), log_id(instance->type)); + auto &port = instance->getPort(portname); + if (bit.offset >= port.size()) + log_error("Bit %d of input port %s on instance %s of %s unconnected\n", + bit.offset, log_id(portname), log_id(instance), log_id(instance->type)); + ret = visit(cursor, port[bit.offset]); + } + cursor.enter(*this, instance); + } + + lits[idx] = ret; + return ret; + } + + Lit &pi_literal(SigBit bit, HierCursor *cursor=nullptr) + { + log_assert(bit.wire); + + if (!cursor) { + log_assert(bit.wire->module == top); + log_assert(bit.wire->port_input); + return lits[top_minfo->windices[bit.wire] + bit.offset]; + } else { + log_assert(bit.wire->module == cursor->leaf_module(*this)); + return lits[cursor->bitwire_index(*this, bit)]; + } + } + + Lit eval_po(SigBit bit, HierCursor *cursor=nullptr) + { + Lit ret; + if (!cursor) { + HierCursor cursor_; + ret = visit(cursor_, bit); + log_assert(cursor_.is_top()); + log_assert(cursor_.instance_offset == 0); + } else { + ret = visit(*cursor, bit); + } + return ret; + } + + void visit_hierarchy(std::function f, + HierCursor &cursor) + { + f(cursor); + + ModuleInfo &minfo = cursor.leaf_minfo(*this); + for (auto cell : minfo.module->cells()) { + if (minfo.suboffsets.count(cell)) { + cursor.enter(*this, cell); + visit_hierarchy(f, cursor); + cursor.exit(*this); + } + } + } + + void visit_hierarchy(std::function f) + { + HierCursor cursor; + visit_hierarchy(f, cursor); + } +}; + +struct AigerWriter : Index { + typedef unsigned int Lit; + + const static Lit CONST_FALSE = 0; + const static Lit CONST_TRUE = 1; + const static constexpr Lit EMPTY_LIT = std::numeric_limits::max(); + + static Lit negate(Lit lit) { + return lit ^ 1; + } + + std::ostream *f; + Lit lit_counter; + int ninputs, nlatches, noutputs, nands; + + void encode(int delta) + { + log_assert(delta >= 0); + unsigned int x = delta; + while (x & ~0x7f) { + f->put((x & 0x7f) | 0x80); + x = x >> 7; + } + f->put(x); + } + + Lit emit_gate(Lit a, Lit b) + { + Lit out = lit_counter; + nands++; + lit_counter += 2; + + if (a < b) std::swap(a, b); + encode(out - a); + encode(a - b); + return out; + } + + void reset_counters() + { + lit_counter = 2; + ninputs = nlatches = noutputs = nands = 0; + } + + void write_header() { + log_assert(lit_counter == (Lit) (ninputs + nlatches + nands) * 2 + 2); + + char buf[128]; + snprintf(buf, sizeof(buf) - 1, "aig %08d %08d %08d %08d %08d\n", + ninputs + nlatches + nands, ninputs, nlatches, noutputs, nands); + f->write(buf, strlen(buf)); + } + + void write(std::ostream *f) { + reset_counters(); + + auto file_start = f->tellp(); + + // populate inputs + std::vector inputs; + for (auto id : top->ports) { + Wire *w = top->wire(id); + log_assert(w); + if (w->port_input) + for (int i = 0; i < w->width; i++) { + pi_literal(SigBit(w, i)) = lit_counter; + inputs.push_back(SigBit(w, i)); + lit_counter += 2; + ninputs++; + } + } + + this->f = f; + // start with the header + write_header(); + // insert padding where output literals will go (once known) + for (auto id : top->ports) { + Wire *w = top->wire(id); + log_assert(w); + if (w->port_output) { + for (auto bit : SigSpec(w)) { + (void) bit; + char buf[16]; + snprintf(buf, sizeof(buf) - 1, "%08d\n", 0); + f->write(buf, strlen(buf)); + noutputs++; + } + } + } + auto data_start = f->tellp(); + + // now the guts + std::vector> outputs; + for (auto w : top->wires()) + if (w->port_output) { + for (auto bit : SigSpec(w)) + outputs.push_back({bit, eval_po(bit)}); + } + auto data_end = f->tellp(); + + // revisit header and the list of outputs + f->seekp(file_start); + write_header(); + for (auto pair : outputs) { + char buf[16]; + snprintf(buf, sizeof(buf) - 1, "%08d\n", pair.second); + f->write(buf, strlen(buf)); + } + // double check we arrived at the same offset for the + // main data section + log_assert(data_start == f->tellp()); + + f->seekp(data_end); + int i = 0; + for (auto pair : outputs) { + if (SigSpec(pair.first).is_wire()) { + char buf[32]; + snprintf(buf, sizeof(buf) - 1, "o%d ", i); + f->write(buf, strlen(buf)); + std::string name = RTLIL::unescape_id(pair.first.wire->name); + f->write(name.data(), name.size()); + f->put('\n'); + } + i++; + } + i = 0; + for (auto bit : inputs) { + if (SigSpec(bit).is_wire()) { + char buf[32]; + snprintf(buf, sizeof(buf) - 1, "i%d ", i); + f->write(buf, strlen(buf)); + std::string name = RTLIL::unescape_id(bit.wire->name); + f->write(name.data(), name.size()); + f->put('\n'); + } + i++; + } + } +}; + +struct XAigerAnalysis : Index { + const static int CONST_FALSE = 0; + const static int CONST_TRUE = 0; + const static constexpr int EMPTY_LIT = -1; + + XAigerAnalysis() + { + allow_blackboxes = true; + + // Disable const folding and strashing as literal values are not unique + const_folding = false; + strashing = false; + } + + static int negate(int lit) + { + return lit; + } + + int emit_gate(int a, int b) + { + return max(a, b) + 1; + } + + pool seen; + + bool visit_hook(int idx, HierCursor &cursor, SigBit bit) + { + log_assert(cursor.is_top()); // TOOD: fix analyzer to work with hierarchy + + if (bit.wire->port_input) + return false; + + Cell *driver = bit.wire->driverCell(); + if (!driver->type.isPublic()) + return false; + + Module *mod = design->module(driver->type); + log_assert(mod); + if (!mod->has_attribute(ID::abc9_box_id)) + return false; + + int max = 1; + for (auto wire : mod->wires()) + if (wire->port_input) + for (int i = 0; i < wire->width; i++) { + int ilevel = visit(cursor, driver->getPort(wire->name)[i]); + max = std::max(max, ilevel + 1); + } + lits[idx] = max; + + if (!seen.count(driver)) + seen.insert(driver); + + return true; + } + + void analyze(Module *top) + { + setup(top); + + for (auto id : top->ports) { + Wire *w = top->wire(id); + log_assert(w); + if (w->port_input) + for (int i = 0; i < w->width; i++) + pi_literal(SigBit(w, i)) = 0; + } + + HierCursor cursor; + for (auto box : top_minfo->found_blackboxes) { + Module *def = design->module(box->type); + if (!box->type.isPublic() || (def && !def->has_attribute(ID::abc9_box_id))) + for (auto &conn : box->connections_) + if (box->output(conn.first)) + for (auto bit : conn.second) + pi_literal(bit, &cursor) = 0; + } + + for (auto w : top->wires()) + if (w->port_output) { + for (auto bit : SigSpec(w)) + (void) eval_po(bit); + } + + for (auto box : top_minfo->found_blackboxes) { + Module *def = design->module(box->type); + if (!box->type.isPublic() || (def && !def->has_attribute(ID::abc9_box_id))) + for (auto &conn : box->connections_) + if (box->input(conn.first)) + for (auto bit : conn.second) + (void) eval_po(bit); + } + } +}; + +struct XAigerWriter : AigerWriter { + XAigerWriter() + { + allow_blackboxes = true; + } + + bool mapping_prep = false; + pool keep_wires; + std::ofstream map_file; + + typedef std::pair HierBit; + std::vector pos; + std::vector pis; + int proper_pos_counter = 0; + + pool driven_by_opaque_box; + + void ensure_pi(SigBit bit, HierCursor cursor={}, + bool box_port=false) + { + Lit &lit = pi_literal(bit, &cursor); + if (lit == EMPTY_LIT) { + lit = lit_counter; + pis.push_back(std::make_pair(bit, cursor)); + lit_counter += 2; + if (map_file.is_open() && !box_port) { + log_assert(cursor.is_top()); // TODO + driven_by_opaque_box.insert(bit); + map_file << "pi " << pis.size() - 1 << " " << bit.offset + << " " << bit.wire->name.c_str() << "\n"; + } + } else { + log_assert(!box_port); + } + } + + bool is_pi(SigBit bit, HierCursor cursor={}) + { + return pi_literal(bit, &cursor) != EMPTY_LIT; + } + + void pad_pi() + { + pis.push_back(std::make_pair(RTLIL::Sx, HierCursor{})); + lit_counter += 2; + } + + void append_box_ports(Cell *box, HierCursor &cursor, bool inputs) + { + for (auto &conn : box->connections_) { + bool is_input = box->input(conn.first); + bool is_output = box->output(conn.first); + + if (!(is_input || is_output) || (is_input && is_output)) + log_error("Ambiguous port direction on %s/%s\n", + log_id(box->type), log_id(conn.first)); + + if (is_input && inputs) { + int bitp = 0; + for (auto bit : conn.second) { + if (!bit.wire) { + bitp++; + continue; + } + + if (map_file.is_open()) { + log_assert(cursor.is_top()); + map_file << "pseudopo " << proper_pos_counter++ << " " << bitp + << " " << box->name.c_str() + << " " << conn.first.c_str() << "\n"; + } + + pos.push_back(std::make_pair(bit, cursor)); + + if (mapping_prep) + conn.second[bitp] = RTLIL::Sx; + + bitp++; + } + } else if (is_output && !inputs) { + for (auto &bit : conn.second) { + if (!bit.wire || bit.wire->port_input) + log_error("Bad connection"); + + + ensure_pi(bit, cursor); + keep_wires.insert(bit.wire); + } + } + } + } + + RTLIL::Module *holes_module; + + std::stringstream h_buffer; + static void write_be32(std::ostream &buffer, uint32_t u32) + { + typedef unsigned char uchar; + unsigned char u32_be[4] = { + (uchar) (u32 >> 24), (uchar) (u32 >> 16), (uchar) (u32 >> 8), (uchar) u32 + }; + buffer.write((char *) u32_be, sizeof(u32_be)); + } + + void prep_boxes(int pending_pos_num) + { + XAigerAnalysis analysis; + log_debug("preforming analysis on '%s'\n", log_id(top)); + analysis.analyze(top); + log_debug("analysis on '%s' done\n", log_id(top)); + + // boxes which have timing data, maybe a whitebox model + std::vector> nonopaque_boxes; + // boxes which are fully opaque + std::vector> opaque_boxes; + + log_debug("found boxes:\n"); + visit_hierarchy([&](HierCursor &cursor) { + auto &minfo = cursor.leaf_minfo(*this); + + for (auto box : minfo.found_blackboxes) { + log_debug(" - %s.%s (type %s): ", cursor.path().c_str(), + RTLIL::unescape_id(box->name).c_str(), + log_id(box->type)); + + Module *box_module = design->module(box->type), *box_derived; + + if (box_module && !box->parameters.empty()) { + // TODO: This is potentially costly even if a cached derivation exists + box_derived = design->module(box_module->derive(design, box->parameters)); + log_assert(box_derived); + } else { + box_derived = box_module; + } + + if (box_derived && box_derived->has_attribute(ID::abc9_box_id)) { + // This is an ABC9 box, we have timing data, maybe even a whitebox model + // These need to go last in the AIGER port list. + nonopaque_boxes.push_back(std::make_tuple(cursor, box, box_derived)); + log_debug("non-opaque\n"); + } else { + opaque_boxes.push_back(std::make_tuple(cursor, box, box_derived)); + log_debug("opaque\n"); + } + } + }); + + for (auto [cursor, box, def] : opaque_boxes) + append_box_ports(box, cursor, false); + + holes_module = design->addModule(NEW_ID); + std::vector holes_pis; + int boxes_ci_num = 0, boxes_co_num = 0; + + int box_seq = 0; + + std::vector boxes_order(analysis.seen.begin(), analysis.seen.end()); + std::reverse(boxes_order.begin(), boxes_order.end()); + + nonopaque_boxes.clear(); + for (auto box : boxes_order) { + HierCursor cursor; + Module *def = design->module(box->type); + nonopaque_boxes.push_back(std::make_tuple(cursor, box, def)); + } + + for (auto [cursor, box, def] : nonopaque_boxes) { + // use `def->name` not `box->type` as we want the derived type + Cell *holes_wb = holes_module->addCell(NEW_ID, def->name); + int holes_pi_idx = 0; + + if (map_file.is_open()) { + log_assert(cursor.is_top()); + map_file << "box " << box_seq << " " << box->name.c_str() << "\n"; + } + box_seq++; + + for (auto port_id : def->ports) { + Wire *port = def->wire(port_id); + log_assert(port); + + SigSpec conn = box->hasPort(port_id) ? box->getPort(port_id) : SigSpec{}; + + if (port->port_input && !port->port_output) { + // primary + for (int i = 0; i < port->width; i++) { + SigBit bit; + if (i < conn.size()) { + bit = conn[i]; + } else { + // FIXME: hierarchical path + log_warning("connection on port %s[%d] of instance %s (type %s) missing, using 1'bx\n", + log_id(port_id), i, log_id(box), log_id(box->type)); + bit = RTLIL::Sx; + } + + pos.push_back(std::make_pair(bit, cursor)); + } + boxes_co_num += port->width; + + if (mapping_prep && !conn.empty()) + box->setPort(port_id, SigSpec(RTLIL::Sx, conn.size())); + + // holes + SigSpec in_conn; + for (int i = 0; i < port->width; i++) { + while (holes_pi_idx >= (int) holes_pis.size()) { + Wire *w = holes_module->addWire(NEW_ID, 1); + w->port_input = true; + holes_module->ports.push_back(w->name); + holes_pis.push_back(w); + } + in_conn.append(holes_pis[i]); + holes_pi_idx++; + } + holes_wb->setPort(port_id, in_conn); + } else if (port->port_output && !port->port_input) { + // primary + for (int i = 0; i < port->width; i++) { + SigBit bit; + if (i < conn.size() && conn[i].is_wire()) { + bit = conn[i]; + } else { + // FIXME: hierarchical path + log_warning("connection on port %s[%d] of instance %s (type %s) missing\n", + log_id(port_id), i, log_id(box), log_id(box->type)); + pad_pi(); + continue; + } + + ensure_pi(bit, cursor, true); + keep_wires.insert(bit.wire); + } + boxes_ci_num += port->width; + + // holes + Wire *w = holes_module->addWire(NEW_ID, port->width); + w->port_output = true; + holes_module->ports.push_back(w->name); + holes_wb->setPort(port_id, w); + } else { + log_error("Ambiguous port direction on %s/%s\n", + log_id(box->type), log_id(port_id)); + } + } + } + + for (auto [cursor, box, def] : opaque_boxes) + append_box_ports(box, cursor, true); + + write_be32(h_buffer, 1); + write_be32(h_buffer, pis.size()); + log_debug("ciNum = %zu\n", pis.size()); + write_be32(h_buffer, pending_pos_num + pos.size()); + log_debug("coNum = %zu\n", pending_pos_num + pos.size()); + write_be32(h_buffer, pis.size() - boxes_ci_num); + log_debug("piNum = %zu\n", pis.size() - boxes_ci_num); + write_be32(h_buffer, pending_pos_num + pos.size() - boxes_co_num); + log_debug("poNum = %zu\n", pending_pos_num + pos.size() - boxes_co_num); + write_be32(h_buffer, nonopaque_boxes.size()); + + box_seq = 0; + for (auto [cursor, box, def] : nonopaque_boxes) { + int box_ci_num = 0, box_co_num = 0; + for (auto port_id : def->ports) { + Wire *port = def->wire(port_id); + log_assert(port); + if (port->port_input && !port->port_output) { + box_co_num += port->width; + } else if (port->port_output && !port->port_input) { + box_ci_num += port->width; + } else { + log_abort(); + } + } + + write_be32(h_buffer, box_co_num); + write_be32(h_buffer, box_ci_num); + write_be32(h_buffer, def->attributes.at(ID::abc9_box_id).as_int()); + write_be32(h_buffer, box_seq++); + } + } + + void clear_boxes() + { + design->remove(holes_module); + } + + void write(std::ostream *f) { + reset_counters(); + + for (auto w : top->wires()) + if (w->port_input) + for (int i = 0; i < w->width; i++) + ensure_pi(SigBit(w, i)); + + int proper_po_num = 0; + for (auto w : top->wires()) + if (w->port_output) + proper_po_num += w->width; + + prep_boxes(proper_po_num); + for (auto w : top->wires()) + if (w->port_output) + for (int i = 0; i < w->width; i++) { + if (map_file.is_open() && !driven_by_opaque_box.count(SigBit(w, i))) { + map_file << "po " << proper_pos_counter++ << " " << i + << " " << w->name.c_str() << "\n"; + } + pos.push_back(std::make_pair(SigBit(w, i), HierCursor{})); + } + + this->f = f; + // start with the header + ninputs = pis.size(); + noutputs = pos.size(); + write_header(); + // insert padding where output literals will go (once known) + for (auto _ : pos) { + char buf[16]; + snprintf(buf, sizeof(buf) - 1, "%08d\n", 0); + f->write(buf, strlen(buf)); + } + auto data_start = f->tellp(); + + // now the guts + std::vector outlits; + for (auto &pair : pos) + outlits.push_back(eval_po(pair.first, &pair.second)); + + // revisit header and the list of outputs + f->seekp(0); + ninputs = pis.size(); + noutputs = pos.size(); + write_header(); + for (auto lit : outlits) { + char buf[16]; + snprintf(buf, sizeof(buf) - 1, "%08d\n", lit); + f->write(buf, strlen(buf)); + } + // double check we arrived at the same offset for the + // main data section + log_assert(data_start == f->tellp()); + + // extensions + f->seekp(0, std::ios::end); + + f->put('c'); + + // insert empty 'r' and 's' sections (abc crashes if we provide 'a' without those) + f->put('r'); + write_be32(*f, 4); + write_be32(*f, 0); + f->put('s'); + write_be32(*f, 4); + write_be32(*f, 0); + + f->put('h'); + // TODO: get rid of std::string copy + std::string h_buffer_str = h_buffer.str(); + write_be32(*f, h_buffer_str.size()); + f->write(h_buffer_str.data(), h_buffer_str.size()); + +#if 1 + f->put('a'); + write_be32(*f, 0); // size to be filled later + auto holes_aiger_start = f->tellp(); + { + AigerWriter holes_writer; + holes_writer.flatten = true; + holes_writer.inline_whiteboxes = true; + holes_writer.setup(holes_module); + holes_writer.write(f); + } + auto holes_aiger_size = f->tellp() - holes_aiger_start; + f->seekp(holes_aiger_start, std::ios::beg); + f->seekp(-4, std::ios::cur); + write_be32(*f, holes_aiger_size); +#endif + f->seekp(0, std::ios::end); + + if (mapping_prep) { + std::vector to_remove_cells; + for (auto cell : top->cells()) + if (!top_minfo->found_blackboxes.count(cell)) + to_remove_cells.push_back(cell); + for (auto cell : to_remove_cells) + top->remove(cell); + pool to_remove; + for (auto wire : top->wires()) + if (!wire->port_input && !wire->port_output && !keep_wires.count(wire)) + to_remove.insert(wire); + top->remove(to_remove); + } + + clear_boxes(); + } +}; + +struct Aiger2Backend : Backend { + Aiger2Backend() : Backend("aiger2", "(experimental) write design to AIGER file") + { + experimental(); + } + + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" write_aiger2 [options] [filename]\n"); + log("\n"); + log("Write the selected module to an AIGER file.\n"); + log("\n"); + log(" -strash\n"); + log(" perform structural hashing while writing\n"); + log("\n"); + log(" -flatten\n"); + log(" allow descending into submodules and write a flattened view of the design\n"); + log(" hierarchy starting at the selected top\n"); + log("\n"); + log("This command is able to ingest all combinational cells except for:\n"); + log("\n"); + pool supported = {KNOWN_OPS}; + CellTypes ct; + ct.setup_internals_eval(); + log(" "); + int col = 0; + for (auto pair : ct.cell_types) + if (!supported.count(pair.first)) { + if (col + pair.first.size() + 2 > 72) { + log("\n "); + col = 0; + } + col += pair.first.size() + 2; + log("%s, ", log_id(pair.first)); + } + log("\n"); + log("\n"); + log("And all combinational gates except for:\n"); + log("\n"); + CellTypes ct2; + ct2.setup_stdcells(); + log(" "); + col = 0; + for (auto pair : ct2.cell_types) + if (!supported.count(pair.first)) { + if (col + pair.first.size() + 2 > 72) { + log("\n "); + col = 0; + } + col += pair.first.size() + 2; + log("%s, ", log_id(pair.first)); + } + log("\n"); + } + + void execute(std::ostream *&f, std::string filename, std::vector args, Design *design) override + { + log_header(design, "Executing AIGER2 backend.\n"); + + size_t argidx; + AigerWriter writer; + writer.const_folding = true; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-strash") + writer.strashing = true; + else if (args[argidx] == "-flatten") + writer.flatten = true; + else + break; + } + extra_args(f, filename, args, argidx); + + Module *top = design->top_module(); + + if (!top || !design->selected_whole_module(top)) + log_cmd_error("No top module selected\n"); + + design->bufNormalize(true); + writer.setup(top); + writer.write(f); + + // we are leaving the sacred land, un-bufnormalize + // (if not, this will lead to bugs: the buf-normalized + // flag must not be kept on past the code that can work + // with it) + design->bufNormalize(false); + } +} Aiger2Backend; + +struct XAiger2Backend : Backend { + XAiger2Backend() : Backend("xaiger2", "(experimental) write module to XAIGER file") + { + experimental(); + } + + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" write_xaiger2 [options] [filename]\n"); + log("\n"); + log("Write the selected module to a XAIGER file including the 'h' and 'a' extensions\n"); + log("with box information for ABC.\n"); + log("\n"); + log(" -strash\n"); + log(" perform structural hashing while writing\n"); + log("\n"); + log(" -flatten\n"); + log(" allow descending into submodules and write a flattened view of the design\n"); + log(" hierarchy starting at the selected top\n"); + log("\n"); + log(" -mapping_prep\n"); + log(" after the file is written, prepare the module for reintegration of\n"); + log(" a mapping in a subsequent command. all cells which are not blackboxed nor\n"); + log(" whiteboxed are removed from the design as well as all wires which only\n"); + log(" connect to removed cells\n"); + log(" (conflicts with -flatten)\n"); + log("\n"); + log(" -map2 \n"); + log(" write a map2 file which 'read_xaiger2 -sc_mapping' can read to\n"); + log(" reintegrate a mapping\n"); + log(" (conflicts with -flatten)\n"); + log("\n"); + } + + void execute(std::ostream *&f, std::string filename, std::vector args, Design *design) override + { + log_header(design, "Executing XAIGER2 backend.\n"); + + size_t argidx; + XAigerWriter writer; + std::string map_filename; + writer.const_folding = true; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-strash") + writer.strashing = true; + else if (args[argidx] == "-flatten") + writer.flatten = true; + else if (args[argidx] == "-mapping_prep") + writer.mapping_prep = true; + else if (args[argidx] == "-map2" && argidx + 1 < args.size()) + map_filename = args[++argidx]; + else + break; + } + extra_args(f, filename, args, argidx); + + Module *top = design->top_module(); + + if (!top || !design->selected_whole_module(top)) + log_cmd_error("No top module selected\n"); + + if (!map_filename.empty()) { + writer.map_file.open(map_filename); + if (!writer.map_file) + log_cmd_error("Failed to open '%s' for writing\n", map_filename.c_str()); + } + + design->bufNormalize(true); + writer.setup(top); + writer.write(f); + + // we are leaving the sacred land, un-bufnormalize + // (if not, this will lead to bugs: the buf-normalized + // flag must not be kept on past the code that can work + // with it) + design->bufNormalize(false); + } +} XAiger2Backend; + +PRIVATE_NAMESPACE_END diff --git a/frontends/aiger2/Makefile.inc b/frontends/aiger2/Makefile.inc new file mode 100644 index 000000000..b4a9f6b89 --- /dev/null +++ b/frontends/aiger2/Makefile.inc @@ -0,0 +1,2 @@ + +OBJS += frontends/aiger2/xaiger.o diff --git a/frontends/aiger2/xaiger.cc b/frontends/aiger2/xaiger.cc new file mode 100644 index 000000000..04beee396 --- /dev/null +++ b/frontends/aiger2/xaiger.cc @@ -0,0 +1,473 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) Martin Povišer + * + * 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/register.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +uint32_t read_be32(std::istream &f) { + return ((uint32_t) f.get() << 24) | + ((uint32_t) f.get() << 16) | + ((uint32_t) f.get() << 8) | (uint32_t) f.get(); +} + +IdString read_idstring(std::istream &f) +{ + std::string str; + std::getline(f, str, '\0'); + if (!f.good()) + log_error("failed to read string\n"); + return RTLIL::escape_id(str); +} + +struct Xaiger2Frontend : public Frontend { + Xaiger2Frontend() : Frontend("xaiger2", "(experimental) read XAIGER file") + { + experimental(); + } + + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" read_xaiger2 -sc_mapping [options] \n"); + log("\n"); + log("Read a standard cell mapping from a XAIGER file into an existing module.\n"); + log("\n"); + log(" -module_name \n"); + log(" name of the target module\n"); + log("\n"); + log(" -map2 \n"); + log(" read file with symbol information\n"); + log("\n"); + } + + void read_sc_mapping(std::istream *&f, std::string filename, std::vector args, Design *design) + { + IdString module_name; + std::string map_filename; + + size_t argidx; + for (argidx = 2; argidx < args.size(); argidx++) { + std::string arg = args[argidx]; + if (arg == "-module_name" && argidx + 1 < args.size()) { + module_name = RTLIL::escape_id(args[++argidx]); + continue; + } + if (arg == "-map2" && argidx + 1 < args.size()) { + map_filename = args[++argidx]; + continue; + } + break; + } + extra_args(f, filename, args, argidx, true); + + if (map_filename.empty()) + log_error("A '-map2' argument required\n"); + if (module_name.empty()) + log_error("A '-module_name' argument required\n"); + + Module *module = design->module(module_name); + if (!module) + log_error("Module '%s' not found\n", log_id(module_name)); + + std::ifstream map_file; + map_file.open(map_filename); + if (!map_file) + log_error("Failed to open map file '%s'\n", map_filename.c_str()); + + unsigned int M, I, L, O, A; + std::string header; + if (!(*f >> header >> M >> I >> L >> O >> A) || header != "aig") + log_error("Bad header\n"); + std::string line; + std::getline(*f, line); + log_debug("M=%u I=%u L=%u O=%u A=%u\n", M, I, L, O, A); + + if (L != 0) + log_error("Latches unsupported\n"); + if (I + L + A != M) + log_error("Inconsistent header\n"); + + std::vector outputs; + for (int i = 0; i < (int) O; i++) { + int po; + *f >> po; + log_assert(f->get() == '\n'); + outputs.push_back(po); + } + + std::vector> boxes; + std::vector retained_boxes; + std::vector bits(2 + 2*M, RTLIL::Sm); + bits[0] = RTLIL::S0; + bits[1] = RTLIL::S1; + + std::string type; + while (map_file >> type) { + if (type == "pi") { + int pi_idx; + int woffset; + std::string name; + if (!(map_file >> pi_idx >> woffset >> name)) + log_error("Bad map file (1)\n"); + int lit = (2 * pi_idx) + 2; + if (lit < 0 || lit >= (int) bits.size()) + log_error("Bad map file (2)\n"); + Wire *w = module->wire(name); + if (!w || woffset < 0 || woffset >= w->width) + log_error("Map file references non-existent signal bit %s[%d]\n", + name.c_str(), woffset); + bits[lit] = SigBit(w, woffset); + } else if (type == "box") { + int box_seq; + std::string name; + if (!(map_file >> box_seq >> name)) + log_error("Bad map file (20)\n"); + if (box_seq < 0) + log_error("Bad map file (21)\n"); + + Cell *box = module->cell(RTLIL::escape_id(name)); + if (!box) + log_error("Map file references non-existent box %s\n", + name.c_str()); + + Module *def = design->module(box->type); + if (def && !box->parameters.empty()) { + // TODO: This is potentially costly even if a cached derivation exists + def = design->module(def->derive(design, box->parameters)); + log_assert(def); + } + + if (!def) + log_error("Bad map file (22)\n"); + + if (box_seq >= (int) boxes.size()) { + boxes.resize(box_seq + 1); + retained_boxes.resize(box_seq + 1); + } + boxes[box_seq] = std::make_pair(box, def); + } else { + std::string scratch; + std::getline(map_file, scratch); + } + } + + for (int i = 0; i < (int) A; i++) { + while (f->get() & 0x80 && !f->eof()); + while (f->get() & 0x80 && !f->eof()); + } + + if (f->get() != 'c') + log_error("Missing 'c' ahead of extensions\n"); + if (f->peek() == '\n') + f->get(); + auto extensions_start = f->tellg(); + + log_debug("reading 'h' (first pass)\n"); + for (int c = f->get(); c != EOF; c = f->get()) { + if (c == 'h') { + uint32_t len, ci_num, co_num, pi_num, po_num, no_boxes; + len = read_be32(*f); + read_be32(*f); + ci_num = read_be32(*f); + co_num = read_be32(*f); + pi_num = read_be32(*f); + po_num = read_be32(*f); + no_boxes = read_be32(*f); + + log_debug("len=%u ci_num=%u co_num=%u pi_num=%u po_nun=%u no_boxes=%u\n", + len, ci_num, co_num, pi_num, po_num, no_boxes); + + int ci_counter = 0; + for (uint32_t i = 0; i < no_boxes; i++) { + uint32_t box_inputs, box_outputs, box_id, box_seq; + box_inputs = read_be32(*f); + box_outputs = read_be32(*f); + box_id = read_be32(*f); + box_seq = read_be32(*f); + + log("box_seq=%d boxes.size=%d\n", box_seq, (int) boxes.size()); + log_assert(box_seq < boxes.size()); + + auto [cell, def] = boxes[box_seq]; + log_assert(cell && def); + retained_boxes[box_seq] = true; + + int box_ci_idx = 0; + for (auto port_id : def->ports) { + Wire *port = def->wire(port_id); + if (port->port_output) { + if (!cell->hasPort(port_id) || cell->getPort(port_id).size() != port->width) + log_error("Malformed design (1)\n"); + + SigSpec &conn = cell->connections_[port_id]; + for (int j = 0; j < port->width; j++) { + if (conn[j].wire && conn[j].wire->port_output) + conn[j] = module->addWire(module->uniquify( + stringf("$box$%s$%s$%d", + cell->name.isPublic() ? cell->name.c_str() + 1 : cell->name.c_str(), + port_id.isPublic() ? port_id.c_str() + 1 : port_id.c_str(), + j))); + + bits[2*(pi_num + ci_counter + box_ci_idx++) + 2] = conn[j]; + } + } + } + + log_assert(box_ci_idx == (int) box_outputs); + ci_counter += box_ci_idx; + } + log_assert(pi_num + ci_counter == ci_num); + } else if (c == '\n') { + break; + } else if (c == 'c') { + break; + } else { + uint32_t len = read_be32(*f); + f->ignore(len); + log_debug(" section '%c' (%d): ignoring %d bytes\n", c, c, len); + } + } + + log_debug("reading 'M' (second pass)\n"); + + f->seekg(extensions_start); + bool read_mapping = false; + uint32_t no_cells, no_instances; + for (int c = f->get(); c != EOF; c = f->get()) { + if (c == 'M') { + uint32_t len = read_be32(*f); + read_mapping = true; + + no_cells = read_be32(*f); + no_instances = read_be32(*f); + + log_debug("M: len=%u no_cells=%u no_instances=%u\n", len, no_cells, no_instances); + + struct MappingCell { + RTLIL::IdString type; + RTLIL::IdString out; + std::vector ins; + }; + std::vector cells; + cells.resize(no_cells); + + for (unsigned i = 0; i < no_cells; ++i) { + auto &cell = cells[i]; + cell.type = read_idstring(*f); + cell.out = read_idstring(*f); + uint32_t nins = read_be32(*f); + for (uint32_t j = 0; j < nins; j++) + cell.ins.push_back(read_idstring(*f)); + log_debug("M: Cell %s (out %s, ins", log_id(cell.type), log_id(cell.out)); + for (auto in : cell.ins) + log_debug(" %s", log_id(in)); + log_debug(")\n"); + } + + for (unsigned i = 0; i < no_instances; ++i) { + uint32_t cell_id = read_be32(*f); + uint32_t out_lit = read_be32(*f); + + log_assert(out_lit < bits.size()); + log_assert(bits[out_lit] == RTLIL::Sm); + log_assert(cell_id < cells.size()); + auto &cell = cells[cell_id]; + Cell *instance = module->addCell(module->uniquify(stringf("$sc%d", out_lit)), cell.type); + auto out_w = module->addWire(module->uniquify(stringf("$lit%d", out_lit))); + instance->setPort(cell.out, out_w); + bits[out_lit] = out_w; + for (auto in : cell.ins) { + uint32_t in_lit = read_be32(*f); + log_assert(out_lit < bits.size()); + log_assert(bits[in_lit] != RTLIL::Sm); + instance->setPort(in, bits[in_lit]); + } + } + } else if (c == '\n') { + break; + } else if (c == 'c') { + break; + } else { + uint32_t len = read_be32(*f); + f->ignore(len); + log_debug(" section '%c' (%d): ignoring %d bytes\n", c, c, len); + } + } + + if (!read_mapping) + log_error("Missing mapping (no 'M' section)\n"); + + log("Read %d instances with cell library of size %d.\n", + no_instances, no_cells); + + f->seekg(extensions_start); + log_debug("reading 'h' (second pass)\n"); + int co_counter = 0; + for (int c = f->get(); c != EOF; c = f->get()) { + if (c == 'h') { + uint32_t len, ci_num, co_num, pi_num, po_num, no_boxes; + len = read_be32(*f); + read_be32(*f); + ci_num = read_be32(*f); + co_num = read_be32(*f); + pi_num = read_be32(*f); + po_num = read_be32(*f); + no_boxes = read_be32(*f); + + log_debug("len=%u ci_num=%u co_num=%u pi_num=%u po_nun=%u no_boxes=%u\n", + len, ci_num, co_num, pi_num, po_num, no_boxes); + + for (uint32_t i = 0; i < no_boxes; i++) { + uint32_t box_inputs, box_outputs, box_id, box_seq; + box_inputs = read_be32(*f); + box_outputs = read_be32(*f); + box_id = read_be32(*f); + box_seq = read_be32(*f); + + log("box_seq=%d boxes.size=%d\n", box_seq, (int) boxes.size()); + log_assert(box_seq < boxes.size()); + + auto [cell, def] = boxes[box_seq]; + log_assert(cell && def); + + int box_co_idx = 0; + for (auto port_id : def->ports) { + Wire *port = def->wire(port_id); + SigSpec conn; + if (port->port_input) { + if (!cell->hasPort(port_id) || cell->getPort(port_id).size() != port->width) + log_error("Malformed design (2)\n"); + + SigSpec conn; + for (int j = 0; j < port->width; j++) { + log_assert(co_counter + box_co_idx < (int) outputs.size()); + int lit = outputs[co_counter + box_co_idx++]; + log_assert(lit >= 0 && lit < (int) bits.size()); + SigBit bit = bits[lit]; + if (bit == RTLIL::Sm) + log_error("Malformed mapping (1)\n"); + conn.append(bit); + } + cell->setPort(port_id, conn); + } + } + + log_assert(box_co_idx == (int) box_inputs); + co_counter += box_co_idx; + } + log_assert(po_num + co_counter == co_num); + } else if (c == '\n') { + break; + } else if (c == 'c') { + break; + } else { + uint32_t len = read_be32(*f); + f->ignore(len); + log_debug(" section '%c' (%d): ignoring %d bytes\n", c, c, len); + } + } + + while (true) { + std::string scratch; + std::getline(*f, scratch); + if (f->eof()) + break; + log_assert(!f->fail()); + log("input file: %s\n", scratch.c_str()); + } + + log_debug("co_counter=%d\n", co_counter); + + // TODO: seek without close/open + map_file.close(); + map_file.open(map_filename); + while (map_file >> type) { + if (type == "po") { + int po_idx; + int woffset; + std::string name; + if (!(map_file >> po_idx >> woffset >> name)) + log_error("Bad map file (3)\n"); + po_idx += co_counter; + if (po_idx < 0 || po_idx >= (int) outputs.size()) + log_error("Bad map file (4)\n"); + int lit = outputs[po_idx]; + if (lit < 0 || lit >= (int) bits.size()) + log_error("Bad map file (5)\n"); + if (bits[lit] == RTLIL::Sm) + log_error("Bad map file (6)\n"); + Wire *w = module->wire(name); + if (!w || woffset < 0 || woffset >= w->width) + log_error("Map file references non-existent signal bit %s[%d]\n", + name.c_str(), woffset); + module->connect(SigBit(w, woffset), bits[lit]); + } else if (type == "pseudopo") { + int po_idx; + int poffset; + std::string box_name; + std::string box_port; + if (!(map_file >> po_idx >> poffset >> box_name >> box_port)) + log_error("Bad map file (7)\n"); + po_idx += co_counter; + if (po_idx < 0 || po_idx >= (int) outputs.size()) + log_error("Bad map file (8)\n"); + int lit = outputs[po_idx]; + if (lit < 0 || lit >= (int) bits.size()) + log_error("Bad map file (9)\n"); + if (bits[lit] == RTLIL::Sm) + log_error("Bad map file (10)\n"); + Cell *cell = module->cell(box_name); + if (!cell || !cell->hasPort(box_port)) + log_error("Map file references non-existent box port %s/%s\n", + box_name.c_str(), box_port.c_str()); + SigSpec &port = cell->connections_[box_port]; + if (poffset < 0 || poffset >= port.size()) + log_error("Map file references non-existent box port bit %s/%s[%d]\n", + box_name.c_str(), box_port.c_str(), poffset); + port[poffset] = bits[lit]; + } else { + std::string scratch; + std::getline(map_file, scratch); + } + } + + int box_seq = 0; + for (auto [cell, def] : boxes) { + if (!retained_boxes[box_seq++]) + module->remove(cell); + } + } + + void execute(std::istream *&f, std::string filename, std::vector args, Design *design) override + { + log_header(design, "Executing XAIGER2 frontend.\n"); + + if (args.size() > 1 && args[1] == "-sc_mapping") { + read_sc_mapping(f, filename, args, design); + return; + } + + log_cmd_error("Mode '-sc_mapping' must be selected\n"); + } +} Xaiger2Frontend; + +PRIVATE_NAMESPACE_END diff --git a/kernel/celltypes.h b/kernel/celltypes.h index 9868827e6..b6d89a805 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -381,11 +381,10 @@ struct CellTypes HANDLE_CELL_TYPE(modfloor) HANDLE_CELL_TYPE(pow) HANDLE_CELL_TYPE(pos) - HANDLE_CELL_TYPE(buf) HANDLE_CELL_TYPE(neg) #undef HANDLE_CELL_TYPE - if (type == ID($_BUF_)) + if (type.in(ID($_BUF_), ID($buf))) return arg1; if (type == ID($_NOT_)) return eval_not(arg1); diff --git a/passes/techmap/Makefile.inc b/passes/techmap/Makefile.inc index 6bf40434d..4e1d16744 100644 --- a/passes/techmap/Makefile.inc +++ b/passes/techmap/Makefile.inc @@ -12,10 +12,12 @@ OBJS += passes/techmap/abc.o OBJS += passes/techmap/abc9.o OBJS += passes/techmap/abc9_exe.o OBJS += passes/techmap/abc9_ops.o +OBJS += passes/techmap/abc_new.o ifneq ($(ABCEXTERNAL),) passes/techmap/abc.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' passes/techmap/abc9.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' passes/techmap/abc9_exe.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' +passes/techmap/abc_new.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' endif endif diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc index 876917e56..a96a82659 100644 --- a/passes/techmap/abc9.cc +++ b/passes/techmap/abc9.cc @@ -220,7 +220,8 @@ struct Abc9Pass : public ScriptPass std::string arg = args[argidx]; if ((arg == "-exe" || arg == "-script" || arg == "-D" || /*arg == "-S" ||*/ arg == "-lut" || arg == "-luts" || - /*arg == "-box" ||*/ arg == "-W") && + /*arg == "-box" ||*/ arg == "-W" || arg == "-genlib" || + arg == "-constr" || arg == "-dont_use" || arg == "-liberty") && argidx+1 < args.size()) { if (arg == "-lut" || arg == "-luts") lut_mode = true; diff --git a/passes/techmap/abc9_exe.cc b/passes/techmap/abc9_exe.cc index 8e02e25a4..651a8375c 100644 --- a/passes/techmap/abc9_exe.cc +++ b/passes/techmap/abc9_exe.cc @@ -167,8 +167,8 @@ struct abc9_output_filter void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe_file, vector lut_costs, bool dff_mode, std::string delay_target, std::string /*lutin_shared*/, bool fast_mode, bool show_tempdir, std::string box_file, std::string lut_file, - std::string wire_delay, std::string tempdir_name -) + std::vector liberty_files, std::string wire_delay, std::string tempdir_name, + std::string constr_file, std::vector dont_use_cells) { std::string abc9_script; @@ -176,8 +176,17 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe abc9_script += stringf("read_lut %s/lutdefs.txt; ", tempdir_name.c_str()); else if (!lut_file.empty()) abc9_script += stringf("read_lut \"%s\"; ", lut_file.c_str()); - else - log_abort(); + else if (!liberty_files.empty()) { + std::string dont_use_args; + for (std::string dont_use_cell : dont_use_cells) { + dont_use_args += stringf("-X \"%s\" ", dont_use_cell.c_str()); + } + for (std::string liberty_file : liberty_files) { + abc9_script += stringf("read_lib %s -w \"%s\" ; ", dont_use_args.c_str(), liberty_file.c_str()); + } + if (!constr_file.empty()) + abc9_script += stringf("read_constr -v \"%s\"; ", constr_file.c_str()); + } log_assert(!box_file.empty()); abc9_script += stringf("read_box \"%s\"; ", box_file.c_str()); @@ -359,6 +368,26 @@ struct Abc9ExePass : public Pass { log(" of output quality):\n"); log("%s\n", fold_abc9_cmd(RTLIL::constpad.at("abc9.script.default.fast").substr(1,std::string::npos)).c_str()); log("\n"); + log(" -constr \n"); + log(" pass this file with timing constraints to ABC.\n"); + log(" use with -liberty.\n"); + log("\n"); + log(" a constr file contains two lines:\n"); + log(" set_driving_cell \n"); + log(" set_load \n"); + log("\n"); + log(" the set_driving_cell statement defines which cell type is assumed to\n"); + log(" drive the primary inputs and the set_load statement sets the load in\n"); + log(" femtofarads for each primary output.\n"); + log("\n"); + log(" -liberty \n"); + log(" read the given Liberty file as a description of the target cell library.\n"); + log(" this option can be used multiple times.\n"); + log("\n"); + log(" -dont_use \n"); + log(" avoid usage of the technology cell when mapping the design.\n"); + log(" this option can be used multiple times.\n"); + log("\n"); log(" -D \n"); log(" set delay target. the string {D} in the default scripts above is\n"); log(" replaced by this option when used, and an empty string otherwise\n"); @@ -411,7 +440,8 @@ struct Abc9ExePass : public Pass { log_header(design, "Executing ABC9_EXE pass (technology mapping using ABC9).\n"); std::string exe_file = yosys_abc_executable; - std::string script_file, clk_str, box_file, lut_file; + std::string script_file, clk_str, box_file, lut_file, constr_file; + std::vector liberty_files, dont_use_cells; std::string delay_target, lutin_shared = "-S 1", wire_delay; std::string tempdir_name; bool fast_mode = false, dff_mode = false; @@ -499,6 +529,18 @@ struct Abc9ExePass : public Pass { tempdir_name = args[++argidx]; continue; } + if (arg == "-liberty" && argidx+1 < args.size()) { + liberty_files.push_back(args[++argidx]); + continue; + } + if (arg == "-dont_use" && argidx+1 < args.size()) { + dont_use_cells.push_back(args[++argidx]); + continue; + } + if (arg == "-constr" && argidx+1 < args.size()) { + constr_file = args[++argidx]; + continue; + } break; } extra_args(args, argidx, design); @@ -562,7 +604,8 @@ struct Abc9ExePass : public Pass { abc9_module(design, script_file, exe_file, lut_costs, dff_mode, delay_target, lutin_shared, fast_mode, show_tempdir, - box_file, lut_file, wire_delay, tempdir_name); + box_file, lut_file, liberty_files, wire_delay, tempdir_name, + constr_file, dont_use_cells); } } Abc9ExePass; diff --git a/passes/techmap/abc_new.cc b/passes/techmap/abc_new.cc new file mode 100644 index 000000000..eefe34f84 --- /dev/null +++ b/passes/techmap/abc_new.cc @@ -0,0 +1,153 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2024 Martin Povišer + * + * 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/register.h" +#include "kernel/rtlil.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct AbcNewPass : public ScriptPass { + AbcNewPass() : ScriptPass("abc_new", "(experimental) use ABC for SC technology mapping (new)") + { + experimental(); + } + + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" abc_new [options] [selection]\n"); + log("\n"); + log("This command uses the ABC tool [1] to optimize the current design and map it to\n"); + log("the target standard cell library.\n"); + log("\n"); + log(" -run :\n"); + log(" only run the commands between the labels (see below). an empty\n"); + log(" from label is synonymous to 'begin', and empty to label is\n"); + log(" synonymous to the end of the command list.\n"); + log("\n"); + log(" -exe \n"); + log(" -script \n"); + log(" -D \n"); + log(" -constr \n"); + log(" -dont_use \n"); + log(" -liberty \n"); + log(" these options are passed on to the 'abc9_exe' command which invokes\n"); + log(" the ABC tool on individual modules of the design. please see\n"); + log(" 'help abc9_exe' for more details\n"); + log("\n"); + log("[1] http://www.eecs.berkeley.edu/~alanmi/abc/\n"); + log("\n"); + help_script(); + log("\n"); + } + + bool cleanup; + std::string abc_exe_options; + + void execute(std::vector args, RTLIL::Design *d) override + { + std::string run_from, run_to; + cleanup = true; + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-exe" || args[argidx] == "-script" || + args[argidx] == "-D" || + args[argidx] == "-constr" || args[argidx] == "-dont_use" || + args[argidx] == "-liberty") { + abc_exe_options += " " + args[argidx] + " " + args[argidx + 1]; + argidx++; + } else if (args[argidx] == "-run" && argidx + 1 < args.size()) { + size_t pos = args[++argidx].find(':'); + if (pos == std::string::npos) + break; + run_from = args[argidx].substr(0, pos); + run_to = args[argidx].substr(pos + 1); + } else if (args[argidx] == "-nocleanup") { + cleanup = false; + } else { + break; + } + } + extra_args(args, argidx, d); + + log_header(d, "Executing ABC_NEW pass.\n"); + log_push(); + run_script(d, run_from, run_to); + log_pop(); + } + + void script() override + { + if (check_label("check")) { + run("abc9_ops -check"); + } + + if (check_label("prep_boxes")) { + run("box_derive"); + run("abc9_ops -prep_box"); + } + + if (check_label("map")) { + std::vector selected_modules; + + if (!help_mode) { + selected_modules = active_design->selected_whole_modules_warn(); + active_design->selection_stack.emplace_back(false); + } else { + selected_modules = {nullptr}; + run("foreach module in selection"); + } + + for (auto mod : selected_modules) { + std::string tmpdir = ""; + std::string modname = ""; + std::string exe_options = "[options]"; + if (!help_mode) { + tmpdir = cleanup ? (get_base_tmpdir() + "/") : "_tmp_"; + tmpdir += proc_program_prefix() + "yosys-abc-XXXXXX"; + tmpdir = make_temp_dir(tmpdir); + modname = mod->name.str(); + exe_options = abc_exe_options; + log_header(active_design, "Mapping module '%s'.\n", log_id(mod)); + log_push(); + active_design->selection().select(mod); + } + + run(stringf(" abc9_ops -write_box %s/input.box", tmpdir.c_str())); + run(stringf(" write_xaiger2 -mapping_prep -map2 %s/input.map2 %s/input.xaig", tmpdir.c_str(), tmpdir.c_str())); + run(stringf(" abc9_exe %s -cwd %s -box %s/input.box", exe_options.c_str(), tmpdir.c_str(), tmpdir.c_str())); + run(stringf(" read_xaiger2 -sc_mapping -module_name %s -map2 %s/input.map2 %s/output.aig", + modname.c_str(), tmpdir.c_str(), tmpdir.c_str())); + + if (!help_mode) { + active_design->selection().selected_modules.clear(); + log_pop(); + } + } + + if (!help_mode) { + active_design->selection_stack.pop_back(); + } + } + } +} AbcNewPass; + +PRIVATE_NAMESPACE_END diff --git a/tests/techmap/aigmap.ys b/tests/techmap/aigmap.ys index 6f6cdd1f2..deec440e2 100644 --- a/tests/techmap/aigmap.ys +++ b/tests/techmap/aigmap.ys @@ -84,14 +84,14 @@ assign name``_y2 = op name``_a2; `BIOP(xnor, ~^, 3, 3, 3) `BIOP(logic_and, &&, 3, 3, 1) `BIOP(logic_or, ||, 3, 3, 1) -`BIOP(logic_eq, ==, 3, 3, 1) -`BIOP(logic_ne, !=, 3, 3, 1) -`BIOP(logic_lt, <, 3, 3, 1) -`BIOP(logic_le, <=, 3, 3, 1) -`BIOP(logic_gt, >, 3, 3, 1) -`BIOP(logic_ge, >=, 3, 3, 1) +`BIOP(eq, ==, 3, 3, 1) +`BIOP(ne, !=, 3, 3, 1) +`BIOP(lt, <, 3, 3, 1) +`BIOP(le, <=, 3, 3, 1) +`BIOP(gt, >, 3, 3, 1) +`BIOP(ge, >=, 3, 3, 1) `UNOP(pos, +, 3) -`UNOP(neg, ~, 3) +`UNOP(not, ~, 3) `UNOP_REDUCE(logic_not, !, 3) `UNOP_REDUCE(reduce_and, &, 3) `UNOP_REDUCE(reduce_or, |, 3) diff --git a/tests/various/aiger2.ys b/tests/various/aiger2.ys new file mode 100644 index 000000000..d2b024d2f --- /dev/null +++ b/tests/various/aiger2.ys @@ -0,0 +1,224 @@ +read_verilog -icells <, 3, 3, 1) +`BIOP(ge, >=, 3, 3, 1) +`UNOP(not, ~, 3) +`UNOP_REDUCE(logic_not, !, 3) +`UNOP_REDUCE(reduce_and, &, 3) +`UNOP_REDUCE(reduce_or, |, 3) +`UNOP_REDUCE(reduce_xor, ^, 3) +`UNOP_REDUCE(reduce_xnor, ~^, 3) + +wire [3:0] mux_a, mux_b, mux_s, mux_y; +assign mux_y = mux_s ? mux_b : mux_a; + +wire [1:0] fa_a, fa_b, fa_c, fa_x, fa_y; +\$fa #( + .WIDTH(2) +) fa(.A(fa_a), .B(fa_b), .C(fa_c), .X(fa_x), .Y(fa_y)); + +wire [1:0] bwmux_a, bwmux_b, bwmux_s, bwmux_y; +\$bwmux #( + .WIDTH(2) +) bwmux(.A(bwmux_a), .B(bwmux_b), .S(bwmux_s), .Y(bwmux_y)); +endmodule +EOF + +expose -input c:* %ci* w:* %i +expose c:* %co* w:* %i +splitnets -ports +copy test gold +select test +write_aiger2 aiger2_ops.aig +select -clear +delete test +read_aiger -module_name test aiger2_ops.aig +select -assert-none test/t:$_AND_ test/t:$_NOT_ %% test/c:* %D +miter -equiv -make_outcmp -flatten gold test miter +sat -verify -show-ports -prove trigger 0 miter + +design -reset +read_verilog -icells <