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 hide_internal = true;
  81         bool writeback = false;
  82         bool zinit = false;
  83         int rstlen = 1;
  84         FstData *fst = nullptr;
  85         double start_time = 0;
  86         double stop_time = -1;
  87         SimulationMode sim_mode = SimulationMode::sim;
  88         bool cycles_set = false;
  89         std::vector<std::unique_ptr<OutputWriter>> outputfiles;
  90         std::vector<std::pair<int,std::map<int,Const>>> output_data;
  91         bool ignore_x = false;
  92         bool date = false;
  93 };
  94
  95 void zinit(State &v)
  96 {
  97         if (v != State::S1)
  98                 v = State::S0;
  99 }
 100
 101 void zinit(Const &v)
 102 {
 103         for (auto &bit : v.bits)
 104                 zinit(bit);
 105 }
 106
 107 struct SimInstance
 108 {
 109         SimShared *shared;
 110
 111         std::string scope;
 112         Module *module;
 113         Cell *instance;
 114
 115         SimInstance *parent;
 116         dict<Cell*, SimInstance*> children;
 117
 118         SigMap sigmap;
 119         dict<SigBit, State> state_nets;
 120         dict<SigBit, pool<Cell*>> upd_cells;
 121         dict<SigBit, pool<Wire*>> upd_outports;
 122
 123         pool<SigBit> dirty_bits;
 124         pool<Cell*> dirty_cells;
 125         pool<IdString> dirty_memories;
 126         pool<SimInstance*, hash_ptr_ops> dirty_children;
 127
 128         struct ff_state_t
 129         {
 130                 Const past_d;
 131                 Const past_ad;
 132                 State past_clk;
 133                 State past_ce;
 134                 State past_srst;
 135
 136                 FfData data;
 137         };
 138
 139         struct mem_state_t
 140         {
 141                 Mem *mem;
 142                 std::vector<Const> past_wr_clk;
 143                 std::vector<Const> past_wr_en;
 144                 std::vector<Const> past_wr_addr;
 145                 std::vector<Const> past_wr_data;
 146                 Const data;
 147         };
 148
 149         dict<Cell*, ff_state_t> ff_database;
 150         dict<IdString, mem_state_t> mem_database;
 151         pool<Cell*> formal_database;
 152         dict<Cell*, IdString> mem_cells;
 153
 154         std::vector<Mem> memories;
 155
 156         dict<Wire*, pair<int, Const>> signal_database;
 157         dict<Wire*, fstHandle> fst_handles;
 158
 159         SimInstance(SimShared *shared, std::string scope, Module *module, Cell *instance = nullptr, SimInstance *parent = nullptr) :
 160                         shared(shared), scope(scope), module(module), instance(instance), parent(parent), sigmap(module)
 161         {
 162                 log_assert(module);
 163
 164                 if (parent) {
 165                         log_assert(parent->children.count(instance) == 0);
 166                         parent->children[instance] = this;
 167                 }
 168
 169                 for (auto wire : module->wires())
 170                 {
 171                         SigSpec sig = sigmap(wire);
 172
 173                         for (int i = 0; i < GetSize(sig); i++) {
 174                                 if (state_nets.count(sig[i]) == 0)
 175                                         state_nets[sig[i]] = State::Sx;
 176                                 if (wire->port_output) {
 177                                         upd_outports[sig[i]].insert(wire);
 178                                         dirty_bits.insert(sig[i]);
 179                                 }
 180                         }
 181
 182                         if ((shared->fst) && !(shared->hide_internal && wire->name[0] == '$')) {
 183                                 fstHandle id = shared->fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name));
 184                                 if (id==0 && wire->name.isPublic())
 185                                         log_warning("Unable to found wire %s in input file.\n", (scope + "." + RTLIL::unescape_id(wire->name)).c_str());
 186                                 fst_handles[wire] = id;
 187                         }
 188
 189                         if (wire->attributes.count(ID::init)) {
 190                                 Const initval = wire->attributes.at(ID::init);
 191                                 for (int i = 0; i < GetSize(sig) && i < GetSize(initval); i++)
 192                                         if (initval[i] == State::S0 || initval[i] == State::S1) {
 193                                                 state_nets[sig[i]] = initval[i];
 194                                                 dirty_bits.insert(sig[i]);
 195                                         }
 196                         }
 197                 }
 198
 199                 memories = Mem::get_all_memories(module);
 200                 for (auto &mem : memories) {
 201                         auto &mdb = mem_database[mem.memid];
 202                         mdb.mem = &mem;
 203                         for (auto &port : mem.wr_ports) {
 204                                 mdb.past_wr_clk.push_back(Const(State::Sx));
 205                                 mdb.past_wr_en.push_back(Const(State::Sx, GetSize(port.en)));
 206                                 mdb.past_wr_addr.push_back(Const(State::Sx, GetSize(port.addr)));
 207                                 mdb.past_wr_data.push_back(Const(State::Sx, GetSize(port.data)));
 208                         }
 209                         mdb.data = mem.get_init_data();
 210                 }
 211
 212                 for (auto cell : module->cells())
 213                 {
 214                         Module *mod = module->design->module(cell->type);
 215
 216                         if (mod != nullptr) {
 217                                 dirty_children.insert(new SimInstance(shared, scope + "." + RTLIL::unescape_id(cell->name), mod, cell, this));
 218                         }
 219
 220                         for (auto &port : cell->connections()) {
 221                                 if (cell->input(port.first))
 222                                         for (auto bit : sigmap(port.second)) {
 223                                                 upd_cells[bit].insert(cell);
 224                                                 // Make sure cell inputs connected to constants are updated in the first cycle
 225                                                 if (bit.wire == nullptr)
 226                                                         dirty_bits.insert(bit);
 227                                         }
 228                         }
 229
 230                         if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
 231                                 FfData ff_data(nullptr, cell);
 232                                 ff_state_t ff;
 233                                 ff.past_d = Const(State::Sx, ff_data.width);
 234                                 ff.past_ad = Const(State::Sx, ff_data.width);
 235                                 ff.past_clk = State::Sx;
 236                                 ff.past_ce = State::Sx;
 237                                 ff.past_srst = State::Sx;
 238                                 ff.data = ff_data;
 239                                 ff_database[cell] = ff;
 240                         }
 241
 242                         if (cell->is_mem_cell())
 243                         {
 244                                 mem_cells[cell] = cell->parameters.at(ID::MEMID).decode_string();
 245                         }
 246                         if (cell->type.in(ID($assert), ID($cover), ID($assume))) {
 247                                 formal_database.insert(cell);
 248                         }
 249                 }
 250
 251                 if (shared->zinit)
 252                 {
 253                         for (auto &it : ff_database)
 254                         {
 255                                 ff_state_t &ff = it.second;
 256                                 zinit(ff.past_d);
 257
 258                                 SigSpec qsig = it.second.data.sig_q;
 259                                 Const qdata = get_state(qsig);
 260                                 zinit(qdata);
 261                                 set_state(qsig, qdata);
 262                         }
 263
 264                         for (auto &it : mem_database) {
 265                                 mem_state_t &mem = it.second;
 266                                 for (auto &val : mem.past_wr_en)
 267                                         zinit(val);
 268                                 zinit(mem.data);
 269                         }
 270                 }
 271         }
 272
 273         ~SimInstance()
 274         {
 275                 for (auto child : children)
 276                         delete child.second;
 277         }
 278
 279         IdString name() const
 280         {
 281                 if (instance != nullptr)
 282                         return instance->name;
 283                 return module->name;
 284         }
 285
 286         std::string hiername() const
 287         {
 288                 if (instance != nullptr)
 289                         return parent->hiername() + "." + log_id(instance->name);
 290
 291                 return log_id(module->name);
 292         }
 293
 294         Const get_state(SigSpec sig)
 295         {
 296                 Const value;
 297
 298                 for (auto bit : sigmap(sig))
 299                         if (bit.wire == nullptr)
 300                                 value.bits.push_back(bit.data);
 301                         else if (state_nets.count(bit))
 302                                 value.bits.push_back(state_nets.at(bit));
 303                         else
 304                                 value.bits.push_back(State::Sz);
 305
 306                 if (shared->debug)
 307                         log("[%s] get %s: %s\n", hiername().c_str(), log_signal(sig), log_signal(value));
 308                 return value;
 309         }
 310
 311         bool set_state(SigSpec sig, Const value)
 312         {
 313                 bool did_something = false;
 314
 315                 sig = sigmap(sig);
 316                 log_assert(GetSize(sig) <= GetSize(value));
 317
 318                 for (int i = 0; i < GetSize(sig); i++)
 319                         if (state_nets.at(sig[i]) != value[i]) {
 320                                 state_nets.at(sig[i]) = value[i];
 321                                 dirty_bits.insert(sig[i]);
 322                                 did_something = true;
 323                         }
 324
 325                 if (shared->debug)
 326                         log("[%s] set %s: %s\n", hiername().c_str(), log_signal(sig), log_signal(value));
 327                 return did_something;
 328         }
 329
 330         void set_memory_state(IdString memid, Const addr, Const data)
 331         {
 332                 auto &state = mem_database[memid];
 333
 334                 int offset = (addr.as_int() - state.mem->start_offset) * state.mem->width;
 335                 for (int i = 0; i < GetSize(data); i++)
 336                         if (0 <= i+offset && i+offset < GetSize(data))
 337                                 state.data.bits[i+offset] = data.bits[i];
 338         }
 339
 340         void update_cell(Cell *cell)
 341         {
 342                 if (ff_database.count(cell))
 343                         return;
 344
 345                 if (formal_database.count(cell))
 346                         return;
 347
 348                 if (mem_cells.count(cell))
 349                 {
 350                         dirty_memories.insert(mem_cells[cell]);
 351                         return;
 352                 }
 353
 354                 if (children.count(cell))
 355                 {
 356                         auto child = children.at(cell);
 357                         for (auto &conn: cell->connections())
 358                                 if (cell->input(conn.first) && GetSize(conn.second)) {
 359                                         Const value = get_state(conn.second);
 360                                         child->set_state(child->module->wire(conn.first), value);
 361                                 }
 362                         dirty_children.insert(child);
 363                         return;
 364                 }
 365
 366                 if (yosys_celltypes.cell_evaluable(cell->type))
 367                 {
 368                         RTLIL::SigSpec sig_a, sig_b, sig_c, sig_d, sig_s, sig_y;
 369                         bool has_a, has_b, has_c, has_d, has_s, has_y;
 370
 371                         has_a = cell->hasPort(ID::A);
 372                         has_b = cell->hasPort(ID::B);
 373                         has_c = cell->hasPort(ID::C);
 374                         has_d = cell->hasPort(ID::D);
 375                         has_s = cell->hasPort(ID::S);
 376                         has_y = cell->hasPort(ID::Y);
 377
 378                         if (has_a) sig_a = cell->getPort(ID::A);
 379                         if (has_b) sig_b = cell->getPort(ID::B);
 380                         if (has_c) sig_c = cell->getPort(ID::C);
 381                         if (has_d) sig_d = cell->getPort(ID::D);
 382                         if (has_s) sig_s = cell->getPort(ID::S);
 383                         if (has_y) sig_y = cell->getPort(ID::Y);
 384
 385                         if (shared->debug)
 386                                 log("[%s] eval %s (%s)\n", hiername().c_str(), log_id(cell), log_id(cell->type));
 387
 388                         // Simple (A -> Y) and (A,B -> Y) cells
 389                         if (has_a && !has_c && !has_d && !has_s && has_y) {
 390                                 set_state(sig_y, CellTypes::eval(cell, get_state(sig_a), get_state(sig_b)));
 391                                 return;
 392                         }
 393
 394                         // (A,B,C -> Y) cells
 395                         if (has_a && has_b && has_c && !has_d && !has_s && has_y) {
 396                                 set_state(sig_y, CellTypes::eval(cell, get_state(sig_a), get_state(sig_b), get_state(sig_c)));
 397                                 return;
 398                         }
 399
 400                         // (A,S -> Y) cells
 401                         if (has_a && !has_b && !has_c && !has_d && has_s && has_y) {
 402                                 set_state(sig_y, CellTypes::eval(cell, get_state(sig_a), get_state(sig_s)));
 403                                 return;
 404                         }
 405
 406                         // (A,B,S -> Y) cells
 407                         if (has_a && has_b && !has_c && !has_d && has_s && has_y) {
 408                                 set_state(sig_y, CellTypes::eval(cell, get_state(sig_a), get_state(sig_b), get_state(sig_s)));
 409                                 return;
 410                         }
 411
 412                         log_warning("Unsupported evaluable cell type: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
 413                         return;
 414                 }
 415
 416                 log_error("Unsupported cell type: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
 417         }
 418
 419         void update_memory(IdString id) {
 420                 auto &mdb = mem_database[id];
 421                 auto &mem = *mdb.mem;
 422
 423                 for (int port_idx = 0; port_idx < GetSize(mem.rd_ports); port_idx++)
 424                 {
 425                         auto &port = mem.rd_ports[port_idx];
 426                         Const addr = get_state(port.addr);
 427                         Const data = Const(State::Sx, mem.width << port.wide_log2);
 428
 429                         if (port.clk_enable)
 430                                 log_error("Memory %s.%s has clocked read ports. Run 'memory' with -nordff.\n", log_id(module), log_id(mem.memid));
 431
 432                         if (addr.is_fully_def()) {
 433                                 int index = addr.as_int() - mem.start_offset;
 434                                 if (index >= 0 && index < mem.size)
 435                                         data = mdb.data.extract(index*mem.width, mem.width << port.wide_log2);
 436                         }
 437
 438                         set_state(port.data, data);
 439                 }
 440         }
 441
 442         void update_ph1()
 443         {
 444                 pool<Cell*> queue_cells;
 445                 pool<Wire*> queue_outports;
 446
 447                 queue_cells.swap(dirty_cells);
 448
 449                 while (1)
 450                 {
 451                         for (auto bit : dirty_bits)
 452                         {
 453                                 if (upd_cells.count(bit))
 454                                         for (auto cell : upd_cells.at(bit))
 455                                                 queue_cells.insert(cell);
 456
 457                                 if (upd_outports.count(bit) && parent != nullptr)
 458                                         for (auto wire : upd_outports.at(bit))
 459                                                 queue_outports.insert(wire);
 460                         }
 461
 462                         dirty_bits.clear();
 463
 464                         if (!queue_cells.empty())
 465                         {
 466                                 for (auto cell : queue_cells)
 467                                         update_cell(cell);
 468
 469                                 queue_cells.clear();
 470                                 continue;
 471                         }
 472
 473                         for (auto &memid : dirty_memories)
 474                                 update_memory(memid);
 475                         dirty_memories.clear();
 476
 477                         for (auto wire : queue_outports)
 478                                 if (instance->hasPort(wire->name)) {
 479                                         Const value = get_state(wire);
 480                                         parent->set_state(instance->getPort(wire->name), value);
 481                                 }
 482
 483                         queue_outports.clear();
 484
 485                         for (auto child : dirty_children)
 486                                 child->update_ph1();
 487
 488                         dirty_children.clear();
 489
 490                         if (dirty_bits.empty())
 491                                 break;
 492                 }
 493         }
 494
 495         bool update_ph2()
 496         {
 497                 bool did_something = false;
 498
 499                 for (auto &it : ff_database)
 500                 {
 501                         ff_state_t &ff = it.second;
 502                         FfData &ff_data = ff.data;
 503
 504                         Const current_q = get_state(ff.data.sig_q);
 505
 506                         if (ff_data.has_clk) {
 507                                 // flip-flops
 508                                 State current_clk = get_state(ff_data.sig_clk)[0];
 509                                 if (ff_data.pol_clk ? (ff.past_clk == State::S0 && current_clk != State::S0) :
 510                                                         (ff.past_clk == State::S1 && current_clk != State::S1)) {
 511                                         bool ce = ff.past_ce == (ff_data.pol_ce ? State::S1 : State::S0);
 512                                         // set if no ce, or ce is enabled
 513                                         if (!ff_data.has_ce || (ff_data.has_ce && ce)) {
 514                                                 current_q = ff.past_d;
 515                                         }
 516                                         // override if sync reset
 517                                         if ((ff_data.has_srst) && (ff.past_srst == (ff_data.pol_srst ? State::S1 : State::S0)) &&
 518                                                 ((!ff_data.ce_over_srst) || (ff_data.ce_over_srst && ce))) {
 519                                                 current_q = ff_data.val_srst;
 520                                         }
 521                                 }
 522                         }
 523                         // async load
 524                         if (ff_data.has_aload) {
 525                                 State current_aload = get_state(ff_data.sig_aload)[0];
 526                                 if (current_aload == (ff_data.pol_aload ? State::S1 : State::S0)) {
 527                                         current_q = ff_data.has_clk ? ff.past_ad : get_state(ff.data.sig_ad);
 528                                 }
 529                         }
 530                         // async reset
 531                         if (ff_data.has_arst) {
 532                                 State current_arst = get_state(ff_data.sig_arst)[0];
 533                                 if (current_arst == (ff_data.pol_arst ? State::S1 : State::S0)) {
 534                                         current_q = ff_data.val_arst;
 535                                 }
 536                         }
 537                         // handle set/reset
 538                         if (ff.data.has_sr) {
 539                                 Const current_clr = get_state(ff.data.sig_clr);
 540                                 Const current_set = get_state(ff.data.sig_set);
 541
 542                                 for(int i=0;i<ff.past_d.size();i++) {
 543                                         if (current_clr[i] == (ff_data.pol_clr ? State::S1 : State::S0)) {
 544                                                 current_q[i] = State::S0;
 545                                         }
 546                                         else if (current_set[i] == (ff_data.pol_set ? State::S1 : State::S0)) {
 547                                                 current_q[i] = State::S1;
 548                                         }
 549                                 }
 550                         }
 551                         if (ff_data.has_gclk) {
 552                                 // $ff
 553                                 current_q = ff.past_d;
 554                         }
 555                         if (set_state(ff_data.sig_q, current_q))
 556                                 did_something = true;
 557                 }
 558
 559                 for (auto &it : mem_database)
 560                 {
 561                         mem_state_t &mdb = it.second;
 562                         auto &mem = *mdb.mem;
 563
 564                         for (int port_idx = 0; port_idx < GetSize(mem.wr_ports); port_idx++)
 565                         {
 566                                 auto &port = mem.wr_ports[port_idx];
 567                                 Const addr, data, enable;
 568
 569                                 if (!port.clk_enable)
 570                                 {
 571                                         addr = get_state(port.addr);
 572                                         data = get_state(port.data);
 573                                         enable = get_state(port.en);
 574                                 }
 575                                 else
 576                                 {
 577                                         if (port.clk_polarity ?
 578                                                         (mdb.past_wr_clk[port_idx] == State::S1 || get_state(port.clk) != State::S1) :
 579                                                         (mdb.past_wr_clk[port_idx] == State::S0 || get_state(port.clk) != State::S0))
 580                                                 continue;
 581
 582                                         addr = mdb.past_wr_addr[port_idx];
 583                                         data = mdb.past_wr_data[port_idx];
 584                                         enable = mdb.past_wr_en[port_idx];
 585                                 }
 586
 587                                 if (addr.is_fully_def())
 588                                 {
 589                                         int index = addr.as_int() - mem.start_offset;
 590                                         if (index >= 0 && index < mem.size)
 591                                                 for (int i = 0; i < (mem.width << port.wide_log2); i++)
 592                                                         if (enable[i] == State::S1 && mdb.data.bits.at(index*mem.width+i) != data[i]) {
 593                                                                 mdb.data.bits.at(index*mem.width+i) = data[i];
 594                                                                 dirty_memories.insert(mem.memid);
 595                                                                 did_something = true;
 596                                                         }
 597                                 }
 598                         }
 599                 }
 600
 601                 for (auto it : children)
 602                         if (it.second->update_ph2()) {
 603                                 dirty_children.insert(it.second);
 604                                 did_something = true;
 605                         }
 606
 607                 return did_something;
 608         }
 609
 610         void update_ph3()
 611         {
 612                 for (auto &it : ff_database)
 613                 {
 614                         ff_state_t &ff = it.second;
 615
 616                         if (ff.data.has_aload)
 617                                 ff.past_ad = get_state(ff.data.sig_ad);
 618
 619                         if (ff.data.has_clk || ff.data.has_gclk)
 620                                 ff.past_d = get_state(ff.data.sig_d);
 621
 622                         if (ff.data.has_clk)
 623                                 ff.past_clk = get_state(ff.data.sig_clk)[0];
 624
 625                         if (ff.data.has_ce)
 626                                 ff.past_ce = get_state(ff.data.sig_ce)[0];
 627
 628                         if (ff.data.has_srst)
 629                                 ff.past_srst = get_state(ff.data.sig_srst)[0];
 630                 }
 631
 632                 for (auto &it : mem_database)
 633                 {
 634                         mem_state_t &mem = it.second;
 635
 636                         for (int i = 0; i < GetSize(mem.mem->wr_ports); i++) {
 637                                 auto &port = mem.mem->wr_ports[i];
 638                                 mem.past_wr_clk[i]  = get_state(port.clk);
 639                                 mem.past_wr_en[i]   = get_state(port.en);
 640                                 mem.past_wr_addr[i] = get_state(port.addr);
 641                                 mem.past_wr_data[i] = get_state(port.data);
 642                         }
 643                 }
 644
 645                 for (auto cell : formal_database)
 646                 {
 647                         string label = log_id(cell);
 648                         if (cell->attributes.count(ID::src))
 649                                 label = cell->attributes.at(ID::src).decode_string();
 650
 651                         State a = get_state(cell->getPort(ID::A))[0];
 652                         State en = get_state(cell->getPort(ID::EN))[0];
 653
 654                         if (cell->type == ID($cover) && en == State::S1 && a != State::S1)
 655                                 log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str());
 656
 657                         if (cell->type == ID($assume) && en == State::S1 && a != State::S1)
 658                                 log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
 659
 660                         if (cell->type == ID($assert) && en == State::S1 && a != State::S1)
 661                                 log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
 662                 }
 663
 664                 for (auto it : children)
 665                         it.second->update_ph3();
 666         }
 667
 668         void writeback(pool<Module*> &wbmods)
 669         {
 670                 if (wbmods.count(module))
 671                         log_error("Instance %s of module %s is not unique: Writeback not possible. (Fix by running 'uniquify'.)\n", hiername().c_str(), log_id(module));
 672
 673                 wbmods.insert(module);
 674
 675                 for (auto wire : module->wires())
 676                         wire->attributes.erase(ID::init);
 677
 678                 for (auto &it : ff_database)
 679                 {
 680                         SigSpec sig_q = it.second.data.sig_q;
 681                         Const initval = get_state(sig_q);
 682
 683                         for (int i = 0; i < GetSize(sig_q); i++)
 684                         {
 685                                 Wire *w = sig_q[i].wire;
 686
 687                                 if (w->attributes.count(ID::init) == 0)
 688                                         w->attributes[ID::init] = Const(State::Sx, GetSize(w));
 689
 690                                 w->attributes[ID::init][sig_q[i].offset] = initval[i];
 691                         }
 692                 }
 693
 694                 for (auto &it : mem_database)
 695                 {
 696                         mem_state_t &mem = it.second;
 697                         mem.mem->clear_inits();
 698                         MemInit minit;
 699                         minit.addr = mem.mem->start_offset;
 700                         minit.data = mem.data;
 701                         minit.en = Const(State::S1, mem.mem->width);
 702                         mem.mem->inits.push_back(minit);
 703                         mem.mem->emit();
 704                 }
 705
 706                 for (auto it : children)
 707                         it.second->writeback(wbmods);
 708         }
 709
 710         void register_signals(int &id)
 711         {
 712                 for (auto wire : module->wires())
 713                 {
 714                         if (shared->hide_internal && wire->name[0] == '$')
 715                                 continue;
 716
 717                         signal_database[wire] = make_pair(id, Const());
 718                         id++;
 719                 }
 720
 721                 for (auto child : children)
 722                         child.second->register_signals(id);
 723         }
 724
 725         void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(Wire*, int)> register_signal)
 726         {
 727                 enter_scope(name());
 728
 729                 for (auto signal : signal_database)
 730                 {
 731                         register_signal(signal.first, signal.second.first);
 732                 }
 733
 734                 for (auto child : children)
 735                         child.second->write_output_header(enter_scope, exit_scope, register_signal);
 736
 737                 exit_scope();
 738         }
 739
 740         void register_output_step_values(std::map<int,Const> *data)
 741         {
 742                 for (auto &it : signal_database)
 743                 {
 744                         Wire *wire = it.first;
 745                         Const value = get_state(wire);
 746                         int id = it.second.first;
 747
 748                         if (it.second.second == value)
 749                                 continue;
 750
 751                         it.second.second = value;
 752                         data->emplace(id, value);
 753                 }
 754
 755                 for (auto child : children)
 756                         child.second->register_output_step_values(data);
 757         }
 758
 759         void setInitState()
 760         {
 761                 for (auto &it : ff_database)
 762                 {
 763                         SigSpec qsig = it.second.data.sig_q;
 764                         if (qsig.is_wire()) {
 765                                 IdString name = qsig.as_wire()->name;
 766                                 fstHandle id = shared->fst->getHandle(scope + "." + RTLIL::unescape_id(name));
 767                                 if (id==0 && name.isPublic())
 768                                         log_warning("Unable to found wire %s in input file.\n", (scope + "." + RTLIL::unescape_id(name)).c_str());
 769                                 if (id!=0) {
 770                                         Const fst_val = Const::from_string(shared->fst->valueOf(id));
 771                                         set_state(qsig, fst_val);
 772                                 }
 773                         }
 774                 }
 775                 for (auto child : children)
 776                         child.second->setInitState();
 777         }
 778
 779         void setState(dict<int, std::pair<SigBit,bool>> bits, std::string values)
 780         {
 781                 for(auto bit : bits) {
 782                         if (bit.first >= GetSize(values))
 783                                 log_error("Too few input data bits in file.\n");
 784                         switch(values.at(bit.first)) {
 785                                 case '0': set_state(bit.second.first, bit.second.second ? State::S1 : State::S0); break;
 786                                 case '1': set_state(bit.second.first, bit.second.second ? State::S0 : State::S1); break;
 787                                 default: set_state(bit.second.first, State::Sx); break;
 788                         }
 789                 }
 790         }
 791
 792         bool checkSignals()
 793         {
 794                 bool retVal = false;
 795                 for(auto &item : fst_handles) {
 796                         if (item.second==0) continue; // Ignore signals not found
 797                         Const fst_val = Const::from_string(shared->fst->valueOf(item.second));
 798                         Const sim_val = get_state(item.first);
 799                         if (sim_val.size()!=fst_val.size())
 800                                 log_error("Signal '%s' size is different in gold and gate.\n", log_id(item.first));
 801                         if (shared->sim_mode == SimulationMode::sim) {
 802                                 // No checks performed when using stimulus
 803                         } else if (shared->sim_mode == SimulationMode::gate && !fst_val.is_fully_def()) { // FST data contains X
 804                                 for(int i=0;i<fst_val.size();i++) {
 805                                         if (fst_val[i]!=State::Sx && fst_val[i]!=sim_val[i]) {
 806                                                 log_warning("Signal '%s' in file %s in simulation %s\n", log_id(item.first), log_signal(fst_val), log_signal(sim_val));
 807                                                 retVal = true;
 808                                                 break;
 809                                         }
 810                                 }
 811                         } else if (shared->sim_mode == SimulationMode::gold && !sim_val.is_fully_def()) { // sim data contains X
 812                                 for(int i=0;i<sim_val.size();i++) {
 813                                         if (sim_val[i]!=State::Sx && fst_val[i]!=sim_val[i]) {
 814                                                 log_warning("Signal '%s' in file %s in simulation %s\n", log_id(item.first), log_signal(fst_val), log_signal(sim_val));
 815                                                 retVal = true;
 816                                                 break;
 817                                         }
 818                                 }
 819                         } else {
 820                                 if (fst_val!=sim_val) {
 821                                         log_warning("Signal '%s' in file %s in simulation '%s'\n", log_id(item.first), log_signal(fst_val), log_signal(sim_val));
 822                                         retVal = true;
 823                                 }
 824                         }
 825                 }
 826                 for (auto child : children)
 827                         retVal |= child.second->checkSignals();
 828                 return retVal;
 829         }
 830 };
 831
 832 struct SimWorker : SimShared
 833 {
 834         SimInstance *top = nullptr;
 835         pool<IdString> clock, clockn, reset, resetn;
 836         std::string timescale;
 837         std::string sim_filename;
 838         std::string map_filename;
 839         std::string scope;
 840
 841         ~SimWorker()
 842         {
 843                 outputfiles.clear();
 844                 delete top;
 845         }
 846
 847         void register_signals()
 848         {
 849                 int id = 1;
 850                 top->register_signals(id);
 851         }
 852
 853         void register_output_step(int t)
 854         {
 855                 std::map<int,Const> data;
 856                 top->register_output_step_values(&data);
 857                 output_data.emplace_back(t, data);
 858         }
 859
 860         void write_output_files()
 861         {
 862                 std::map<int, bool> use_signal;
 863                 bool first = ignore_x;
 864                 for(auto& d : output_data)
 865                 {
 866                         if (first) {
 867                                 for (auto &data : d.second)
 868                                         use_signal[data.first] = !data.second.is_fully_undef();
 869                                 first = false;
 870                         } else {
 871                                 for (auto &data : d.second)
 872                                         use_signal[data.first] = true;
 873                         }
 874                         if (!ignore_x) break;
 875                 }
 876                 for(auto& writer : outputfiles)
 877                         writer->write(use_signal);
 878         }
 879
 880         void update()
 881         {
 882                 while (1)
 883                 {
 884                         if (debug)
 885                                 log("\n-- ph1 --\n");
 886
 887                         top->update_ph1();
 888
 889                         if (debug)
 890                                 log("\n-- ph2 --\n");
 891
 892                         if (!top->update_ph2())
 893                                 break;
 894                 }
 895
 896                 if (debug)
 897                         log("\n-- ph3 --\n");
 898
 899                 top->update_ph3();
 900         }
 901
 902         void set_inports(pool<IdString> ports, State value)
 903         {
 904                 for (auto portname : ports)
 905                 {
 906                         Wire *w = top->module->wire(portname);
 907
 908                         if (w == nullptr)
 909                                 log_error("Can't find port %s on module %s.\n", log_id(portname), log_id(top->module));
 910
 911                         top->set_state(w, value);
 912                 }
 913         }
 914
 915         void run(Module *topmod, int numcycles)
 916         {
 917                 log_assert(top == nullptr);
 918                 top = new SimInstance(this, scope, topmod);
 919                 register_signals();
 920
 921                 if (debug)
 922                         log("\n===== 0 =====\n");
 923                 else
 924                         log("Simulating cycle 0.\n");
 925
 926                 set_inports(reset, State::S1);
 927                 set_inports(resetn, State::S0);
 928
 929                 set_inports(clock, State::Sx);
 930                 set_inports(clockn, State::Sx);
 931
 932                 update();
 933
 934                 register_output_step(0);
 935
 936                 for (int cycle = 0; cycle < numcycles; cycle++)
 937                 {
 938                         if (debug)
 939                                 log("\n===== %d =====\n", 10*cycle + 5);
 940                         else
 941                                 log("Simulating cycle %d.\n", (cycle*2)+1);
 942                         set_inports(clock, State::S0);
 943                         set_inports(clockn, State::S1);
 944
 945                         update();
 946                         register_output_step(10*cycle + 5);
 947
 948                         if (debug)
 949                                 log("\n===== %d =====\n", 10*cycle + 10);
 950                         else
 951                                 log("Simulating cycle %d.\n", (cycle*2)+2);
 952
 953                         set_inports(clock, State::S1);
 954                         set_inports(clockn, State::S0);
 955
 956                         if (cycle+1 == rstlen) {
 957                                 set_inports(reset, State::S0);
 958                                 set_inports(resetn, State::S1);
 959                         }
 960
 961                         update();
 962                         register_output_step(10*cycle + 10);
 963                 }
 964
 965                 register_output_step(10*numcycles + 2);
 966
 967                 write_output_files();
 968
 969                 if (writeback) {
 970                         pool<Module*> wbmods;
 971                         top->writeback(wbmods);
 972                 }
 973         }
 974
 975         void run_cosim_fst(Module *topmod, int numcycles)
 976         {
 977                 log_assert(top == nullptr);
 978                 fst = new FstData(sim_filename);
 979
 980                 if (scope.empty())
 981                         log_error("Scope must be defined for co-simulation.\n");
 982
 983                 top = new SimInstance(this, scope, topmod);
 984                 register_signals();
 985
 986                 std::vector<fstHandle> fst_clock;
 987
 988                 for (auto portname : clock)
 989                 {
 990                         Wire *w = topmod->wire(portname);
 991                         if (!w)
 992                                 log_error("Can't find port %s on module %s.\n", log_id(portname), log_id(top->module));
 993                         if (!w->port_input)
 994                                 log_error("Clock port %s on module %s is not input.\n", log_id(portname), log_id(top->module));
 995                         fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(portname));
 996                         if (id==0)
 997                                 log_error("Can't find port %s.%s in FST.\n", scope.c_str(), log_id(portname));
 998                         fst_clock.push_back(id);
 999                 }
1000                 for (auto portname : clockn)
1001                 {
1002                         Wire *w = topmod->wire(portname);
1003                         if (!w)
1004                                 log_error("Can't find port %s on module %s.\n", log_id(portname), log_id(top->module));
1005                         if (!w->port_input)
1006                                 log_error("Clock port %s on module %s is not input.\n", log_id(portname), log_id(top->module));
1007                         fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(portname));
1008                         if (id==0)
1009                                 log_error("Can't find port %s.%s in FST.\n", scope.c_str(), log_id(portname));
1010                         fst_clock.push_back(id);
1011                 }
1012
1013                 SigMap sigmap(topmod);
1014                 std::map<Wire*,fstHandle> inputs;
1015
1016                 for (auto wire : topmod->wires()) {
1017                         if (wire->port_input) {
1018                                 fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name));
1019                                 if (id==0)
1020                                         log_error("Unable to find required '%s' signal in file\n",(scope + "." + RTLIL::unescape_id(wire->name)).c_str());
1021                                 inputs[wire] = id;
1022                         }
1023                 }
1024
1025                 uint64_t startCount = 0;
1026                 uint64_t stopCount = 0;
1027                 if (start_time==0) {
1028                         if (start_time < fst->getStartTime())
1029                                 log_warning("Start time is before simulation file start time\n");
1030                         startCount = fst->getStartTime();
1031                 } else if (start_time==-1)
1032                         startCount = fst->getEndTime();
1033                 else {
1034                         startCount = start_time / fst->getTimescale();
1035                         if (startCount > fst->getEndTime()) {
1036                                 startCount = fst->getEndTime();
1037                                 log_warning("Start time is after simulation file end time\n");
1038                         }
1039                 }
1040                 if (stop_time==0) {
1041                         if (stop_time < fst->getStartTime())
1042                                 log_warning("Stop time is before simulation file start time\n");
1043                         stopCount = fst->getStartTime();
1044                 } else if (stop_time==-1)
1045                         stopCount = fst->getEndTime();
1046                 else {
1047                         stopCount = stop_time / fst->getTimescale();
1048                         if (stopCount > fst->getEndTime()) {
1049                                 stopCount = fst->getEndTime();
1050                                 log_warning("Stop time is after simulation file end time\n");
1051                         }
1052                 }
1053                 if (stopCount<startCount) {
1054                         log_error("Stop time is before start time\n");
1055                 }
1056
1057                 bool initial = true;
1058                 int cycle = 0;
1059                 log("Co-simulation from %lu%s to %lu%s", (unsigned long)startCount, fst->getTimescaleString(), (unsigned long)stopCount, fst->getTimescaleString());
1060                 if (cycles_set)
1061                         log(" for %d clock cycle(s)",numcycles);
1062                 log("\n");
1063                 bool all_samples = fst_clock.empty();
1064
1065                 try {
1066                         fst->reconstructAllAtTimes(fst_clock, startCount, stopCount, [&](uint64_t time) {
1067                                 log("Co-simulating %s %d [%lu%s].\n", (all_samples ? "sample" : "cycle"), cycle, (unsigned long)time, fst->getTimescaleString());
1068                                 bool did_something = false;
1069                                 for(auto &item : inputs) {
1070                                         std::string v = fst->valueOf(item.second);
1071                                         did_something |= top->set_state(item.first, Const::from_string(v));
1072                                 }
1073
1074                                 if (initial) {
1075                                         top->setInitState();
1076                                         initial = false;
1077                                 }
1078                                 if (did_something)
1079                                         update();
1080                                 register_output_step(time);
1081
1082                                 bool status = top->checkSignals();
1083                                 if (status)
1084                                         log_error("Signal difference\n");
1085                                 cycle++;
1086
1087                                 // Limit to number of cycles if provided
1088                                 if (cycles_set && cycle > numcycles *2)
1089                                         throw fst_end_of_data_exception();
1090                                 if (time==stopCount)
1091                                         throw fst_end_of_data_exception();
1092                         });
1093                 } catch(fst_end_of_data_exception) {
1094                         // end of data detected
1095                 }
1096
1097                 write_output_files();
1098
1099                 if (writeback) {
1100                         pool<Module*> wbmods;
1101                         top->writeback(wbmods);
1102                 }
1103                 delete fst;
1104         }
1105
1106         void run_cosim_aiger_witness(Module *topmod)
1107         {
1108                 log_assert(top == nullptr);
1109                 if ((clock.size()+clockn.size())==0)
1110                         log_error("Clock signal must be specified.\n");
1111                 std::ifstream mf(map_filename);
1112                 std::string type, symbol;
1113                 int variable, index;
1114                 dict<int, std::pair<SigBit,bool>> inputs, inits, latches;
1115                 if (mf.fail())
1116                         log_cmd_error("Not able to read AIGER witness map file.\n");
1117                 while (mf >> type >> variable >> index >> symbol) {
1118                         RTLIL::IdString escaped_s = RTLIL::escape_id(symbol);
1119                         Wire *w = topmod->wire(escaped_s);
1120                         if (!w)
1121                                 log_error("Wire %s not present in module %s\n",log_signal(w),log_id(topmod));
1122                         if (index < w->start_offset || index > w->start_offset + w->width)
1123                                 log_error("Index %d for wire %s is out of range\n", index, log_signal(w));
1124                         if (type == "input") {
1125                                 inputs[variable] = {SigBit(w,index), false};
1126                         } else if (type == "init") {
1127                                 inits[variable] = {SigBit(w,index), false};
1128                         } else if (type == "latch") {
1129                                 latches[variable] = {SigBit(w,index), false};
1130                         } else if (type == "invlatch") {
1131                                 latches[variable] = {SigBit(w,index), true};
1132                         }
1133                 }
1134
1135                 std::ifstream f;
1136                 f.open(sim_filename.c_str());
1137                 if (f.fail() || GetSize(sim_filename) == 0)
1138                         log_error("Can not open file `%s`\n", sim_filename.c_str());
1139
1140                 int state = 0;
1141                 std::string status;
1142                 int cycle = 0;
1143                 top = new SimInstance(this, scope, topmod);
1144                 register_signals();
1145
1146                 while (!f.eof())
1147                 {
1148                         std::string line;
1149                         std::getline(f, line);
1150                         if (line.size()==0 || line[0]=='#') continue;
1151                         if (line[0]=='.') break;
1152                         if (state==0 && line.size()!=1) {
1153                                 // old format detected, latch data
1154                                 state = 2;
1155                         }
1156                         if (state==1 && line[0]!='b' && line[0]!='c') {
1157                                 // was old format but with 1 bit latch
1158                                 top->setState(latches, status);
1159                                 state = 3;
1160                         }
1161
1162                         switch(state)
1163                         {
1164                                 case 0:
1165                                         status = line;
1166                                         state = 1;
1167                                         break;
1168                                 case 1:
1169                                         state = 2;
1170                                         break;
1171                                 case 2:
1172                                         top->setState(latches, line);
1173                                         state = 3;
1174                                         break;
1175                                 default:
1176                                         log("Simulating cycle %d.\n", cycle);
1177                                         top->setState(inputs, line);
1178                                         if (cycle) {
1179                                                 set_inports(clock, State::S1);
1180                                                 set_inports(clockn, State::S0);
1181                                         } else {
1182                                                 top->setState(inits, line);
1183                                                 set_inports(clock, State::S0);
1184                                                 set_inports(clockn, State::S1);
1185                                         }
1186                                         update();
1187                                         register_output_step(10*cycle);
1188                                         if (cycle) {
1189                                                 set_inports(clock, State::S0);
1190                                                 set_inports(clockn, State::S1);
1191                                                 update();
1192                                                 register_output_step(10*cycle + 5);
1193                                         }
1194                                         cycle++;
1195                                         break;
1196                         }
1197                 }
1198                 register_output_step(10*cycle);
1199                 write_output_files();
1200         }
1201
1202         std::vector<std::string> split(std::string text, const char *delim)
1203         {
1204                 std::vector<std::string> list;
1205                 char *p = strdup(text.c_str());
1206                 char *t = strtok(p, delim);
1207                 while (t != NULL) {
1208                         list.push_back(t);
1209                         t = strtok(NULL, delim);
1210                 }
1211                 free(p);
1212                 return list;
1213         }
1214
1215         std::string signal_name(std::string const & name)
1216         {
1217                 size_t pos = name.find_first_of("@");
1218                 if (pos==std::string::npos) {
1219                         pos = name.find_first_of("#");
1220                         if (pos==std::string::npos)
1221                                 log_error("Line does not contain proper signal name `%s`\n", name.c_str());
1222                 }
1223                 return name.substr(0, pos);
1224         }
1225
1226         void run_cosim_btor2_witness(Module *topmod)
1227         {
1228                 log_assert(top == nullptr);
1229                 if ((clock.size()+clockn.size())==0)
1230                         log_error("Clock signal must be specified.\n");
1231                 std::ifstream f;
1232                 f.open(sim_filename.c_str());
1233                 if (f.fail() || GetSize(sim_filename) == 0)
1234                         log_error("Can not open file `%s`\n", sim_filename.c_str());
1235
1236                 int state = 0;
1237                 int cycle = 0;
1238                 top = new SimInstance(this, scope, topmod);
1239                 register_signals();
1240                 int prev_cycle = 0;
1241                 int curr_cycle = 0;
1242                 std::vector<std::string> parts;
1243                 size_t len = 0;
1244                 while (!f.eof())
1245                 {
1246                         std::string line;
1247                         std::getline(f, line);
1248                         if (line.size()==0) continue;
1249
1250                         if (line[0]=='#' || line[0]=='@' || line[0]=='.') {
1251                                 if (line[0]!='.')
1252                                         curr_cycle = atoi(line.c_str()+1);
1253                                 else
1254                                         curr_cycle = -1; // force detect change
1255
1256                                 if (curr_cycle != prev_cycle) {
1257                                         log("Simulating cycle %d.\n", cycle);
1258                                         set_inports(clock, State::S1);
1259                                         set_inports(clockn, State::S0);
1260                                         update();
1261                                         register_output_step(10*cycle+0);
1262                                         set_inports(clock, State::S0);
1263                                         set_inports(clockn, State::S1);
1264                                         update();
1265                                         register_output_step(10*cycle+5);
1266                                         cycle++;
1267                                         prev_cycle = curr_cycle;
1268                                 }
1269                                 if (line[0]=='.') break;
1270                                 continue;
1271                         }
1272
1273                         switch(state)
1274                         {
1275                                 case 0:
1276                                         if (line=="sat")
1277                                                 state = 1;
1278                                         break;
1279                                 case 1:
1280                                         if (line[0]=='b' || line[0]=='j')
1281                                                 state = 2;
1282                                         else
1283                                                 log_error("Line does not contain property.\n");
1284                                         break;
1285                                 default: // set state or inputs
1286                                         parts = split(line, " ");
1287                                         len = parts.size();
1288                                         if (len<3 || len>4)
1289                                                 log_error("Invalid set state line content.\n");
1290
1291                                         RTLIL::IdString escaped_s = RTLIL::escape_id(signal_name(parts[len-1]));
1292                                         if (len==3) {
1293                                                 Wire *w = topmod->wire(escaped_s);
1294                                                 if (!w) {
1295                                                         Cell *c = topmod->cell(escaped_s);
1296                                                         if (!c)
1297                                                                 log_warning("Wire/cell %s not present in module %s\n",log_id(escaped_s),log_id(topmod));
1298                                                         else if (c->type.in(ID($anyconst), ID($anyseq))) {
1299                                                                 SigSpec sig_y= c->getPort(ID::Y);
1300                                                                 if ((int)parts[1].size() != GetSize(sig_y))
1301                                                                         log_error("Size of wire %s is different than provided data.\n", log_signal(sig_y));
1302                                                                 top->set_state(sig_y, Const::from_string(parts[1]));
1303                                                         }
1304                                                 } else {
1305                                                         if ((int)parts[1].size() != w->width)
1306                                                                 log_error("Size of wire %s is different than provided data.\n", log_signal(w));
1307                                                         top->set_state(w, Const::from_string(parts[1]));
1308                                                 }
1309                                         } else {
1310                                                 Cell *c = topmod->cell(escaped_s);
1311                                                 if (!c)
1312                                                         log_error("Cell %s not present in module %s\n",log_id(escaped_s),log_id(topmod));
1313                                                 if (!c->is_mem_cell())
1314                                                         log_error("Cell %s is not memory cell in module %s\n",log_id(escaped_s),log_id(topmod));
1315
1316                                                 Const addr = Const::from_string(parts[1].substr(1,parts[1].size()-2));
1317                                                 Const data = Const::from_string(parts[2]);
1318                                                 top->set_memory_state(c->parameters.at(ID::MEMID).decode_string(), addr, data);
1319                                         }
1320                                         break;
1321                         }
1322                 }
1323                 register_output_step(10*cycle);
1324                 write_output_files();
1325         }
1326 };
1327
1328 struct VCDWriter : public OutputWriter
1329 {
1330         VCDWriter(SimWorker *worker, std::string filename) : OutputWriter(worker) {
1331                 vcdfile.open(filename.c_str());
1332         }
1333
1334         void write(std::map<int, bool> &use_signal) override
1335         {
1336                 if (!vcdfile.is_open()) return;
1337                 vcdfile << stringf("$version %s $end\n", worker->date ? yosys_version_str : "Yosys");
1338
1339                 if (worker->date) {
1340                         std::time_t t = std::time(nullptr);
1341                         char mbstr[255];
1342                         if (std::strftime(mbstr, sizeof(mbstr), "%c", std::localtime(&t))) {
1343                                 vcdfile << stringf("$date ") << mbstr << stringf(" $end\n");
1344                         }
1345                 }
1346
1347                 if (!worker->timescale.empty())
1348                         vcdfile << stringf("$timescale %s $end\n", worker->timescale.c_str());
1349
1350                 worker->top->write_output_header(
1351                         [this](IdString name) { vcdfile << stringf("$scope module %s $end\n", log_id(name)); },
1352                         [this]() { vcdfile << stringf("$upscope $end\n");},
1353                         [this,use_signal](Wire *wire, int id) { if (use_signal.at(id)) vcdfile << stringf("$var wire %d n%d %s%s $end\n", GetSize(wire), id, wire->name[0] == '$' ? "\\" : "", log_id(wire)); }
1354                 );
1355
1356                 vcdfile << stringf("$enddefinitions $end\n");
1357
1358                 for(auto& d : worker->output_data)
1359                 {
1360                         vcdfile << stringf("#%d\n", d.first);
1361                         for (auto &data : d.second)
1362                         {
1363                                 if (!use_signal.at(data.first)) continue;
1364                                 Const value = data.second;
1365                                 vcdfile << "b";
1366                                 for (int i = GetSize(value)-1; i >= 0; i--) {
1367                                         switch (value[i]) {
1368                                                 case State::S0: vcdfile << "0"; break;
1369                                                 case State::S1: vcdfile << "1"; break;
1370                                                 case State::Sx: vcdfile << "x"; break;
1371                                                 default: vcdfile << "z";
1372                                         }
1373                                 }
1374                                 vcdfile << stringf(" n%d\n", data.first);
1375                         }
1376                 }
1377         }
1378
1379         std::ofstream vcdfile;
1380 };
1381
1382 struct FSTWriter : public OutputWriter
1383 {
1384         FSTWriter(SimWorker *worker, std::string filename) : OutputWriter(worker) {
1385                 fstfile = (struct fstContext *)fstWriterCreate(filename.c_str(),1);
1386         }
1387
1388         virtual ~FSTWriter()
1389         {
1390                 fstWriterClose(fstfile);
1391         }
1392
1393         void write(std::map<int, bool> &use_signal) override
1394         {
1395                 if (!fstfile) return;
1396                 std::time_t t = std::time(nullptr);
1397                 fstWriterSetVersion(fstfile, worker->date ? yosys_version_str : "Yosys");
1398                 if (worker->date)
1399                         fstWriterSetDate(fstfile, asctime(std::localtime(&t)));
1400                 else
1401                         fstWriterSetDate(fstfile, "");
1402                 if (!worker->timescale.empty())
1403                         fstWriterSetTimescaleFromString(fstfile, worker->timescale.c_str());
1404
1405                 fstWriterSetPackType(fstfile, FST_WR_PT_FASTLZ);
1406                 fstWriterSetRepackOnClose(fstfile, 1);
1407
1408                 worker->top->write_output_header(
1409                         [this](IdString name) { fstWriterSetScope(fstfile, FST_ST_VCD_MODULE, stringf("%s",log_id(name)).c_str(), nullptr); },
1410                         [this]() { fstWriterSetUpscope(fstfile); },
1411                         [this,use_signal](Wire *wire, int id) {
1412                                 if (!use_signal.at(id)) return;
1413                                 fstHandle fst_id = fstWriterCreateVar(fstfile, FST_VT_VCD_WIRE, FST_VD_IMPLICIT, GetSize(wire),
1414                                                                                                 stringf("%s%s", wire->name[0] == '$' ? "\\" : "", log_id(wire)).c_str(), 0);
1415
1416                                 mapping.emplace(id, fst_id);
1417                         }
1418                 );
1419
1420                 for(auto& d : worker->output_data)
1421                 {
1422                         fstWriterEmitTimeChange(fstfile, d.first);
1423                         for (auto &data : d.second)
1424                         {
1425                                 if (!use_signal.at(data.first)) continue;
1426                                 Const value = data.second;
1427                                 std::stringstream ss;
1428                                 for (int i = GetSize(value)-1; i >= 0; i--) {
1429                                         switch (value[i]) {
1430                                                 case State::S0: ss << "0"; break;
1431                                                 case State::S1: ss << "1"; break;
1432                                                 case State::Sx: ss << "x"; break;
1433                                                 default: ss << "z";
1434                                         }
1435                                 }
1436                                 fstWriterEmitValueChange(fstfile, mapping[data.first], ss.str().c_str());
1437                         }
1438                 }
1439         }
1440
1441         struct fstContext *fstfile = nullptr;
1442         std::map<int,fstHandle> mapping;
1443 };
1444
1445 struct AIWWriter : public OutputWriter
1446 {
1447         AIWWriter(SimWorker *worker, std::string filename) : OutputWriter(worker) {
1448                 aiwfile.open(filename.c_str());
1449         }
1450
1451         virtual ~AIWWriter()
1452         {
1453                 aiwfile << '.' << '\n';
1454         }
1455
1456         void write(std::map<int, bool> &) override
1457         {
1458                 if (!aiwfile.is_open()) return;
1459                 if (worker->map_filename.empty())
1460                         log_cmd_error("For AIGER witness file map parameter is mandatory.\n");
1461
1462                 std::ifstream mf(worker->map_filename);
1463                 std::string type, symbol;
1464                 int variable, index;
1465                 if (mf.fail())
1466                         log_cmd_error("Not able to read AIGER witness map file.\n");
1467                 while (mf >> type >> variable >> index >> symbol) {
1468                         RTLIL::IdString escaped_s = RTLIL::escape_id(symbol);
1469                         Wire *w = worker->top->module->wire(escaped_s);
1470                         if (!w)
1471                                 log_error("Wire %s not present in module %s\n",log_id(escaped_s),log_id(worker->top->module));
1472                         if (index < w->start_offset || index > w->start_offset + w->width)
1473                                 log_error("Index %d for wire %s is out of range\n", index, log_signal(w));
1474                         if (type == "input") {
1475                                 aiw_inputs[variable] = SigBit(w,index);
1476                         } else if (type == "init") {
1477                                 aiw_inits[variable] = SigBit(w,index);
1478                         } else if (type == "latch") {
1479                                 aiw_latches[variable] = {SigBit(w,index), false};
1480                         } else if (type == "invlatch") {
1481                                 aiw_latches[variable] = {SigBit(w,index), true};
1482                         }
1483                 }
1484
1485                 worker->top->write_output_header(
1486                         [](IdString) {},
1487                         []() {},
1488                         [this](Wire *wire, int id) { mapping[wire] = id; }
1489                 );
1490
1491                 std::map<int, Yosys::RTLIL::Const> current;
1492                 bool first = true;
1493                 for(auto& d : worker->output_data)
1494                 {
1495                         for (auto &data : d.second)
1496                         {
1497                                 current[data.first] = data.second;
1498                         }
1499                         if (first) {
1500                                 for (int i = 0;; i++)
1501                                 {
1502                                         if (aiw_latches.count(i)) {
1503                                                 SigBit bit = aiw_latches.at(i).first;
1504                                                 auto v = current[mapping[bit.wire]].bits.at(bit.offset);
1505                                                 if (v == State::S1)
1506                                                         aiwfile << (aiw_latches.at(i).second ? '0' : '1');
1507                                                 else
1508                                                         aiwfile << (aiw_latches.at(i).second ? '1' : '0');
1509                                                 continue;
1510                                         }
1511                                         aiwfile << '\n';
1512                                         break;
1513                                 }
1514                                 first = false;
1515                         }
1516
1517                         for (int i = 0;; i++)
1518                         {
1519                                 if (aiw_inputs.count(i)) {
1520                                         SigBit bit = aiw_inputs.at(i);
1521                                         auto v = current[mapping[bit.wire]].bits.at(bit.offset);
1522                                         if (v == State::S1)
1523                                                 aiwfile << '1';
1524                                         else
1525                                                 aiwfile << '0';
1526                                         continue;
1527                                 }
1528                                 if (aiw_inits.count(i)) {
1529                                         SigBit bit = aiw_inits.at(i);
1530                                         auto v = current[mapping[bit.wire]].bits.at(bit.offset);
1531                                         if (v == State::S1)
1532                                                 aiwfile << '1';
1533                                         else
1534                                                 aiwfile << '0';
1535                                         continue;
1536                                 }
1537                                 aiwfile << '\n';
1538                                 break;
1539                         }
1540                 }
1541         }
1542
1543         std::ofstream aiwfile;
1544         dict<int, std::pair<SigBit, bool>> aiw_latches;
1545         dict<int, SigBit> aiw_inputs, aiw_inits;
1546         std::map<Wire*,int> mapping;
1547 };
1548
1549 struct SimPass : public Pass {
1550         SimPass() : Pass("sim", "simulate the circuit") { }
1551         void help() override
1552         {
1553                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1554                 log("\n");
1555                 log("    sim [options] [top-level]\n");
1556                 log("\n");
1557                 log("This command simulates the circuit using the given top-level module.\n");
1558                 log("\n");
1559                 log("    -vcd <filename>\n");
1560                 log("        write the simulation results to the given VCD file\n");
1561                 log("\n");
1562                 log("    -fst <filename>\n");
1563                 log("        write the simulation results to the given FST file\n");
1564                 log("\n");
1565                 log("    -aiw <filename>\n");
1566                 log("        write the simulation results to an AIGER witness file\n");
1567                 log("        (requires a *.aim file via -map)\n");
1568                 log("\n");
1569                 log("    -x\n");
1570                 log("        ignore constant x outputs in simulation file.\n");
1571                 log("\n");
1572                 log("    -date\n");
1573                 log("        include date and full version info in output.\n");
1574                 log("\n");
1575                 log("    -clock <portname>\n");
1576                 log("        name of top-level clock input\n");
1577                 log("\n");
1578                 log("    -clockn <portname>\n");
1579                 log("        name of top-level clock input (inverse polarity)\n");
1580                 log("\n");
1581                 log("    -reset <portname>\n");
1582                 log("        name of top-level reset input (active high)\n");
1583                 log("\n");
1584                 log("    -resetn <portname>\n");
1585                 log("        name of top-level inverted reset input (active low)\n");
1586                 log("\n");
1587                 log("    -rstlen <integer>\n");
1588                 log("        number of cycles reset should stay active (default: 1)\n");
1589                 log("\n");
1590                 log("    -zinit\n");
1591                 log("        zero-initialize all uninitialized regs and memories\n");
1592                 log("\n");
1593                 log("    -timescale <string>\n");
1594                 log("        include the specified timescale declaration in the vcd\n");
1595                 log("\n");
1596                 log("    -n <integer>\n");
1597                 log("        number of clock cycles to simulate (default: 20)\n");
1598                 log("\n");
1599                 log("    -a\n");
1600                 log("        use all nets in VCD/FST operations, not just those with public names\n");
1601                 log("\n");
1602                 log("    -w\n");
1603                 log("        writeback mode: use final simulation state as new init state\n");
1604                 log("\n");
1605                 log("    -r\n");
1606                 log("        read simulation results file (file formats supported: FST)\n");
1607                 log("\n");
1608                 log("    -map <filename>\n");
1609                 log("        read file with port and latch symbols, needed for AIGER witness input\n");
1610                 log("\n");
1611                 log("    -scope <name>\n");
1612                 log("        scope of simulation top model\n");
1613                 log("\n");
1614                 log("    -at <time>\n");
1615                 log("        sets start and stop time\n");
1616                 log("\n");
1617                 log("    -start <time>\n");
1618                 log("        start co-simulation in arbitary time (default 0)\n");
1619                 log("\n");
1620                 log("    -stop <time>\n");
1621                 log("        stop co-simulation in arbitary time (default END)\n");
1622                 log("\n");
1623                 log("    -sim\n");
1624                 log("        simulation with stimulus from FST (default)\n");
1625                 log("\n");
1626                 log("    -sim-cmp\n");
1627                 log("        co-simulation expect exact match\n");
1628                 log("\n");
1629                 log("    -sim-gold\n");
1630                 log("        co-simulation, x in simulation can match any value in FST\n");
1631                 log("\n");
1632                 log("    -sim-gate\n");
1633                 log("        co-simulation, x in FST can match any value in simulation\n");
1634                 log("\n");
1635                 log("    -d\n");
1636                 log("        enable debug output\n");
1637                 log("\n");
1638         }
1639
1640
1641         static std::string file_base_name(std::string const & path)
1642         {
1643                 return path.substr(path.find_last_of("/\\") + 1);
1644         }
1645
1646         void execute(std::vector<std::string> args, RTLIL::Design *design) override
1647         {
1648                 SimWorker worker;
1649                 int numcycles = 20;
1650                 bool start_set = false, stop_set = false, at_set = false;
1651
1652                 log_header(design, "Executing SIM pass (simulate the circuit).\n");
1653
1654                 size_t argidx;
1655                 for (argidx = 1; argidx < args.size(); argidx++) {
1656                         if (args[argidx] == "-vcd" && argidx+1 < args.size()) {
1657                                 std::string vcd_filename = args[++argidx];
1658                                 rewrite_filename(vcd_filename);
1659                                 worker.outputfiles.emplace_back(std::unique_ptr<VCDWriter>(new VCDWriter(&worker, vcd_filename.c_str())));
1660                                 continue;
1661                         }
1662                         if (args[argidx] == "-fst" && argidx+1 < args.size()) {
1663                                 std::string fst_filename = args[++argidx];
1664                                 rewrite_filename(fst_filename);
1665                                 worker.outputfiles.emplace_back(std::unique_ptr<FSTWriter>(new FSTWriter(&worker, fst_filename.c_str())));
1666                                 continue;
1667                         }
1668                         if (args[argidx] == "-aiw" && argidx+1 < args.size()) {
1669                                 std::string aiw_filename = args[++argidx];
1670                                 rewrite_filename(aiw_filename);
1671                                 worker.outputfiles.emplace_back(std::unique_ptr<AIWWriter>(new AIWWriter(&worker, aiw_filename.c_str())));
1672                                 continue;
1673                         }
1674                         if (args[argidx] == "-n" && argidx+1 < args.size()) {
1675                                 numcycles = atoi(args[++argidx].c_str());
1676                                 worker.cycles_set = true;
1677                                 continue;
1678                         }
1679                         if (args[argidx] == "-rstlen" && argidx+1 < args.size()) {
1680                                 worker.rstlen = atoi(args[++argidx].c_str());
1681                                 continue;
1682                         }
1683                         if (args[argidx] == "-clock" && argidx+1 < args.size()) {
1684                                 worker.clock.insert(RTLIL::escape_id(args[++argidx]));
1685                                 continue;
1686                         }
1687                         if (args[argidx] == "-clockn" && argidx+1 < args.size()) {
1688                                 worker.clockn.insert(RTLIL::escape_id(args[++argidx]));
1689                                 continue;
1690                         }
1691                         if (args[argidx] == "-reset" && argidx+1 < args.size()) {
1692                                 worker.reset.insert(RTLIL::escape_id(args[++argidx]));
1693                                 continue;
1694                         }
1695                         if (args[argidx] == "-resetn" && argidx+1 < args.size()) {
1696                                 worker.resetn.insert(RTLIL::escape_id(args[++argidx]));
1697                                 continue;
1698                         }
1699                         if (args[argidx] == "-timescale" && argidx+1 < args.size()) {
1700                                 worker.timescale = args[++argidx];
1701                                 continue;
1702                         }
1703                         if (args[argidx] == "-a") {
1704                                 worker.hide_internal = false;
1705                                 continue;
1706                         }
1707                         if (args[argidx] == "-d") {
1708                                 worker.debug = true;
1709                                 continue;
1710                         }
1711                         if (args[argidx] == "-w") {
1712                                 worker.writeback = true;
1713                                 continue;
1714                         }
1715                         if (args[argidx] == "-zinit") {
1716                                 worker.zinit = true;
1717                                 continue;
1718                         }
1719                         if (args[argidx] == "-r" && argidx+1 < args.size()) {
1720                                 std::string sim_filename = args[++argidx];
1721                                 rewrite_filename(sim_filename);
1722                                 worker.sim_filename = sim_filename;
1723                                 continue;
1724                         }
1725                         if (args[argidx] == "-map" && argidx+1 < args.size()) {
1726                                 std::string map_filename = args[++argidx];
1727                                 rewrite_filename(map_filename);
1728                                 worker.map_filename = map_filename;
1729                                 continue;
1730                         }
1731                         if (args[argidx] == "-scope" && argidx+1 < args.size()) {
1732                                 worker.scope = args[++argidx];
1733                                 continue;
1734                         }
1735                         if (args[argidx] == "-start" && argidx+1 < args.size()) {
1736                                 worker.start_time = stringToTime(args[++argidx]);
1737                                 start_set = true;
1738                                 continue;
1739                         }
1740                         if (args[argidx] == "-stop" && argidx+1 < args.size()) {
1741                                 worker.stop_time = stringToTime(args[++argidx]);
1742                                 stop_set = true;
1743                                 continue;
1744                         }
1745                         if (args[argidx] == "-at" && argidx+1 < args.size()) {
1746                                 worker.start_time = stringToTime(args[++argidx]);
1747                                 worker.stop_time = worker.start_time;
1748                                 at_set = true;
1749                                 continue;
1750                         }
1751                         if (args[argidx] == "-sim") {
1752                                 worker.sim_mode = SimulationMode::sim;
1753                                 continue;
1754                         }
1755                         if (args[argidx] == "-sim-cmp") {
1756                                 worker.sim_mode = SimulationMode::cmp;
1757                                 continue;
1758                         }
1759                         if (args[argidx] == "-sim-gold") {
1760                                 worker.sim_mode = SimulationMode::gold;
1761                                 continue;
1762                         }
1763                         if (args[argidx] == "-sim-gate") {
1764                                 worker.sim_mode = SimulationMode::gate;
1765                                 continue;
1766                         }
1767                         if (args[argidx] == "-x") {
1768                                 worker.ignore_x = true;
1769                                 continue;
1770                         }
1771                         if (args[argidx] == "-date") {
1772                                 worker.date = true;
1773                                 continue;
1774                         }
1775                         break;
1776                 }
1777                 extra_args(args, argidx, design);
1778                 if (at_set && (start_set || stop_set || worker.cycles_set))
1779                         log_error("'at' option can only be defined separate of 'start','stop' and 'n'\n");
1780                 if (stop_set && worker.cycles_set)
1781                         log_error("'stop' and 'n' can only be used exclusively'\n");
1782
1783                 Module *top_mod = nullptr;
1784
1785                 if (design->full_selection()) {
1786                         top_mod = design->top_module();
1787
1788                         if (!top_mod)
1789                                 log_cmd_error("Design has no top module, use the 'hierarchy' command to specify one.\n");
1790                 } else {
1791                         auto mods = design->selected_whole_modules();
1792                         if (GetSize(mods) != 1)
1793                                 log_cmd_error("Only one top module must be selected.\n");
1794                         top_mod = mods.front();
1795                 }
1796
1797                 if (worker.sim_filename.empty())
1798                         worker.run(top_mod, numcycles);
1799                 else {
1800                         std::string filename_trim = file_base_name(worker.sim_filename);
1801                         if (filename_trim.size() > 4 && ((filename_trim.compare(filename_trim.size()-4, std::string::npos, ".fst") == 0) ||
1802                                 filename_trim.compare(filename_trim.size()-4, std::string::npos, ".vcd") == 0)) {
1803                                 worker.run_cosim_fst(top_mod, numcycles);
1804                         } else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".aiw") == 0) {
1805                                 if (worker.map_filename.empty())
1806                                         log_cmd_error("For AIGER witness file map parameter is mandatory.\n");
1807                                 worker.run_cosim_aiger_witness(top_mod);
1808                         } else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".wit") == 0) {
1809                                 worker.run_cosim_btor2_witness(top_mod);
1810                         } else {
1811                                 log_cmd_error("Unhandled extension for simulation input file `%s`.\n", worker.sim_filename.c_str());
1812                         }
1813                 }
1814         }
1815 } SimPass;
1816
1817 PRIVATE_NAMESPACE_END