mirror of https://github.com/YosysHQ/yosys.git
Start an 'aiger2' backend
This commit is contained in:
Martin Povišer
parent
4cfdb7ab50
commit
fb26945a20
|
|
@ -0,0 +1 @@
|
|||
OBJS += backends/aiger2/aiger.o
|
||||
|
|
@ -0,0 +1,593 @@
|
|||
/*
|
||||
* yosys -- Yosys Open SYnthesis Suite
|
||||
*
|
||||
* Copyright (C) Martin Povišer <povik@cutebit.org>
|
||||
*
|
||||
* 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)
|
||||
|
||||
#include "kernel/register.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)
|
||||
|
||||
#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_)
|
||||
|
||||
// TODO
|
||||
//#define ARITH_OPS ID($add), ID($sub), ID($lt), ID($le), ID($ge), ID($gt), ID($neg)
|
||||
|
||||
#define KNOWN_OPS BITWISE_OPS, REDUCE_OPS, LOGIC_OPS, GATE_OPS /*, ARITH_OPS*/
|
||||
|
||||
template<typename Writer, typename Lit>
|
||||
struct Index {
|
||||
struct HierCursor;
|
||||
struct ModuleInfo {
|
||||
Module *module;
|
||||
int len;
|
||||
dict<Wire *, int> windices;
|
||||
dict<Cell *, int> suboffsets;
|
||||
|
||||
bool indexing = false;
|
||||
bool indexed = false;
|
||||
};
|
||||
|
||||
dict<Module *, ModuleInfo> 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;
|
||||
}
|
||||
|
||||
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))
|
||||
continue;
|
||||
|
||||
Module *submodule = m->design->module(cell->type);
|
||||
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.suboffsets[cell] = pos;
|
||||
pos += index_module(submodule);
|
||||
}
|
||||
|
||||
info.len = pos;
|
||||
return info.len;
|
||||
}
|
||||
|
||||
Design *design;
|
||||
Module *top;
|
||||
ModuleInfo *top_minfo;
|
||||
std::vector<Lit> lits;
|
||||
|
||||
Index(RTLIL::Module *top)
|
||||
: design(top->design), 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 = false;
|
||||
|
||||
Lit AND(Lit a, Lit b)
|
||||
{
|
||||
if (const_folding) {
|
||||
if (a == Writer::CONST_FALSE || b == Writer::CONST_FALSE)
|
||||
return Writer::CONST_FALSE;
|
||||
if (a == Writer::CONST_TRUE)
|
||||
return b;
|
||||
if (b == Writer::CONST_TRUE)
|
||||
return a;
|
||||
}
|
||||
|
||||
return (static_cast<Writer*>(this))->emit_gate(a, b);
|
||||
}
|
||||
|
||||
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 == Writer::CONST_FALSE)
|
||||
return a;
|
||||
if (s == Writer::CONST_TRUE)
|
||||
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 impl_op(HierCursor &cursor, Cell *cell, IdString oport, int obit)
|
||||
{
|
||||
if (cell->type.in(REDUCE_OPS, LOGIC_OPS) && obit != 0) {
|
||||
return Writer::CONST_FALSE;
|
||||
} else if (cell->type.in(REDUCE_OPS, ID($logic_not))) {
|
||||
SigSpec inport = cell->getPort(ID::A);
|
||||
|
||||
log_assert(inport.size() > 0); // TODO
|
||||
|
||||
Lit acc = visit(cursor, inport[0]);
|
||||
for (int i = 1; i < inport.size(); i++) {
|
||||
Lit l = visit(cursor, inport[i]);
|
||||
if (cell->type == ID($reduce_and)) {
|
||||
acc = AND(acc, l);
|
||||
} else if (cell->type.in(ID($reduce_or), ID($reduce_bool), ID($logic_not))) {
|
||||
acc = OR(acc, l);
|
||||
} else if (cell->type.in(ID($reduce_xor), ID($reduce_xnor))) {
|
||||
acc = XOR(acc, l);
|
||||
}
|
||||
}
|
||||
|
||||
if (!cell->type.in(ID($reduce_xnor), ID($logic_not)))
|
||||
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)) {
|
||||
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 = Writer::CONST_FALSE;
|
||||
}
|
||||
|
||||
if (cell->type.in(ID($buf), 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 = Writer::CONST_FALSE;
|
||||
}
|
||||
|
||||
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($_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 {
|
||||
log_abort();
|
||||
}
|
||||
}
|
||||
|
||||
struct HierCursor {
|
||||
typedef std::pair<ModuleInfo&, Cell*> Level;
|
||||
std::vector<Level> levels;
|
||||
int instance_offset = 0;
|
||||
|
||||
HierCursor(ModuleInfo &top)
|
||||
{
|
||||
levels.push_back(Level(top, nullptr));
|
||||
}
|
||||
|
||||
ModuleInfo ¤t_minfo()
|
||||
{
|
||||
log_assert(!levels.empty());
|
||||
return levels.back().first;
|
||||
}
|
||||
|
||||
int bitwire_index(SigBit bit)
|
||||
{
|
||||
log_assert(bit.wire != nullptr);
|
||||
return instance_offset + current_minfo().windices[bit.wire] + bit.offset;
|
||||
}
|
||||
|
||||
Cell *exit()
|
||||
{
|
||||
log_assert(levels.size() > 1);
|
||||
Cell *instance = levels.back().second;
|
||||
|
||||
levels.pop_back();
|
||||
instance_offset -= current_minfo().suboffsets.at(instance);
|
||||
|
||||
// return the instance we just exited
|
||||
return instance;
|
||||
}
|
||||
|
||||
Module *enter(Index &index, Cell *cell)
|
||||
{
|
||||
Design *design = index.design;
|
||||
auto &minfo = current_minfo();
|
||||
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;
|
||||
}
|
||||
};
|
||||
|
||||
int visit(HierCursor &cursor, SigBit bit)
|
||||
{
|
||||
if (!bit.wire) {
|
||||
if (bit == State::S1)
|
||||
return Writer::CONST_TRUE;
|
||||
else if (bit == State::S0)
|
||||
return Writer::CONST_FALSE;
|
||||
else
|
||||
log_error("Unhandled state %s\n", log_signal(bit));
|
||||
}
|
||||
|
||||
int idx = cursor.bitwire_index(bit);
|
||||
if (lits[idx] != Writer::empty_lit()) {
|
||||
// literal already assigned
|
||||
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();
|
||||
}
|
||||
|
||||
} else {
|
||||
// a module input: we cannot be the top module, otherwise
|
||||
// the branch for pre-existing literals would have been taken
|
||||
log_assert(cursor.levels.size() > 1);
|
||||
|
||||
// step into the upper module
|
||||
Cell *instance = cursor.exit();
|
||||
{
|
||||
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;
|
||||
}
|
||||
|
||||
void set_top_port(SigBit bit, Lit lit)
|
||||
{
|
||||
log_assert(bit.wire);
|
||||
log_assert(bit.wire->module == top);
|
||||
log_assert(bit.wire->port_input);
|
||||
|
||||
lits[top_minfo->windices[bit.wire] + bit.offset] = lit;
|
||||
}
|
||||
|
||||
Lit get_top_port(SigBit bit)
|
||||
{
|
||||
HierCursor cursor(*top_minfo);
|
||||
Lit ret = visit(cursor, bit);
|
||||
log_assert(cursor.levels.size() == 1);
|
||||
log_assert(cursor.instance_offset == 0);
|
||||
return ret;
|
||||
}
|
||||
};
|
||||
|
||||
struct AigerWriter : Index<AigerWriter, unsigned int> {
|
||||
typedef unsigned int Lit;
|
||||
|
||||
const static Lit CONST_FALSE = 0;
|
||||
const static Lit CONST_TRUE = 1;
|
||||
|
||||
// for some reason having a 'const static int EMPTY_LIT'
|
||||
// led to linkage errors
|
||||
static Lit empty_lit()
|
||||
{
|
||||
return 0x80000000;
|
||||
}
|
||||
|
||||
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 == (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->seekp(0);
|
||||
f->write(buf, strlen(buf));
|
||||
}
|
||||
|
||||
void write(std::ostream *f) {
|
||||
reset_counters();
|
||||
|
||||
// populate inputs
|
||||
std::vector<SigBit> inputs;
|
||||
for (auto w : top->wires())
|
||||
if (w->port_input)
|
||||
for (int i = 0; i < w->width; i++) {
|
||||
set_top_port(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 w : top->wires())
|
||||
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<std::pair<SigBit, int>> outputs;
|
||||
for (auto w : top->wires())
|
||||
if (w->port_output) {
|
||||
for (auto bit : SigSpec(w))
|
||||
outputs.push_back({bit, get_top_port(bit)});
|
||||
}
|
||||
auto data_end = f->tellp();
|
||||
|
||||
// revisit header and the list of outputs
|
||||
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 (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 (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++;
|
||||
}
|
||||
}
|
||||
|
||||
AigerWriter(RTLIL::Module *top)
|
||||
: Index(top) {}
|
||||
};
|
||||
|
||||
struct Aiger2Backend : Backend {
|
||||
Aiger2Backend() : Backend("aiger2", "write design to AIGER file (new)")
|
||||
{
|
||||
experimental();
|
||||
}
|
||||
|
||||
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
|
||||
{
|
||||
log_header(design, "Executing AIGER2 backend.\n");
|
||||
|
||||
size_t argidx;
|
||||
for (argidx = 1; argidx < args.size(); argidx++) {
|
||||
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);
|
||||
AigerWriter writer(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;
|
||||
|
||||
PRIVATE_NAMESPACE_END
|
||||
|
|
@ -0,0 +1,156 @@
|
|||
read_verilog -icells <<EOF
|
||||
module test();
|
||||
`define CELL_AY(typ) \
|
||||
wire typ``_a, typ``_y; \
|
||||
$``typ typ(.A(typ``_a), .Y(typ``_y));
|
||||
`define CELL_ABY(typ) \
|
||||
wire typ``_a, typ``_b, typ``_y; \
|
||||
$``typ typ(.A(typ``_a), .B(typ``_b), .Y(typ``_y));
|
||||
`define CELL_SABY(typ) \
|
||||
wire typ``_a, typ``_b, typ``_y, typ``_s; \
|
||||
$``typ typ(.A(typ``_a), .B(typ``_b), .Y(typ``_y), .S(typ``_s));
|
||||
`define CELL_ABCY(typ) \
|
||||
wire typ``_a, typ``_b, typ``_c, typ``_y; \
|
||||
$``typ typ(.A(typ``_a), .B(typ``_b), .C(typ``_c), .Y(typ``_y));
|
||||
`define CELL_ABCDY(typ) \
|
||||
wire typ``_a, typ``_b, typ``_c, typ``_d, typ``_y; \
|
||||
$``typ typ(.A(typ``_a), .B(typ``_b), .C(typ``_c), .D(typ``_d), .Y(typ``_y));
|
||||
|
||||
`CELL_AY(_BUF_)
|
||||
`CELL_AY(_NOT_)
|
||||
`CELL_ABY(_AND_)
|
||||
`CELL_ABY(_NAND_)
|
||||
`CELL_ABY(_OR_)
|
||||
`CELL_ABY(_NOR_)
|
||||
`CELL_ABY(_XOR_)
|
||||
`CELL_ABY(_XNOR_)
|
||||
`CELL_ABY(_ANDNOT_)
|
||||
`CELL_ABY(_ORNOT_)
|
||||
`CELL_SABY(_MUX_)
|
||||
`CELL_SABY(_NMUX_)
|
||||
`CELL_ABCY(_AOI3_)
|
||||
`CELL_ABCY(_OAI3_)
|
||||
`CELL_ABCDY(_AOI4_)
|
||||
`CELL_ABCDY(_OAI4_)
|
||||
endmodule
|
||||
EOF
|
||||
|
||||
expose -input c:* %ci* w:* %i
|
||||
expose c:* %co* w:* %i
|
||||
copy test gold
|
||||
select test
|
||||
write_aiger2 aiger2_gates.aig
|
||||
select -clear
|
||||
delete test
|
||||
read_aiger -module_name test aiger2_gates.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 <<EOF
|
||||
module test();
|
||||
|
||||
`define BIOP(name,op,w1,w2,wy) \
|
||||
wire [w1-1:0] name``_a1; \
|
||||
wire [w2-1:0] name``_b1; \
|
||||
wire [wy-1:0] name``_y1; \
|
||||
assign name``_y1 = name``_a1 op name``_b1; \
|
||||
wire signed [w1-1:0] name``_a2; \
|
||||
wire signed [w2-1:0] name``_b2; \
|
||||
wire [wy-1:0] name``_y2; \
|
||||
assign name``_y2 = name``_a2 op name``_b2;
|
||||
|
||||
`define UNOP(name,op,w1) \
|
||||
wire signed [w1-1:0] name``_a1; \
|
||||
wire signed [w1-1:0] name``_y1; \
|
||||
assign name``_y1 = op name``_a1; \
|
||||
wire [w1-1:0] name``_a2; \
|
||||
wire [w1-1:0] name``_y2; \
|
||||
assign name``_y2 = op name``_a2;
|
||||
|
||||
`define UNOP_REDUCE(name,op,w1) \
|
||||
wire signed [w1-1:0] name``_a1; \
|
||||
wire name``_y1; \
|
||||
assign name``_y1 = op name``_a1; \
|
||||
wire [w1-1:0] name``_a2; \
|
||||
wire name``_y2; \
|
||||
assign name``_y2 = op name``_a2;
|
||||
|
||||
`BIOP(and, &, 3, 4, 5)
|
||||
`BIOP(or, |, 4, 3, 2)
|
||||
`BIOP(xor, ^, 3, 3, 3)
|
||||
`BIOP(xnor, ~^, 3, 3, 3)
|
||||
`BIOP(logic_and, &&, 4, 3, 1)
|
||||
`BIOP(logic_or, ||, 3, 3, 2)
|
||||
`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));
|
||||
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 -flatten gold test miter
|
||||
sat -verify -prove trigger 0 miter
|
||||
|
||||
design -reset
|
||||
read_verilog -icells <<EOF
|
||||
module submodule1(a, y1, y2);
|
||||
input wire [2:0] a;
|
||||
output wire [2:0] y1 = a + 1;
|
||||
output wire [2:0] y2 = a + 2;
|
||||
endmodule
|
||||
|
||||
module submodule2(a, y1);
|
||||
input wire [2:0] a;
|
||||
output wire [2:0] y1 = ~a;
|
||||
endmodule
|
||||
|
||||
module test(a, y1, y2);
|
||||
input wire [2:0] a;
|
||||
output wire [2:0] y1;
|
||||
output wire [2:0] y2;
|
||||
|
||||
wire [2:0] m1;
|
||||
wire [2:0] m2;
|
||||
|
||||
submodule2 s1(.a(a), .y1(m1));
|
||||
submodule1 s2(.a(m1), .y1(y1), .y2(m2));
|
||||
submodule2 s3(.a(m2), .y1(y2));
|
||||
endmodule
|
||||
EOF
|
||||
|
||||
expose -input c:* %ci* w:* %i
|
||||
expose c:* %co* w:* %i
|
||||
splitnets -ports
|
||||
copy test gold
|
||||
flatten gold
|
||||
techmap submodule1
|
||||
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 -flatten gold test miter
|
||||
sat -verify -prove trigger 0 miter
|
||||
Loading…
Reference in New Issue