passes/sat/sim.cc

   1 /*
   2  *  yosys -- Yosys Open SYnthesis Suite
   3  *
   4  *  Copyright (C) 2012  Claire Xenia Wolf <claire@yosyshq.com>
   5  *
   6  *  Permission to use, copy, modify, and/or distribute this software for any
   7  *  purpose with or without fee is hereby granted, provided that the above
   8  *  copyright notice and this permission notice appear in all copies.
   9  *
  10  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17  *
  18  */
  19
  20 #include "kernel/yosys.h"
  21 #include "kernel/sigtools.h"
  22 #include "kernel/celltypes.h"
  23 #include "kernel/mem.h"
  24 #include "kernel/fstdata.h"
  25 #include "kernel/ff.h"
  26
  27 #include <ctime>
  28
  29 USING_YOSYS_NAMESPACE
  30 PRIVATE_NAMESPACE_BEGIN
  31
  32 enum class SimulationMode {
  33         sim,
  34         cmp,
  35         gold,
  36         gate,
  37 };
  38
  39 static const std::map<std::string, int> g_units =
  40 {
  41         { "",    -9 }, // default is ns
  42         { "s",    0 },
  43         { "ms",  -3 },
  44         { "us",  -6 },
  45         { "ns",  -9 },
  46         { "ps", -12 },
  47         { "fs", -15 },
  48         { "as", -18 },
  49         { "zs", -21 },
  50 };
  51
  52 static double stringToTime(std::string str)
  53 {
  54         if (str=="END") return -1;
  55
  56         char *endptr;
  57         long value = strtol(str.c_str(), &endptr, 10);
  58
  59         if (g_units.find(endptr)==g_units.end())
  60                 log_error("Cannot parse '%s', bad unit '%s'\n", str.c_str(), endptr);
  61
  62         if (value < 0)
  63                 log_error("Time value '%s' must be positive\n", str.c_str());
  64
  65         return value * pow(10.0, g_units.at(endptr));
  66 }
  67
  68 struct SimWorker;
  69 struct OutputWriter
  70 {
  71         OutputWriter(SimWorker *w) { worker = w;};
  72         virtual ~OutputWriter() {};
  73         virtual void write(std::map<int, bool> &use_signal) = 0;
  74         SimWorker *worker;
  75 };
  76
  77 struct SimShared
  78 {
  79         bool debug = false;
  80         bool verbose = true;
  81         bool hide_internal = true;
  82         bool writeback = false;
  83         bool zinit = false;
  84         int rstlen = 1;
  85         FstData *fst = nullptr;
  86         double start_time = 0;
  87         double stop_time = -1;
  88         SimulationMode sim_mode = SimulationMode::sim;
  89         bool cycles_set = false;
  90         std::vector<std::unique_ptr<OutputWriter>> outputfiles;
  91         std::vector<std::pair<int,std::map<int,Const>>> output_data;
  92         bool ignore_x = false;
  93         bool date = false;
  94         bool multiclock = false;
  95 };
  96
  97 void zinit(State &v)
  98 {
  99         if (v != State::S1)
 100                 v = State::S0;
 101 }
 102
 103 void zinit(Const &v)
 104 {
 105         for (auto &bit : v.bits)
 106                 zinit(bit);
 107 }
 108
 109 struct SimInstance
 110 {
 111         SimShared *shared;
 112
 113         std::string scope;
 114         Module *module;
 115         Cell *instance;
 116
 117         SimInstance *parent;
 118         dict<Cell*, SimInstance*> children;
 119
 120         SigMap sigmap;
 121         dict<SigBit, State> state_nets;
 122         dict<SigBit, pool<Cell*>> upd_cells;
 123         dict<SigBit, pool<Wire*>> upd_outports;
 124
 125         pool<SigBit> dirty_bits;
 126         pool<Cell*> dirty_cells;
 127         pool<IdString> dirty_memories;
 128         pool<SimInstance*, hash_ptr_ops> dirty_children;
 129
 130         struct ff_state_t
 131         {
 132                 Const past_d;
 133                 Const past_ad;
 134                 State past_clk;
 135                 State past_ce;
 136                 State past_srst;
 137
 138                 FfData data;
 139         };
 140
 141         struct mem_state_t
 142         {
 143                 Mem *mem;
 144                 std::vector<Const> past_wr_clk;
 145                 std::vector<Const> past_wr_en;
 146                 std::vector<Const> past_wr_addr;
 147                 std::vector<Const> past_wr_data;
 148                 Const data;
 149         };
 150
 151         dict<Cell*, ff_state_t> ff_database;
 152         dict<IdString, mem_state_t> mem_database;
 153         pool<Cell*> formal_database;
 154         dict<Cell*, IdString> mem_cells;
 155
 156         std::vector<Mem> memories;
 157
 158         dict<Wire*, pair<int, Const>> signal_database;
 159         dict<Wire*, fstHandle> fst_handles;
 160         dict<IdString, dict<int,fstHandle>> fst_memories;
 161
 162         SimInstance(SimShared *shared, std::string scope, Module *module, Cell *instance = nullptr, SimInstance *parent = nullptr) :
 163                         shared(shared), scope(scope), module(module), instance(instance), parent(parent), sigmap(module)
 164         {
 165                 log_assert(module);
 166
 167                 if (parent) {
 168                         log_assert(parent->children.count(instance) == 0);
 169                         parent->children[instance] = this;
 170                 }
 171
 172                 for (auto wire : module->wires())
 173                 {
 174                         SigSpec sig = sigmap(wire);
 175
 176                         for (int i = 0; i < GetSize(sig); i++) {
 177                                 if (state_nets.count(sig[i]) == 0)
 178                                         state_nets[sig[i]] = State::Sx;
 179                                 if (wire->port_output) {
 180                                         upd_outports[sig[i]].insert(wire);
 181                                         dirty_bits.insert(sig[i]);
 182                                 }
 183                         }
 184
 185                         if ((shared->fst) && !(shared->hide_internal && wire->name[0] == '$')) {
 186                                 fstHandle id = shared->fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name));
 187                                 if (id==0 && wire->name.isPublic())
 188                                         log_warning("Unable to find wire %s in input file.\n", (scope + "." + RTLIL::unescape_id(wire->name)).c_str());
 189                                 fst_handles[wire] = id;
 190                         }
 191
 192                         if (wire->attributes.count(ID::init)) {
 193                                 Const initval = wire->attributes.at(ID::init);
 194                                 for (int i = 0; i < GetSize(sig) && i < GetSize(initval); i++)
 195                                         if (initval[i] == State::S0 || initval[i] == State::S1) {
 196                                                 state_nets[sig[i]] = initval[i];
 197                                                 dirty_bits.insert(sig[i]);
 198                                         }
 199                         }
 200                 }
 201
 202                 memories = Mem::get_all_memories(module);
 203                 for (auto &mem : memories) {
 204                         auto &mdb = mem_database[mem.memid];
 205                         mdb.mem = &mem;
 206                         for (auto &port : mem.wr_ports) {
 207                                 mdb.past_wr_clk.push_back(Const(State::Sx));
 208                                 mdb.past_wr_en.push_back(Const(State::Sx, GetSize(port.en)));
 209                                 mdb.past_wr_addr.push_back(Const(State::Sx, GetSize(port.addr)));
 210                                 mdb.past_wr_data.push_back(Const(State::Sx, GetSize(port.data)));
 211                         }
 212                         mdb.data = mem.get_init_data();
 213                 }
 214
 215                 for (auto cell : module->cells())
 216                 {
 217                         Module *mod = module->design->module(cell->type);
 218
 219                         if (mod != nullptr) {
 220                                 dirty_children.insert(new SimInstance(shared, scope + "." + RTLIL::unescape_id(cell->name), mod, cell, this));
 221                         }
 222
 223                         for (auto &port : cell->connections()) {
 224                                 if (cell->input(port.first))
 225                                         for (auto bit : sigmap(port.second)) {
 226                                                 upd_cells[bit].insert(cell);
 227                                                 // Make sure cell inputs connected to constants are updated in the first cycle
 228                                                 if (bit.wire == nullptr)
 229                                                         dirty_bits.insert(bit);
 230                                         }
 231                         }
 232
 233                         if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
 234                                 FfData ff_data(nullptr, cell);
 235                                 ff_state_t ff;
 236                                 ff.past_d = Const(State::Sx, ff_data.width);
 237                                 ff.past_ad = Const(State::Sx, ff_data.width);
 238                                 ff.past_clk = State::Sx;
 239                                 ff.past_ce = State::Sx;
 240                                 ff.past_srst = State::Sx;
 241                                 ff.data = ff_data;
 242                                 ff_database[cell] = ff;
 243                         }
 244
 245                         if (cell->is_mem_cell())
 246                         {
 247                                 std::string name = cell->parameters.at(ID::MEMID).decode_string();
 248                                 mem_cells[cell] = name;
 249                                 if (shared->fst)
 250                                         fst_memories[name] = shared->fst->getMemoryHandles(scope + "." + RTLIL::unescape_id(name));
 251                         }
 252                         if (cell->type.in(ID($assert), ID($cover), ID($assume))) {
 253                                 formal_database.insert(cell);
 254                         }
 255                 }
 256
 257                 if (shared->zinit)
 258                 {
 259                         for (auto &it : ff_database)
 260                         {
 261                                 ff_state_t &ff = it.second;
 262                                 zinit(ff.past_d);
 263                                 zinit(ff.past_ad);
 264
 265                                 SigSpec qsig = it.second.data.sig_q;
 266                                 Const qdata = get_state(qsig);
 267                                 zinit(qdata);
 268                                 set_state(qsig, qdata);
 269                         }
 270
 271                         for (auto &it : mem_database) {
 272                                 mem_state_t &mem = it.second;
 273                                 for (auto &val : mem.past_wr_en)
 274                                         zinit(val);
 275                                 zinit(mem.data);
 276                         }
 277                 }
 278         }
 279
 280         ~SimInstance()
 281         {
 282                 for (auto child : children)
 283                         delete child.second;
 284         }
 285
 286         IdString name() const
 287         {
 288                 if (instance != nullptr)
 289                         return instance->name;
 290                 return module->name;
 291         }
 292
 293         std::string hiername() const
 294         {
 295                 if (instance != nullptr)
 296                         return parent->hiername() + "." + log_id(instance->name);
 297
 298                 return log_id(module->name);
 299         }
 300
 301         Const get_state(SigSpec sig)
 302         {
 303                 Const value;
 304
 305                 for (auto bit : sigmap(sig))
 306                         if (bit.wire == nullptr)
 307                                 value.bits.push_back(bit.data);
 308                         else if (state_nets.count(bit))
 309                                 value.bits.push_back(state_nets.at(bit));
 310                         else
 311                                 value.bits.push_back(State::Sz);
 312
 313                 if (shared->debug)
 314                         log("[%s] get %s: %s\n", hiername().c_str(), log_signal(sig), log_signal(value));
 315                 return value;
 316         }
 317
 318         bool set_state(SigSpec sig, Const value)
 319         {
 320                 bool did_something = false;
 321
 322                 sig = sigmap(sig);
 323                 log_assert(GetSize(sig) <= GetSize(value));
 324
 325                 for (int i = 0; i < GetSize(sig); i++)
 326                         if (state_nets.at(sig[i]) != value[i]) {
 327                                 state_nets.at(sig[i]) = value[i];
 328                                 dirty_bits.insert(sig[i]);
 329                                 did_something = true;
 330                         }
 331
 332                 if (shared->debug)
 333                         log("[%s] set %s: %s\n", hiername().c_str(), log_signal(sig), log_signal(value));
 334                 return did_something;
 335         }
 336
 337         void set_memory_state(IdString memid, Const addr, Const data)
 338         {
 339                 auto &state = mem_database[memid];
 340
 341                 int offset = (addr.as_int() - state.mem->start_offset) * state.mem->width;
 342                 for (int i = 0; i < GetSize(data); i++)
 343                         if (0 <= i+offset && i+offset < state.mem->size * state.mem->width)
 344                                 state.data.bits[i+offset] = data.bits[i];
 345         }
 346
 347         void set_memory_state_bit(IdString memid, int offset, State data)
 348         {
 349                 auto &state = mem_database[memid];
 350                 if (offset >= state.mem->size * state.mem->width)
 351                         log_error("Addressing out of bounds bit %d/%d of memory %s\n", offset, state.mem->size * state.mem->width, log_id(memid));
 352                 state.data.bits[offset] = data;
 353         }
 354
 355         void update_cell(Cell *cell)
 356         {
 357                 if (ff_database.count(cell))
 358                         return;
 359
 360                 if (formal_database.count(cell))
 361                         return;
 362
 363                 if (mem_cells.count(cell))
 364                 {
 365                         dirty_memories.insert(mem_cells[cell]);
 366                         return;
 367                 }
 368
 369                 if (children.count(cell))
 370                 {
 371                         auto child = children.at(cell);
 372                         for (auto &conn: cell->connections())
 373                                 if (cell->input(conn.first) && GetSize(conn.second)) {
 374                                         Const value = get_state(conn.second);
 375                                         child->set_state(child->module->wire(conn.first), value);
 376                                 }
 377                         dirty_children.insert(child);
 378                         return;
 379                 }
 380
 381                 if (yosys_celltypes.cell_evaluable(cell->type))
 382                 {
 383                         RTLIL::SigSpec sig_a, sig_b, sig_c, sig_d, sig_s, sig_y;
 384                         bool has_a, has_b, has_c, has_d, has_s, has_y;
 385
 386                         has_a = cell->hasPort(ID::A);
 387                         has_b = cell->hasPort(ID::B);
 388                         has_c = cell->hasPort(ID::C);
 389                         has_d = cell->hasPort(ID::D);
 390                         has_s = cell->hasPort(ID::S);
 391                         has_y = cell->hasPort(ID::Y);
 392
 393                         if (has_a) sig_a = cell->getPort(ID::A);
 394                         if (has_b) sig_b = cell->getPort(ID::B);
 395                         if (has_c) sig_c = cell->getPort(ID::C);
 396                         if (has_d) sig_d = cell->getPort(ID::D);
 397                         if (has_s) sig_s = cell->getPort(ID::S);
 398                         if (has_y) sig_y = cell->getPort(ID::Y);
 399
 400                         if (shared->debug)
 401                                 log("[%s] eval %s (%s)\n", hiername().c_str(), log_id(cell), log_id(cell->type));
 402
 403                         // Simple (A -> Y) and (A,B -> Y) cells
 404                         if (has_a && !has_c && !has_d && !has_s && has_y) {
 405                                 set_state(sig_y, CellTypes::eval(cell, get_state(sig_a), get_state(sig_b)));
 406                                 return;
 407                         }
 408
 409                         // (A,B,C -> Y) cells
 410                         if (has_a && has_b && has_c && !has_d && !has_s && has_y) {
 411                                 set_state(sig_y, CellTypes::eval(cell, get_state(sig_a), get_state(sig_b), get_state(sig_c)));
 412                                 return;
 413                         }
 414
 415                         // (A,S -> Y) cells
 416                         if (has_a && !has_b && !has_c && !has_d && has_s && has_y) {
 417                                 set_state(sig_y, CellTypes::eval(cell, get_state(sig_a), get_state(sig_s)));
 418                                 return;
 419                         }
 420
 421                         // (A,B,S -> Y) cells
 422                         if (has_a && has_b && !has_c && !has_d && has_s && has_y) {
 423                                 set_state(sig_y, CellTypes::eval(cell, get_state(sig_a), get_state(sig_b), get_state(sig_s)));
 424                                 return;
 425                         }
 426
 427                         log_warning("Unsupported evaluable cell type: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
 428                         return;
 429                 }
 430
 431                 log_error("Unsupported cell type: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
 432         }
 433
 434         void update_memory(IdString id) {
 435                 auto &mdb = mem_database[id];
 436                 auto &mem = *mdb.mem;
 437
 438                 for (int port_idx = 0; port_idx < GetSize(mem.rd_ports); port_idx++)
 439                 {
 440                         auto &port = mem.rd_ports[port_idx];
 441                         Const addr = get_state(port.addr);
 442                         Const data = Const(State::Sx, mem.width << port.wide_log2);
 443
 444                         if (port.clk_enable)
 445                                 log_error("Memory %s.%s has clocked read ports. Run 'memory' with -nordff.\n", log_id(module), log_id(mem.memid));
 446
 447                         if (addr.is_fully_def()) {
 448                                 int index = addr.as_int() - mem.start_offset;
 449                                 if (index >= 0 && index < mem.size)
 450                                         data = mdb.data.extract(index*mem.width, mem.width << port.wide_log2);
 451                         }
 452
 453                         set_state(port.data, data);
 454                 }
 455         }
 456
 457         void update_ph1()
 458         {
 459                 pool<Cell*> queue_cells;
 460                 pool<Wire*> queue_outports;
 461
 462                 queue_cells.swap(dirty_cells);
 463
 464                 while (1)
 465                 {
 466                         for (auto bit : dirty_bits)
 467                         {
 468                                 if (upd_cells.count(bit))
 469                                         for (auto cell : upd_cells.at(bit))
 470                                                 queue_cells.insert(cell);
 471
 472                                 if (upd_outports.count(bit) && parent != nullptr)
 473                                         for (auto wire : upd_outports.at(bit))
 474                                                 queue_outports.insert(wire);
 475                         }
 476
 477                         dirty_bits.clear();
 478
 479                         if (!queue_cells.empty())
 480                         {
 481                                 for (auto cell : queue_cells)
 482                                         update_cell(cell);
 483
 484                                 queue_cells.clear();
 485                                 continue;
 486                         }
 487
 488                         for (auto &memid : dirty_memories)
 489                                 update_memory(memid);
 490                         dirty_memories.clear();
 491
 492                         for (auto wire : queue_outports)
 493                                 if (instance->hasPort(wire->name)) {
 494                                         Const value = get_state(wire);
 495                                         parent->set_state(instance->getPort(wire->name), value);
 496                                 }
 497
 498                         queue_outports.clear();
 499
 500                         for (auto child : dirty_children)
 501                                 child->update_ph1();
 502
 503                         dirty_children.clear();
 504
 505                         if (dirty_bits.empty())
 506                                 break;
 507                 }
 508         }
 509
 510         bool update_ph2()
 511         {
 512                 bool did_something = false;
 513
 514                 for (auto &it : ff_database)
 515                 {
 516                         ff_state_t &ff = it.second;
 517                         FfData &ff_data = ff.data;
 518
 519                         Const current_q = get_state(ff.data.sig_q);
 520
 521                         if (ff_data.has_clk) {
 522                                 // flip-flops
 523                                 State current_clk = get_state(ff_data.sig_clk)[0];
 524                                 if (ff_data.pol_clk ? (ff.past_clk == State::S0 && current_clk != State::S0) :
 525                                                         (ff.past_clk == State::S1 && current_clk != State::S1)) {
 526                                         bool ce = ff.past_ce == (ff_data.pol_ce ? State::S1 : State::S0);
 527                                         // set if no ce, or ce is enabled
 528                                         if (!ff_data.has_ce || (ff_data.has_ce && ce)) {
 529                                                 current_q = ff.past_d;
 530                                         }
 531                                         // override if sync reset
 532                                         if ((ff_data.has_srst) && (ff.past_srst == (ff_data.pol_srst ? State::S1 : State::S0)) &&
 533                                                 ((!ff_data.ce_over_srst) || (ff_data.ce_over_srst && ce))) {
 534                                                 current_q = ff_data.val_srst;
 535                                         }
 536                                 }
 537                         }
 538                         // async load
 539                         if (ff_data.has_aload) {
 540                                 State current_aload = get_state(ff_data.sig_aload)[0];
 541                                 if (current_aload == (ff_data.pol_aload ? State::S1 : State::S0)) {
 542                                         current_q = ff_data.has_clk ? ff.past_ad : get_state(ff.data.sig_ad);
 543                                 }
 544                         }
 545                         // async reset
 546                         if (ff_data.has_arst) {
 547                                 State current_arst = get_state(ff_data.sig_arst)[0];
 548                                 if (current_arst == (ff_data.pol_arst ? State::S1 : State::S0)) {
 549                                         current_q = ff_data.val_arst;
 550                                 }
 551                         }
 552                         // handle set/reset
 553                         if (ff.data.has_sr) {
 554                                 Const current_clr = get_state(ff.data.sig_clr);
 555                                 Const current_set = get_state(ff.data.sig_set);
 556
 557                                 for(int i=0;i<ff.past_d.size();i++) {
 558                                         if (current_clr[i] == (ff_data.pol_clr ? State::S1 : State::S0)) {
 559                                                 current_q[i] = State::S0;
 560                                         }
 561                                         else if (current_set[i] == (ff_data.pol_set ? State::S1 : State::S0)) {
 562                                                 current_q[i] = State::S1;
 563                                         }
 564                                 }
 565                         }
 566                         if (ff_data.has_gclk) {
 567                                 // $ff
 568                                 current_q = ff.past_d;
 569                         }
 570                         if (set_state(ff_data.sig_q, current_q))
 571                                 did_something = true;
 572                 }
 573
 574                 for (auto &it : mem_database)
 575                 {
 576                         mem_state_t &mdb = it.second;
 577                         auto &mem = *mdb.mem;
 578
 579                         for (int port_idx = 0; port_idx < GetSize(mem.wr_ports); port_idx++)
 580                         {
 581                                 auto &port = mem.wr_ports[port_idx];
 582                                 Const addr, data, enable;
 583
 584                                 if (!port.clk_enable)
 585                                 {
 586                                         addr = get_state(port.addr);
 587                                         data = get_state(port.data);
 588                                         enable = get_state(port.en);
 589                                 }
 590                                 else
 591                                 {
 592                                         if (port.clk_polarity ?
 593                                                         (mdb.past_wr_clk[port_idx] == State::S1 || get_state(port.clk) != State::S1) :
 594                                                         (mdb.past_wr_clk[port_idx] == State::S0 || get_state(port.clk) != State::S0))
 595                                                 continue;
 596
 597                                         addr = mdb.past_wr_addr[port_idx];
 598                                         data = mdb.past_wr_data[port_idx];
 599                                         enable = mdb.past_wr_en[port_idx];
 600                                 }
 601
 602                                 if (addr.is_fully_def())
 603                                 {
 604                                         int index = addr.as_int() - mem.start_offset;
 605                                         if (index >= 0 && index < mem.size)
 606                                                 for (int i = 0; i < (mem.width << port.wide_log2); i++)
 607                                                         if (enable[i] == State::S1 && mdb.data.bits.at(index*mem.width+i) != data[i]) {
 608                                                                 mdb.data.bits.at(index*mem.width+i) = data[i];
 609                                                                 dirty_memories.insert(mem.memid);
 610                                                                 did_something = true;
 611                                                         }
 612                                 }
 613                         }
 614                 }
 615
 616                 for (auto it : children)
 617                         if (it.second->update_ph2()) {
 618                                 dirty_children.insert(it.second);
 619                                 did_something = true;
 620                         }
 621
 622                 return did_something;
 623         }
 624
 625         void update_ph3()
 626         {
 627                 for (auto &it : ff_database)
 628                 {
 629                         ff_state_t &ff = it.second;
 630
 631                         if (ff.data.has_aload)
 632                                 ff.past_ad = get_state(ff.data.sig_ad);
 633
 634                         if (ff.data.has_clk || ff.data.has_gclk)
 635                                 ff.past_d = get_state(ff.data.sig_d);
 636
 637                         if (ff.data.has_clk)
 638                                 ff.past_clk = get_state(ff.data.sig_clk)[0];
 639
 640                         if (ff.data.has_ce)
 641                                 ff.past_ce = get_state(ff.data.sig_ce)[0];
 642
 643                         if (ff.data.has_srst)
 644                                 ff.past_srst = get_state(ff.data.sig_srst)[0];
 645                 }
 646
 647                 for (auto &it : mem_database)
 648                 {
 649                         mem_state_t &mem = it.second;
 650
 651                         for (int i = 0; i < GetSize(mem.mem->wr_ports); i++) {
 652                                 auto &port = mem.mem->wr_ports[i];
 653                                 mem.past_wr_clk[i]  = get_state(port.clk);
 654                                 mem.past_wr_en[i]   = get_state(port.en);
 655                                 mem.past_wr_addr[i] = get_state(port.addr);
 656                                 mem.past_wr_data[i] = get_state(port.data);
 657                         }
 658                 }
 659
 660                 for (auto cell : formal_database)
 661                 {
 662                         string label = log_id(cell);
 663                         if (cell->attributes.count(ID::src))
 664                                 label = cell->attributes.at(ID::src).decode_string();
 665
 666                         State a = get_state(cell->getPort(ID::A))[0];
 667                         State en = get_state(cell->getPort(ID::EN))[0];
 668
 669                         if (cell->type == ID($cover) && en == State::S1 && a != State::S1)
 670                                 log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str());
 671
 672                         if (cell->type == ID($assume) && en == State::S1 && a != State::S1)
 673                                 log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
 674
 675                         if (cell->type == ID($assert) && en == State::S1 && a != State::S1)
 676                                 log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
 677                 }
 678
 679                 for (auto it : children)
 680                         it.second->update_ph3();
 681         }
 682
 683         void writeback(pool<Module*> &wbmods)
 684         {
 685                 if (wbmods.count(module))
 686                         log_error("Instance %s of module %s is not unique: Writeback not possible. (Fix by running 'uniquify'.)\n", hiername().c_str(), log_id(module));
 687
 688                 wbmods.insert(module);
 689
 690                 for (auto wire : module->wires())
 691                         wire->attributes.erase(ID::init);
 692
 693                 for (auto &it : ff_database)
 694                 {
 695                         SigSpec sig_q = it.second.data.sig_q;
 696                         Const initval = get_state(sig_q);
 697
 698                         for (int i = 0; i < GetSize(sig_q); i++)
 699                         {
 700                                 Wire *w = sig_q[i].wire;
 701
 702                                 if (w->attributes.count(ID::init) == 0)
 703                                         w->attributes[ID::init] = Const(State::Sx, GetSize(w));
 704
 705                                 w->attributes[ID::init][sig_q[i].offset] = initval[i];
 706                         }
 707                 }
 708
 709                 for (auto &it : mem_database)
 710                 {
 711                         mem_state_t &mem = it.second;
 712                         mem.mem->clear_inits();
 713                         MemInit minit;
 714                         minit.addr = mem.mem->start_offset;
 715                         minit.data = mem.data;
 716                         minit.en = Const(State::S1, mem.mem->width);
 717                         mem.mem->inits.push_back(minit);
 718                         mem.mem->emit();
 719                 }
 720
 721                 for (auto it : children)
 722                         it.second->writeback(wbmods);
 723         }
 724
 725         void register_signals(int &id)
 726         {
 727                 for (auto wire : module->wires())
 728                 {
 729                         if (shared->hide_internal && wire->name[0] == '$')
 730                                 continue;
 731
 732                         signal_database[wire] = make_pair(id, Const());
 733                         id++;
 734                 }
 735
 736                 for (auto child : children)
 737                         child.second->register_signals(id);
 738         }
 739
 740         void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(Wire*, int, bool)> register_signal)
 741         {
 742                 enter_scope(name());
 743
 744                 dict<Wire*,bool> registers;
 745                 for (auto cell : module->cells())
 746                 {
 747                         if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
 748                                 FfData ff_data(nullptr, cell);
 749                                 SigSpec q = sigmap(ff_data.sig_q);
 750                                 if (q.is_wire() && signal_database.count(q.as_wire()) != 0) {
 751                                         registers[q.as_wire()] = true;
 752                                 }
 753                         }
 754                 }
 755
 756                 for (auto signal : signal_database)
 757                 {
 758                         register_signal(signal.first, signal.second.first, registers.count(signal.first)!=0);
 759                 }
 760
 761                 for (auto child : children)
 762                         child.second->write_output_header(enter_scope, exit_scope, register_signal);
 763
 764                 exit_scope();
 765         }
 766
 767         void register_output_step_values(std::map<int,Const> *data)
 768         {
 769                 for (auto &it : signal_database)
 770                 {
 771                         Wire *wire = it.first;
 772                         Const value = get_state(wire);
 773                         int id = it.second.first;
 774
 775                         if (it.second.second == value)
 776                                 continue;
 777
 778                         it.second.second = value;
 779                         data->emplace(id, value);
 780                 }
 781
 782                 for (auto child : children)
 783                         child.second->register_output_step_values(data);
 784         }
 785
 786         bool setInitState()
 787         {
 788                 bool did_something = false;
 789                 for(auto &item : fst_handles) {
 790                         if (item.second==0) continue; // Ignore signals not found
 791                         std::string v = shared->fst->valueOf(item.second);
 792                         did_something |= set_state(item.first, Const::from_string(v));
 793                 }
 794                 for (auto &it : ff_database)
 795                 {
 796                         ff_state_t &ff = it.second;
 797                         SigSpec dsig = it.second.data.sig_d;
 798                         Const value = get_state(dsig);
 799                         if (dsig.is_wire()) {
 800                                 ff.past_d = value;
 801                                 if (ff.data.has_aload)
 802                                         ff.past_ad = value;
 803                                 did_something |= true;
 804                         }
 805                 }
 806                 for (auto cell : module->cells())
 807                 {
 808                         if (cell->is_mem_cell()) {
 809                                 std::string memid = cell->parameters.at(ID::MEMID).decode_string();
 810                                 for (auto &data : fst_memories[memid])
 811                                 {
 812                                         std::string v = shared->fst->valueOf(data.second);
 813                                         set_memory_state(memid, Const(data.first), Const::from_string(v));
 814                                 }
 815                         }
 816                 }
 817
 818                 for (auto child : children)
 819                         did_something |= child.second->setInitState();
 820                 return did_something;
 821         }
 822
 823         void addAdditionalInputs(std::map<Wire*,fstHandle> &inputs)
 824         {
 825                 for (auto cell : module->cells())
 826                 {
 827                         if (cell->type.in(ID($anyseq))) {
 828                                 SigSpec sig_y = sigmap(cell->getPort(ID::Y));
 829                                 if (sig_y.is_wire()) {
 830                                         bool found = false;
 831                                         for(auto &item : fst_handles) {
 832                                                 if (item.second==0) continue; // Ignore signals not found
 833                                                 if (sig_y == sigmap(item.first)) {
 834                                                         inputs[sig_y.as_wire()] = item.second;
 835                                                         found = true;
 836                                                         break;
 837                                                 }
 838                                         }
 839                                         if (!found)
 840                                                 log_error("Unable to find required '%s' signal in file\n",(scope + "." + RTLIL::unescape_id(sig_y.as_wire()->name)).c_str());
 841                                 }
 842                         }
 843                 }
 844                 for (auto child : children)
 845                         child.second->addAdditionalInputs(inputs);
 846         }
 847
 848         void setState(dict<int, std::pair<SigBit,bool>> bits, std::string values)
 849         {
 850                 for(auto bit : bits) {
 851                         if (bit.first >= GetSize(values))
 852                                 log_error("Too few input data bits in file.\n");
 853                         switch(values.at(bit.first)) {
 854                                 case '0': set_state(bit.second.first, bit.second.second ? State::S1 : State::S0); break;
 855                                 case '1': set_state(bit.second.first, bit.second.second ? State::S0 : State::S1); break;
 856                                 default: set_state(bit.second.first, State::Sx); break;
 857                         }
 858                 }
 859         }
 860
 861         void setMemState(dict<int, std::pair<std::string,int>> bits, std::string values)
 862         {
 863                 for(auto bit : bits) {
 864                         if (bit.first >= GetSize(values))
 865                                 log_error("Too few input data bits in file.\n");
 866                         switch(values.at(bit.first)) {
 867                                 case '0': set_memory_state_bit(bit.second.first, bit.second.second, State::S0); break;
 868                                 case '1': set_memory_state_bit(bit.second.first, bit.second.second, State::S1); break;
 869                                 default: set_memory_state_bit(bit.second.first, bit.second.second, State::Sx); break;
 870                         }
 871                 }
 872         }
 873
 874         bool checkSignals()
 875         {
 876                 bool retVal = false;
 877                 for(auto &item : fst_handles) {
 878                         if (item.second==0) continue; // Ignore signals not found
 879                         Const fst_val = Const::from_string(shared->fst->valueOf(item.second));
 880                         Const sim_val = get_state(item.first);
 881                         if (sim_val.size()!=fst_val.size()) {
 882                                 log_warning("Signal '%s.%s' size is different in gold and gate.\n", scope.c_str(), log_id(item.first));
 883                                 continue;
 884                         }
 885                         if (shared->sim_mode == SimulationMode::sim) {
 886                                 // No checks performed when using stimulus
 887                         } else if (shared->sim_mode == SimulationMode::gate && !fst_val.is_fully_def()) { // FST data contains X
 888                                 for(int i=0;i<fst_val.size();i++) {
 889                                         if (fst_val[i]!=State::Sx && fst_val[i]!=sim_val[i]) {
 890                                                 log_warning("Signal '%s.%s' in file %s in simulation %s\n", scope.c_str(), log_id(item.first), log_signal(fst_val), log_signal(sim_val));
 891                                                 retVal = true;
 892                                                 break;
 893                                         }
 894                                 }
 895                         } else if (shared->sim_mode == SimulationMode::gold && !sim_val.is_fully_def()) { // sim data contains X
 896                                 for(int i=0;i<sim_val.size();i++) {
 897                                         if (sim_val[i]!=State::Sx && fst_val[i]!=sim_val[i]) {
 898                                                 log_warning("Signal '%s.%s' in file %s in simulation %s\n", scope.c_str(), log_id(item.first), log_signal(fst_val), log_signal(sim_val));
 899                                                 retVal = true;
 900                                                 break;
 901                                         }
 902                                 }
 903                         } else {
 904                                 if (fst_val!=sim_val) {
 905                                         log_warning("Signal '%s.%s' in file %s in simulation '%s'\n", scope.c_str(), log_id(item.first), log_signal(fst_val), log_signal(sim_val));
 906                                         retVal = true;
 907                                 }
 908                         }
 909                 }
 910                 for (auto child : children)
 911                         retVal |= child.second->checkSignals();
 912                 return retVal;
 913         }
 914 };
 915
 916 struct SimWorker : SimShared
 917 {
 918         SimInstance *top = nullptr;
 919         pool<IdString> clock, clockn, reset, resetn;
 920         std::string timescale;
 921         std::string sim_filename;
 922         std::string map_filename;
 923         std::string scope;
 924
 925         ~SimWorker()
 926         {
 927                 outputfiles.clear();
 928                 delete top;
 929         }
 930
 931         void register_signals()
 932         {
 933                 int id = 1;
 934                 top->register_signals(id);
 935         }
 936
 937         void register_output_step(int t)
 938         {
 939                 std::map<int,Const> data;
 940                 top->register_output_step_values(&data);
 941                 output_data.emplace_back(t, data);
 942         }
 943
 944         void write_output_files()
 945         {
 946                 std::map<int, bool> use_signal;
 947                 bool first = ignore_x;
 948                 for(auto& d : output_data)
 949                 {
 950                         if (first) {
 951                                 for (auto &data : d.second)
 952                                         use_signal[data.first] = !data.second.is_fully_undef();
 953                                 first = false;
 954                         } else {
 955                                 for (auto &data : d.second)
 956                                         use_signal[data.first] = true;
 957                         }
 958                         if (!ignore_x) break;
 959                 }
 960                 for(auto& writer : outputfiles)
 961                         writer->write(use_signal);
 962         }
 963
 964         void update()
 965         {
 966                 while (1)
 967                 {
 968                         if (debug)
 969                                 log("\n-- ph1 --\n");
 970
 971                         top->update_ph1();
 972
 973                         if (debug)
 974                                 log("\n-- ph2 --\n");
 975
 976                         if (!top->update_ph2())
 977                                 break;
 978                 }
 979
 980                 if (debug)
 981                         log("\n-- ph3 --\n");
 982
 983                 top->update_ph3();
 984         }
 985
 986         void set_inports(pool<IdString> ports, State value)
 987         {
 988                 for (auto portname : ports)
 989                 {
 990                         Wire *w = top->module->wire(portname);
 991
 992                         if (w == nullptr)
 993                                 log_error("Can't find port %s on module %s.\n", log_id(portname), log_id(top->module));
 994
 995                         top->set_state(w, value);
 996                 }
 997         }
 998
 999         void run(Module *topmod, int numcycles)
1000         {
1001                 log_assert(top == nullptr);
1002                 top = new SimInstance(this, scope, topmod);
1003                 register_signals();
1004
1005                 if (debug)
1006                         log("\n===== 0 =====\n");
1007                 else if (verbose)
1008                         log("Simulating cycle 0.\n");
1009
1010                 set_inports(reset, State::S1);
1011                 set_inports(resetn, State::S0);
1012
1013                 set_inports(clock, State::Sx);
1014                 set_inports(clockn, State::Sx);
1015
1016                 update();
1017
1018                 register_output_step(0);
1019
1020                 for (int cycle = 0; cycle < numcycles; cycle++)
1021                 {
1022                         if (debug)
1023                                 log("\n===== %d =====\n", 10*cycle + 5);
1024                         else if (verbose)
1025                                 log("Simulating cycle %d.\n", (cycle*2)+1);
1026                         set_inports(clock, State::S0);
1027                         set_inports(clockn, State::S1);
1028
1029                         update();
1030                         register_output_step(10*cycle + 5);
1031
1032                         if (debug)
1033                                 log("\n===== %d =====\n", 10*cycle + 10);
1034                         else if (verbose)
1035                                 log("Simulating cycle %d.\n", (cycle*2)+2);
1036
1037                         set_inports(clock, State::S1);
1038                         set_inports(clockn, State::S0);
1039
1040                         if (cycle+1 == rstlen) {
1041                                 set_inports(reset, State::S0);
1042                                 set_inports(resetn, State::S1);
1043                         }
1044
1045                         update();
1046                         register_output_step(10*cycle + 10);
1047                 }
1048
1049                 register_output_step(10*numcycles + 2);
1050
1051                 write_output_files();
1052
1053                 if (writeback) {
1054                         pool<Module*> wbmods;
1055                         top->writeback(wbmods);
1056                 }
1057         }
1058
1059         void run_cosim_fst(Module *topmod, int numcycles)
1060         {
1061                 log_assert(top == nullptr);
1062                 fst = new FstData(sim_filename);
1063
1064                 if (scope.empty())
1065                         log_error("Scope must be defined for co-simulation.\n");
1066
1067                 top = new SimInstance(this, scope, topmod);
1068                 register_signals();
1069
1070                 std::vector<fstHandle> fst_clock;
1071
1072                 for (auto portname : clock)
1073                 {
1074                         Wire *w = topmod->wire(portname);
1075                         if (!w)
1076                                 log_error("Can't find port %s on module %s.\n", log_id(portname), log_id(top->module));
1077                         if (!w->port_input)
1078                                 log_error("Clock port %s on module %s is not input.\n", log_id(portname), log_id(top->module));
1079                         fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(portname));
1080                         if (id==0)
1081                                 log_error("Can't find port %s.%s in FST.\n", scope.c_str(), log_id(portname));
1082                         fst_clock.push_back(id);
1083                 }
1084                 for (auto portname : clockn)
1085                 {
1086                         Wire *w = topmod->wire(portname);
1087                         if (!w)
1088                                 log_error("Can't find port %s on module %s.\n", log_id(portname), log_id(top->module));
1089                         if (!w->port_input)
1090                                 log_error("Clock port %s on module %s is not input.\n", log_id(portname), log_id(top->module));
1091                         fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(portname));
1092                         if (id==0)
1093                                 log_error("Can't find port %s.%s in FST.\n", scope.c_str(), log_id(portname));
1094                         fst_clock.push_back(id);
1095                 }
1096
1097                 SigMap sigmap(topmod);
1098                 std::map<Wire*,fstHandle> inputs;
1099
1100                 for (auto wire : topmod->wires()) {
1101                         if (wire->port_input) {
1102                                 fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name));
1103                                 if (id==0)
1104                                         log_error("Unable to find required '%s' signal in file\n",(scope + "." + RTLIL::unescape_id(wire->name)).c_str());
1105                                 inputs[wire] = id;
1106                         }
1107                 }
1108
1109                 top->addAdditionalInputs(inputs);
1110
1111                 uint64_t startCount = 0;
1112                 uint64_t stopCount = 0;
1113                 if (start_time==0) {
1114                         if (start_time < fst->getStartTime())
1115                                 log_warning("Start time is before simulation file start time\n");
1116                         startCount = fst->getStartTime();
1117                 } else if (start_time==-1)
1118                         startCount = fst->getEndTime();
1119                 else {
1120                         startCount = start_time / fst->getTimescale();
1121                         if (startCount > fst->getEndTime()) {
1122                                 startCount = fst->getEndTime();
1123                                 log_warning("Start time is after simulation file end time\n");
1124                         }
1125                 }
1126                 if (stop_time==0) {
1127                         if (stop_time < fst->getStartTime())
1128                                 log_warning("Stop time is before simulation file start time\n");
1129                         stopCount = fst->getStartTime();
1130                 } else if (stop_time==-1)
1131                         stopCount = fst->getEndTime();
1132                 else {
1133                         stopCount = stop_time / fst->getTimescale();
1134                         if (stopCount > fst->getEndTime()) {
1135                                 stopCount = fst->getEndTime();
1136                                 log_warning("Stop time is after simulation file end time\n");
1137                         }
1138                 }
1139                 if (stopCount<startCount) {
1140                         log_error("Stop time is before start time\n");
1141                 }
1142
1143                 bool initial = true;
1144                 int cycle = 0;
1145                 log("Co-simulation from %lu%s to %lu%s", (unsigned long)startCount, fst->getTimescaleString(), (unsigned long)stopCount, fst->getTimescaleString());
1146                 if (cycles_set)
1147                         log(" for %d clock cycle(s)",numcycles);
1148                 log("\n");
1149                 bool all_samples = fst_clock.empty();
1150
1151                 try {
1152                         fst->reconstructAllAtTimes(fst_clock, startCount, stopCount, [&](uint64_t time) {
1153                                 if (verbose)
1154                                         log("Co-simulating %s %d [%lu%s].\n", (all_samples ? "sample" : "cycle"), cycle, (unsigned long)time, fst->getTimescaleString());
1155                                 bool did_something = false;
1156                                 for(auto &item : inputs) {
1157                                         std::string v = fst->valueOf(item.second);
1158                                         did_something |= top->set_state(item.first, Const::from_string(v));
1159                                 }
1160
1161                                 if (initial) {
1162                                         did_something |= top->setInitState();
1163                                         initial = false;
1164                                 }
1165                                 if (did_something)
1166                                         update();
1167                                 register_output_step(time);
1168
1169                                 bool status = top->checkSignals();
1170                                 if (status)
1171                                         log_error("Signal difference\n");
1172                                 cycle++;
1173
1174                                 // Limit to number of cycles if provided
1175                                 if (cycles_set && cycle > numcycles *2)
1176                                         throw fst_end_of_data_exception();
1177                                 if (time==stopCount)
1178                                         throw fst_end_of_data_exception();
1179                         });
1180                 } catch(fst_end_of_data_exception) {
1181                         // end of data detected
1182                 }
1183
1184                 write_output_files();
1185
1186                 if (writeback) {
1187                         pool<Module*> wbmods;
1188                         top->writeback(wbmods);
1189                 }
1190                 delete fst;
1191         }
1192
1193         std::string cell_name(std::string const & name)
1194         {
1195                 size_t pos = name.find_last_of("[");
1196                 if (pos!=std::string::npos)
1197                         return name.substr(0, pos);
1198                 return name;
1199         }
1200
1201         int mem_cell_addr(std::string const & name)
1202         {
1203                 size_t pos = name.find_last_of("[");
1204                 return atoi(name.substr(pos+1).c_str());
1205         }
1206
1207         void run_cosim_aiger_witness(Module *topmod)
1208         {
1209                 log_assert(top == nullptr);
1210                 if (!multiclock && (clock.size()+clockn.size())==0)
1211                         log_error("Clock signal must be specified.\n");
1212                 if (multiclock && (clock.size()+clockn.size())>0)
1213                         log_error("For multiclock witness there should be no clock signal.\n");
1214
1215                 top = new SimInstance(this, scope, topmod);
1216                 register_signals();
1217
1218                 std::ifstream mf(map_filename);
1219                 std::string type, symbol;
1220                 int variable, index;
1221                 dict<int, std::pair<SigBit,bool>> inputs, inits, latches;
1222                 dict<int, std::pair<std::string,int>> mem_inits, mem_latches;
1223                 if (mf.fail())
1224                         log_cmd_error("Not able to read AIGER witness map file.\n");
1225                 while (mf >> type >> variable >> index >> symbol) {
1226                         RTLIL::IdString escaped_s = RTLIL::escape_id(symbol);
1227                         Wire *w = topmod->wire(escaped_s);
1228                         if (!w) {
1229                                 escaped_s = RTLIL::escape_id(cell_name(symbol));
1230                                 Cell *c = topmod->cell(escaped_s);
1231                                 if (!c)
1232                                         log_warning("Wire/cell %s not present in module %s\n",symbol.c_str(),log_id(topmod));
1233
1234                                 if (c->is_mem_cell()) {
1235                                         std::string memid = c->parameters.at(ID::MEMID).decode_string();
1236                                         auto &state = top->mem_database[memid];
1237
1238                                         int offset = (mem_cell_addr(symbol) - state.mem->start_offset) * state.mem->width + index;
1239                                         if (type == "init")
1240                                                 mem_inits[variable] = { memid, offset };
1241                                         else if (type == "latch")
1242                                                 mem_latches[variable] = { memid, offset };
1243                                         else
1244                                                 log_error("Map file addressing cell %s as type %s\n", symbol.c_str(), type.c_str());
1245                                 } else {
1246                                         log_error("Cell %s in map file is not memory cell\n", symbol.c_str());
1247                                 }
1248                         } else {
1249                                 if (index < w->start_offset || index > w->start_offset + w->width)
1250                                         log_error("Index %d for wire %s is out of range\n", index, log_signal(w));
1251                                 if (type == "input") {
1252                                         inputs[variable] = {SigBit(w,index-w->start_offset), false};
1253                                 } else if (type == "init") {
1254                                         inits[variable] = {SigBit(w,index-w->start_offset), false};
1255                                 } else if (type == "latch") {
1256                                         latches[variable] = {SigBit(w,index-w->start_offset), false};
1257                                 } else if (type == "invlatch") {
1258                                         latches[variable] = {SigBit(w,index-w->start_offset), true};
1259                                 }
1260                         }
1261                 }
1262
1263                 std::ifstream f;
1264                 f.open(sim_filename.c_str());
1265                 if (f.fail() || GetSize(sim_filename) == 0)
1266                         log_error("Can not open file `%s`\n", sim_filename.c_str());
1267
1268                 int state = 0;
1269                 std::string status;
1270                 int cycle = 0;
1271
1272                 while (!f.eof())
1273                 {
1274                         std::string line;
1275                         std::getline(f, line);
1276                         if (line.size()==0 || line[0]=='#' || line[0]=='c' || line[0]=='f' || line[0]=='u') continue;
1277                         if (line[0]=='.') break;
1278                         if (state==0 && line.size()!=1) {
1279                                 // old format detected, latch data
1280                                 state = 2;
1281                         }
1282                         if (state==1 && line[0]!='b' && line[0]!='j') {
1283                                 // was old format but with 1 bit latch
1284                                 top->setState(latches, status);
1285                                 state = 3;
1286                         }
1287
1288                         switch(state)
1289                         {
1290                                 case 0:
1291                                         status = line;
1292                                         state = 1;
1293                                         break;
1294                                 case 1:
1295                                         state = 2;
1296                                         break;
1297                                 case 2:
1298                                         top->setState(latches, line);
1299                                         top->setMemState(mem_latches, line);
1300                                         state = 3;
1301                                         break;
1302                                 default:
1303                                         if (verbose)
1304                                                 log("Simulating cycle %d.\n", cycle);
1305                                         top->setState(inputs, line);
1306                                         if (cycle) {
1307                                                 set_inports(clock, State::S1);
1308                                                 set_inports(clockn, State::S0);
1309                                         } else {
1310                                                 top->setState(inits, line);
1311                                                 top->setMemState(mem_inits, line);
1312                                                 set_inports(clock, State::S0);
1313                                                 set_inports(clockn, State::S1);
1314                                         }
1315                                         update();
1316                                         register_output_step(10*cycle);
1317                                         if (!multiclock && cycle) {
1318                                                 set_inports(clock, State::S0);
1319                                                 set_inports(clockn, State::S1);
1320                                                 update();
1321                                                 register_output_step(10*cycle + 5);
1322                                         }
1323                                         cycle++;
1324                                         break;
1325                         }
1326                 }
1327                 register_output_step(10*cycle);
1328                 write_output_files();
1329         }
1330
1331         std::vector<std::string> split(std::string text, const char *delim)
1332         {
1333                 std::vector<std::string> list;
1334                 char *p = strdup(text.c_str());
1335                 char *t = strtok(p, delim);
1336                 while (t != NULL) {
1337                         list.push_back(t);
1338                         t = strtok(NULL, delim);
1339                 }
1340                 free(p);
1341                 return list;
1342         }
1343
1344         std::string signal_name(std::string const & name)
1345         {
1346                 size_t pos = name.find_first_of("@");
1347                 if (pos==std::string::npos) {
1348                         pos = name.find_first_of("#");
1349                         if (pos==std::string::npos)
1350                                 log_error("Line does not contain proper signal name `%s`\n", name.c_str());
1351                 }
1352                 return name.substr(0, pos);
1353         }
1354
1355         void run_cosim_btor2_witness(Module *topmod)
1356         {
1357                 log_assert(top == nullptr);
1358                 if (!multiclock && (clock.size()+clockn.size())==0)
1359                         log_error("Clock signal must be specified.\n");
1360                 if (multiclock && (clock.size()+clockn.size())>0)
1361                         log_error("For multiclock witness there should be no clock signal.\n");
1362                 std::ifstream f;
1363                 f.open(sim_filename.c_str());
1364                 if (f.fail() || GetSize(sim_filename) == 0)
1365                         log_error("Can not open file `%s`\n", sim_filename.c_str());
1366
1367                 int state = 0;
1368                 int cycle = 0;
1369                 top = new SimInstance(this, scope, topmod);
1370                 register_signals();
1371                 int prev_cycle = 0;
1372                 int curr_cycle = 0;
1373                 std::vector<std::string> parts;
1374                 size_t len = 0;
1375                 while (!f.eof())
1376                 {
1377                         std::string line;
1378                         std::getline(f, line);
1379                         if (line.size()==0) continue;
1380
1381                         if (line[0]=='#' || line[0]=='@' || line[0]=='.') {
1382                                 if (line[0]!='.')
1383                                         curr_cycle = atoi(line.c_str()+1);
1384                                 else
1385                                         curr_cycle = -1; // force detect change
1386
1387                                 if (curr_cycle != prev_cycle) {
1388                                         if (verbose)
1389                                                 log("Simulating cycle %d.\n", cycle);
1390                                         set_inports(clock, State::S1);
1391                                         set_inports(clockn, State::S0);
1392                                         update();
1393                                         register_output_step(10*cycle+0);
1394                                         if (!multiclock) {
1395                                                 set_inports(clock, State::S0);
1396                                                 set_inports(clockn, State::S1);
1397                                                 update();
1398                                                 register_output_step(10*cycle+5);
1399                                         }
1400                                         cycle++;
1401                                         prev_cycle = curr_cycle;
1402                                 }
1403                                 if (line[0]=='.') break;
1404                                 continue;
1405                         }
1406
1407                         switch(state)
1408                         {
1409                                 case 0:
1410                                         if (line=="sat")
1411                                                 state = 1;
1412                                         break;
1413                                 case 1:
1414                                         if (line[0]=='b' || line[0]=='j')
1415                                                 state = 2;
1416                                         else
1417                                                 log_error("Line does not contain property.\n");
1418                                         break;
1419                                 default: // set state or inputs
1420                                         parts = split(line, " ");
1421                                         len = parts.size();
1422                                         if (len<3 || len>4)
1423                                                 log_error("Invalid set state line content.\n");
1424
1425                                         RTLIL::IdString escaped_s = RTLIL::escape_id(signal_name(parts[len-1]));
1426                                         if (len==3) {
1427                                                 Wire *w = topmod->wire(escaped_s);
1428                                                 if (!w) {
1429                                                         Cell *c = topmod->cell(escaped_s);
1430                                                         if (!c)
1431                                                                 log_warning("Wire/cell %s not present in module %s\n",log_id(escaped_s),log_id(topmod));
1432                                                         else if (c->type.in(ID($anyconst), ID($anyseq))) {
1433                                                                 SigSpec sig_y= c->getPort(ID::Y);
1434                                                                 if ((int)parts[1].size() != GetSize(sig_y))
1435                                                                         log_error("Size of wire %s is different than provided data.\n", log_signal(sig_y));
1436                                                                 top->set_state(sig_y, Const::from_string(parts[1]));
1437                                                         }
1438                                                 } else {
1439                                                         if ((int)parts[1].size() != w->width)
1440                                                                 log_error("Size of wire %s is different than provided data.\n", log_signal(w));
1441                                                         top->set_state(w, Const::from_string(parts[1]));
1442                                                 }
1443                                         } else {
1444                                                 Cell *c = topmod->cell(escaped_s);
1445                                                 if (!c)
1446                                                         log_error("Cell %s not present in module %s\n",log_id(escaped_s),log_id(topmod));
1447                                                 if (!c->is_mem_cell())
1448                                                         log_error("Cell %s is not memory cell in module %s\n",log_id(escaped_s),log_id(topmod));
1449
1450                                                 Const addr = Const::from_string(parts[1].substr(1,parts[1].size()-2));
1451                                                 Const data = Const::from_string(parts[2]);
1452                                                 top->set_memory_state(c->parameters.at(ID::MEMID).decode_string(), addr, data);
1453                                         }
1454                                         break;
1455                         }
1456                 }
1457                 register_output_step(10*cycle);
1458                 write_output_files();
1459         }
1460
1461         std::string define_signal(Wire *wire)
1462         {
1463                 std::stringstream f;
1464
1465                 if (wire->width==1)
1466                         f << stringf("%s", RTLIL::unescape_id(wire->name).c_str());
1467                 else
1468                         if (wire->upto)
1469                                 f << stringf("[%d:%d] %s", wire->start_offset, wire->width - 1 + wire->start_offset, RTLIL::unescape_id(wire->name).c_str());
1470                         else
1471                                 f << stringf("[%d:%d] %s", wire->width - 1 + wire->start_offset, wire->start_offset, RTLIL::unescape_id(wire->name).c_str());
1472                 return f.str();
1473         }
1474
1475         std::string signal_list(std::map<Wire*,fstHandle> &signals)
1476         {
1477                 std::stringstream f;
1478                 for(auto item=signals.begin();item!=signals.end();item++)
1479                         f << stringf("%c%s", (item==signals.begin() ? ' ' : ','), RTLIL::unescape_id(item->first->name).c_str());
1480                 return f.str();
1481         }
1482
1483         void generate_tb(Module *topmod, std::string tb_filename, int numcycles)
1484         {
1485                 fst = new FstData(sim_filename);
1486
1487                 if (scope.empty())
1488                         log_error("Scope must be defined for co-simulation.\n");
1489
1490                 if ((clock.size()+clockn.size())==0)
1491                         log_error("Clock signal must be specified.\n");
1492
1493                 std::vector<fstHandle> fst_clock;
1494                 std::map<Wire*,fstHandle> clocks;
1495
1496                 for (auto portname : clock)
1497                 {
1498                         Wire *w = topmod->wire(portname);
1499                         if (!w)
1500                                 log_error("Can't find port %s on module %s.\n", log_id(portname), log_id(top->module));
1501                         if (!w->port_input)
1502                                 log_error("Clock port %s on module %s is not input.\n", log_id(portname), log_id(top->module));
1503                         fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(portname));
1504                         if (id==0)
1505                                 log_error("Can't find port %s.%s in FST.\n", scope.c_str(), log_id(portname));
1506                         fst_clock.push_back(id);
1507                         clocks[w] = id;
1508                 }
1509                 for (auto portname : clockn)
1510                 {
1511                         Wire *w = topmod->wire(portname);
1512                         if (!w)
1513                                 log_error("Can't find port %s on module %s.\n", log_id(portname), log_id(top->module));
1514                         if (!w->port_input)
1515                                 log_error("Clock port %s on module %s is not input.\n", log_id(portname), log_id(top->module));
1516                         fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(portname));
1517                         if (id==0)
1518                                 log_error("Can't find port %s.%s in FST.\n", scope.c_str(), log_id(portname));
1519                         fst_clock.push_back(id);
1520                         clocks[w] = id;
1521                 }
1522
1523                 SigMap sigmap(topmod);
1524                 std::map<Wire*,fstHandle> inputs;
1525                 std::map<Wire*,fstHandle> outputs;
1526
1527                 for (auto wire : topmod->wires()) {
1528                         fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name));
1529                         if (id==0 && (wire->port_input || wire->port_output))
1530                                 log_error("Unable to find required '%s' signal in file\n",(scope + "." + RTLIL::unescape_id(wire->name)).c_str());
1531                         if (wire->port_input)
1532                                 if (clocks.find(wire)==clocks.end())
1533                                         inputs[wire] = id;
1534                         if (wire->port_output)
1535                                 outputs[wire] = id;
1536                 }
1537
1538                 uint64_t startCount = 0;
1539                 uint64_t stopCount = 0;
1540                 if (start_time==0) {
1541                         if (start_time < fst->getStartTime())
1542                                 log_warning("Start time is before simulation file start time\n");
1543                         startCount = fst->getStartTime();
1544                 } else if (start_time==-1)
1545                         startCount = fst->getEndTime();
1546                 else {
1547                         startCount = start_time / fst->getTimescale();
1548                         if (startCount > fst->getEndTime()) {
1549                                 startCount = fst->getEndTime();
1550                                 log_warning("Start time is after simulation file end time\n");
1551                         }
1552                 }
1553                 if (stop_time==0) {
1554                         if (stop_time < fst->getStartTime())
1555                                 log_warning("Stop time is before simulation file start time\n");
1556                         stopCount = fst->getStartTime();
1557                 } else if (stop_time==-1)
1558                         stopCount = fst->getEndTime();
1559                 else {
1560                         stopCount = stop_time / fst->getTimescale();
1561                         if (stopCount > fst->getEndTime()) {
1562                                 stopCount = fst->getEndTime();
1563                                 log_warning("Stop time is after simulation file end time\n");
1564                         }
1565                 }
1566                 if (stopCount<startCount) {
1567                         log_error("Stop time is before start time\n");
1568                 }
1569
1570                 int cycle = 0;
1571                 log("Generate testbench data from %lu%s to %lu%s", (unsigned long)startCount, fst->getTimescaleString(), (unsigned long)stopCount, fst->getTimescaleString());
1572                 if (cycles_set)
1573                         log(" for %d clock cycle(s)",numcycles);
1574                 log("\n");
1575
1576                 std::stringstream f;
1577                 f << stringf("`timescale 1%s/1%s\n", fst->getTimescaleString(),fst->getTimescaleString());
1578                 f << stringf("module %s();\n",tb_filename.c_str());
1579                 int clk_len = 0;
1580                 int inputs_len = 0;
1581                 int outputs_len = 0;
1582                 for(auto &item : clocks) {
1583                         clk_len += item.first->width;
1584                         f << "\treg " << define_signal(item.first) << ";\n";
1585                 }
1586                 for(auto &item : inputs) {
1587                         inputs_len += item.first->width;
1588                         f << "\treg " << define_signal(item.first) << ";\n";
1589                 }
1590                 for(auto &item : outputs) {
1591                         outputs_len += item.first->width;
1592                         f << "\twire " << define_signal(item.first) << ";\n";
1593                 }
1594                 int data_len = clk_len + inputs_len + outputs_len + 32;
1595                 f << "\n";
1596                 f << stringf("\t%s uut(",RTLIL::unescape_id(topmod->name).c_str());
1597                 for(auto item=clocks.begin();item!=clocks.end();item++)
1598                         f << stringf("%c.%s(%s)", (item==clocks.begin() ? ' ' : ','), RTLIL::unescape_id(item->first->name).c_str(), RTLIL::unescape_id(item->first->name).c_str());
1599                 for(auto &item : inputs)
1600                         f << stringf(",.%s(%s)", RTLIL::unescape_id(item.first->name).c_str(), RTLIL::unescape_id(item.first->name).c_str());
1601                 for(auto &item : outputs)
1602                         f << stringf(",.%s(%s)", RTLIL::unescape_id(item.first->name).c_str(), RTLIL::unescape_id(item.first->name).c_str());
1603                 f << ");\n";
1604                 f << "\n";
1605                 f << "\tinteger i;\n";
1606                 uint64_t prev_time = startCount;
1607                 log("Writing data to `%s`\n", (tb_filename+".txt").c_str());
1608                 std::ofstream data_file(tb_filename+".txt");
1609                 std::stringstream initstate;
1610                 try {
1611                         fst->reconstructAllAtTimes(fst_clock, startCount, stopCount, [&](uint64_t time) {
1612                                 for(auto &item : clocks)
1613                                         data_file << stringf("%s",fst->valueOf(item.second).c_str());
1614                                 for(auto &item : inputs)
1615                                         data_file << stringf("%s",fst->valueOf(item.second).c_str());
1616                                 for(auto &item : outputs)
1617                                         data_file << stringf("%s",fst->valueOf(item.second).c_str());
1618                                 data_file << stringf("%s\n",Const(time-prev_time).as_string().c_str());
1619
1620                                 if (time==startCount) {
1621                                         // initial state
1622                                         for(auto var : fst->getVars()) {
1623                                                 if (var.is_reg && !Const::from_string(fst->valueOf(var.id).c_str()).is_fully_undef()) {
1624                                                         if (var.scope == scope) {
1625                                                                 initstate << stringf("\t\tuut.%s = %d'b%s;\n", var.name.c_str(), var.width, fst->valueOf(var.id).c_str());
1626                                                         } else if (var.scope.find(scope+".")==0) {
1627                                                                 initstate << stringf("\t\tuut.%s.%s = %d'b%s;\n",var.scope.substr(scope.size()+1).c_str(), var.name.c_str(), var.width, fst->valueOf(var.id).c_str());
1628                                                         }
1629                                                 }
1630                                         }
1631                                 }
1632                                 cycle++;
1633                                 prev_time = time;
1634
1635                                 // Limit to number of cycles if provided
1636                                 if (cycles_set && cycle > numcycles *2)
1637                                         throw fst_end_of_data_exception();
1638                                 if (time==stopCount)
1639                                         throw fst_end_of_data_exception();
1640                         });
1641                 } catch(fst_end_of_data_exception) {
1642                         // end of data detected
1643                 }
1644
1645                 f << stringf("\treg [0:%d] data [0:%d];\n", data_len-1, cycle-1);
1646                 f << "\tinitial begin;\n";
1647                 f << stringf("\t\t$dumpfile(\"%s\");\n",tb_filename.c_str());
1648                 f << stringf("\t\t$dumpvars(0,%s);\n",tb_filename.c_str());
1649                 f << initstate.str();
1650                 f << stringf("\t\t$readmemb(\"%s.txt\", data);\n",tb_filename.c_str());
1651
1652                 f << stringf("\t\t#(data[0][%d:%d]);\n", data_len-32, data_len-1);
1653                 f << stringf("\t\t{%s } = data[0][%d:%d];\n", signal_list(clocks).c_str(), 0, clk_len-1);
1654                 f << stringf("\t\t{%s } <= data[0][%d:%d];\n", signal_list(inputs).c_str(), clk_len, clk_len+inputs_len-1);
1655
1656                 f << stringf("\t\tfor (i = 1; i < %d; i++) begin\n",cycle);
1657
1658                 f << stringf("\t\t\t#(data[i][%d:%d]);\n", data_len-32, data_len-1);
1659                 f << stringf("\t\t\t{%s } = data[i][%d:%d];\n", signal_list(clocks).c_str(), 0, clk_len-1);
1660                 f << stringf("\t\t\t{%s } <= data[i][%d:%d];\n", signal_list(inputs).c_str(), clk_len, clk_len+inputs_len-1);
1661
1662                 f << stringf("\t\t\tif ({%s } != data[i-1][%d:%d]) begin\n", signal_list(outputs).c_str(), clk_len+inputs_len, clk_len+inputs_len+outputs_len-1);
1663                 f << "\t\t\t\t$error(\"Signal difference detected\\n\");\n";
1664                 f << "\t\t\tend\n";
1665
1666                 f << "\t\tend\n";
1667
1668                 f << "\t\t$finish;\n";
1669                 f << "\tend\n";
1670                 f << "endmodule\n";
1671
1672                 log("Writing testbench to `%s`\n", (tb_filename+".v").c_str());
1673                 std::ofstream tb_file(tb_filename+".v");
1674                 tb_file << f.str();
1675
1676                 delete fst;
1677         }
1678 };
1679
1680 struct VCDWriter : public OutputWriter
1681 {
1682         VCDWriter(SimWorker *worker, std::string filename) : OutputWriter(worker) {
1683                 vcdfile.open(filename.c_str());
1684         }
1685
1686         void write(std::map<int, bool> &use_signal) override
1687         {
1688                 if (!vcdfile.is_open()) return;
1689                 vcdfile << stringf("$version %s $end\n", worker->date ? yosys_version_str : "Yosys");
1690
1691                 if (worker->date) {
1692                         std::time_t t = std::time(nullptr);
1693                         char mbstr[255];
1694                         if (std::strftime(mbstr, sizeof(mbstr), "%c", std::localtime(&t))) {
1695                                 vcdfile << stringf("$date ") << mbstr << stringf(" $end\n");
1696                         }
1697                 }
1698
1699                 if (!worker->timescale.empty())
1700                         vcdfile << stringf("$timescale %s $end\n", worker->timescale.c_str());
1701
1702                 worker->top->write_output_header(
1703                         [this](IdString name) { vcdfile << stringf("$scope module %s $end\n", log_id(name)); },
1704                         [this]() { vcdfile << stringf("$upscope $end\n");},
1705                         [this,use_signal](Wire *wire, int id, bool is_reg) { if (use_signal.at(id)) vcdfile << stringf("$var %s %d n%d %s%s $end\n", is_reg ? "reg" : "wire", GetSize(wire), id, wire->name[0] == '$' ? "\\" : "", log_id(wire)); }
1706                 );
1707
1708                 vcdfile << stringf("$enddefinitions $end\n");
1709
1710                 for(auto& d : worker->output_data)
1711                 {
1712                         vcdfile << stringf("#%d\n", d.first);
1713                         for (auto &data : d.second)
1714                         {
1715                                 if (!use_signal.at(data.first)) continue;
1716                                 Const value = data.second;
1717                                 vcdfile << "b";
1718                                 for (int i = GetSize(value)-1; i >= 0; i--) {
1719                                         switch (value[i]) {
1720                                                 case State::S0: vcdfile << "0"; break;
1721                                                 case State::S1: vcdfile << "1"; break;
1722                                                 case State::Sx: vcdfile << "x"; break;
1723                                                 default: vcdfile << "z";
1724                                         }
1725                                 }
1726                                 vcdfile << stringf(" n%d\n", data.first);
1727                         }
1728                 }
1729         }
1730
1731         std::ofstream vcdfile;
1732 };
1733
1734 struct FSTWriter : public OutputWriter
1735 {
1736         FSTWriter(SimWorker *worker, std::string filename) : OutputWriter(worker) {
1737                 fstfile = (struct fstContext *)fstWriterCreate(filename.c_str(),1);
1738         }
1739
1740         virtual ~FSTWriter()
1741         {
1742                 fstWriterClose(fstfile);
1743         }
1744
1745         void write(std::map<int, bool> &use_signal) override
1746         {
1747                 if (!fstfile) return;
1748                 std::time_t t = std::time(nullptr);
1749                 fstWriterSetVersion(fstfile, worker->date ? yosys_version_str : "Yosys");
1750                 if (worker->date)
1751                         fstWriterSetDate(fstfile, asctime(std::localtime(&t)));
1752                 else
1753                         fstWriterSetDate(fstfile, "");
1754                 if (!worker->timescale.empty())
1755                         fstWriterSetTimescaleFromString(fstfile, worker->timescale.c_str());
1756
1757                 fstWriterSetPackType(fstfile, FST_WR_PT_FASTLZ);
1758                 fstWriterSetRepackOnClose(fstfile, 1);
1759
1760                 worker->top->write_output_header(
1761                         [this](IdString name) { fstWriterSetScope(fstfile, FST_ST_VCD_MODULE, stringf("%s",log_id(name)).c_str(), nullptr); },
1762                         [this]() { fstWriterSetUpscope(fstfile); },
1763                         [this,use_signal](Wire *wire, int id, bool is_reg) {
1764                                 if (!use_signal.at(id)) return;
1765                                 fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, GetSize(wire),
1766                                                                                                 stringf("%s%s", wire->name[0] == '$' ? "\\" : "", log_id(wire)).c_str(), 0);
1767
1768                                 mapping.emplace(id, fst_id);
1769                         }
1770                 );
1771
1772                 for(auto& d : worker->output_data)
1773                 {
1774                         fstWriterEmitTimeChange(fstfile, d.first);
1775                         for (auto &data : d.second)
1776                         {
1777                                 if (!use_signal.at(data.first)) continue;
1778                                 Const value = data.second;
1779                                 std::stringstream ss;
1780                                 for (int i = GetSize(value)-1; i >= 0; i--) {
1781                                         switch (value[i]) {
1782                                                 case State::S0: ss << "0"; break;
1783                                                 case State::S1: ss << "1"; break;
1784                                                 case State::Sx: ss << "x"; break;
1785                                                 default: ss << "z";
1786                                         }
1787                                 }
1788                                 fstWriterEmitValueChange(fstfile, mapping[data.first], ss.str().c_str());
1789                         }
1790                 }
1791         }
1792
1793         struct fstContext *fstfile = nullptr;
1794         std::map<int,fstHandle> mapping;
1795 };
1796
1797 struct AIWWriter : public OutputWriter
1798 {
1799         AIWWriter(SimWorker *worker, std::string filename) : OutputWriter(worker) {
1800                 aiwfile.open(filename.c_str());
1801         }
1802
1803         virtual ~AIWWriter()
1804         {
1805                 aiwfile << '.' << '\n';
1806         }
1807
1808         void write(std::map<int, bool> &) override
1809         {
1810                 if (!aiwfile.is_open()) return;
1811                 if (worker->map_filename.empty())
1812                         log_cmd_error("For AIGER witness file map parameter is mandatory.\n");
1813
1814                 std::ifstream mf(worker->map_filename);
1815                 std::string type, symbol;
1816                 int variable, index;
1817                 int max_input = 0;
1818                 if (mf.fail())
1819                         log_cmd_error("Not able to read AIGER witness map file.\n");
1820                 while (mf >> type >> variable >> index >> symbol) {
1821                         RTLIL::IdString escaped_s = RTLIL::escape_id(symbol);
1822                         Wire *w = worker->top->module->wire(escaped_s);
1823                         if (!w)
1824                                 log_error("Wire %s not present in module %s\n",log_id(escaped_s),log_id(worker->top->module));
1825                         if (index < w->start_offset || index > w->start_offset + w->width)
1826                                 log_error("Index %d for wire %s is out of range\n", index, log_signal(w));
1827                         if (type == "input") {
1828                                 aiw_inputs[variable] = SigBit(w,index-w->start_offset);
1829                                 if (worker->clock.count(escaped_s)) {
1830                                         clocks[variable] = true;
1831                                 }
1832                                 if (worker->clockn.count(escaped_s)) {
1833                                         clocks[variable] = false;
1834                                 }
1835                                 max_input = max(max_input,variable);
1836                         } else if (type == "init") {
1837                                 aiw_inits[variable] = SigBit(w,index-w->start_offset);
1838                                 max_input = max(max_input,variable);
1839                         } else if (type == "latch") {
1840                                 aiw_latches[variable] = {SigBit(w,index-w->start_offset), false};
1841                         } else if (type == "invlatch") {
1842                                 aiw_latches[variable] = {SigBit(w,index-w->start_offset), true};
1843                         }
1844                 }
1845
1846                 worker->top->write_output_header(
1847                         [](IdString) {},
1848                         []() {},
1849                         [this](Wire *wire, int id, bool) { mapping[wire] = id; }
1850                 );
1851
1852                 std::map<int, Yosys::RTLIL::Const> current;
1853                 bool first = true;
1854                 for (auto iter = worker->output_data.begin(); iter != std::prev(worker->output_data.end()); ++iter)
1855                 {
1856                         auto& d = *iter;
1857                         for (auto &data : d.second)
1858                         {
1859                                 current[data.first] = data.second;
1860                         }
1861                         if (first) {
1862                                 for (int i = 0;; i++)
1863                                 {
1864                                         if (aiw_latches.count(i)) {
1865                                                 aiwfile << '0';
1866                                                 continue;
1867                                         }
1868                                         aiwfile << '\n';
1869                                         break;
1870                                 }
1871                                 first = false;
1872                         }
1873
1874                         bool skip = false;
1875                         for (auto it : clocks)
1876                         {
1877                                 auto val = it.second ? State::S1 : State::S0;
1878                                 SigBit bit = aiw_inputs.at(it.first);
1879                                 auto v = current[mapping[bit.wire]].bits.at(bit.offset);
1880                                 if (v == val)
1881                                         skip = true;
1882                         }
1883                         if (skip)
1884                                 continue;
1885                         for (int i = 0; i <= max_input; i++)
1886                         {
1887                                 if (aiw_inputs.count(i)) {
1888                                         SigBit bit = aiw_inputs.at(i);
1889                                         auto v = current[mapping[bit.wire]].bits.at(bit.offset);
1890                                         if (v == State::S1)
1891                                                 aiwfile << '1';
1892                                         else
1893                                                 aiwfile << '0';
1894                                         continue;
1895                                 }
1896                                 if (aiw_inits.count(i)) {
1897                                         SigBit bit = aiw_inits.at(i);
1898                                         auto v = current[mapping[bit.wire]].bits.at(bit.offset);
1899                                         if (v == State::S1)
1900                                                 aiwfile << '1';
1901                                         else
1902                                                 aiwfile << '0';
1903                                         continue;
1904                                 }
1905                                 aiwfile << '0';
1906                         }
1907                         aiwfile << '\n';
1908                 }
1909         }
1910
1911         std::ofstream aiwfile;
1912         dict<int, std::pair<SigBit, bool>> aiw_latches;
1913         dict<int, SigBit> aiw_inputs, aiw_inits;
1914         dict<int, bool> clocks;
1915         std::map<Wire*,int> mapping;
1916 };
1917
1918 struct SimPass : public Pass {
1919         SimPass() : Pass("sim", "simulate the circuit") { }
1920         void help() override
1921         {
1922                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1923                 log("\n");
1924                 log("    sim [options] [top-level]\n");
1925                 log("\n");
1926                 log("This command simulates the circuit using the given top-level module.\n");
1927                 log("\n");
1928                 log("    -vcd <filename>\n");
1929                 log("        write the simulation results to the given VCD file\n");
1930                 log("\n");
1931                 log("    -fst <filename>\n");
1932                 log("        write the simulation results to the given FST file\n");
1933                 log("\n");
1934                 log("    -aiw <filename>\n");
1935                 log("        write the simulation results to an AIGER witness file\n");
1936                 log("        (requires a *.aim file via -map)\n");
1937                 log("\n");
1938                 log("    -x\n");
1939                 log("        ignore constant x outputs in simulation file.\n");
1940                 log("\n");
1941                 log("    -date\n");
1942                 log("        include date and full version info in output.\n");
1943                 log("\n");
1944                 log("    -clock <portname>\n");
1945                 log("        name of top-level clock input\n");
1946                 log("\n");
1947                 log("    -clockn <portname>\n");
1948                 log("        name of top-level clock input (inverse polarity)\n");
1949                 log("\n");
1950                 log("    -multiclock\n");
1951                 log("        mark that witness file is multiclock.\n");
1952                 log("\n");
1953                 log("    -reset <portname>\n");
1954                 log("        name of top-level reset input (active high)\n");
1955                 log("\n");
1956                 log("    -resetn <portname>\n");
1957                 log("        name of top-level inverted reset input (active low)\n");
1958                 log("\n");
1959                 log("    -rstlen <integer>\n");
1960                 log("        number of cycles reset should stay active (default: 1)\n");
1961                 log("\n");
1962                 log("    -zinit\n");
1963                 log("        zero-initialize all uninitialized regs and memories\n");
1964                 log("\n");
1965                 log("    -timescale <string>\n");
1966                 log("        include the specified timescale declaration in the vcd\n");
1967                 log("\n");
1968                 log("    -n <integer>\n");
1969                 log("        number of clock cycles to simulate (default: 20)\n");
1970                 log("\n");
1971                 log("    -a\n");
1972                 log("        use all nets in VCD/FST operations, not just those with public names\n");
1973                 log("\n");
1974                 log("    -w\n");
1975                 log("        writeback mode: use final simulation state as new init state\n");
1976                 log("\n");
1977                 log("    -r\n");
1978                 log("        read simulation results file (file formats supported: FST, VCD, AIW and WIT)\n");
1979                 log("            VCD support requires vcd2fst external tool to be present\n");
1980                 log("\n");
1981                 log("    -map <filename>\n");
1982                 log("        read file with port and latch symbols, needed for AIGER witness input\n");
1983                 log("\n");
1984                 log("    -scope <name>\n");
1985                 log("        scope of simulation top model\n");
1986                 log("\n");
1987                 log("    -at <time>\n");
1988                 log("        sets start and stop time\n");
1989                 log("\n");
1990                 log("    -start <time>\n");
1991                 log("        start co-simulation in arbitary time (default 0)\n");
1992                 log("\n");
1993                 log("    -stop <time>\n");
1994                 log("        stop co-simulation in arbitary time (default END)\n");
1995                 log("\n");
1996                 log("    -sim\n");
1997                 log("        simulation with stimulus from FST (default)\n");
1998                 log("\n");
1999                 log("    -sim-cmp\n");
2000                 log("        co-simulation expect exact match\n");
2001                 log("\n");
2002                 log("    -sim-gold\n");
2003                 log("        co-simulation, x in simulation can match any value in FST\n");
2004                 log("\n");
2005                 log("    -sim-gate\n");
2006                 log("        co-simulation, x in FST can match any value in simulation\n");
2007                 log("\n");
2008                 log("    -q\n");
2009                 log("        disable per-cycle/sample log message\n");
2010                 log("\n");
2011                 log("    -d\n");
2012                 log("        enable debug output\n");
2013                 log("\n");
2014         }
2015
2016
2017         static std::string file_base_name(std::string const & path)
2018         {
2019                 return path.substr(path.find_last_of("/\\") + 1);
2020         }
2021
2022         void execute(std::vector<std::string> args, RTLIL::Design *design) override
2023         {
2024                 SimWorker worker;
2025                 int numcycles = 20;
2026                 bool start_set = false, stop_set = false, at_set = false;
2027
2028                 log_header(design, "Executing SIM pass (simulate the circuit).\n");
2029
2030                 size_t argidx;
2031                 for (argidx = 1; argidx < args.size(); argidx++) {
2032                         if (args[argidx] == "-vcd" && argidx+1 < args.size()) {
2033                                 std::string vcd_filename = args[++argidx];
2034                                 rewrite_filename(vcd_filename);
2035                                 worker.outputfiles.emplace_back(std::unique_ptr<VCDWriter>(new VCDWriter(&worker, vcd_filename.c_str())));
2036                                 continue;
2037                         }
2038                         if (args[argidx] == "-fst" && argidx+1 < args.size()) {
2039                                 std::string fst_filename = args[++argidx];
2040                                 rewrite_filename(fst_filename);
2041                                 worker.outputfiles.emplace_back(std::unique_ptr<FSTWriter>(new FSTWriter(&worker, fst_filename.c_str())));
2042                                 continue;
2043                         }
2044                         if (args[argidx] == "-aiw" && argidx+1 < args.size()) {
2045                                 std::string aiw_filename = args[++argidx];
2046                                 rewrite_filename(aiw_filename);
2047                                 worker.outputfiles.emplace_back(std::unique_ptr<AIWWriter>(new AIWWriter(&worker, aiw_filename.c_str())));
2048                                 continue;
2049                         }
2050                         if (args[argidx] == "-n" && argidx+1 < args.size()) {
2051                                 numcycles = atoi(args[++argidx].c_str());
2052                                 worker.cycles_set = true;
2053                                 continue;
2054                         }
2055                         if (args[argidx] == "-rstlen" && argidx+1 < args.size()) {
2056                                 worker.rstlen = atoi(args[++argidx].c_str());
2057                                 continue;
2058                         }
2059                         if (args[argidx] == "-clock" && argidx+1 < args.size()) {
2060                                 worker.clock.insert(RTLIL::escape_id(args[++argidx]));
2061                                 continue;
2062                         }
2063                         if (args[argidx] == "-clockn" && argidx+1 < args.size()) {
2064                                 worker.clockn.insert(RTLIL::escape_id(args[++argidx]));
2065                                 continue;
2066                         }
2067                         if (args[argidx] == "-reset" && argidx+1 < args.size()) {
2068                                 worker.reset.insert(RTLIL::escape_id(args[++argidx]));
2069                                 continue;
2070                         }
2071                         if (args[argidx] == "-resetn" && argidx+1 < args.size()) {
2072                                 worker.resetn.insert(RTLIL::escape_id(args[++argidx]));
2073                                 continue;
2074                         }
2075                         if (args[argidx] == "-timescale" && argidx+1 < args.size()) {
2076                                 worker.timescale = args[++argidx];
2077                                 continue;
2078                         }
2079                         if (args[argidx] == "-a") {
2080                                 worker.hide_internal = false;
2081                                 continue;
2082                         }
2083                         if (args[argidx] == "-q") {
2084                                 worker.verbose = false;
2085                                 continue;
2086                         }
2087                         if (args[argidx] == "-d") {
2088                                 worker.debug = true;
2089                                 continue;
2090                         }
2091                         if (args[argidx] == "-w") {
2092                                 worker.writeback = true;
2093                                 continue;
2094                         }
2095                         if (args[argidx] == "-zinit") {
2096                                 worker.zinit = true;
2097                                 continue;
2098                         }
2099                         if (args[argidx] == "-r" && argidx+1 < args.size()) {
2100                                 std::string sim_filename = args[++argidx];
2101                                 rewrite_filename(sim_filename);
2102                                 worker.sim_filename = sim_filename;
2103                                 continue;
2104                         }
2105                         if (args[argidx] == "-map" && argidx+1 < args.size()) {
2106                                 std::string map_filename = args[++argidx];
2107                                 rewrite_filename(map_filename);
2108                                 worker.map_filename = map_filename;
2109                                 continue;
2110                         }
2111                         if (args[argidx] == "-scope" && argidx+1 < args.size()) {
2112                                 worker.scope = args[++argidx];
2113                                 continue;
2114                         }
2115                         if (args[argidx] == "-start" && argidx+1 < args.size()) {
2116                                 worker.start_time = stringToTime(args[++argidx]);
2117                                 start_set = true;
2118                                 continue;
2119                         }
2120                         if (args[argidx] == "-stop" && argidx+1 < args.size()) {
2121                                 worker.stop_time = stringToTime(args[++argidx]);
2122                                 stop_set = true;
2123                                 continue;
2124                         }
2125                         if (args[argidx] == "-at" && argidx+1 < args.size()) {
2126                                 worker.start_time = stringToTime(args[++argidx]);
2127                                 worker.stop_time = worker.start_time;
2128                                 at_set = true;
2129                                 continue;
2130                         }
2131                         if (args[argidx] == "-sim") {
2132                                 worker.sim_mode = SimulationMode::sim;
2133                                 continue;
2134                         }
2135                         if (args[argidx] == "-sim-cmp") {
2136                                 worker.sim_mode = SimulationMode::cmp;
2137                                 continue;
2138                         }
2139                         if (args[argidx] == "-sim-gold") {
2140                                 worker.sim_mode = SimulationMode::gold;
2141                                 continue;
2142                         }
2143                         if (args[argidx] == "-sim-gate") {
2144                                 worker.sim_mode = SimulationMode::gate;
2145                                 continue;
2146                         }
2147                         if (args[argidx] == "-x") {
2148                                 worker.ignore_x = true;
2149                                 continue;
2150                         }
2151                         if (args[argidx] == "-date") {
2152                                 worker.date = true;
2153                                 continue;
2154                         }
2155                         if (args[argidx] == "-multiclock") {
2156                                 worker.multiclock = true;
2157                                 continue;
2158                         }
2159                         break;
2160                 }
2161                 extra_args(args, argidx, design);
2162                 if (at_set && (start_set || stop_set || worker.cycles_set))
2163                         log_error("'at' option can only be defined separate of 'start','stop' and 'n'\n");
2164                 if (stop_set && worker.cycles_set)
2165                         log_error("'stop' and 'n' can only be used exclusively'\n");
2166
2167                 Module *top_mod = nullptr;
2168
2169                 if (design->full_selection()) {
2170                         top_mod = design->top_module();
2171
2172                         if (!top_mod)
2173                                 log_cmd_error("Design has no top module, use the 'hierarchy' command to specify one.\n");
2174                 } else {
2175                         auto mods = design->selected_whole_modules();
2176                         if (GetSize(mods) != 1)
2177                                 log_cmd_error("Only one top module must be selected.\n");
2178                         top_mod = mods.front();
2179                 }
2180
2181                 if (worker.sim_filename.empty())
2182                         worker.run(top_mod, numcycles);
2183                 else {
2184                         std::string filename_trim = file_base_name(worker.sim_filename);
2185                         if (filename_trim.size() > 4 && ((filename_trim.compare(filename_trim.size()-4, std::string::npos, ".fst") == 0) ||
2186                                 filename_trim.compare(filename_trim.size()-4, std::string::npos, ".vcd") == 0)) {
2187                                 worker.run_cosim_fst(top_mod, numcycles);
2188                         } else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".aiw") == 0) {
2189                                 if (worker.map_filename.empty())
2190                                         log_cmd_error("For AIGER witness file map parameter is mandatory.\n");
2191                                 worker.run_cosim_aiger_witness(top_mod);
2192                         } else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".wit") == 0) {
2193                                 worker.run_cosim_btor2_witness(top_mod);
2194                         } else {
2195                                 log_cmd_error("Unhandled extension for simulation input file `%s`.\n", worker.sim_filename.c_str());
2196                         }
2197                 }
2198         }
2199 } SimPass;
2200
2201 struct Fst2TbPass : public Pass {
2202         Fst2TbPass() : Pass("fst2tb", "generate testbench out of fst file") { }
2203         void help() override
2204         {
2205                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
2206                 log("\n");
2207                 log("    fst2tb [options] [top-level]\n");
2208                 log("\n");
2209                 log("This command generates testbench for the circuit using the given top-level module\n");
2210                 log("and simulus signal from FST file\n");
2211                 log("\n");
2212                 log("    -tb <name>\n");
2213                 log("        generated testbench name.\n");
2214                 log("        files <name>.v and <name>.txt are created as result.\n");
2215                 log("\n");
2216                 log("    -r <filename>\n");
2217                 log("        read simulation FST file\n");
2218                 log("\n");
2219                 log("    -clock <portname>\n");
2220                 log("        name of top-level clock input\n");
2221                 log("\n");
2222                 log("    -clockn <portname>\n");
2223                 log("        name of top-level clock input (inverse polarity)\n");
2224                 log("\n");
2225                 log("    -scope <name>\n");
2226                 log("        scope of simulation top model\n");
2227                 log("\n");
2228                 log("    -start <time>\n");
2229                 log("        start co-simulation in arbitary time (default 0)\n");
2230                 log("\n");
2231                 log("    -stop <time>\n");
2232                 log("        stop co-simulation in arbitary time (default END)\n");
2233                 log("\n");
2234                 log("    -n <integer>\n");
2235                 log("        number of clock cycles to simulate (default: 20)\n");
2236                 log("\n");
2237         }
2238
2239         void execute(std::vector<std::string> args, RTLIL::Design *design) override
2240         {
2241                 SimWorker worker;
2242                 int numcycles = 20;
2243                 bool stop_set = false;
2244                 std::string tb_filename;
2245
2246                 log_header(design, "Executing FST2FB pass.\n");
2247
2248                 size_t argidx;
2249                 for (argidx = 1; argidx < args.size(); argidx++) {
2250                         if (args[argidx] == "-clock" && argidx+1 < args.size()) {
2251                                 worker.clock.insert(RTLIL::escape_id(args[++argidx]));
2252                                 continue;
2253                         }
2254                         if (args[argidx] == "-clockn" && argidx+1 < args.size()) {
2255                                 worker.clockn.insert(RTLIL::escape_id(args[++argidx]));
2256                                 continue;
2257                         }
2258                         if (args[argidx] == "-r" && argidx+1 < args.size()) {
2259                                 std::string sim_filename = args[++argidx];
2260                                 rewrite_filename(sim_filename);
2261                                 worker.sim_filename = sim_filename;
2262                                 continue;
2263                         }
2264                         if (args[argidx] == "-n" && argidx+1 < args.size()) {
2265                                 numcycles = atoi(args[++argidx].c_str());
2266                                 worker.cycles_set = true;
2267                                 continue;
2268                         }
2269                         if (args[argidx] == "-scope" && argidx+1 < args.size()) {
2270                                 worker.scope = args[++argidx];
2271                                 continue;
2272                         }
2273                         if (args[argidx] == "-start" && argidx+1 < args.size()) {
2274                                 worker.start_time = stringToTime(args[++argidx]);
2275                                 continue;
2276                         }
2277                         if (args[argidx] == "-stop" && argidx+1 < args.size()) {
2278                                 worker.stop_time = stringToTime(args[++argidx]);
2279                                 stop_set = true;
2280                                 continue;
2281                         }
2282                         if (args[argidx] == "-tb" && argidx+1 < args.size()) {
2283                                 tb_filename = args[++argidx];
2284                                 continue;
2285                         }
2286                         break;
2287                 }
2288                 extra_args(args, argidx, design);
2289                 if (stop_set && worker.cycles_set)
2290                         log_error("'stop' and 'n' can only be used exclusively'\n");
2291
2292                 Module *top_mod = nullptr;
2293
2294                 if (design->full_selection()) {
2295                         top_mod = design->top_module();
2296
2297                         if (!top_mod)
2298                                 log_cmd_error("Design has no top module, use the 'hierarchy' command to specify one.\n");
2299                 } else {
2300                         auto mods = design->selected_whole_modules();
2301                         if (GetSize(mods) != 1)
2302                                 log_cmd_error("Only one top module must be selected.\n");
2303                         top_mod = mods.front();
2304                 }
2305
2306                 if (tb_filename.empty())
2307                         log_cmd_error("Testbench name must be defined.\n");
2308
2309                 if (worker.sim_filename.empty())
2310                         log_cmd_error("Stimulus FST file must be defined.\n");
2311
2312                 worker.generate_tb(top_mod, tb_filename, numcycles);
2313         }
2314 } Fst2TbPass;
2315
2316 PRIVATE_NAMESPACE_END