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 // [[CITE]] Btor2 , BtorMC and Boolector 3.0 21 // Aina Niemetz, Mathias Preiner, C. Wolf, Armin Biere 22 // Computer Aided Verification - 30th International Conference, CAV 2018 23 // https://cs.stanford.edu/people/niemetz/publication/2018/niemetzpreinerwolfbiere-cav18/ 24 25 #include "kernel/rtlil.h" 26 #include "kernel/register.h" 27 #include "kernel/sigtools.h" 28 #include "kernel/celltypes.h" 29 #include "kernel/log.h" 30 #include "kernel/mem.h" 31 #include <string> 32 33 USING_YOSYS_NAMESPACE 34 PRIVATE_NAMESPACE_BEGIN 35 36 struct BtorWorker 37 { 38 std::ostream &f; 39 SigMap sigmap; 40 RTLIL::Module *module; 41 bool verbose; 42 bool single_bad; 43 bool cover_mode; 44 bool print_internal_names; 45 46 int next_nid = 1; 47 int initstate_nid = -1; 48 49 // <width> => <sid> 50 dict<int, int> sorts_bv; 51 52 // (<address-width>, <data-width>) => <sid> 53 dict<pair<int, int>, int> sorts_mem; 54 55 // SigBit => (<nid>, <bitidx>) 56 dict<SigBit, pair<int, int>> bit_nid; 57 58 // <nid> => <bvwidth> 59 dict<int, int> nid_width; 60 61 // SigSpec => <nid> 62 dict<SigSpec, int> sig_nid; 63 64 // bit to driving cell 65 dict<SigBit, Cell*> bit_cell; 66 67 // nids for constants 68 dict<Const, int> consts; 69 70 // ff inputs that need to be evaluated (<nid>, <ff_cell>) 71 vector<pair<int, Cell*>> ff_todo; 72 vector<pair<int, Mem*>> mem_todo; 73 74 pool<Cell*> cell_recursion_guard; 75 vector<int> bad_properties; 76 dict<SigBit, bool> initbits; 77 pool<Wire*> statewires; 78 pool<string> srcsymbols; 79 vector<Mem> memories; 80 dict<Cell*, Mem*> mem_cells; 81 82 string indent, info_filename; 83 vector<string> info_lines; 84 dict<int, int> info_clocks; 85 btorfBtorWorker86 void btorf(const char *fmt, ...) YS_ATTRIBUTE(format(printf, 2, 3)) 87 { 88 va_list ap; 89 va_start(ap, fmt); 90 f << indent << vstringf(fmt, ap); 91 va_end(ap); 92 } 93 infofBtorWorker94 void infof(const char *fmt, ...) YS_ATTRIBUTE(format(printf, 2, 3)) 95 { 96 va_list ap; 97 va_start(ap, fmt); 98 info_lines.push_back(vstringf(fmt, ap)); 99 va_end(ap); 100 } 101 102 template<typename T> getinfoBtorWorker103 string getinfo(T *obj, bool srcsym = false) 104 { 105 string infostr = log_id(obj); 106 if (!srcsym && !print_internal_names && infostr[0] == '$') return ""; 107 if (obj->attributes.count(ID::src)) { 108 string src = obj->attributes.at(ID::src).decode_string().c_str(); 109 if (srcsym && infostr[0] == '$') { 110 std::replace(src.begin(), src.end(), ' ', '_'); 111 if (srcsymbols.count(src) || module->count_id("\\" + src)) { 112 for (int i = 1;; i++) { 113 string s = stringf("%s-%d", src.c_str(), i); 114 if (!srcsymbols.count(s) && !module->count_id("\\" + s)) { 115 src = s; 116 break; 117 } 118 } 119 } 120 srcsymbols.insert(src); 121 infostr = src; 122 } else { 123 infostr += " ; " + src; 124 } 125 } 126 return " " + infostr; 127 } 128 btorf_pushBtorWorker129 void btorf_push(const string &id) 130 { 131 if (verbose) { 132 f << indent << stringf(" ; begin %s\n", id.c_str()); 133 indent += " "; 134 } 135 } 136 btorf_popBtorWorker137 void btorf_pop(const string &id) 138 { 139 if (verbose) { 140 indent = indent.substr(4); 141 f << indent << stringf(" ; end %s\n", id.c_str()); 142 } 143 } 144 get_bv_sidBtorWorker145 int get_bv_sid(int width) 146 { 147 if (sorts_bv.count(width) == 0) { 148 int nid = next_nid++; 149 btorf("%d sort bitvec %d\n", nid, width); 150 sorts_bv[width] = nid; 151 } 152 return sorts_bv.at(width); 153 } 154 get_mem_sidBtorWorker155 int get_mem_sid(int abits, int dbits) 156 { 157 pair<int, int> key(abits, dbits); 158 if (sorts_mem.count(key) == 0) { 159 int addr_sid = get_bv_sid(abits); 160 int data_sid = get_bv_sid(dbits); 161 int nid = next_nid++; 162 btorf("%d sort array %d %d\n", nid, addr_sid, data_sid); 163 sorts_mem[key] = nid; 164 } 165 return sorts_mem.at(key); 166 } 167 add_nid_sigBtorWorker168 void add_nid_sig(int nid, const SigSpec &sig) 169 { 170 if (verbose) 171 f << indent << stringf("; %d %s\n", nid, log_signal(sig)); 172 173 for (int i = 0; i < GetSize(sig); i++) 174 bit_nid[sig[i]] = make_pair(nid, i); 175 176 sig_nid[sig] = nid; 177 nid_width[nid] = GetSize(sig); 178 } 179 export_cellBtorWorker180 void export_cell(Cell *cell) 181 { 182 if (cell_recursion_guard.count(cell)) { 183 string cell_list; 184 for (auto c : cell_recursion_guard) 185 cell_list += stringf("\n %s", log_id(c)); 186 log_error("Found topological loop while processing cell %s. Active cells:%s\n", log_id(cell), cell_list.c_str()); 187 } 188 189 cell_recursion_guard.insert(cell); 190 btorf_push(log_id(cell)); 191 192 if (cell->type.in(ID($add), ID($sub), ID($mul), ID($and), ID($or), ID($xor), ID($xnor), ID($shl), ID($sshl), ID($shr), ID($sshr), ID($shift), ID($shiftx), 193 ID($concat), ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_))) 194 { 195 string btor_op; 196 if (cell->type == ID($add)) btor_op = "add"; 197 if (cell->type == ID($sub)) btor_op = "sub"; 198 if (cell->type == ID($mul)) btor_op = "mul"; 199 if (cell->type.in(ID($shl), ID($sshl))) btor_op = "sll"; 200 if (cell->type == ID($shr)) btor_op = "srl"; 201 if (cell->type == ID($sshr)) btor_op = "sra"; 202 if (cell->type.in(ID($shift), ID($shiftx))) btor_op = "shift"; 203 if (cell->type.in(ID($and), ID($_AND_))) btor_op = "and"; 204 if (cell->type.in(ID($or), ID($_OR_))) btor_op = "or"; 205 if (cell->type.in(ID($xor), ID($_XOR_))) btor_op = "xor"; 206 if (cell->type == ID($concat)) btor_op = "concat"; 207 if (cell->type == ID($_NAND_)) btor_op = "nand"; 208 if (cell->type == ID($_NOR_)) btor_op = "nor"; 209 if (cell->type.in(ID($xnor), ID($_XNOR_))) btor_op = "xnor"; 210 log_assert(!btor_op.empty()); 211 212 int width_ay = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y))); 213 int width = std::max(width_ay, GetSize(cell->getPort(ID::B))); 214 215 bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false; 216 bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false; 217 218 if (btor_op == "shift" && !b_signed) 219 btor_op = "srl"; 220 221 if (cell->type.in(ID($shl), ID($sshl), ID($shr), ID($sshr))) 222 b_signed = false; 223 224 if (cell->type == ID($sshr) && !a_signed) 225 btor_op = "srl"; 226 227 int sid = get_bv_sid(width); 228 int nid; 229 230 int nid_a; 231 if (cell->type.in(ID($shl), ID($shr), ID($shift), ID($shiftx)) && a_signed && width_ay < width) { 232 // sign-extend A up to the width of Y 233 int nid_a_padded = get_sig_nid(cell->getPort(ID::A), width_ay, a_signed); 234 235 // zero-extend the rest 236 int zeroes = get_sig_nid(Const(0, width-width_ay)); 237 nid_a = next_nid++; 238 btorf("%d concat %d %d %d\n", nid_a, sid, zeroes, nid_a_padded); 239 } else { 240 nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); 241 } 242 243 int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); 244 245 if (btor_op == "shift") 246 { 247 int nid_r = next_nid++; 248 btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b); 249 250 int nid_b_neg = next_nid++; 251 btorf("%d neg %d %d\n", nid_b_neg, sid, nid_b); 252 253 int nid_l = next_nid++; 254 btorf("%d sll %d %d %d\n", nid_l, sid, nid_a, nid_b_neg); 255 256 int sid_bit = get_bv_sid(1); 257 int nid_zero = get_sig_nid(Const(0, width)); 258 int nid_b_ltz = next_nid++; 259 btorf("%d slt %d %d %d\n", nid_b_ltz, sid_bit, nid_b, nid_zero); 260 261 nid = next_nid++; 262 btorf("%d ite %d %d %d %d%s\n", nid, sid, nid_b_ltz, nid_l, nid_r, getinfo(cell).c_str()); 263 } 264 else 265 { 266 nid = next_nid++; 267 btorf("%d %s %d %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); 268 } 269 270 SigSpec sig = sigmap(cell->getPort(ID::Y)); 271 272 if (GetSize(sig) < width) { 273 int sid = get_bv_sid(GetSize(sig)); 274 int nid2 = next_nid++; 275 btorf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig)-1); 276 nid = nid2; 277 } 278 279 add_nid_sig(nid, sig); 280 goto okay; 281 } 282 283 if (cell->type.in(ID($div), ID($mod), ID($modfloor))) 284 { 285 bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false; 286 bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false; 287 288 string btor_op; 289 if (cell->type == ID($div)) btor_op = "div"; 290 // "rem" = truncating modulo 291 if (cell->type == ID($mod)) btor_op = "rem"; 292 // "mod" = flooring modulo 293 if (cell->type == ID($modfloor)) { 294 // "umod" doesn't exist because it's the same as "urem" 295 btor_op = a_signed || b_signed ? "mod" : "rem"; 296 } 297 log_assert(!btor_op.empty()); 298 299 int width = GetSize(cell->getPort(ID::Y)); 300 width = std::max(width, GetSize(cell->getPort(ID::A))); 301 width = std::max(width, GetSize(cell->getPort(ID::B))); 302 303 int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); 304 int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); 305 306 int sid = get_bv_sid(width); 307 int nid = next_nid++; 308 btorf("%d %c%s %d %d %d%s\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); 309 310 SigSpec sig = sigmap(cell->getPort(ID::Y)); 311 312 if (GetSize(sig) < width) { 313 int sid = get_bv_sid(GetSize(sig)); 314 int nid2 = next_nid++; 315 btorf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig)-1); 316 nid = nid2; 317 } 318 319 add_nid_sig(nid, sig); 320 goto okay; 321 } 322 323 if (cell->type.in(ID($_ANDNOT_), ID($_ORNOT_))) 324 { 325 int sid = get_bv_sid(1); 326 int nid_a = get_sig_nid(cell->getPort(ID::A)); 327 int nid_b = get_sig_nid(cell->getPort(ID::B)); 328 329 int nid1 = next_nid++; 330 int nid2 = next_nid++; 331 332 if (cell->type == ID($_ANDNOT_)) { 333 btorf("%d not %d %d\n", nid1, sid, nid_b); 334 btorf("%d and %d %d %d%s\n", nid2, sid, nid_a, nid1, getinfo(cell).c_str()); 335 } 336 337 if (cell->type == ID($_ORNOT_)) { 338 btorf("%d not %d %d\n", nid1, sid, nid_b); 339 btorf("%d or %d %d %d%s\n", nid2, sid, nid_a, nid1, getinfo(cell).c_str()); 340 } 341 342 SigSpec sig = sigmap(cell->getPort(ID::Y)); 343 add_nid_sig(nid2, sig); 344 goto okay; 345 } 346 347 if (cell->type.in(ID($_OAI3_), ID($_AOI3_))) 348 { 349 int sid = get_bv_sid(1); 350 int nid_a = get_sig_nid(cell->getPort(ID::A)); 351 int nid_b = get_sig_nid(cell->getPort(ID::B)); 352 int nid_c = get_sig_nid(cell->getPort(ID::C)); 353 354 int nid1 = next_nid++; 355 int nid2 = next_nid++; 356 int nid3 = next_nid++; 357 358 if (cell->type == ID($_OAI3_)) { 359 btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b); 360 btorf("%d and %d %d %d\n", nid2, sid, nid1, nid_c); 361 btorf("%d not %d %d%s\n", nid3, sid, nid2, getinfo(cell).c_str()); 362 } 363 364 if (cell->type == ID($_AOI3_)) { 365 btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b); 366 btorf("%d or %d %d %d\n", nid2, sid, nid1, nid_c); 367 btorf("%d not %d %d%s\n", nid3, sid, nid2, getinfo(cell).c_str()); 368 } 369 370 SigSpec sig = sigmap(cell->getPort(ID::Y)); 371 add_nid_sig(nid3, sig); 372 goto okay; 373 } 374 375 if (cell->type.in(ID($_OAI4_), ID($_AOI4_))) 376 { 377 int sid = get_bv_sid(1); 378 int nid_a = get_sig_nid(cell->getPort(ID::A)); 379 int nid_b = get_sig_nid(cell->getPort(ID::B)); 380 int nid_c = get_sig_nid(cell->getPort(ID::C)); 381 int nid_d = get_sig_nid(cell->getPort(ID::D)); 382 383 int nid1 = next_nid++; 384 int nid2 = next_nid++; 385 int nid3 = next_nid++; 386 int nid4 = next_nid++; 387 388 if (cell->type == ID($_OAI4_)) { 389 btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b); 390 btorf("%d or %d %d %d\n", nid2, sid, nid_c, nid_d); 391 btorf("%d and %d %d %d\n", nid3, sid, nid1, nid2); 392 btorf("%d not %d %d%s\n", nid4, sid, nid3, getinfo(cell).c_str()); 393 } 394 395 if (cell->type == ID($_AOI4_)) { 396 btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b); 397 btorf("%d and %d %d %d\n", nid2, sid, nid_c, nid_d); 398 btorf("%d or %d %d %d\n", nid3, sid, nid1, nid2); 399 btorf("%d not %d %d%s\n", nid4, sid, nid3, getinfo(cell).c_str()); 400 } 401 402 SigSpec sig = sigmap(cell->getPort(ID::Y)); 403 add_nid_sig(nid4, sig); 404 goto okay; 405 } 406 407 if (cell->type.in(ID($lt), ID($le), ID($eq), ID($eqx), ID($ne), ID($nex), ID($ge), ID($gt))) 408 { 409 string btor_op; 410 if (cell->type == ID($lt)) btor_op = "lt"; 411 if (cell->type == ID($le)) btor_op = "lte"; 412 if (cell->type.in(ID($eq), ID($eqx))) btor_op = "eq"; 413 if (cell->type.in(ID($ne), ID($nex))) btor_op = "neq"; 414 if (cell->type == ID($ge)) btor_op = "gte"; 415 if (cell->type == ID($gt)) btor_op = "gt"; 416 log_assert(!btor_op.empty()); 417 418 int width = 1; 419 width = std::max(width, GetSize(cell->getPort(ID::A))); 420 width = std::max(width, GetSize(cell->getPort(ID::B))); 421 422 bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false; 423 bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false; 424 425 int sid = get_bv_sid(1); 426 int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); 427 int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); 428 429 int nid = next_nid++; 430 if (cell->type.in(ID($lt), ID($le), ID($ge), ID($gt))) { 431 btorf("%d %c%s %d %d %d%s\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); 432 } else { 433 btorf("%d %s %d %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); 434 } 435 436 SigSpec sig = sigmap(cell->getPort(ID::Y)); 437 438 if (GetSize(sig) > 1) { 439 int sid = get_bv_sid(GetSize(sig)); 440 int nid2 = next_nid++; 441 btorf("%d uext %d %d %d\n", nid2, sid, nid, GetSize(sig) - 1); 442 nid = nid2; 443 } 444 445 add_nid_sig(nid, sig); 446 goto okay; 447 } 448 449 if (cell->type.in(ID($not), ID($neg), ID($_NOT_))) 450 { 451 string btor_op; 452 if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not"; 453 if (cell->type == ID($neg)) btor_op = "neg"; 454 log_assert(!btor_op.empty()); 455 456 int width = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y))); 457 458 bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false; 459 460 int sid = get_bv_sid(width); 461 int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); 462 463 int nid = next_nid++; 464 btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str()); 465 466 SigSpec sig = sigmap(cell->getPort(ID::Y)); 467 468 if (GetSize(sig) < width) { 469 int sid = get_bv_sid(GetSize(sig)); 470 int nid2 = next_nid++; 471 btorf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig)-1); 472 nid = nid2; 473 } 474 475 add_nid_sig(nid, sig); 476 goto okay; 477 } 478 479 if (cell->type.in(ID($logic_and), ID($logic_or), ID($logic_not))) 480 { 481 string btor_op; 482 if (cell->type == ID($logic_and)) btor_op = "and"; 483 if (cell->type == ID($logic_or)) btor_op = "or"; 484 if (cell->type == ID($logic_not)) btor_op = "not"; 485 log_assert(!btor_op.empty()); 486 487 int sid = get_bv_sid(1); 488 int nid_a = get_sig_nid(cell->getPort(ID::A)); 489 int nid_b = btor_op != "not" ? get_sig_nid(cell->getPort(ID::B)) : 0; 490 491 if (GetSize(cell->getPort(ID::A)) > 1) { 492 int nid_red_a = next_nid++; 493 btorf("%d redor %d %d\n", nid_red_a, sid, nid_a); 494 nid_a = nid_red_a; 495 } 496 497 if (btor_op != "not" && GetSize(cell->getPort(ID::B)) > 1) { 498 int nid_red_b = next_nid++; 499 btorf("%d redor %d %d\n", nid_red_b, sid, nid_b); 500 nid_b = nid_red_b; 501 } 502 503 int nid = next_nid++; 504 if (btor_op != "not") 505 btorf("%d %s %d %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); 506 else 507 btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str()); 508 509 SigSpec sig = sigmap(cell->getPort(ID::Y)); 510 511 if (GetSize(sig) > 1) { 512 int sid = get_bv_sid(GetSize(sig)); 513 int zeros_nid = get_sig_nid(Const(0, GetSize(sig)-1)); 514 int nid2 = next_nid++; 515 btorf("%d concat %d %d %d\n", nid2, sid, zeros_nid, nid); 516 nid = nid2; 517 } 518 519 add_nid_sig(nid, sig); 520 goto okay; 521 } 522 523 if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool), ID($reduce_xor), ID($reduce_xnor))) 524 { 525 string btor_op; 526 if (cell->type == ID($reduce_and)) btor_op = "redand"; 527 if (cell->type.in(ID($reduce_or), ID($reduce_bool))) btor_op = "redor"; 528 if (cell->type.in(ID($reduce_xor), ID($reduce_xnor))) btor_op = "redxor"; 529 log_assert(!btor_op.empty()); 530 531 int sid = get_bv_sid(1); 532 int nid_a = get_sig_nid(cell->getPort(ID::A)); 533 534 int nid = next_nid++; 535 536 if (cell->type == ID($reduce_xnor)) { 537 int nid2 = next_nid++; 538 btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str()); 539 btorf("%d not %d %d\n", nid2, sid, nid); 540 nid = nid2; 541 } else { 542 btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str()); 543 } 544 545 SigSpec sig = sigmap(cell->getPort(ID::Y)); 546 547 if (GetSize(sig) > 1) { 548 int sid = get_bv_sid(GetSize(sig)); 549 int zeros_nid = get_sig_nid(Const(0, GetSize(sig)-1)); 550 int nid2 = next_nid++; 551 btorf("%d concat %d %d %d\n", nid2, sid, zeros_nid, nid); 552 nid = nid2; 553 } 554 555 add_nid_sig(nid, sig); 556 goto okay; 557 } 558 559 if (cell->type.in(ID($mux), ID($_MUX_), ID($_NMUX_))) 560 { 561 SigSpec sig_a = sigmap(cell->getPort(ID::A)); 562 SigSpec sig_b = sigmap(cell->getPort(ID::B)); 563 SigSpec sig_s = sigmap(cell->getPort(ID::S)); 564 SigSpec sig_y = sigmap(cell->getPort(ID::Y)); 565 566 int nid_a = get_sig_nid(sig_a); 567 int nid_b = get_sig_nid(sig_b); 568 int nid_s = get_sig_nid(sig_s); 569 570 int sid = get_bv_sid(GetSize(sig_y)); 571 int nid = next_nid++; 572 573 if (cell->type == ID($_NMUX_)) { 574 int tmp = nid; 575 nid = next_nid++; 576 btorf("%d ite %d %d %d %d\n", tmp, sid, nid_s, nid_b, nid_a); 577 btorf("%d not %d %d%s\n", nid, sid, tmp, getinfo(cell).c_str()); 578 } else { 579 btorf("%d ite %d %d %d %d%s\n", nid, sid, nid_s, nid_b, nid_a, getinfo(cell).c_str()); 580 } 581 582 add_nid_sig(nid, sig_y); 583 goto okay; 584 } 585 586 if (cell->type == ID($pmux)) 587 { 588 SigSpec sig_a = sigmap(cell->getPort(ID::A)); 589 SigSpec sig_b = sigmap(cell->getPort(ID::B)); 590 SigSpec sig_s = sigmap(cell->getPort(ID::S)); 591 SigSpec sig_y = sigmap(cell->getPort(ID::Y)); 592 593 int width = GetSize(sig_a); 594 int sid = get_bv_sid(width); 595 int nid = get_sig_nid(sig_a); 596 597 for (int i = 0; i < GetSize(sig_s); i++) { 598 int nid_b = get_sig_nid(sig_b.extract(i*width, width)); 599 int nid_s = get_sig_nid(sig_s.extract(i)); 600 int nid2 = next_nid++; 601 if (i == GetSize(sig_s)-1) 602 btorf("%d ite %d %d %d %d%s\n", nid2, sid, nid_s, nid_b, nid, getinfo(cell).c_str()); 603 else 604 btorf("%d ite %d %d %d %d\n", nid2, sid, nid_s, nid_b, nid); 605 nid = nid2; 606 } 607 608 add_nid_sig(nid, sig_y); 609 goto okay; 610 } 611 612 if (cell->type.in(ID($dff), ID($ff), ID($_DFF_P_), ID($_DFF_N), ID($_FF_))) 613 { 614 SigSpec sig_d = sigmap(cell->getPort(ID::D)); 615 SigSpec sig_q = sigmap(cell->getPort(ID::Q)); 616 617 if (!info_filename.empty() && cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_))) 618 { 619 SigSpec sig_c = sigmap(cell->getPort(cell->type == ID($dff) ? ID::CLK : ID::C)); 620 int nid = get_sig_nid(sig_c); 621 bool negedge = false; 622 623 if (cell->type == ID($_DFF_N_)) 624 negedge = true; 625 626 if (cell->type == ID($dff) && !cell->getParam(ID::CLK_POLARITY).as_bool()) 627 negedge = true; 628 629 info_clocks[nid] |= negedge ? 2 : 1; 630 } 631 632 IdString symbol; 633 634 if (sig_q.is_wire()) { 635 Wire *w = sig_q.as_wire(); 636 if (w->port_id == 0) { 637 statewires.insert(w); 638 symbol = w->name; 639 } 640 } 641 642 Const initval; 643 for (int i = 0; i < GetSize(sig_q); i++) 644 if (initbits.count(sig_q[i])) 645 initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0); 646 else 647 initval.bits.push_back(State::Sx); 648 649 int nid_init_val = -1; 650 651 if (!initval.is_fully_undef()) 652 nid_init_val = get_sig_nid(initval, -1, false, true); 653 654 int sid = get_bv_sid(GetSize(sig_q)); 655 int nid = next_nid++; 656 657 if (symbol.empty() || (!print_internal_names && symbol[0] == '$')) 658 btorf("%d state %d\n", nid, sid); 659 else 660 btorf("%d state %d %s\n", nid, sid, log_id(symbol)); 661 662 if (nid_init_val >= 0) { 663 int nid_init = next_nid++; 664 if (verbose) 665 btorf("; initval = %s\n", log_signal(initval)); 666 btorf("%d init %d %d %d\n", nid_init, sid, nid, nid_init_val); 667 } 668 669 ff_todo.push_back(make_pair(nid, cell)); 670 add_nid_sig(nid, sig_q); 671 goto okay; 672 } 673 674 if (cell->type.in(ID($anyconst), ID($anyseq))) 675 { 676 SigSpec sig_y = sigmap(cell->getPort(ID::Y)); 677 678 int sid = get_bv_sid(GetSize(sig_y)); 679 int nid = next_nid++; 680 681 btorf("%d state %d\n", nid, sid); 682 683 if (cell->type == ID($anyconst)) { 684 int nid2 = next_nid++; 685 btorf("%d next %d %d %d\n", nid2, sid, nid, nid); 686 } 687 688 add_nid_sig(nid, sig_y); 689 goto okay; 690 } 691 692 if (cell->type == ID($initstate)) 693 { 694 SigSpec sig_y = sigmap(cell->getPort(ID::Y)); 695 696 if (initstate_nid < 0) 697 { 698 int sid = get_bv_sid(1); 699 int one_nid = get_sig_nid(State::S1); 700 int zero_nid = get_sig_nid(State::S0); 701 initstate_nid = next_nid++; 702 btorf("%d state %d\n", initstate_nid, sid); 703 btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid); 704 btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid); 705 } 706 707 add_nid_sig(initstate_nid, sig_y); 708 goto okay; 709 } 710 711 if (cell->is_mem_cell()) 712 { 713 Mem *mem = mem_cells[cell]; 714 715 int abits = ceil_log2(mem->size); 716 717 bool asyncwr = false; 718 bool syncwr = false; 719 720 for (auto &port : mem->wr_ports) { 721 if (port.clk_enable) 722 syncwr = true; 723 else 724 asyncwr = true; 725 } 726 727 if (asyncwr && syncwr) 728 log_error("Memory %s.%s has mixed async/sync write ports.\n", 729 log_id(module), log_id(mem->memid)); 730 731 for (auto &port : mem->rd_ports) { 732 if (port.clk_enable) 733 log_error("Memory %s.%s has sync read ports. Please use memory_nordff to convert them first.\n", 734 log_id(module), log_id(mem->memid)); 735 } 736 737 int data_sid = get_bv_sid(mem->width); 738 int bool_sid = get_bv_sid(1); 739 int sid = get_mem_sid(abits, mem->width); 740 741 int nid_init_val = -1; 742 743 if (!mem->inits.empty()) 744 { 745 Const initdata = mem->get_init_data(); 746 bool constword = true; 747 Const firstword = initdata.extract(0, mem->width); 748 749 for (int i = 1; i < mem->size; i++) { 750 Const thisword = initdata.extract(i*mem->width, mem->width); 751 if (thisword != firstword) { 752 constword = false; 753 break; 754 } 755 } 756 757 if (constword) 758 { 759 if (verbose) 760 btorf("; initval = %s\n", log_signal(firstword)); 761 nid_init_val = get_sig_nid(firstword, -1, false, true); 762 } 763 else 764 { 765 nid_init_val = next_nid++; 766 btorf("%d state %d\n", nid_init_val, sid); 767 768 for (int i = 0; i < mem->size; i++) { 769 Const thisword = initdata.extract(i*mem->width, mem->width); 770 if (thisword.is_fully_undef()) 771 continue; 772 Const thisaddr(i, abits); 773 int nid_thisword = get_sig_nid(thisword, -1, false, true); 774 int nid_thisaddr = get_sig_nid(thisaddr, -1, false, true); 775 int last_nid_init_val = nid_init_val; 776 nid_init_val = next_nid++; 777 if (verbose) 778 btorf("; initval[%d] = %s\n", i, log_signal(thisword)); 779 btorf("%d write %d %d %d %d\n", nid_init_val, sid, last_nid_init_val, nid_thisaddr, nid_thisword); 780 } 781 } 782 } 783 784 785 int nid = next_nid++; 786 int nid_head = nid; 787 788 if (mem->memid[0] == '$') 789 btorf("%d state %d\n", nid, sid); 790 else 791 btorf("%d state %d %s\n", nid, sid, log_id(mem->memid)); 792 793 if (nid_init_val >= 0) 794 { 795 int nid_init = next_nid++; 796 btorf("%d init %d %d %d\n", nid_init, sid, nid, nid_init_val); 797 } 798 799 if (asyncwr) 800 { 801 for (auto &port : mem->wr_ports) 802 { 803 SigSpec wa = port.addr; 804 wa.extend_u0(abits); 805 806 int wa_nid = get_sig_nid(wa); 807 int wd_nid = get_sig_nid(port.data); 808 int we_nid = get_sig_nid(port.en); 809 810 int nid2 = next_nid++; 811 btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid); 812 813 int nid3 = next_nid++; 814 btorf("%d not %d %d\n", nid3, data_sid, we_nid); 815 816 int nid4 = next_nid++; 817 btorf("%d and %d %d %d\n", nid4, data_sid, nid2, nid3); 818 819 int nid5 = next_nid++; 820 btorf("%d and %d %d %d\n", nid5, data_sid, wd_nid, we_nid); 821 822 int nid6 = next_nid++; 823 btorf("%d or %d %d %d\n", nid6, data_sid, nid5, nid4); 824 825 int nid7 = next_nid++; 826 btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6); 827 828 int nid8 = next_nid++; 829 btorf("%d redor %d %d\n", nid8, bool_sid, we_nid); 830 831 int nid9 = next_nid++; 832 btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head); 833 834 nid_head = nid9; 835 } 836 } 837 838 for (auto &port : mem->rd_ports) 839 { 840 SigSpec ra = port.addr; 841 ra.extend_u0(abits); 842 843 int ra_nid = get_sig_nid(ra); 844 int rd_nid = next_nid++; 845 846 btorf("%d read %d %d %d\n", rd_nid, data_sid, nid_head, ra_nid); 847 848 add_nid_sig(rd_nid, port.data); 849 } 850 851 if (!asyncwr) 852 { 853 mem_todo.push_back(make_pair(nid, mem)); 854 } 855 else 856 { 857 int nid2 = next_nid++; 858 btorf("%d next %d %d %d\n", nid2, sid, nid, nid_head); 859 } 860 861 goto okay; 862 } 863 864 if (cell->type.in(ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)) || cell->type.str().substr(0, 6) == "$_SDFF" || (cell->type.str().substr(0, 6) == "$_DFFE" && cell->type.str().size() == 10)) { 865 log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_btor`.\n", 866 log_id(cell->type), log_id(module), log_id(cell)); 867 } 868 if (cell->type.in(ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF" || cell->type.str().substr(0, 7) == "$_ALDFF") { 869 log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_btor`.\n", 870 log_id(cell->type), log_id(module), log_id(cell)); 871 } 872 if (cell->type.in(ID($sr), ID($dlatch), ID($adlatch), ID($dlatchsr)) || cell->type.str().substr(0, 8) == "$_DLATCH" || cell->type.str().substr(0, 5) == "$_SR_") { 873 log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_btor`.\n", 874 log_id(cell->type), log_id(module), log_id(cell)); 875 } 876 log_error("Unsupported cell type %s for cell %s.%s.\n", 877 log_id(cell->type), log_id(module), log_id(cell)); 878 879 okay: 880 btorf_pop(log_id(cell)); 881 cell_recursion_guard.erase(cell); 882 } 883 get_sig_nidBtorWorker884 int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false, bool is_init = false) 885 { 886 int nid = -1; 887 sigmap.apply(sig); 888 889 for (auto bit : sig) 890 if (bit == State::Sx) 891 goto has_undef_bits; 892 893 if (0) 894 { 895 has_undef_bits: 896 SigSpec sig_mask_undef, sig_noundef; 897 int first_undef = -1; 898 899 for (int i = 0; i < GetSize(sig); i++) 900 if (sig[i] == State::Sx) { 901 if (first_undef < 0) 902 first_undef = i; 903 sig_mask_undef.append(State::S1); 904 sig_noundef.append(State::S0); 905 } else { 906 sig_mask_undef.append(State::S0); 907 sig_noundef.append(sig[i]); 908 } 909 910 if (to_width < 0 || first_undef < to_width) 911 { 912 int sid = get_bv_sid(GetSize(sig)); 913 914 int nid_input = next_nid++; 915 if (is_init) 916 btorf("%d state %d\n", nid_input, sid); 917 else 918 btorf("%d input %d\n", nid_input, sid); 919 920 int nid_masked_input; 921 if (sig_mask_undef.is_fully_ones()) { 922 nid_masked_input = nid_input; 923 } else { 924 int nid_mask_undef = get_sig_nid(sig_mask_undef); 925 nid_masked_input = next_nid++; 926 btorf("%d and %d %d %d\n", nid_masked_input, sid, nid_input, nid_mask_undef); 927 } 928 929 if (sig_noundef.is_fully_zero()) { 930 nid = nid_masked_input; 931 } else { 932 int nid_noundef = get_sig_nid(sig_noundef); 933 nid = next_nid++; 934 btorf("%d or %d %d %d\n", nid, sid, nid_masked_input, nid_noundef); 935 } 936 937 goto extend_or_trim; 938 } 939 940 sig = sig_noundef; 941 } 942 943 if (sig_nid.count(sig) == 0) 944 { 945 // <nid>, <bitidx> 946 vector<pair<int, int>> nidbits; 947 948 // collect all bits 949 for (int i = 0; i < GetSize(sig); i++) 950 { 951 SigBit bit = sig[i]; 952 953 if (bit_nid.count(bit) == 0) 954 { 955 if (bit.wire == nullptr) 956 { 957 Const c(bit.data); 958 959 while (i+GetSize(c) < GetSize(sig) && sig[i+GetSize(c)].wire == nullptr) 960 c.bits.push_back(sig[i+GetSize(c)].data); 961 962 if (consts.count(c) == 0) { 963 int sid = get_bv_sid(GetSize(c)); 964 int nid = next_nid++; 965 btorf("%d const %d %s\n", nid, sid, c.as_string().c_str()); 966 consts[c] = nid; 967 nid_width[nid] = GetSize(c); 968 } 969 970 int nid = consts.at(c); 971 972 for (int j = 0; j < GetSize(c); j++) 973 nidbits.push_back(make_pair(nid, j)); 974 975 i += GetSize(c)-1; 976 continue; 977 } 978 else 979 { 980 if (bit_cell.count(bit) == 0) 981 { 982 SigSpec s = bit; 983 984 while (i+GetSize(s) < GetSize(sig) && sig[i+GetSize(s)].wire != nullptr && 985 bit_cell.count(sig[i+GetSize(s)]) == 0) 986 s.append(sig[i+GetSize(s)]); 987 988 log_warning("No driver for signal %s.\n", log_signal(s)); 989 990 int sid = get_bv_sid(GetSize(s)); 991 int nid = next_nid++; 992 btorf("%d input %d\n", nid, sid); 993 nid_width[nid] = GetSize(s); 994 995 for (int j = 0; j < GetSize(s); j++) 996 nidbits.push_back(make_pair(nid, j)); 997 998 i += GetSize(s)-1; 999 continue; 1000 } 1001 else 1002 { 1003 export_cell(bit_cell.at(bit)); 1004 log_assert(bit_nid.count(bit)); 1005 } 1006 } 1007 } 1008 1009 nidbits.push_back(bit_nid.at(bit)); 1010 } 1011 1012 int width = 0; 1013 int nid = -1; 1014 1015 // group bits and emit slice-concat chain 1016 for (int i = 0; i < GetSize(nidbits); i++) 1017 { 1018 int nid2 = nidbits[i].first; 1019 int lower = nidbits[i].second; 1020 int upper = lower; 1021 1022 while (i+1 < GetSize(nidbits) && nidbits[i+1].first == nidbits[i].first && 1023 nidbits[i+1].second == nidbits[i].second+1) 1024 upper++, i++; 1025 1026 int nid3 = nid2; 1027 1028 if (lower != 0 || upper+1 != nid_width.at(nid2)) { 1029 int sid = get_bv_sid(upper-lower+1); 1030 nid3 = next_nid++; 1031 btorf("%d slice %d %d %d %d\n", nid3, sid, nid2, upper, lower); 1032 } 1033 1034 int nid4 = nid3; 1035 1036 if (nid >= 0) { 1037 int sid = get_bv_sid(width+upper-lower+1); 1038 nid4 = next_nid++; 1039 btorf("%d concat %d %d %d\n", nid4, sid, nid3, nid); 1040 } 1041 1042 width += upper-lower+1; 1043 nid = nid4; 1044 } 1045 1046 sig_nid[sig] = nid; 1047 nid_width[nid] = width; 1048 } 1049 1050 nid = sig_nid.at(sig); 1051 1052 extend_or_trim: 1053 if (to_width >= 0 && to_width != GetSize(sig)) 1054 { 1055 if (to_width < GetSize(sig)) 1056 { 1057 int sid = get_bv_sid(to_width); 1058 int nid2 = next_nid++; 1059 btorf("%d slice %d %d %d 0\n", nid2, sid, nid, to_width-1); 1060 nid = nid2; 1061 } 1062 else 1063 { 1064 int sid = get_bv_sid(to_width); 1065 int nid2 = next_nid++; 1066 btorf("%d %s %d %d %d\n", nid2, is_signed ? "sext" : "uext", 1067 sid, nid, to_width - GetSize(sig)); 1068 nid = nid2; 1069 } 1070 } 1071 1072 return nid; 1073 } 1074 BtorWorkerBtorWorker1075 BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad, bool cover_mode, bool print_internal_names, string info_filename) : 1076 f(f), sigmap(module), module(module), verbose(verbose), single_bad(single_bad), cover_mode(cover_mode), print_internal_names(print_internal_names), info_filename(info_filename) 1077 { 1078 if (!info_filename.empty()) 1079 infof("name %s\n", log_id(module)); 1080 1081 memories = Mem::get_all_memories(module); 1082 1083 dict<IdString, Mem*> mem_dict; 1084 for (auto &mem : memories) { 1085 mem.narrow(); 1086 mem_dict[mem.memid] = &mem; 1087 } 1088 for (auto cell : module->cells()) 1089 if (cell->is_mem_cell()) 1090 mem_cells[cell] = mem_dict[cell->parameters.at(ID::MEMID).decode_string()]; 1091 1092 btorf_push("inputs"); 1093 1094 for (auto wire : module->wires()) 1095 { 1096 if (wire->attributes.count(ID::init)) { 1097 Const attrval = wire->attributes.at(ID::init); 1098 for (int i = 0; i < GetSize(wire) && i < GetSize(attrval); i++) 1099 if (attrval[i] == State::S0 || attrval[i] == State::S1) 1100 initbits[sigmap(SigBit(wire, i))] = (attrval[i] == State::S1); 1101 } 1102 1103 if (!wire->port_id || !wire->port_input) 1104 continue; 1105 1106 SigSpec sig = sigmap(wire); 1107 int sid = get_bv_sid(GetSize(sig)); 1108 int nid = next_nid++; 1109 1110 btorf("%d input %d%s\n", nid, sid, getinfo(wire).c_str()); 1111 add_nid_sig(nid, sig); 1112 } 1113 1114 btorf_pop("inputs"); 1115 1116 for (auto cell : module->cells()) 1117 for (auto &conn : cell->connections()) 1118 { 1119 if (!cell->output(conn.first)) 1120 continue; 1121 1122 for (auto bit : sigmap(conn.second)) 1123 bit_cell[bit] = cell; 1124 } 1125 1126 for (auto wire : module->wires()) 1127 { 1128 if (!wire->port_id || !wire->port_output) 1129 continue; 1130 1131 btorf_push(stringf("output %s", log_id(wire))); 1132 1133 int nid = get_sig_nid(wire); 1134 btorf("%d output %d%s\n", next_nid++, nid, getinfo(wire).c_str()); 1135 1136 btorf_pop(stringf("output %s", log_id(wire))); 1137 } 1138 1139 for (auto cell : module->cells()) 1140 { 1141 if (cell->type == ID($assume)) 1142 { 1143 btorf_push(log_id(cell)); 1144 1145 int sid = get_bv_sid(1); 1146 int nid_a = get_sig_nid(cell->getPort(ID::A)); 1147 int nid_en = get_sig_nid(cell->getPort(ID::EN)); 1148 int nid_not_en = next_nid++; 1149 int nid_a_or_not_en = next_nid++; 1150 int nid = next_nid++; 1151 1152 btorf("%d not %d %d\n", nid_not_en, sid, nid_en); 1153 btorf("%d or %d %d %d\n", nid_a_or_not_en, sid, nid_a, nid_not_en); 1154 btorf("%d constraint %d\n", nid, nid_a_or_not_en); 1155 1156 btorf_pop(log_id(cell)); 1157 } 1158 1159 if (cell->type == ID($assert)) 1160 { 1161 btorf_push(log_id(cell)); 1162 1163 int sid = get_bv_sid(1); 1164 int nid_a = get_sig_nid(cell->getPort(ID::A)); 1165 int nid_en = get_sig_nid(cell->getPort(ID::EN)); 1166 int nid_not_a = next_nid++; 1167 int nid_en_and_not_a = next_nid++; 1168 1169 btorf("%d not %d %d\n", nid_not_a, sid, nid_a); 1170 btorf("%d and %d %d %d\n", nid_en_and_not_a, sid, nid_en, nid_not_a); 1171 1172 if (single_bad && !cover_mode) { 1173 bad_properties.push_back(nid_en_and_not_a); 1174 } else { 1175 if (cover_mode) { 1176 infof("bad %d%s\n", nid_en_and_not_a, getinfo(cell, true).c_str()); 1177 } else { 1178 int nid = next_nid++; 1179 btorf("%d bad %d%s\n", nid, nid_en_and_not_a, getinfo(cell, true).c_str()); 1180 } 1181 } 1182 1183 btorf_pop(log_id(cell)); 1184 } 1185 1186 if (cell->type == ID($cover) && cover_mode) 1187 { 1188 btorf_push(log_id(cell)); 1189 1190 int sid = get_bv_sid(1); 1191 int nid_a = get_sig_nid(cell->getPort(ID::A)); 1192 int nid_en = get_sig_nid(cell->getPort(ID::EN)); 1193 int nid_en_and_a = next_nid++; 1194 1195 btorf("%d and %d %d %d\n", nid_en_and_a, sid, nid_en, nid_a); 1196 1197 if (single_bad) { 1198 bad_properties.push_back(nid_en_and_a); 1199 } else { 1200 int nid = next_nid++; 1201 btorf("%d bad %d%s\n", nid, nid_en_and_a, getinfo(cell, true).c_str()); 1202 } 1203 1204 btorf_pop(log_id(cell)); 1205 } 1206 } 1207 1208 for (auto wire : module->wires()) 1209 { 1210 if (wire->port_id || wire->name[0] == '$') 1211 continue; 1212 1213 btorf_push(stringf("wire %s", log_id(wire))); 1214 1215 int sid = get_bv_sid(GetSize(wire)); 1216 int nid = get_sig_nid(sigmap(wire)); 1217 1218 if (statewires.count(wire)) 1219 continue; 1220 1221 int this_nid = next_nid++; 1222 btorf("%d uext %d %d %d%s\n", this_nid, sid, nid, 0, getinfo(wire).c_str()); 1223 1224 btorf_pop(stringf("wire %s", log_id(wire))); 1225 continue; 1226 } 1227 1228 while (!ff_todo.empty() || !mem_todo.empty()) 1229 { 1230 vector<pair<int, Cell*>> todo; 1231 todo.swap(ff_todo); 1232 1233 for (auto &it : todo) 1234 { 1235 int nid = it.first; 1236 Cell *cell = it.second; 1237 1238 btorf_push(stringf("next %s", log_id(cell))); 1239 1240 SigSpec sig = sigmap(cell->getPort(ID::D)); 1241 int nid_q = get_sig_nid(sig); 1242 int sid = get_bv_sid(GetSize(sig)); 1243 btorf("%d next %d %d %d%s\n", next_nid++, sid, nid, nid_q, getinfo(cell).c_str()); 1244 1245 btorf_pop(stringf("next %s", log_id(cell))); 1246 } 1247 1248 vector<pair<int, Mem*>> mtodo; 1249 mtodo.swap(mem_todo); 1250 1251 for (auto &it : mtodo) 1252 { 1253 int nid = it.first; 1254 Mem *mem = it.second; 1255 1256 btorf_push(stringf("next %s", log_id(mem->memid))); 1257 1258 int abits = ceil_log2(mem->size); 1259 1260 int data_sid = get_bv_sid(mem->width); 1261 int bool_sid = get_bv_sid(1); 1262 int sid = get_mem_sid(abits, mem->width); 1263 int nid_head = nid; 1264 1265 for (auto &port : mem->wr_ports) 1266 { 1267 SigSpec wa = port.addr; 1268 wa.extend_u0(abits); 1269 1270 int wa_nid = get_sig_nid(wa); 1271 int wd_nid = get_sig_nid(port.data); 1272 int we_nid = get_sig_nid(port.en); 1273 1274 int nid2 = next_nid++; 1275 btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid); 1276 1277 int nid3 = next_nid++; 1278 btorf("%d not %d %d\n", nid3, data_sid, we_nid); 1279 1280 int nid4 = next_nid++; 1281 btorf("%d and %d %d %d\n", nid4, data_sid, nid2, nid3); 1282 1283 int nid5 = next_nid++; 1284 btorf("%d and %d %d %d\n", nid5, data_sid, wd_nid, we_nid); 1285 1286 int nid6 = next_nid++; 1287 btorf("%d or %d %d %d\n", nid6, data_sid, nid5, nid4); 1288 1289 int nid7 = next_nid++; 1290 btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6); 1291 1292 int nid8 = next_nid++; 1293 btorf("%d redor %d %d\n", nid8, bool_sid, we_nid); 1294 1295 int nid9 = next_nid++; 1296 btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head); 1297 1298 nid_head = nid9; 1299 } 1300 1301 int nid2 = next_nid++; 1302 btorf("%d next %d %d %d%s\n", nid2, sid, nid, nid_head, (mem->cell ? getinfo(mem->cell) : getinfo(mem->mem)).c_str()); 1303 1304 btorf_pop(stringf("next %s", log_id(mem->memid))); 1305 } 1306 } 1307 1308 while (!bad_properties.empty()) 1309 { 1310 vector<int> todo; 1311 bad_properties.swap(todo); 1312 1313 int sid = get_bv_sid(1); 1314 int cursor = 0; 1315 1316 while (cursor+1 < GetSize(todo)) 1317 { 1318 int nid_a = todo[cursor++]; 1319 int nid_b = todo[cursor++]; 1320 int nid = next_nid++; 1321 1322 bad_properties.push_back(nid); 1323 btorf("%d or %d %d %d\n", nid, sid, nid_a, nid_b); 1324 } 1325 1326 if (!bad_properties.empty()) { 1327 if (cursor < GetSize(todo)) 1328 bad_properties.push_back(todo[cursor++]); 1329 log_assert(cursor == GetSize(todo)); 1330 } else { 1331 int nid = next_nid++; 1332 log_assert(cursor == 0); 1333 log_assert(GetSize(todo) == 1); 1334 btorf("%d bad %d\n", nid, todo[cursor]); 1335 } 1336 } 1337 1338 if (!info_filename.empty()) 1339 { 1340 for (auto &it : info_clocks) 1341 { 1342 switch (it.second) 1343 { 1344 case 1: 1345 infof("posedge %d\n", it.first); 1346 break; 1347 case 2: 1348 infof("negedge %d\n", it.first); 1349 break; 1350 case 3: 1351 infof("event %d\n", it.first); 1352 break; 1353 default: 1354 log_abort(); 1355 } 1356 } 1357 1358 std::ofstream f; 1359 f.open(info_filename.c_str(), std::ofstream::trunc); 1360 if (f.fail()) 1361 log_error("Can't open file `%s' for writing: %s\n", info_filename.c_str(), strerror(errno)); 1362 for (auto &it : info_lines) 1363 f << it; 1364 f.close(); 1365 } 1366 } 1367 }; 1368 1369 struct BtorBackend : public Backend { BtorBackendBtorBackend1370 BtorBackend() : Backend("btor", "write design to BTOR file") { } helpBtorBackend1371 void help() override 1372 { 1373 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| 1374 log("\n"); 1375 log(" write_btor [options] [filename]\n"); 1376 log("\n"); 1377 log("Write a BTOR description of the current design.\n"); 1378 log("\n"); 1379 log(" -v\n"); 1380 log(" Add comments and indentation to BTOR output file\n"); 1381 log("\n"); 1382 log(" -s\n"); 1383 log(" Output only a single bad property for all asserts\n"); 1384 log("\n"); 1385 log(" -c\n"); 1386 log(" Output cover properties using 'bad' statements instead of asserts\n"); 1387 log("\n"); 1388 log(" -i <filename>\n"); 1389 log(" Create additional info file with auxiliary information\n"); 1390 log("\n"); 1391 log(" -x\n"); 1392 log(" Output symbols for internal netnames (starting with '$')\n"); 1393 log("\n"); 1394 } executeBtorBackend1395 void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override 1396 { 1397 bool verbose = false, single_bad = false, cover_mode = false, print_internal_names = false; 1398 string info_filename; 1399 1400 log_header(design, "Executing BTOR backend.\n"); 1401 1402 size_t argidx; 1403 for (argidx = 1; argidx < args.size(); argidx++) 1404 { 1405 if (args[argidx] == "-v") { 1406 verbose = true; 1407 continue; 1408 } 1409 if (args[argidx] == "-s") { 1410 single_bad = true; 1411 continue; 1412 } 1413 if (args[argidx] == "-c") { 1414 cover_mode = true; 1415 continue; 1416 } 1417 if (args[argidx] == "-i" && argidx+1 < args.size()) { 1418 info_filename = args[++argidx]; 1419 continue; 1420 } 1421 if (args[argidx] == "-x") { 1422 print_internal_names = true; 1423 continue; 1424 } 1425 break; 1426 } 1427 extra_args(f, filename, args, argidx); 1428 1429 RTLIL::Module *topmod = design->top_module(); 1430 1431 if (topmod == nullptr) 1432 log_cmd_error("No top module found.\n"); 1433 1434 *f << stringf("; BTOR description generated by %s for module %s.\n", 1435 yosys_version_str, log_id(topmod)); 1436 1437 BtorWorker(*f, topmod, verbose, single_bad, cover_mode, print_internal_names, info_filename); 1438 1439 *f << stringf("; end of yosys output\n"); 1440 } 1441 } BtorBackend; 1442 1443 PRIVATE_NAMESPACE_END 1444