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/rtlil.h" 21 #include "kernel/register.h" 22 #include "kernel/sigtools.h" 23 #include "kernel/celltypes.h" 24 #include "kernel/log.h" 25 #include "kernel/mem.h" 26 #include <string> 27 28 USING_YOSYS_NAMESPACE 29 PRIVATE_NAMESPACE_BEGIN 30 31 struct Smt2Worker 32 { 33 CellTypes ct; 34 SigMap sigmap; 35 RTLIL::Module *module; 36 bool bvmode, memmode, wiresmode, verbose, statebv, statedt, forallmode; 37 dict<IdString, int> &mod_stbv_width; 38 int idcounter = 0, statebv_width = 0; 39 40 std::vector<std::string> decls, trans, hier, dtmembers; 41 std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver; 42 std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue; 43 pool<Cell*> recursive_cells, registers; 44 std::vector<Mem> memories; 45 dict<Cell*, Mem*> mem_cells; 46 std::set<Mem*> memory_queue; 47 48 pool<SigBit> clock_posedge, clock_negedge; 49 vector<string> ex_state_eq, ex_input_eq; 50 51 std::map<RTLIL::SigBit, std::pair<int, int>> fcache; 52 std::map<Mem*, int> memarrays; 53 std::map<int, int> bvsizes; 54 dict<IdString, char*> ids; 55 get_idSmt2Worker56 const char *get_id(IdString n) 57 { 58 if (ids.count(n) == 0) { 59 std::string str = log_id(n); 60 for (int i = 0; i < GetSize(str); i++) { 61 if (str[i] == '\\') 62 str[i] = '/'; 63 } 64 ids[n] = strdup(str.c_str()); 65 } 66 return ids[n]; 67 } 68 69 template<typename T> get_idSmt2Worker70 const char *get_id(T *obj) { 71 return get_id(obj->name); 72 } 73 makebitsSmt2Worker74 void makebits(std::string name, int width = 0, std::string comment = std::string()) 75 { 76 std::string decl_str; 77 78 if (statebv) 79 { 80 if (width == 0) { 81 decl_str = stringf("(define-fun |%s| ((state |%s_s|)) Bool (= ((_ extract %d %d) state) #b1))", name.c_str(), get_id(module), statebv_width, statebv_width); 82 statebv_width += 1; 83 } else { 84 decl_str = stringf("(define-fun |%s| ((state |%s_s|)) (_ BitVec %d) ((_ extract %d %d) state))", name.c_str(), get_id(module), width, statebv_width+width-1, statebv_width); 85 statebv_width += width; 86 } 87 } 88 else if (statedt) 89 { 90 if (width == 0) { 91 decl_str = stringf(" (|%s| Bool)", name.c_str()); 92 } else { 93 decl_str = stringf(" (|%s| (_ BitVec %d))", name.c_str(), width); 94 } 95 } 96 else 97 { 98 if (width == 0) { 99 decl_str = stringf("(declare-fun |%s| (|%s_s|) Bool)", name.c_str(), get_id(module)); 100 } else { 101 decl_str = stringf("(declare-fun |%s| (|%s_s|) (_ BitVec %d))", name.c_str(), get_id(module), width); 102 } 103 } 104 105 if (!comment.empty()) 106 decl_str += " ; " + comment; 107 108 if (statedt) 109 dtmembers.push_back(decl_str + "\n"); 110 else 111 decls.push_back(decl_str + "\n"); 112 } 113 Smt2WorkerSmt2Worker114 Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, bool forallmode, 115 dict<IdString, int> &mod_stbv_width, dict<IdString, dict<IdString, pair<bool, bool>>> &mod_clk_cache) : 116 ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode), 117 verbose(verbose), statebv(statebv), statedt(statedt), forallmode(forallmode), mod_stbv_width(mod_stbv_width) 118 { 119 pool<SigBit> noclock; 120 121 makebits(stringf("%s_is", get_id(module))); 122 123 dict<IdString, Mem*> mem_dict; 124 memories = Mem::get_all_memories(module); 125 for (auto &mem : memories) 126 { 127 mem.narrow(); 128 mem_dict[mem.memid] = &mem; 129 for (auto &port : mem.wr_ports) 130 { 131 if (port.clk_enable) { 132 SigSpec clk = sigmap(port.clk); 133 for (int i = 0; i < GetSize(clk); i++) 134 { 135 if (clk[i].wire == nullptr) 136 continue; 137 if (port.clk_polarity) 138 clock_posedge.insert(clk[i]); 139 else 140 clock_negedge.insert(clk[i]); 141 } 142 } 143 for (auto bit : sigmap(port.en)) 144 noclock.insert(bit); 145 for (auto bit : sigmap(port.addr)) 146 noclock.insert(bit); 147 for (auto bit : sigmap(port.data)) 148 noclock.insert(bit); 149 } 150 for (auto &port : mem.rd_ports) 151 { 152 if (port.clk_enable) { 153 SigSpec clk = sigmap(port.clk); 154 for (int i = 0; i < GetSize(clk); i++) 155 { 156 if (clk[i].wire == nullptr) 157 continue; 158 if (port.clk_polarity) 159 clock_posedge.insert(clk[i]); 160 else 161 clock_negedge.insert(clk[i]); 162 } 163 } 164 for (auto bit : sigmap(port.en)) 165 noclock.insert(bit); 166 for (auto bit : sigmap(port.addr)) 167 noclock.insert(bit); 168 for (auto bit : sigmap(port.data)) 169 noclock.insert(bit); 170 Cell *driver = port.cell ? port.cell : mem.cell; 171 for (auto bit : sigmap(port.data)) { 172 if (bit_driver.count(bit)) 173 log_error("Found multiple drivers for %s.\n", log_signal(bit)); 174 bit_driver[bit] = driver; 175 } 176 } 177 } 178 179 for (auto cell : module->cells()) 180 for (auto &conn : cell->connections()) 181 { 182 if (GetSize(conn.second) == 0) 183 continue; 184 185 // Handled above. 186 if (cell->is_mem_cell()) { 187 mem_cells[cell] = mem_dict[cell->parameters.at(ID::MEMID).decode_string()]; 188 continue; 189 } 190 191 bool is_input = ct.cell_input(cell->type, conn.first); 192 bool is_output = ct.cell_output(cell->type, conn.first); 193 194 if (is_output && !is_input) 195 for (auto bit : sigmap(conn.second)) { 196 if (bit_driver.count(bit)) 197 log_error("Found multiple drivers for %s.\n", log_signal(bit)); 198 bit_driver[bit] = cell; 199 } 200 else if (is_output || !is_input) 201 log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n", 202 log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type)); 203 204 if (cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)) && conn.first.in(ID::CLK, ID::C)) 205 { 206 bool posedge = (cell->type == ID($_DFF_N_)) || (cell->type == ID($dff) && cell->getParam(ID::CLK_POLARITY).as_bool()); 207 for (auto bit : sigmap(conn.second)) { 208 if (posedge) 209 clock_posedge.insert(bit); 210 else 211 clock_negedge.insert(bit); 212 } 213 } 214 else 215 if (mod_clk_cache.count(cell->type) && mod_clk_cache.at(cell->type).count(conn.first)) 216 { 217 for (auto bit : sigmap(conn.second)) { 218 if (mod_clk_cache.at(cell->type).at(conn.first).first) 219 clock_posedge.insert(bit); 220 if (mod_clk_cache.at(cell->type).at(conn.first).second) 221 clock_negedge.insert(bit); 222 } 223 } 224 else 225 { 226 for (auto bit : sigmap(conn.second)) 227 noclock.insert(bit); 228 } 229 } 230 231 for (auto bit : noclock) { 232 clock_posedge.erase(bit); 233 clock_negedge.erase(bit); 234 } 235 236 for (auto wire : module->wires()) 237 { 238 if (!wire->port_input || GetSize(wire) != 1) 239 continue; 240 SigBit bit = sigmap(wire); 241 if (clock_posedge.count(bit)) 242 mod_clk_cache[module->name][wire->name].first = true; 243 if (clock_negedge.count(bit)) 244 mod_clk_cache[module->name][wire->name].second = true; 245 } 246 } 247 ~Smt2WorkerSmt2Worker248 ~Smt2Worker() 249 { 250 for (auto &it : ids) 251 free(it.second); 252 ids.clear(); 253 } 254 get_idSmt2Worker255 const char *get_id(Module *m) 256 { 257 return get_id(m->name); 258 } 259 get_idSmt2Worker260 const char *get_id(Cell *c) 261 { 262 return get_id(c->name); 263 } 264 get_idSmt2Worker265 const char *get_id(Wire *w) 266 { 267 return get_id(w->name); 268 } 269 register_boolSmt2Worker270 void register_bool(RTLIL::SigBit bit, int id) 271 { 272 if (verbose) log("%*s-> register_bool: %s %d\n", 2+2*GetSize(recursive_cells), "", 273 log_signal(bit), id); 274 275 sigmap.apply(bit); 276 log_assert(fcache.count(bit) == 0); 277 fcache[bit] = std::pair<int, int>(id, -1); 278 } 279 register_bvSmt2Worker280 void register_bv(RTLIL::SigSpec sig, int id) 281 { 282 if (verbose) log("%*s-> register_bv: %s %d\n", 2+2*GetSize(recursive_cells), "", 283 log_signal(sig), id); 284 285 log_assert(bvmode); 286 sigmap.apply(sig); 287 288 log_assert(bvsizes.count(id) == 0); 289 bvsizes[id] = GetSize(sig); 290 291 for (int i = 0; i < GetSize(sig); i++) { 292 log_assert(fcache.count(sig[i]) == 0); 293 fcache[sig[i]] = std::pair<int, int>(id, i); 294 } 295 } 296 register_boolvecSmt2Worker297 void register_boolvec(RTLIL::SigSpec sig, int id) 298 { 299 if (verbose) log("%*s-> register_boolvec: %s %d\n", 2+2*GetSize(recursive_cells), "", 300 log_signal(sig), id); 301 302 log_assert(bvmode); 303 sigmap.apply(sig); 304 register_bool(sig[0], id); 305 306 for (int i = 1; i < GetSize(sig); i++) 307 sigmap.add(sig[i], RTLIL::State::S0); 308 } 309 get_boolSmt2Worker310 std::string get_bool(RTLIL::SigBit bit, const char *state_name = "state") 311 { 312 sigmap.apply(bit); 313 314 if (bit.wire == nullptr) 315 return bit == RTLIL::State::S1 ? "true" : "false"; 316 317 if (bit_driver.count(bit)) 318 export_cell(bit_driver.at(bit)); 319 sigmap.apply(bit); 320 321 if (fcache.count(bit) == 0) { 322 if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "", 323 log_signal(bit)); 324 makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(bit)); 325 register_bool(bit, idcounter++); 326 } 327 328 auto f = fcache.at(bit); 329 if (f.second >= 0) 330 return stringf("(= ((_ extract %d %d) (|%s#%d| %s)) #b1)", f.second, f.second, get_id(module), f.first, state_name); 331 return stringf("(|%s#%d| %s)", get_id(module), f.first, state_name); 332 } 333 get_boolSmt2Worker334 std::string get_bool(RTLIL::SigSpec sig, const char *state_name = "state") 335 { 336 return get_bool(sig.as_bit(), state_name); 337 } 338 get_bvSmt2Worker339 std::string get_bv(RTLIL::SigSpec sig, const char *state_name = "state") 340 { 341 log_assert(bvmode); 342 sigmap.apply(sig); 343 344 std::vector<std::string> subexpr; 345 346 SigSpec orig_sig; 347 while (orig_sig != sig) { 348 for (auto bit : sig) 349 if (bit_driver.count(bit)) 350 export_cell(bit_driver.at(bit)); 351 orig_sig = sig; 352 sigmap.apply(sig); 353 } 354 355 for (int i = 0, j = 1; i < GetSize(sig); i += j, j = 1) 356 { 357 if (sig[i].wire == nullptr) { 358 while (i+j < GetSize(sig) && sig[i+j].wire == nullptr) j++; 359 subexpr.push_back("#b"); 360 for (int k = i+j-1; k >= i; k--) 361 subexpr.back() += sig[k] == RTLIL::State::S1 ? "1" : "0"; 362 continue; 363 } 364 365 if (fcache.count(sig[i]) && fcache.at(sig[i]).second == -1) { 366 subexpr.push_back(stringf("(ite %s #b1 #b0)", get_bool(sig[i], state_name).c_str())); 367 continue; 368 } 369 370 if (fcache.count(sig[i])) { 371 auto t1 = fcache.at(sig[i]); 372 while (i+j < GetSize(sig)) { 373 if (fcache.count(sig[i+j]) == 0) 374 break; 375 auto t2 = fcache.at(sig[i+j]); 376 if (t1.first != t2.first) 377 break; 378 if (t1.second+j != t2.second) 379 break; 380 j++; 381 } 382 if (t1.second == 0 && j == bvsizes.at(t1.first)) 383 subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), t1.first, state_name)); 384 else 385 subexpr.push_back(stringf("((_ extract %d %d) (|%s#%d| %s))", 386 t1.second + j - 1, t1.second, get_id(module), t1.first, state_name)); 387 continue; 388 } 389 390 std::set<RTLIL::SigBit> seen_bits = { sig[i] }; 391 while (i+j < GetSize(sig) && sig[i+j].wire && !fcache.count(sig[i+j]) && !seen_bits.count(sig[i+j])) 392 seen_bits.insert(sig[i+j]), j++; 393 394 if (verbose) log("%*s-> external bv: %s\n", 2+2*GetSize(recursive_cells), "", 395 log_signal(sig.extract(i, j))); 396 for (auto bit : sig.extract(i, j)) 397 log_assert(bit_driver.count(bit) == 0); 398 makebits(stringf("%s#%d", get_id(module), idcounter), j, log_signal(sig.extract(i, j))); 399 subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), idcounter, state_name)); 400 register_bv(sig.extract(i, j), idcounter++); 401 } 402 403 if (GetSize(subexpr) > 1) { 404 std::string expr = "", end_str = ""; 405 for (int i = GetSize(subexpr)-1; i >= 0; i--) { 406 if (i > 0) expr += " (concat", end_str += ")"; 407 expr += " " + subexpr[i]; 408 } 409 return expr.substr(1) + end_str; 410 } else { 411 log_assert(GetSize(subexpr) == 1); 412 return subexpr[0]; 413 } 414 } 415 export_gateSmt2Worker416 void export_gate(RTLIL::Cell *cell, std::string expr) 417 { 418 RTLIL::SigBit bit = sigmap(cell->getPort(ID::Y).as_bit()); 419 std::string processed_expr; 420 421 for (char ch : expr) { 422 if (ch == 'A') processed_expr += get_bool(cell->getPort(ID::A)); 423 else if (ch == 'B') processed_expr += get_bool(cell->getPort(ID::B)); 424 else if (ch == 'C') processed_expr += get_bool(cell->getPort(ID::C)); 425 else if (ch == 'D') processed_expr += get_bool(cell->getPort(ID::D)); 426 else if (ch == 'S') processed_expr += get_bool(cell->getPort(ID::S)); 427 else processed_expr += ch; 428 } 429 430 if (verbose) 431 log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell)); 432 433 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n", 434 get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(bit))); 435 register_bool(bit, idcounter++); 436 recursive_cells.erase(cell); 437 } 438 export_bvopSmt2Worker439 void export_bvop(RTLIL::Cell *cell, std::string expr, char type = 0) 440 { 441 RTLIL::SigSpec sig_a, sig_b; 442 RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y)); 443 bool is_signed = cell->getParam(ID::A_SIGNED).as_bool(); 444 int width = GetSize(sig_y); 445 446 if (type == 's' || type == 'd' || type == 'b') { 447 width = max(width, GetSize(cell->getPort(ID::A))); 448 if (cell->hasPort(ID::B)) 449 width = max(width, GetSize(cell->getPort(ID::B))); 450 } 451 452 if (cell->hasPort(ID::A)) { 453 sig_a = cell->getPort(ID::A); 454 sig_a.extend_u0(width, is_signed); 455 } 456 457 if (cell->hasPort(ID::B)) { 458 sig_b = cell->getPort(ID::B); 459 sig_b.extend_u0(width, is_signed && !(type == 's')); 460 } 461 462 std::string processed_expr; 463 464 for (char ch : expr) { 465 if (ch == 'A') processed_expr += get_bv(sig_a); 466 else if (ch == 'B') processed_expr += get_bv(sig_b); 467 else if (ch == 'P') processed_expr += get_bv(cell->getPort(ID::B)); 468 else if (ch == 'L') processed_expr += is_signed ? "a" : "l"; 469 else if (ch == 'U') processed_expr += is_signed ? "s" : "u"; 470 else processed_expr += ch; 471 } 472 473 if (width != GetSize(sig_y) && type != 'b') 474 processed_expr = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, processed_expr.c_str()); 475 476 if (verbose) 477 log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell)); 478 479 if (type == 'b') { 480 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n", 481 get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(sig_y))); 482 register_boolvec(sig_y, idcounter++); 483 } else { 484 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", 485 get_id(module), idcounter, get_id(module), GetSize(sig_y), processed_expr.c_str(), log_signal(sig_y))); 486 register_bv(sig_y, idcounter++); 487 } 488 489 recursive_cells.erase(cell); 490 } 491 export_reduceSmt2Worker492 void export_reduce(RTLIL::Cell *cell, std::string expr, bool identity_val) 493 { 494 RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y)); 495 std::string processed_expr; 496 497 for (char ch : expr) 498 if (ch == 'A' || ch == 'B') { 499 RTLIL::SigSpec sig = sigmap(cell->getPort(stringf("\\%c", ch))); 500 for (auto bit : sig) 501 processed_expr += " " + get_bool(bit); 502 if (GetSize(sig) == 1) 503 processed_expr += identity_val ? " true" : " false"; 504 } else 505 processed_expr += ch; 506 507 if (verbose) 508 log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell)); 509 510 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n", 511 get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(sig_y))); 512 register_boolvec(sig_y, idcounter++); 513 recursive_cells.erase(cell); 514 } 515 export_cellSmt2Worker516 void export_cell(RTLIL::Cell *cell) 517 { 518 if (verbose) 519 log("%*s=> export_cell %s (%s) [%s]\n", 2+2*GetSize(recursive_cells), "", 520 log_id(cell), log_id(cell->type), exported_cells.count(cell) ? "old" : "new"); 521 522 if (recursive_cells.count(cell)) 523 log_error("Found logic loop in module %s! See cell %s.\n", get_id(module), get_id(cell)); 524 525 if (exported_cells.count(cell)) 526 return; 527 528 exported_cells.insert(cell); 529 recursive_cells.insert(cell); 530 531 if (cell->type == ID($initstate)) 532 { 533 SigBit bit = sigmap(cell->getPort(ID::Y).as_bit()); 534 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (|%s_is| state)) ; %s\n", 535 get_id(module), idcounter, get_id(module), get_id(module), log_signal(bit))); 536 register_bool(bit, idcounter++); 537 recursive_cells.erase(cell); 538 return; 539 } 540 541 if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) 542 { 543 registers.insert(cell); 544 makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort(ID::Q))); 545 register_bool(cell->getPort(ID::Q), idcounter++); 546 recursive_cells.erase(cell); 547 return; 548 } 549 550 if (cell->type == ID($_BUF_)) return export_gate(cell, "A"); 551 if (cell->type == ID($_NOT_)) return export_gate(cell, "(not A)"); 552 if (cell->type == ID($_AND_)) return export_gate(cell, "(and A B)"); 553 if (cell->type == ID($_NAND_)) return export_gate(cell, "(not (and A B))"); 554 if (cell->type == ID($_OR_)) return export_gate(cell, "(or A B)"); 555 if (cell->type == ID($_NOR_)) return export_gate(cell, "(not (or A B))"); 556 if (cell->type == ID($_XOR_)) return export_gate(cell, "(xor A B)"); 557 if (cell->type == ID($_XNOR_)) return export_gate(cell, "(not (xor A B))"); 558 if (cell->type == ID($_ANDNOT_)) return export_gate(cell, "(and A (not B))"); 559 if (cell->type == ID($_ORNOT_)) return export_gate(cell, "(or A (not B))"); 560 if (cell->type == ID($_MUX_)) return export_gate(cell, "(ite S B A)"); 561 if (cell->type == ID($_NMUX_)) return export_gate(cell, "(not (ite S B A))"); 562 if (cell->type == ID($_AOI3_)) return export_gate(cell, "(not (or (and A B) C))"); 563 if (cell->type == ID($_OAI3_)) return export_gate(cell, "(not (and (or A B) C))"); 564 if (cell->type == ID($_AOI4_)) return export_gate(cell, "(not (or (and A B) (and C D)))"); 565 if (cell->type == ID($_OAI4_)) return export_gate(cell, "(not (and (or A B) (or C D)))"); 566 567 // FIXME: $lut 568 569 if (bvmode) 570 { 571 if (cell->type.in(ID($ff), ID($dff))) 572 { 573 registers.insert(cell); 574 makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q))); 575 register_bv(cell->getPort(ID::Q), idcounter++); 576 recursive_cells.erase(cell); 577 return; 578 } 579 580 if (cell->type.in(ID($anyconst), ID($anyseq), ID($allconst), ID($allseq))) 581 { 582 registers.insert(cell); 583 string infostr = cell->attributes.count(ID::src) ? cell->attributes.at(ID::src).decode_string().c_str() : get_id(cell); 584 if (cell->attributes.count(ID::reg)) 585 infostr += " " + cell->attributes.at(ID::reg).decode_string(); 586 decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort(ID::Y)), infostr.c_str())); 587 if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::maximize)){ 588 decls.push_back(stringf("; yosys-smt2-maximize %s#%d\n", get_id(module), idcounter)); 589 log("Wire %s is maximized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str()); 590 } 591 else if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::minimize)){ 592 decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter)); 593 log("Wire %s is minimized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str()); 594 } 595 makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Y)), log_signal(cell->getPort(ID::Y))); 596 if (cell->type == ID($anyseq)) 597 ex_input_eq.push_back(stringf(" (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter)); 598 register_bv(cell->getPort(ID::Y), idcounter++); 599 recursive_cells.erase(cell); 600 return; 601 } 602 603 if (cell->type == ID($and)) return export_bvop(cell, "(bvand A B)"); 604 if (cell->type == ID($or)) return export_bvop(cell, "(bvor A B)"); 605 if (cell->type == ID($xor)) return export_bvop(cell, "(bvxor A B)"); 606 if (cell->type == ID($xnor)) return export_bvop(cell, "(bvxnor A B)"); 607 608 if (cell->type == ID($shl)) return export_bvop(cell, "(bvshl A B)", 's'); 609 if (cell->type == ID($shr)) return export_bvop(cell, "(bvlshr A B)", 's'); 610 if (cell->type == ID($sshl)) return export_bvop(cell, "(bvshl A B)", 's'); 611 if (cell->type == ID($sshr)) return export_bvop(cell, "(bvLshr A B)", 's'); 612 613 if (cell->type.in(ID($shift), ID($shiftx))) { 614 if (cell->getParam(ID::B_SIGNED).as_bool()) { 615 return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) " 616 "(bvlshr A B) (bvlshr A (bvneg B)))", 617 GetSize(cell->getPort(ID::B)), 0), 's'); 618 } else { 619 return export_bvop(cell, "(bvlshr A B)", 's'); 620 } 621 } 622 623 if (cell->type == ID($lt)) return export_bvop(cell, "(bvUlt A B)", 'b'); 624 if (cell->type == ID($le)) return export_bvop(cell, "(bvUle A B)", 'b'); 625 if (cell->type == ID($ge)) return export_bvop(cell, "(bvUge A B)", 'b'); 626 if (cell->type == ID($gt)) return export_bvop(cell, "(bvUgt A B)", 'b'); 627 628 if (cell->type == ID($ne)) return export_bvop(cell, "(distinct A B)", 'b'); 629 if (cell->type == ID($nex)) return export_bvop(cell, "(distinct A B)", 'b'); 630 if (cell->type == ID($eq)) return export_bvop(cell, "(= A B)", 'b'); 631 if (cell->type == ID($eqx)) return export_bvop(cell, "(= A B)", 'b'); 632 633 if (cell->type == ID($not)) return export_bvop(cell, "(bvnot A)"); 634 if (cell->type == ID($pos)) return export_bvop(cell, "A"); 635 if (cell->type == ID($neg)) return export_bvop(cell, "(bvneg A)"); 636 637 if (cell->type == ID($add)) return export_bvop(cell, "(bvadd A B)"); 638 if (cell->type == ID($sub)) return export_bvop(cell, "(bvsub A B)"); 639 if (cell->type == ID($mul)) return export_bvop(cell, "(bvmul A B)"); 640 if (cell->type == ID($div)) return export_bvop(cell, "(bvUdiv A B)", 'd'); 641 // "rem" = truncating modulo 642 if (cell->type == ID($mod)) return export_bvop(cell, "(bvUrem A B)", 'd'); 643 // "mod" = flooring modulo 644 if (cell->type == ID($modfloor)) { 645 // bvumod doesn't exist because it's the same as bvurem 646 if (cell->getParam(ID::A_SIGNED).as_bool()) { 647 return export_bvop(cell, "(bvsmod A B)", 'd'); 648 } else { 649 return export_bvop(cell, "(bvurem A B)", 'd'); 650 } 651 } 652 653 if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool)) && 654 2*GetSize(cell->getPort(ID::A).chunks()) < GetSize(cell->getPort(ID::A))) { 655 bool is_and = cell->type == ID($reduce_and); 656 string bits(GetSize(cell->getPort(ID::A)), is_and ? '1' : '0'); 657 return export_bvop(cell, stringf("(%s A #b%s)", is_and ? "=" : "distinct", bits.c_str()), 'b'); 658 } 659 660 if (cell->type == ID($reduce_and)) return export_reduce(cell, "(and A)", true); 661 if (cell->type == ID($reduce_or)) return export_reduce(cell, "(or A)", false); 662 if (cell->type == ID($reduce_xor)) return export_reduce(cell, "(xor A)", false); 663 if (cell->type == ID($reduce_xnor)) return export_reduce(cell, "(not (xor A))", false); 664 if (cell->type == ID($reduce_bool)) return export_reduce(cell, "(or A)", false); 665 666 if (cell->type == ID($logic_not)) return export_reduce(cell, "(not (or A))", false); 667 if (cell->type == ID($logic_and)) return export_reduce(cell, "(and (or A) (or B))", false); 668 if (cell->type == ID($logic_or)) return export_reduce(cell, "(or A B)", false); 669 670 if (cell->type.in(ID($mux), ID($pmux))) 671 { 672 int width = GetSize(cell->getPort(ID::Y)); 673 std::string processed_expr = get_bv(cell->getPort(ID::A)); 674 675 RTLIL::SigSpec sig_b = cell->getPort(ID::B); 676 RTLIL::SigSpec sig_s = cell->getPort(ID::S); 677 get_bv(sig_b); 678 get_bv(sig_s); 679 680 for (int i = 0; i < GetSize(sig_s); i++) 681 processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(), 682 get_bv(sig_b.extract(i*width, width)).c_str(), processed_expr.c_str()); 683 684 if (verbose) 685 log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell)); 686 687 RTLIL::SigSpec sig = sigmap(cell->getPort(ID::Y)); 688 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", 689 get_id(module), idcounter, get_id(module), width, processed_expr.c_str(), log_signal(sig))); 690 register_bv(sig, idcounter++); 691 recursive_cells.erase(cell); 692 return; 693 } 694 695 // FIXME: $slice $concat 696 } 697 698 if (memmode && cell->is_mem_cell()) 699 { 700 Mem *mem = mem_cells[cell]; 701 702 if (memarrays.count(mem)) { 703 recursive_cells.erase(cell); 704 return; 705 } 706 707 int arrayid = idcounter++; 708 memarrays[mem] = arrayid; 709 710 int abits = ceil_log2(mem->size); 711 712 bool has_sync_wr = false; 713 bool has_async_wr = false; 714 for (auto &port : mem->wr_ports) { 715 if (port.clk_enable) 716 has_sync_wr = true; 717 else 718 has_async_wr = true; 719 } 720 if (has_async_wr && has_sync_wr) 721 log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module)); 722 723 decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(mem->memid), abits, mem->width, GetSize(mem->rd_ports), GetSize(mem->wr_ports), has_async_wr ? "async" : "sync")); 724 725 string memstate; 726 if (has_async_wr) { 727 memstate = stringf("%s#%d#final", get_id(module), arrayid); 728 } else { 729 memstate = stringf("%s#%d#0", get_id(module), arrayid); 730 } 731 732 if (statebv) 733 { 734 makebits(memstate, mem->width*mem->size, get_id(mem->memid)); 735 decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s| state))\n", 736 get_id(module), get_id(mem->memid), get_id(module), mem->width*mem->size, memstate.c_str())); 737 738 for (int i = 0; i < GetSize(mem->rd_ports); i++) 739 { 740 auto &port = mem->rd_ports[i]; 741 SigSpec addr_sig = port.addr; 742 addr_sig.extend_u0(abits); 743 std::string addr = get_bv(addr_sig); 744 745 if (port.clk_enable) 746 log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! " 747 "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(port.data), log_id(mem->memid), log_id(module)); 748 749 decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", 750 get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); 751 752 std::string read_expr = "#b"; 753 for (int k = 0; k < mem->width; k++) 754 read_expr += "0"; 755 756 for (int k = 0; k < mem->size; k++) 757 read_expr = stringf("(ite (= (|%s_m:R%dA %s| state) #b%s) ((_ extract %d %d) (|%s| state))\n %s)", 758 get_id(module), i, get_id(mem->memid), Const(k+mem->start_offset, abits).as_string().c_str(), 759 mem->width*(k+1)-1, mem->width*k, memstate.c_str(), read_expr.c_str()); 760 761 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d)\n %s) ; %s\n", 762 get_id(module), idcounter, get_id(module), mem->width, read_expr.c_str(), log_signal(port.data))); 763 764 decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n", 765 get_id(module), i, get_id(mem->memid), get_id(module), mem->width, get_id(module), idcounter)); 766 767 register_bv(port.data, idcounter++); 768 } 769 } 770 else 771 { 772 if (statedt) 773 dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", 774 memstate.c_str(), abits, mem->width, get_id(mem->memid))); 775 else 776 decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", 777 memstate.c_str(), get_id(module), abits, mem->width, get_id(mem->memid))); 778 779 decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s| state))\n", 780 get_id(module), get_id(mem->memid), get_id(module), abits, mem->width, memstate.c_str())); 781 782 for (int i = 0; i < GetSize(mem->rd_ports); i++) 783 { 784 auto &port = mem->rd_ports[i]; 785 SigSpec addr_sig = port.addr; 786 addr_sig.extend_u0(abits); 787 std::string addr = get_bv(addr_sig); 788 789 if (port.clk_enable) 790 log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! " 791 "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(port.data), log_id(mem->memid), log_id(module)); 792 793 decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", 794 get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); 795 796 decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s| state) (|%s_m:R%dA %s| state))) ; %s\n", 797 get_id(module), idcounter, get_id(module), mem->width, memstate.c_str(), get_id(module), i, get_id(mem->memid), log_signal(port.data))); 798 799 decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n", 800 get_id(module), i, get_id(mem->memid), get_id(module), mem->width, get_id(module), idcounter)); 801 802 register_bv(port.data, idcounter++); 803 } 804 } 805 806 memory_queue.insert(mem); 807 recursive_cells.erase(cell); 808 return; 809 } 810 811 Module *m = module->design->module(cell->type); 812 813 if (m != nullptr) 814 { 815 decls.push_back(stringf("; yosys-smt2-cell %s %s\n", get_id(cell->type), get_id(cell->name))); 816 string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name)); 817 818 for (auto &conn : cell->connections()) 819 { 820 if (GetSize(conn.second) == 0) 821 continue; 822 823 Wire *w = m->wire(conn.first); 824 SigSpec sig = sigmap(conn.second); 825 826 if (w->port_output && !w->port_input) { 827 if (GetSize(w) > 1) { 828 if (bvmode) { 829 makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(w), log_signal(sig)); 830 register_bv(sig, idcounter++); 831 } else { 832 for (int i = 0; i < GetSize(w); i++) { 833 makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(sig[i])); 834 register_bool(sig[i], idcounter++); 835 } 836 } 837 } else { 838 makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(sig)); 839 register_bool(sig, idcounter++); 840 } 841 } 842 } 843 844 if (statebv) 845 makebits(stringf("%s_h %s", get_id(module), get_id(cell->name)), mod_stbv_width.at(cell->type)); 846 else if (statedt) 847 dtmembers.push_back(stringf(" (|%s_h %s| |%s_s|)\n", 848 get_id(module), get_id(cell->name), get_id(cell->type))); 849 else 850 decls.push_back(stringf("(declare-fun |%s_h %s| (|%s_s|) |%s_s|)\n", 851 get_id(module), get_id(cell->name), get_id(module), get_id(cell->type))); 852 853 hiercells.insert(cell); 854 hiercells_queue.insert(cell); 855 recursive_cells.erase(cell); 856 return; 857 } 858 859 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)) { 860 log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smt2`.\n", 861 log_id(cell->type), log_id(module), log_id(cell)); 862 } 863 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") { 864 log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smt2`.\n", 865 log_id(cell->type), log_id(module), log_id(cell)); 866 } 867 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_") { 868 log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_smt2`.\n", 869 log_id(cell->type), log_id(module), log_id(cell)); 870 } 871 log_error("Unsupported cell type %s for cell %s.%s.\n", 872 log_id(cell->type), log_id(module), log_id(cell)); 873 } 874 runSmt2Worker875 void run() 876 { 877 if (verbose) log("=> export logic driving outputs\n"); 878 879 pool<SigBit> reg_bits; 880 for (auto cell : module->cells()) 881 if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) { 882 // not using sigmap -- we want the net directly at the dff output 883 for (auto bit : cell->getPort(ID::Q)) 884 reg_bits.insert(bit); 885 } 886 887 for (auto wire : module->wires()) { 888 bool is_register = false; 889 for (auto bit : SigSpec(wire)) 890 if (reg_bits.count(bit)) 891 is_register = true; 892 if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) { 893 RTLIL::SigSpec sig = sigmap(wire); 894 std::vector<std::string> comments; 895 if (wire->port_input) 896 comments.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width)); 897 if (wire->port_output) 898 comments.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width)); 899 if (is_register) 900 comments.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width)); 901 if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) 902 comments.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width)); 903 if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig))) 904 comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire), 905 clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : "")); 906 if (bvmode && GetSize(sig) > 1) { 907 std::string sig_bv = get_bv(sig); 908 if (!comments.empty()) 909 decls.insert(decls.end(), comments.begin(), comments.end()); 910 decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n", 911 get_id(module), get_id(wire), get_id(module), GetSize(sig), sig_bv.c_str())); 912 if (wire->port_input) 913 ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", 914 get_id(module), get_id(wire), get_id(module), get_id(wire))); 915 } else { 916 std::vector<std::string> sig_bool; 917 for (int i = 0; i < GetSize(sig); i++) { 918 sig_bool.push_back(get_bool(sig[i])); 919 } 920 if (!comments.empty()) 921 decls.insert(decls.end(), comments.begin(), comments.end()); 922 for (int i = 0; i < GetSize(sig); i++) { 923 if (GetSize(sig) > 1) { 924 decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n", 925 get_id(module), get_id(wire), i, get_id(module), sig_bool[i].c_str())); 926 if (wire->port_input) 927 ex_input_eq.push_back(stringf(" (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))", 928 get_id(module), get_id(wire), i, get_id(module), get_id(wire), i)); 929 } else { 930 decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n", 931 get_id(module), get_id(wire), get_id(module), sig_bool[i].c_str())); 932 if (wire->port_input) 933 ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", 934 get_id(module), get_id(wire), get_id(module), get_id(wire))); 935 } 936 } 937 } 938 } 939 } 940 941 if (verbose) log("=> export logic associated with the initial state\n"); 942 943 vector<string> init_list; 944 for (auto wire : module->wires()) 945 if (wire->attributes.count(ID::init)) { 946 RTLIL::SigSpec sig = sigmap(wire); 947 Const val = wire->attributes.at(ID::init); 948 val.bits.resize(GetSize(sig), State::Sx); 949 if (bvmode && GetSize(sig) > 1) { 950 Const mask(State::S1, GetSize(sig)); 951 bool use_mask = false; 952 for (int i = 0; i < GetSize(sig); i++) 953 if (val[i] != State::S0 && val[i] != State::S1) { 954 val[i] = State::S0; 955 mask[i] = State::S0; 956 use_mask = true; 957 } 958 if (use_mask) 959 init_list.push_back(stringf("(= (bvand %s #b%s) #b%s) ; %s", get_bv(sig).c_str(), mask.as_string().c_str(), val.as_string().c_str(), get_id(wire))); 960 else 961 init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), get_id(wire))); 962 } else { 963 for (int i = 0; i < GetSize(sig); i++) 964 if (val[i] == State::S0 || val[i] == State::S1) 965 init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val[i] == State::S1 ? "true" : "false", get_id(wire))); 966 } 967 } 968 969 if (verbose) log("=> export logic driving asserts\n"); 970 971 int assert_id = 0, assume_id = 0, cover_id = 0; 972 vector<string> assert_list, assume_list, cover_list; 973 974 for (auto cell : module->cells()) 975 { 976 if (cell->type.in(ID($assert), ID($assume), ID($cover))) 977 { 978 int &id = cell->type == ID($assert) ? assert_id : 979 cell->type == ID($assume) ? assume_id : 980 cell->type == ID($cover) ? cover_id : *(int*)nullptr; 981 982 char postfix = cell->type == ID($assert) ? 'a' : 983 cell->type == ID($assume) ? 'u' : 984 cell->type == ID($cover) ? 'c' : 0; 985 986 string name_a = get_bool(cell->getPort(ID::A)); 987 string name_en = get_bool(cell->getPort(ID::EN)); 988 string infostr = (cell->name[0] == '$' && cell->attributes.count(ID::src)) ? cell->attributes.at(ID::src).decode_string() : get_id(cell); 989 decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str())); 990 991 if (cell->type == ID($cover)) 992 decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n", 993 get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell))); 994 else 995 decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n", 996 get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell))); 997 998 if (cell->type == ID($assert)) 999 assert_list.push_back(stringf("(|%s_a %d| state)", get_id(module), id)); 1000 else if (cell->type == ID($assume)) 1001 assume_list.push_back(stringf("(|%s_u %d| state)", get_id(module), id)); 1002 1003 id++; 1004 } 1005 } 1006 1007 if (verbose) log("=> export logic driving hierarchical cells\n"); 1008 1009 for (auto cell : module->cells()) 1010 if (module->design->module(cell->type) != nullptr) 1011 export_cell(cell); 1012 1013 while (!hiercells_queue.empty()) 1014 { 1015 std::set<RTLIL::Cell*> queue; 1016 queue.swap(hiercells_queue); 1017 1018 for (auto cell : queue) 1019 { 1020 string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name)); 1021 Module *m = module->design->module(cell->type); 1022 log_assert(m != nullptr); 1023 1024 hier.push_back(stringf(" (= (|%s_is| state) (|%s_is| %s))\n", 1025 get_id(module), get_id(cell->type), cell_state.c_str())); 1026 1027 for (auto &conn : cell->connections()) 1028 { 1029 if (GetSize(conn.second) == 0) 1030 continue; 1031 1032 Wire *w = m->wire(conn.first); 1033 SigSpec sig = sigmap(conn.second); 1034 1035 if (bvmode || GetSize(w) == 1) { 1036 hier.push_back(stringf(" (= %s (|%s_n %s| %s)) ; %s.%s\n", (GetSize(w) > 1 ? get_bv(sig) : get_bool(sig)).c_str(), 1037 get_id(cell->type), get_id(w), cell_state.c_str(), get_id(cell->type), get_id(w))); 1038 } else { 1039 for (int i = 0; i < GetSize(w); i++) 1040 hier.push_back(stringf(" (= %s (|%s_n %s %d| %s)) ; %s.%s[%d]\n", get_bool(sig[i]).c_str(), 1041 get_id(cell->type), get_id(w), i, cell_state.c_str(), get_id(cell->type), get_id(w), i)); 1042 } 1043 } 1044 } 1045 } 1046 1047 for (int iter = 1; !registers.empty() || !memory_queue.empty(); iter++) 1048 { 1049 pool<Cell*> this_regs; 1050 this_regs.swap(registers); 1051 1052 if (verbose) log("=> export logic driving registers [iteration %d]\n", iter); 1053 1054 for (auto cell : this_regs) 1055 { 1056 if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) 1057 { 1058 std::string expr_d = get_bool(cell->getPort(ID::D)); 1059 std::string expr_q = get_bool(cell->getPort(ID::Q), "next_state"); 1060 trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort(ID::Q)))); 1061 ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort(ID::Q)).c_str(), get_bool(cell->getPort(ID::Q), "other_state").c_str())); 1062 } 1063 1064 if (cell->type.in(ID($ff), ID($dff))) 1065 { 1066 std::string expr_d = get_bv(cell->getPort(ID::D)); 1067 std::string expr_q = get_bv(cell->getPort(ID::Q), "next_state"); 1068 trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort(ID::Q)))); 1069 ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Q)).c_str(), get_bv(cell->getPort(ID::Q), "other_state").c_str())); 1070 } 1071 1072 if (cell->type.in(ID($anyconst), ID($allconst))) 1073 { 1074 std::string expr_d = get_bv(cell->getPort(ID::Y)); 1075 std::string expr_q = get_bv(cell->getPort(ID::Y), "next_state"); 1076 trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort(ID::Y)))); 1077 if (cell->type == ID($anyconst)) 1078 ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Y)).c_str(), get_bv(cell->getPort(ID::Y), "other_state").c_str())); 1079 } 1080 } 1081 1082 std::set<Mem*> this_mems; 1083 this_mems.swap(memory_queue); 1084 1085 for (auto mem : this_mems) 1086 { 1087 int arrayid = memarrays.at(mem); 1088 1089 int abits = ceil_log2(mem->size);; 1090 1091 bool has_sync_wr = false; 1092 bool has_async_wr = false; 1093 for (auto &port : mem->wr_ports) { 1094 if (port.clk_enable) 1095 has_sync_wr = true; 1096 else 1097 has_async_wr = true; 1098 } 1099 1100 string initial_memstate, final_memstate; 1101 1102 if (has_async_wr) { 1103 log_assert(!has_sync_wr); 1104 initial_memstate = stringf("%s#%d#0", get_id(module), arrayid); 1105 final_memstate = stringf("%s#%d#final", get_id(module), arrayid); 1106 } 1107 1108 if (statebv) 1109 { 1110 if (has_async_wr) { 1111 makebits(final_memstate, mem->width*mem->size, get_id(mem->memid)); 1112 } 1113 1114 for (int i = 0; i < GetSize(mem->wr_ports); i++) 1115 { 1116 auto &port = mem->wr_ports[i]; 1117 SigSpec addr_sig = port.addr; 1118 addr_sig.extend_u0(abits); 1119 1120 std::string addr = get_bv(addr_sig); 1121 std::string data = get_bv(port.data); 1122 std::string mask = get_bv(port.en); 1123 1124 decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", 1125 get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); 1126 addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(mem->memid)); 1127 1128 decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", 1129 get_id(module), i, get_id(mem->memid), get_id(module), mem->width, data.c_str(), log_signal(port.data))); 1130 data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(mem->memid)); 1131 1132 decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", 1133 get_id(module), i, get_id(mem->memid), get_id(module), mem->width, mask.c_str(), log_signal(port.en))); 1134 mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid)); 1135 1136 std::string data_expr; 1137 1138 for (int k = mem->size-1; k >= 0; k--) { 1139 std::string new_data = stringf("(bvor (bvand %s %s) (bvand ((_ extract %d %d) (|%s#%d#%d| state)) (bvnot %s)))", 1140 data.c_str(), mask.c_str(), mem->width*(k+1)-1, mem->width*k, get_id(module), arrayid, i, mask.c_str()); 1141 data_expr += stringf("\n (ite (= %s #b%s) %s ((_ extract %d %d) (|%s#%d#%d| state)))", 1142 addr.c_str(), Const(k+mem->start_offset, abits).as_string().c_str(), new_data.c_str(), 1143 mem->width*(k+1)-1, mem->width*k, get_id(module), arrayid, i); 1144 } 1145 1146 decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (_ BitVec %d) (concat%s)) ; %s\n", 1147 get_id(module), arrayid, i+1, get_id(module), mem->width*mem->size, data_expr.c_str(), get_id(mem->memid))); 1148 } 1149 } 1150 else 1151 { 1152 if (has_async_wr) { 1153 if (statedt) 1154 dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", 1155 initial_memstate.c_str(), abits, mem->width, get_id(mem->memid))); 1156 else 1157 decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", 1158 initial_memstate.c_str(), get_id(module), abits, mem->width, get_id(mem->memid))); 1159 } 1160 1161 for (int i = 0; i < GetSize(mem->wr_ports); i++) 1162 { 1163 auto &port = mem->wr_ports[i]; 1164 SigSpec addr_sig = port.addr; 1165 addr_sig.extend_u0(abits); 1166 1167 std::string addr = get_bv(addr_sig); 1168 std::string data = get_bv(port.data); 1169 std::string mask = get_bv(port.en); 1170 1171 decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", 1172 get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); 1173 addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(mem->memid)); 1174 1175 decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", 1176 get_id(module), i, get_id(mem->memid), get_id(module), mem->width, data.c_str(), log_signal(port.data))); 1177 data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(mem->memid)); 1178 1179 decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", 1180 get_id(module), i, get_id(mem->memid), get_id(module), mem->width, mask.c_str(), log_signal(port.en))); 1181 mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid)); 1182 1183 data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))", 1184 data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str()); 1185 1186 decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) " 1187 "(store (|%s#%d#%d| state) %s %s)) ; %s\n", 1188 get_id(module), arrayid, i+1, get_id(module), abits, mem->width, 1189 get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid))); 1190 } 1191 } 1192 1193 std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, GetSize(mem->wr_ports)); 1194 std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid); 1195 trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(mem->memid))); 1196 ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid)); 1197 1198 if (has_async_wr) 1199 hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(mem->memid))); 1200 1201 Const init_data = mem->get_init_data(); 1202 1203 for (int i = 0; i < mem->size; i++) 1204 { 1205 if (i*mem->width >= GetSize(init_data)) 1206 break; 1207 1208 Const initword = init_data.extract(i*mem->width, mem->width, State::Sx); 1209 Const initmask = initword; 1210 bool gen_init_constr = false; 1211 1212 for (int k = 0; k < GetSize(initword); k++) { 1213 if (initword[k] == State::S0 || initword[k] == State::S1) { 1214 gen_init_constr = true; 1215 initmask[k] = State::S1; 1216 } else { 1217 initmask[k] = State::S0; 1218 initword[k] = State::S0; 1219 } 1220 } 1221 1222 if (gen_init_constr) 1223 { 1224 if (statebv) 1225 /* FIXME */; 1226 else 1227 init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]", 1228 get_id(module), arrayid, Const(i, abits).as_string().c_str(), 1229 initmask.as_string().c_str(), initword.as_string().c_str(), get_id(mem->memid), i)); 1230 } 1231 } 1232 } 1233 } 1234 1235 if (verbose) log("=> finalizing SMT2 representation of %s.\n", log_id(module)); 1236 1237 for (auto c : hiercells) { 1238 assert_list.push_back(stringf("(|%s_a| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name))); 1239 assume_list.push_back(stringf("(|%s_u| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name))); 1240 init_list.push_back(stringf("(|%s_i| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name))); 1241 hier.push_back(stringf(" (|%s_h| (|%s_h %s| state))\n", get_id(c->type), get_id(module), get_id(c->name))); 1242 trans.push_back(stringf(" (|%s_t| (|%s_h %s| state) (|%s_h %s| next_state))\n", 1243 get_id(c->type), get_id(module), get_id(c->name), get_id(module), get_id(c->name))); 1244 ex_state_eq.push_back(stringf("(|%s_ex_state_eq| (|%s_h %s| state) (|%s_h %s| other_state))\n", 1245 get_id(c->type), get_id(module), get_id(c->name), get_id(module), get_id(c->name))); 1246 } 1247 1248 if (forallmode) 1249 { 1250 string expr = ex_state_eq.empty() ? "true" : "(and"; 1251 if (!ex_state_eq.empty()) { 1252 if (GetSize(ex_state_eq) == 1) { 1253 expr = "\n " + ex_state_eq.front() + "\n"; 1254 } else { 1255 for (auto &str : ex_state_eq) 1256 expr += stringf("\n %s", str.c_str()); 1257 expr += "\n)"; 1258 } 1259 } 1260 decls.push_back(stringf("(define-fun |%s_ex_state_eq| ((state |%s_s|) (other_state |%s_s|)) Bool %s)\n", 1261 get_id(module), get_id(module), get_id(module), expr.c_str())); 1262 1263 expr = ex_input_eq.empty() ? "true" : "(and"; 1264 if (!ex_input_eq.empty()) { 1265 if (GetSize(ex_input_eq) == 1) { 1266 expr = "\n " + ex_input_eq.front() + "\n"; 1267 } else { 1268 for (auto &str : ex_input_eq) 1269 expr += stringf("\n %s", str.c_str()); 1270 expr += "\n)"; 1271 } 1272 } 1273 decls.push_back(stringf("(define-fun |%s_ex_input_eq| ((state |%s_s|) (other_state |%s_s|)) Bool %s)\n", 1274 get_id(module), get_id(module), get_id(module), expr.c_str())); 1275 } 1276 1277 string assert_expr = assert_list.empty() ? "true" : "(and"; 1278 if (!assert_list.empty()) { 1279 if (GetSize(assert_list) == 1) { 1280 assert_expr = "\n " + assert_list.front() + "\n"; 1281 } else { 1282 for (auto &str : assert_list) 1283 assert_expr += stringf("\n %s", str.c_str()); 1284 assert_expr += "\n)"; 1285 } 1286 } 1287 decls.push_back(stringf("(define-fun |%s_a| ((state |%s_s|)) Bool %s)\n", 1288 get_id(module), get_id(module), assert_expr.c_str())); 1289 1290 string assume_expr = assume_list.empty() ? "true" : "(and"; 1291 if (!assume_list.empty()) { 1292 if (GetSize(assume_list) == 1) { 1293 assume_expr = "\n " + assume_list.front() + "\n"; 1294 } else { 1295 for (auto &str : assume_list) 1296 assume_expr += stringf("\n %s", str.c_str()); 1297 assume_expr += "\n)"; 1298 } 1299 } 1300 decls.push_back(stringf("(define-fun |%s_u| ((state |%s_s|)) Bool %s)\n", 1301 get_id(module), get_id(module), assume_expr.c_str())); 1302 1303 string init_expr = init_list.empty() ? "true" : "(and"; 1304 if (!init_list.empty()) { 1305 if (GetSize(init_list) == 1) { 1306 init_expr = "\n " + init_list.front() + "\n"; 1307 } else { 1308 for (auto &str : init_list) 1309 init_expr += stringf("\n %s", str.c_str()); 1310 init_expr += "\n)"; 1311 } 1312 } 1313 decls.push_back(stringf("(define-fun |%s_i| ((state |%s_s|)) Bool %s)\n", 1314 get_id(module), get_id(module), init_expr.c_str())); 1315 } 1316 writeSmt2Worker1317 void write(std::ostream &f) 1318 { 1319 f << stringf("; yosys-smt2-module %s\n", get_id(module)); 1320 1321 if (statebv) { 1322 f << stringf("(define-sort |%s_s| () (_ BitVec %d))\n", get_id(module), statebv_width); 1323 mod_stbv_width[module->name] = statebv_width; 1324 } else 1325 if (statedt) { 1326 f << stringf("(declare-datatype |%s_s| ((|%s_mk|\n", get_id(module), get_id(module)); 1327 for (auto it : dtmembers) 1328 f << it; 1329 f << stringf(")))\n"); 1330 } else 1331 f << stringf("(declare-sort |%s_s| 0)\n", get_id(module)); 1332 1333 for (auto it : decls) 1334 f << it; 1335 1336 f << stringf("(define-fun |%s_h| ((state |%s_s|)) Bool ", get_id(module), get_id(module)); 1337 if (GetSize(hier) > 1) { 1338 f << "(and\n"; 1339 for (auto it : hier) 1340 f << it; 1341 f << "))\n"; 1342 } else 1343 if (GetSize(hier) == 1) 1344 f << "\n" + hier.front() + ")\n"; 1345 else 1346 f << "true)\n"; 1347 1348 f << stringf("(define-fun |%s_t| ((state |%s_s|) (next_state |%s_s|)) Bool ", get_id(module), get_id(module), get_id(module)); 1349 if (GetSize(trans) > 1) { 1350 f << "(and\n"; 1351 for (auto it : trans) 1352 f << it; 1353 f << "))"; 1354 } else 1355 if (GetSize(trans) == 1) 1356 f << "\n" + trans.front() + ")"; 1357 else 1358 f << "true)"; 1359 f << stringf(" ; end of module %s\n", get_id(module)); 1360 } 1361 }; 1362 1363 struct Smt2Backend : public Backend { Smt2BackendSmt2Backend1364 Smt2Backend() : Backend("smt2", "write design to SMT-LIBv2 file") { } helpSmt2Backend1365 void help() override 1366 { 1367 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| 1368 log("\n"); 1369 log(" write_smt2 [options] [filename]\n"); 1370 log("\n"); 1371 log("Write a SMT-LIBv2 [1] description of the current design. For a module with name\n"); 1372 log("'<mod>' this will declare the sort '<mod>_s' (state of the module) and will\n"); 1373 log("define and declare functions operating on that state.\n"); 1374 log("\n"); 1375 log("The following SMT2 functions are generated for a module with name '<mod>'.\n"); 1376 log("Some declarations/definitions are printed with a special comment. A prover\n"); 1377 log("using the SMT2 files can use those comments to collect all relevant metadata\n"); 1378 log("about the design.\n"); 1379 log("\n"); 1380 log(" ; yosys-smt2-module <mod>\n"); 1381 log(" (declare-sort |<mod>_s| 0)\n"); 1382 log(" The sort representing a state of module <mod>.\n"); 1383 log("\n"); 1384 log(" (define-fun |<mod>_h| ((state |<mod>_s|)) Bool (...))\n"); 1385 log(" This function must be asserted for each state to establish the\n"); 1386 log(" design hierarchy.\n"); 1387 log("\n"); 1388 log(" ; yosys-smt2-input <wirename> <width>\n"); 1389 log(" ; yosys-smt2-output <wirename> <width>\n"); 1390 log(" ; yosys-smt2-register <wirename> <width>\n"); 1391 log(" ; yosys-smt2-wire <wirename> <width>\n"); 1392 log(" (define-fun |<mod>_n <wirename>| (|<mod>_s|) (_ BitVec <width>))\n"); 1393 log(" (define-fun |<mod>_n <wirename>| (|<mod>_s|) Bool)\n"); 1394 log(" For each port, register, and wire with the 'keep' attribute set an\n"); 1395 log(" accessor function is generated. Single-bit wires are returned as Bool,\n"); 1396 log(" multi-bit wires as BitVec.\n"); 1397 log("\n"); 1398 log(" ; yosys-smt2-cell <submod> <instancename>\n"); 1399 log(" (declare-fun |<mod>_h <instancename>| (|<mod>_s|) |<submod>_s|)\n"); 1400 log(" There is a function like that for each hierarchical instance. It\n"); 1401 log(" returns the sort that represents the state of the sub-module that\n"); 1402 log(" implements the instance.\n"); 1403 log("\n"); 1404 log(" (declare-fun |<mod>_is| (|<mod>_s|) Bool)\n"); 1405 log(" This function must be asserted 'true' for initial states, and 'false'\n"); 1406 log(" otherwise.\n"); 1407 log("\n"); 1408 log(" (define-fun |<mod>_i| ((state |<mod>_s|)) Bool (...))\n"); 1409 log(" This function must be asserted 'true' for initial states. For\n"); 1410 log(" non-initial states it must be left unconstrained.\n"); 1411 log("\n"); 1412 log(" (define-fun |<mod>_t| ((state |<mod>_s|) (next_state |<mod>_s|)) Bool (...))\n"); 1413 log(" This function evaluates to 'true' if the states 'state' and\n"); 1414 log(" 'next_state' form a valid state transition.\n"); 1415 log("\n"); 1416 log(" (define-fun |<mod>_a| ((state |<mod>_s|)) Bool (...))\n"); 1417 log(" This function evaluates to 'true' if all assertions hold in the state.\n"); 1418 log("\n"); 1419 log(" (define-fun |<mod>_u| ((state |<mod>_s|)) Bool (...))\n"); 1420 log(" This function evaluates to 'true' if all assumptions hold in the state.\n"); 1421 log("\n"); 1422 log(" ; yosys-smt2-assert <id> <filename:linenum>\n"); 1423 log(" (define-fun |<mod>_a <id>| ((state |<mod>_s|)) Bool (...))\n"); 1424 log(" Each $assert cell is converted into one of this functions. The function\n"); 1425 log(" evaluates to 'true' if the assert statement holds in the state.\n"); 1426 log("\n"); 1427 log(" ; yosys-smt2-assume <id> <filename:linenum>\n"); 1428 log(" (define-fun |<mod>_u <id>| ((state |<mod>_s|)) Bool (...))\n"); 1429 log(" Each $assume cell is converted into one of this functions. The function\n"); 1430 log(" evaluates to 'true' if the assume statement holds in the state.\n"); 1431 log("\n"); 1432 log(" ; yosys-smt2-cover <id> <filename:linenum>\n"); 1433 log(" (define-fun |<mod>_c <id>| ((state |<mod>_s|)) Bool (...))\n"); 1434 log(" Each $cover cell is converted into one of this functions. The function\n"); 1435 log(" evaluates to 'true' if the cover statement is activated in the state.\n"); 1436 log("\n"); 1437 log("Options:\n"); 1438 log("\n"); 1439 log(" -verbose\n"); 1440 log(" this will print the recursive walk used to export the modules.\n"); 1441 log("\n"); 1442 log(" -stbv\n"); 1443 log(" Use a BitVec sort to represent a state instead of an uninterpreted\n"); 1444 log(" sort. As a side-effect this will prevent use of arrays to model\n"); 1445 log(" memories.\n"); 1446 log("\n"); 1447 log(" -stdt\n"); 1448 log(" Use SMT-LIB 2.6 style datatypes to represent a state instead of an\n"); 1449 log(" uninterpreted sort.\n"); 1450 log("\n"); 1451 log(" -nobv\n"); 1452 log(" disable support for BitVec (FixedSizeBitVectors theory). without this\n"); 1453 log(" option multi-bit wires are represented using the BitVec sort and\n"); 1454 log(" support for coarse grain cells (incl. arithmetic) is enabled.\n"); 1455 log("\n"); 1456 log(" -nomem\n"); 1457 log(" disable support for memories (via ArraysEx theory). this option is\n"); 1458 log(" implied by -nobv. only $mem cells without merged registers in\n"); 1459 log(" read ports are supported. call \"memory\" with -nordff to make sure\n"); 1460 log(" that no registers are merged into $mem read ports. '<mod>_m' functions\n"); 1461 log(" will be generated for accessing the arrays that are used to represent\n"); 1462 log(" memories.\n"); 1463 log("\n"); 1464 log(" -wires\n"); 1465 log(" create '<mod>_n' functions for all public wires. by default only ports,\n"); 1466 log(" registers, and wires with the 'keep' attribute are exported.\n"); 1467 log("\n"); 1468 log(" -tpl <template_file>\n"); 1469 log(" use the given template file. the line containing only the token '%%%%'\n"); 1470 log(" is replaced with the regular output of this command.\n"); 1471 log("\n"); 1472 log(" -solver-option <option> <value>\n"); 1473 log(" emit a `; yosys-smt2-solver-option` directive for yosys-smtbmc to write\n"); 1474 log(" the given option as a `(set-option ...)` command in the SMT-LIBv2.\n"); 1475 log("\n"); 1476 log("[1] For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David\n"); 1477 log("R. Cok's tutorial: https://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf\n"); 1478 log("\n"); 1479 log("---------------------------------------------------------------------------\n"); 1480 log("\n"); 1481 log("Example:\n"); 1482 log("\n"); 1483 log("Consider the following module (test.v). We want to prove that the output can\n"); 1484 log("never transition from a non-zero value to a zero value.\n"); 1485 log("\n"); 1486 log(" module test(input clk, output reg [3:0] y);\n"); 1487 log(" always @(posedge clk)\n"); 1488 log(" y <= (y << 1) | ^y;\n"); 1489 log(" endmodule\n"); 1490 log("\n"); 1491 log("For this proof we create the following template (test.tpl).\n"); 1492 log("\n"); 1493 log(" ; we need QF_UFBV for this proof\n"); 1494 log(" (set-logic QF_UFBV)\n"); 1495 log("\n"); 1496 log(" ; insert the auto-generated code here\n"); 1497 log(" %%%%\n"); 1498 log("\n"); 1499 log(" ; declare two state variables s1 and s2\n"); 1500 log(" (declare-fun s1 () test_s)\n"); 1501 log(" (declare-fun s2 () test_s)\n"); 1502 log("\n"); 1503 log(" ; state s2 is the successor of state s1\n"); 1504 log(" (assert (test_t s1 s2))\n"); 1505 log("\n"); 1506 log(" ; we are looking for a model with y non-zero in s1\n"); 1507 log(" (assert (distinct (|test_n y| s1) #b0000))\n"); 1508 log("\n"); 1509 log(" ; we are looking for a model with y zero in s2\n"); 1510 log(" (assert (= (|test_n y| s2) #b0000))\n"); 1511 log("\n"); 1512 log(" ; is there such a model?\n"); 1513 log(" (check-sat)\n"); 1514 log("\n"); 1515 log("The following yosys script will create a 'test.smt2' file for our proof:\n"); 1516 log("\n"); 1517 log(" read_verilog test.v\n"); 1518 log(" hierarchy -check; proc; opt; check -assert\n"); 1519 log(" write_smt2 -bv -tpl test.tpl test.smt2\n"); 1520 log("\n"); 1521 log("Running 'cvc4 test.smt2' will print 'unsat' because y can never transition\n"); 1522 log("from non-zero to zero in the test design.\n"); 1523 log("\n"); 1524 } executeSmt2Backend1525 void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override 1526 { 1527 std::ifstream template_f; 1528 bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false; 1529 bool forallmode = false; 1530 dict<std::string, std::string> solver_options; 1531 1532 log_header(design, "Executing SMT2 backend.\n"); 1533 1534 size_t argidx; 1535 for (argidx = 1; argidx < args.size(); argidx++) 1536 { 1537 if (args[argidx] == "-tpl" && argidx+1 < args.size()) { 1538 template_f.open(args[++argidx]); 1539 if (template_f.fail()) 1540 log_error("Can't open template file `%s'.\n", args[argidx].c_str()); 1541 continue; 1542 } 1543 if (args[argidx] == "-bv" || args[argidx] == "-mem") { 1544 log_warning("Options -bv and -mem are now the default. Support for -bv and -mem will be removed in the future.\n"); 1545 continue; 1546 } 1547 if (args[argidx] == "-stbv") { 1548 statebv = true; 1549 statedt = false; 1550 continue; 1551 } 1552 if (args[argidx] == "-stdt") { 1553 statebv = false; 1554 statedt = true; 1555 continue; 1556 } 1557 if (args[argidx] == "-nobv") { 1558 bvmode = false; 1559 memmode = false; 1560 continue; 1561 } 1562 if (args[argidx] == "-nomem") { 1563 memmode = false; 1564 continue; 1565 } 1566 if (args[argidx] == "-wires") { 1567 wiresmode = true; 1568 continue; 1569 } 1570 if (args[argidx] == "-verbose") { 1571 verbose = true; 1572 continue; 1573 } 1574 if (args[argidx] == "-solver-option" && argidx+2 < args.size()) { 1575 solver_options.emplace(args[argidx+1], args[argidx+2]); 1576 argidx += 2; 1577 continue; 1578 } 1579 break; 1580 } 1581 extra_args(f, filename, args, argidx); 1582 1583 if (template_f.is_open()) { 1584 std::string line; 1585 while (std::getline(template_f, line)) { 1586 int indent = 0; 1587 while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t')) 1588 indent++; 1589 if (line.compare(indent, 2, "%%") == 0) 1590 break; 1591 *f << line << std::endl; 1592 } 1593 } 1594 1595 *f << stringf("; SMT-LIBv2 description generated by %s\n", yosys_version_str); 1596 1597 if (!bvmode) 1598 *f << stringf("; yosys-smt2-nobv\n"); 1599 1600 if (!memmode) 1601 *f << stringf("; yosys-smt2-nomem\n"); 1602 1603 if (statebv) 1604 *f << stringf("; yosys-smt2-stbv\n"); 1605 1606 if (statedt) 1607 *f << stringf("; yosys-smt2-stdt\n"); 1608 1609 for (auto &it : solver_options) 1610 *f << stringf("; yosys-smt2-solver-option %s %s\n", it.first.c_str(), it.second.c_str()); 1611 1612 std::vector<RTLIL::Module*> sorted_modules; 1613 1614 // extract module dependencies 1615 std::map<RTLIL::Module*, std::set<RTLIL::Module*>> module_deps; 1616 for (auto mod : design->modules()) { 1617 module_deps[mod] = std::set<RTLIL::Module*>(); 1618 for (auto cell : mod->cells()) 1619 if (design->has(cell->type)) 1620 module_deps[mod].insert(design->module(cell->type)); 1621 } 1622 1623 // simple good-enough topological sort 1624 // (O(n*m) on n elements and depth m) 1625 while (module_deps.size() > 0) { 1626 size_t sorted_modules_idx = sorted_modules.size(); 1627 for (auto &it : module_deps) { 1628 for (auto &dep : it.second) 1629 if (module_deps.count(dep) > 0) 1630 goto not_ready_yet; 1631 // log("Next in topological sort: %s\n", log_id(it.first->name)); 1632 sorted_modules.push_back(it.first); 1633 not_ready_yet:; 1634 } 1635 if (sorted_modules_idx == sorted_modules.size()) 1636 log_error("Cyclic dependency between modules found! Cycle includes module %s.\n", log_id(module_deps.begin()->first->name)); 1637 while (sorted_modules_idx < sorted_modules.size()) 1638 module_deps.erase(sorted_modules.at(sorted_modules_idx++)); 1639 } 1640 1641 dict<IdString, int> mod_stbv_width; 1642 dict<IdString, dict<IdString, pair<bool, bool>>> mod_clk_cache; 1643 Module *topmod = design->top_module(); 1644 std::string topmod_id; 1645 1646 for (auto module : sorted_modules) 1647 for (auto cell : module->cells()) 1648 if (cell->type.in(ID($allconst), ID($allseq))) 1649 goto found_forall; 1650 if (0) { 1651 found_forall: 1652 forallmode = true; 1653 *f << stringf("; yosys-smt2-forall\n"); 1654 if (!statebv && !statedt) 1655 log_error("Forall-exists problems are only supported in -stbv or -stdt mode.\n"); 1656 } 1657 1658 for (auto module : sorted_modules) 1659 { 1660 if (module->get_blackbox_attribute() || module->has_processes_warn()) 1661 continue; 1662 1663 log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module)); 1664 1665 Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, forallmode, mod_stbv_width, mod_clk_cache); 1666 worker.run(); 1667 worker.write(*f); 1668 1669 if (module == topmod) 1670 topmod_id = worker.get_id(module); 1671 } 1672 1673 if (topmod) 1674 *f << stringf("; yosys-smt2-topmod %s\n", topmod_id.c_str()); 1675 1676 *f << stringf("; end of yosys output\n"); 1677 1678 if (template_f.is_open()) { 1679 std::string line; 1680 while (std::getline(template_f, line)) 1681 *f << line << std::endl; 1682 } 1683 } 1684 } Smt2Backend; 1685 1686 PRIVATE_NAMESPACE_END 1687