frontends/aiger/aigerparse.cc

   1 /*
   2  *  yosys -- Yosys Open SYnthesis Suite
   3  *
   4  *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
   5  *                      Eddie Hung <eddie@fpgeh.com>
   6  *
   7  *  Permission to use, copy, modify, and/or distribute this software for any
   8  *  purpose with or without fee is hereby granted, provided that the above
   9  *  copyright notice and this permission notice appear in all copies.
  10  *
  11  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  12  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  13  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  14  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  15  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  16  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  17  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  18  *
  19  */
  20
  21 // [[CITE]] The AIGER And-Inverter Graph (AIG) Format Version 20071012
  22 // Armin Biere. The AIGER And-Inverter Graph (AIG) Format Version 20071012. Technical Report 07/1, October 2011, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
  23 // http://fmv.jku.at/papers/Biere-FMV-TR-07-1.pdf
  24
  25 #ifndef _WIN32
  26 #include <libgen.h>
  27 #endif
  28 #include <array>
  29
  30 #include "kernel/yosys.h"
  31 #include "kernel/sigtools.h"
  32 #include "aigerparse.h"
  33
  34 YOSYS_NAMESPACE_BEGIN
  35
  36 AigerReader::AigerReader(RTLIL::Design *design, std::istream &f, RTLIL::IdString module_name, RTLIL::IdString clk_name)
  37     : design(design), f(f), clk_name(clk_name)
  38 {
  39     module = new RTLIL::Module;
  40     module->name = module_name;
  41     if (design->module(module->name))
  42         log_error("Duplicate definition of module %s!\n", log_id(module->name));
  43 }
  44
  45 void AigerReader::parse_aiger()
  46 {
  47     std::string header;
  48     f >> header;
  49     if (header != "aag" && header != "aig")
  50         log_error("Unsupported AIGER file!\n");
  51
  52     // Parse rest of header
  53     if (!(f >> M >> I >> L >> O >> A))
  54         log_error("Invalid AIGER header\n");
  55
  56     // Optional values
  57     B = C = J = F = 0;
  58     if (f.peek() != ' ') goto parse_body;
  59     if (!(f >> B)) log_error("Invalid AIGER header\n");
  60     if (f.peek() != ' ') goto parse_body;
  61     if (!(f >> C)) log_error("Invalid AIGER header\n");
  62     if (f.peek() != ' ') goto parse_body;
  63     if (!(f >> J)) log_error("Invalid AIGER header\n");
  64     if (f.peek() != ' ') goto parse_body;
  65     if (!(f >> F)) log_error("Invalid AIGER header\n");
  66
  67 parse_body:
  68
  69     std::string line;
  70     std::getline(f, line); // Ignore up to start of next line, as standard
  71                            // says anything that follows could be used for
  72                            // optional sections
  73
  74     log_debug("M=%u I=%u L=%u O=%u A=%u B=%u C=%u J=%u F=%u\n", M, I, L, O, A, B, C, J, F);
  75
  76     line_count = 1;
  77
  78     if (header == "aag")
  79         parse_aiger_ascii();
  80     else if (header == "aig")
  81         parse_aiger_binary();
  82     else
  83         log_abort();
  84
  85     // Parse footer (symbol table, comments, etc.)
  86     unsigned l1;
  87     std::string s;
  88     for (int c = f.peek(); c != EOF; c = f.peek(), ++line_count) {
  89         if (c == 'i' || c == 'l' || c == 'o') {
  90             f.ignore(1);
  91             if (!(f >> l1 >> s))
  92                 log_error("Line %u cannot be interpreted as a symbol entry!\n", line_count);
  93
  94             if ((c == 'i' && l1 > inputs.size()) || (c == 'l' && l1 > latches.size()) || (c == 'o' && l1 > outputs.size()))
  95                 log_error("Line %u has invalid symbol position!\n", line_count);
  96
  97             RTLIL::Wire* wire;
  98             if (c == 'i') wire = inputs[l1];
  99             else if (c == 'l') wire = latches[l1];
 100             else if (c == 'o') wire = outputs[l1];
 101             else log_abort();
 102
 103             module->rename(wire, stringf("\\%s", s.c_str()));
 104         }
 105         else if (c == 'b' || c == 'j' || c == 'f') {
 106             // TODO
 107         }
 108         else if (c == 'c') {
 109             f.ignore(1);
 110             if (f.peek() == '\n')
 111                 break;
 112             // Else constraint (TODO)
 113         }
 114         else
 115             log_error("Line %u: cannot interpret first character '%c'!\n", line_count, c);
 116         std::getline(f, line); // Ignore up to start of next line
 117     }
 118
 119     module->fixup_ports();
 120     design->add(module);
 121 }
 122
 123 static RTLIL::Wire* createWireIfNotExists(RTLIL::Module *module, unsigned literal)
 124 {
 125     const unsigned variable = literal >> 1;
 126     const bool invert = literal & 1;
 127     RTLIL::IdString wire_name(stringf("\\n%d%s", variable, invert ? "_inv" : "")); // FIXME: is "_inv" the right suffix?
 128     RTLIL::Wire *wire = module->wire(wire_name);
 129     if (wire) return wire;
 130     log_debug("Creating %s\n", wire_name.c_str());
 131     wire = module->addWire(wire_name);
 132     if (!invert) return wire;
 133     RTLIL::IdString wire_inv_name(stringf("\\n%d", variable));
 134     RTLIL::Wire *wire_inv = module->wire(wire_inv_name);
 135     if (wire_inv) {
 136         if (module->cell(wire_inv_name)) return wire;
 137     }
 138     else {
 139         log_debug("Creating %s\n", wire_inv_name.c_str());
 140         wire_inv = module->addWire(wire_inv_name);
 141     }
 142
 143     log_debug("Creating %s = ~%s\n", wire_name.c_str(), wire_inv_name.c_str());
 144     module->addNotGate(stringf("\\n%d_not", variable), wire_inv, wire); // FIXME: is "_not" the right suffix?
 145
 146     return wire;
 147 }
 148
 149 void AigerReader::parse_aiger_ascii()
 150 {
 151     std::string line;
 152     std::stringstream ss;
 153
 154     unsigned l1, l2, l3;
 155
 156     // Parse inputs
 157     for (unsigned i = 0; i < I; ++i, ++line_count) {
 158         if (!(f >> l1))
 159             log_error("Line %u cannot be interpreted as an input!\n", line_count);
 160         log_debug("%d is an input\n", l1);
 161         log_assert(!(l1 & 1)); // TODO: Inputs can't be inverted?
 162         RTLIL::Wire *wire = createWireIfNotExists(module, l1);
 163         wire->port_input = true;
 164         inputs.push_back(wire);
 165     }
 166
 167     // Parse latches
 168     RTLIL::Wire *clk_wire = nullptr;
 169     if (L > 0) {
 170         clk_wire = module->wire(clk_name);
 171         log_assert(!clk_wire);
 172         log_debug("Creating %s\n", clk_name.c_str());
 173         clk_wire = module->addWire(clk_name);
 174         clk_wire->port_input = true;
 175     }
 176     for (unsigned i = 0; i < L; ++i, ++line_count) {
 177         if (!(f >> l1 >> l2))
 178             log_error("Line %u cannot be interpreted as a latch!\n", line_count);
 179         log_debug("%d %d is a latch\n", l1, l2);
 180         log_assert(!(l1 & 1)); // TODO: Latch outputs can't be inverted?
 181         RTLIL::Wire *q_wire = createWireIfNotExists(module, l1);
 182         RTLIL::Wire *d_wire = createWireIfNotExists(module, l2);
 183
 184         module->addDffGate(NEW_ID, clk_wire, d_wire, q_wire);
 185
 186         // Reset logic is optional in AIGER 1.9
 187         if (f.peek() == ' ') {
 188             if (!(f >> l3))
 189                 log_error("Line %u cannot be interpreted as a latch!\n", line_count);
 190
 191             if (l3 == 0 || l3 == 1)
 192                 q_wire->attributes["\\init"] = RTLIL::Const(l3);
 193             else if (l3 == l1) {
 194                 //q_wire->attributes["\\init"] = RTLIL::Const(RTLIL::State::Sx);
 195             }
 196             else
 197                 log_error("Line %u has invalid reset literal for latch!\n", line_count);
 198         }
 199         else {
 200             // AIGER latches are assumed to be initialized to zero
 201             q_wire->attributes["\\init"] = RTLIL::Const(0);
 202         }
 203         latches.push_back(q_wire);
 204     }
 205
 206     // Parse outputs
 207     for (unsigned i = 0; i < O; ++i, ++line_count) {
 208         if (!(f >> l1))
 209             log_error("Line %u cannot be interpreted as an output!\n", line_count);
 210
 211         log_debug("%d is an output\n", l1);
 212         RTLIL::Wire *wire = createWireIfNotExists(module, l1);
 213         wire->port_output = true;
 214         outputs.push_back(wire);
 215     }
 216     std::getline(f, line); // Ignore up to start of next line
 217
 218     // TODO: Parse bad state properties
 219     for (unsigned i = 0; i < B; ++i, ++line_count)
 220         std::getline(f, line); // Ignore up to start of next line
 221
 222     // TODO: Parse invariant constraints
 223     for (unsigned i = 0; i < C; ++i, ++line_count)
 224         std::getline(f, line); // Ignore up to start of next line
 225
 226     // TODO: Parse justice properties
 227     for (unsigned i = 0; i < J; ++i, ++line_count)
 228         std::getline(f, line); // Ignore up to start of next line
 229
 230     // TODO: Parse fairness constraints
 231     for (unsigned i = 0; i < F; ++i, ++line_count)
 232         std::getline(f, line); // Ignore up to start of next line
 233
 234     // Parse AND
 235     for (unsigned i = 0; i < A; ++i) {
 236         if (!(f >> l1 >> l2 >> l3))
 237             log_error("Line %u cannot be interpreted as an AND!\n", line_count);
 238
 239         log_debug("%d %d %d is an AND\n", l1, l2, l3);
 240         log_assert(!(l1 & 1)); // TODO: Output of ANDs can't be inverted?
 241         RTLIL::Wire *o_wire = createWireIfNotExists(module, l1);
 242         RTLIL::Wire *i1_wire = createWireIfNotExists(module, l2);
 243         RTLIL::Wire *i2_wire = createWireIfNotExists(module, l3);
 244         module->addAndGate(NEW_ID, i1_wire, i2_wire, o_wire);
 245     }
 246     std::getline(f, line); // Ignore up to start of next line
 247 }
 248
 249 static unsigned parse_next_delta_literal(std::istream &f, unsigned ref)
 250 {
 251     unsigned x = 0, i = 0;
 252     unsigned char ch;
 253     while ((ch = f.get()) & 0x80)
 254         x |= (ch & 0x7f) << (7 * i++);
 255     return ref - (x | (ch << (7 * i)));
 256 }
 257
 258 void AigerReader::parse_aiger_binary()
 259 {
 260     unsigned l1, l2, l3;
 261     std::string line;
 262
 263     // Parse inputs
 264     for (unsigned i = 1; i <= I; ++i) {
 265         RTLIL::Wire *wire = createWireIfNotExists(module, i << 1);
 266         wire->port_input = true;
 267         inputs.push_back(wire);
 268     }
 269
 270     // Parse latches
 271     RTLIL::Wire *clk_wire = nullptr;
 272     if (L > 0) {
 273         clk_wire = module->wire(clk_name);
 274         log_assert(!clk_wire);
 275         log_debug("Creating %s\n", clk_name.c_str());
 276         clk_wire = module->addWire(clk_name);
 277         clk_wire->port_input = true;
 278     }
 279     l1 = (I+1) * 2;
 280     for (unsigned i = 0; i < L; ++i, ++line_count, l1 += 2) {
 281         if (!(f >> l2))
 282             log_error("Line %u cannot be interpreted as a latch!\n", line_count);
 283         log_debug("%d %d is a latch\n", l1, l2);
 284         RTLIL::Wire *q_wire = createWireIfNotExists(module, l1);
 285         RTLIL::Wire *d_wire = createWireIfNotExists(module, l2);
 286
 287         module->addDff(NEW_ID, clk_wire, d_wire, q_wire);
 288
 289         // Reset logic is optional in AIGER 1.9
 290         if (f.peek() == ' ') {
 291             if (!(f >> l3))
 292                 log_error("Line %u cannot be interpreted as a latch!\n", line_count);
 293
 294             if (l3 == 0 || l3 == 1)
 295                 q_wire->attributes["\\init"] = RTLIL::Const(l3);
 296             else if (l3 == l1) {
 297                 //q_wire->attributes["\\init"] = RTLIL::Const(RTLIL::State::Sx);
 298             }
 299             else
 300                 log_error("Line %u has invalid reset literal for latch!\n", line_count);
 301         }
 302         else {
 303             // AIGER latches are assumed to be initialized to zero
 304             q_wire->attributes["\\init"] = RTLIL::Const(0);
 305         }
 306         latches.push_back(q_wire);
 307     }
 308
 309     // Parse outputs
 310     for (unsigned i = 0; i < O; ++i, ++line_count) {
 311         if (!(f >> l1))
 312             log_error("Line %u cannot be interpreted as an output!\n", line_count);
 313
 314         log_debug("%d is an output\n", l1);
 315         RTLIL::Wire *wire = createWireIfNotExists(module, l1);
 316         wire->port_output = true;
 317         outputs.push_back(wire);
 318     }
 319     std::getline(f, line); // Ignore up to start of next line
 320
 321     // TODO: Parse bad state properties
 322     for (unsigned i = 0; i < B; ++i, ++line_count)
 323         std::getline(f, line); // Ignore up to start of next line
 324
 325     // TODO: Parse invariant constraints
 326     for (unsigned i = 0; i < C; ++i, ++line_count)
 327         std::getline(f, line); // Ignore up to start of next line
 328
 329     // TODO: Parse justice properties
 330     for (unsigned i = 0; i < J; ++i, ++line_count)
 331         std::getline(f, line); // Ignore up to start of next line
 332
 333     // TODO: Parse fairness constraints
 334     for (unsigned i = 0; i < F; ++i, ++line_count)
 335         std::getline(f, line); // Ignore up to start of next line
 336
 337     // Parse AND
 338     l1 = (I+L+1) << 1;
 339     for (unsigned i = 0; i < A; ++i, ++line_count, l1 += 2) {
 340         l2 = parse_next_delta_literal(f, l1);
 341         l3 = parse_next_delta_literal(f, l2);
 342
 343         log_debug("%d %d %d is an AND\n", l1, l2, l3);
 344         log_assert(!(l1 & 1)); // TODO: Output of ANDs can't be inverted?
 345         RTLIL::Wire *o_wire = createWireIfNotExists(module, l1);
 346         RTLIL::Wire *i1_wire = createWireIfNotExists(module, l2);
 347         RTLIL::Wire *i2_wire = createWireIfNotExists(module, l3);
 348
 349         RTLIL::Cell *and_cell = module->addCell(NEW_ID, "$_AND_");
 350         and_cell->setPort("\\A", i1_wire);
 351         and_cell->setPort("\\B", i2_wire);
 352         and_cell->setPort("\\Y", o_wire);
 353     }
 354 }
 355
 356 struct AigerFrontend : public Frontend {
 357     AigerFrontend() : Frontend("aiger", "read AIGER file") { }
 358     void help() YS_OVERRIDE
 359     {
 360         //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 361         log("\n");
 362         log("    read_aiger [options] [filename]\n");
 363         log("\n");
 364         log("Load module from an AIGER file into the current design.\n");
 365         log("\n");
 366         log("    -module_name <module_name>\n");
 367         log("        Name of module to be created (default: <filename>)"
 368 #ifdef _WIN32
 369                                                                    "top" // FIXME
 370 #else
 371                                                                    "<filename>"
 372 #endif
 373                                                            ")\n");
 374         log("\n");
 375         log("    -clk_name <wire_name>\n");
 376         log("        AIGER latches to be transformed into posedge DFFs clocked by wire of");
 377         log("        this name (default: clk)\n");
 378         log("\n");
 379     }
 380     void execute(std::istream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 381     {
 382         log_header(design, "Executing AIGER frontend.\n");
 383
 384         RTLIL::IdString clk_name = "\\clk";
 385         RTLIL::IdString module_name;
 386
 387                 size_t argidx;
 388                 for (argidx = 1; argidx < args.size(); argidx++) {
 389                         std::string arg = args[argidx];
 390                         if (arg == "-module_name" && argidx+1 < args.size()) {
 391                                 module_name = RTLIL::escape_id(args[++argidx]);
 392                                 continue;
 393                         }
 394                         if (arg == "-clk_name" && argidx+1 < args.size()) {
 395                                 clk_name = RTLIL::escape_id(args[++argidx]);
 396                                 continue;
 397                         }
 398                         break;
 399                 }
 400                 extra_args(f, filename, args, argidx);
 401
 402         if (module_name.empty()) {
 403 #ifdef _WIN32
 404             module_name = "top"; // FIXME: basename equivalent on Win32?
 405 #else
 406             char* bn = strdup(filename.c_str());
 407             module_name = RTLIL::escape_id(bn);
 408             free(bn);
 409 #endif
 410         }
 411
 412         AigerReader reader(design, *f, module_name, clk_name);
 413                 reader.parse_aiger();
 414     }
 415 } AigerFrontend;
 416
 417 YOSYS_NAMESPACE_END