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 <string> 26 27 USING_YOSYS_NAMESPACE 28 PRIVATE_NAMESPACE_BEGIN 29 30 struct SmvWorker 31 { 32 CellTypes ct; 33 SigMap sigmap; 34 RTLIL::Module *module; 35 std::ostream &f; 36 bool verbose; 37 38 int idcounter; 39 dict<IdString, shared_str> idcache; 40 pool<shared_str> used_names; 41 vector<shared_str> strbuf; 42 43 pool<Wire*> partial_assignment_wires; 44 dict<SigBit, std::pair<const char*, int>> partial_assignment_bits; 45 vector<string> inputvars, vars, definitions, assignments, invarspecs; 46 cidSmvWorker47 const char *cid() 48 { 49 while (true) { 50 shared_str s(stringf("_%d", idcounter++)); 51 if (!used_names.count(s)) { 52 used_names.insert(s); 53 return s.c_str(); 54 } 55 } 56 } 57 cidSmvWorker58 const char *cid(IdString id, bool precache = false) 59 { 60 if (!idcache.count(id)) 61 { 62 string name = stringf("_%s", id.c_str()); 63 64 if (name.compare(0, 2, "_\\") == 0) 65 name = "_" + name.substr(2); 66 67 for (auto &c : name) { 68 if (c == '|' || c == '$' || c == '_') continue; 69 if (c >= 'a' && c <='z') continue; 70 if (c >= 'A' && c <='Z') continue; 71 if (c >= '0' && c <='9') continue; 72 if (precache) return nullptr; 73 c = '#'; 74 } 75 76 if (name == "_main") 77 name = "main"; 78 79 while (used_names.count(name)) 80 name += "_"; 81 82 shared_str s(name); 83 used_names.insert(s); 84 idcache[id] = s; 85 } 86 87 return idcache.at(id).c_str(); 88 } 89 SmvWorkerSmvWorker90 SmvWorker(RTLIL::Module *module, bool verbose, std::ostream &f) : 91 ct(module->design), sigmap(module), module(module), f(f), verbose(verbose), idcounter(0) 92 { 93 for (auto mod : module->design->modules()) 94 cid(mod->name, true); 95 96 for (auto wire : module->wires()) 97 cid(wire->name, true); 98 99 for (auto cell : module->cells()) { 100 cid(cell->name, true); 101 cid(cell->type, true); 102 for (auto &conn : cell->connections()) 103 cid(conn.first, true); 104 } 105 } 106 rvalueSmvWorker107 const char *rvalue(SigSpec sig, int width = -1, bool is_signed = false) 108 { 109 string s; 110 int count_chunks = 0; 111 sigmap.apply(sig); 112 113 for (int i = 0; i < GetSize(sig); i++) 114 if (partial_assignment_bits.count(sig[i])) 115 { 116 int width = 1; 117 const auto &bit_a = partial_assignment_bits.at(sig[i]); 118 119 while (i+width < GetSize(sig)) 120 { 121 if (!partial_assignment_bits.count(sig[i+width])) 122 break; 123 124 const auto &bit_b = partial_assignment_bits.at(sig[i+width]); 125 if (strcmp(bit_a.first, bit_b.first)) 126 break; 127 if (bit_a.second+width != bit_b.second) 128 break; 129 130 width++; 131 } 132 133 if (i+width < GetSize(sig)) 134 s = stringf("%s :: ", rvalue(sig.extract(i+width, GetSize(sig)-(width+i)))); 135 136 s += stringf("%s[%d:%d]", bit_a.first, bit_a.second+width-1, bit_a.second); 137 138 if (i > 0) 139 s += stringf(" :: %s", rvalue(sig.extract(0, i))); 140 141 count_chunks = 3; 142 goto continue_with_resize; 143 } 144 145 for (auto &c : sig.chunks()) { 146 count_chunks++; 147 if (!s.empty()) 148 s = " :: " + s; 149 if (c.wire) { 150 if (c.offset != 0 || c.width != c.wire->width) 151 s = stringf("%s[%d:%d]", cid(c.wire->name), c.offset+c.width-1, c.offset) + s; 152 else 153 s = cid(c.wire->name) + s; 154 } else { 155 string v = stringf("0ub%d_", c.width); 156 for (int i = c.width-1; i >= 0; i--) 157 v += c.data.at(i) == State::S1 ? '1' : '0'; 158 s = v + s; 159 } 160 } 161 162 continue_with_resize:; 163 if (width >= 0) { 164 if (is_signed) { 165 if (GetSize(sig) > width) 166 s = stringf("signed(resize(%s, %d))", s.c_str(), width); 167 else 168 s = stringf("resize(signed(%s), %d)", s.c_str(), width); 169 } else 170 s = stringf("resize(%s, %d)", s.c_str(), width); 171 } else if (is_signed) 172 s = stringf("signed(%s)", s.c_str()); 173 else if (count_chunks > 1) 174 s = stringf("(%s)", s.c_str()); 175 176 strbuf.push_back(s); 177 return strbuf.back().c_str(); 178 } 179 rvalue_uSmvWorker180 const char *rvalue_u(SigSpec sig, int width = -1) 181 { 182 return rvalue(sig, width, false); 183 } 184 rvalue_sSmvWorker185 const char *rvalue_s(SigSpec sig, int width = -1, bool is_signed = true) 186 { 187 return rvalue(sig, width, is_signed); 188 } 189 lvalueSmvWorker190 const char *lvalue(SigSpec sig) 191 { 192 sigmap.apply(sig); 193 194 if (sig.is_wire()) 195 return rvalue(sig); 196 197 const char *temp_id = cid(); 198 // f << stringf(" %s : unsigned word[%d]; -- %s\n", temp_id, GetSize(sig), log_signal(sig)); 199 200 int offset = 0; 201 for (auto bit : sig) { 202 log_assert(bit.wire != nullptr); 203 partial_assignment_wires.insert(bit.wire); 204 partial_assignment_bits[bit] = std::pair<const char*, int>(temp_id, offset++); 205 } 206 207 return temp_id; 208 } 209 runSmvWorker210 void run() 211 { 212 f << stringf("MODULE %s\n", cid(module->name)); 213 214 for (auto wire : module->wires()) 215 { 216 if (SigSpec(wire) != sigmap(wire)) 217 partial_assignment_wires.insert(wire); 218 219 if (wire->port_input) 220 inputvars.push_back(stringf("%s : unsigned word[%d]; -- %s", cid(wire->name), wire->width, log_id(wire))); 221 222 if (wire->attributes.count(ID::init)) 223 assignments.push_back(stringf("init(%s) := %s;", lvalue(wire), rvalue(wire->attributes.at(ID::init)))); 224 } 225 226 for (auto cell : module->cells()) 227 { 228 // FIXME: $slice, $concat, $mem 229 230 if (cell->type.in(ID($assert))) 231 { 232 SigSpec sig_a = cell->getPort(ID::A); 233 SigSpec sig_en = cell->getPort(ID::EN); 234 235 invarspecs.push_back(stringf("!bool(%s) | bool(%s);", rvalue(sig_en), rvalue(sig_a))); 236 237 continue; 238 } 239 240 if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx))) 241 { 242 SigSpec sig_a = cell->getPort(ID::A); 243 SigSpec sig_b = cell->getPort(ID::B); 244 245 int width_y = GetSize(cell->getPort(ID::Y)); 246 int shift_b_width = GetSize(sig_b); 247 int width_ay = max(GetSize(sig_a), width_y); 248 int width = width_ay; 249 250 for (int i = 1, j = 0;; i <<= 1, j++) 251 if (width_ay < i) { 252 width = i-1; 253 shift_b_width = min(shift_b_width, j); 254 break; 255 } 256 257 bool signed_a = cell->getParam(ID::A_SIGNED).as_bool(); 258 bool signed_b = cell->getParam(ID::B_SIGNED).as_bool(); 259 string op = cell->type.in(ID($shl), ID($sshl)) ? "<<" : ">>"; 260 string expr, expr_a; 261 262 if (cell->type == ID($sshr) && signed_a) 263 { 264 expr_a = rvalue_s(sig_a, width); 265 expr = stringf("resize(unsigned(%s %s %s), %d)", expr_a.c_str(), op.c_str(), rvalue(sig_b.extract(0, shift_b_width)), width_y); 266 if (shift_b_width < GetSize(sig_b)) 267 expr = stringf("%s != 0ud%d_0 ? (bool(%s) ? !0ud%d_0 : 0ud%d_0) : %s", 268 rvalue(sig_b.extract(shift_b_width, GetSize(sig_b) - shift_b_width)), GetSize(sig_b) - shift_b_width, 269 rvalue(sig_a[GetSize(sig_a)-1]), width_y, width_y, expr.c_str()); 270 } 271 else if (cell->type.in(ID($shift), ID($shiftx)) && signed_b) 272 { 273 expr_a = rvalue_u(sig_a, width); 274 275 const char *b_shr = rvalue_u(sig_b); 276 const char *b_shl = cid(); 277 278 // f << stringf(" %s : unsigned word[%d]; -- neg(%s)\n", b_shl, GetSize(sig_b), log_signal(sig_b)); 279 definitions.push_back(stringf("%s := unsigned(-%s);", b_shl, rvalue_s(sig_b))); 280 281 string expr_shl = stringf("resize(%s << %s[%d:0], %d)", expr_a.c_str(), b_shl, shift_b_width-1, width_y); 282 string expr_shr = stringf("resize(%s >> %s[%d:0], %d)", expr_a.c_str(), b_shr, shift_b_width-1, width_y); 283 284 if (shift_b_width < GetSize(sig_b)) { 285 expr_shl = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shl, GetSize(sig_b)-1, shift_b_width, 286 GetSize(sig_b)-shift_b_width, width_y, expr_shl.c_str()); 287 expr_shr = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shr, GetSize(sig_b)-1, shift_b_width, 288 GetSize(sig_b)-shift_b_width, width_y, expr_shr.c_str()); 289 } 290 291 expr = stringf("bool(%s) ? %s : %s", rvalue(sig_b[GetSize(sig_b)-1]), expr_shl.c_str(), expr_shr.c_str()); 292 } 293 else 294 { 295 if (cell->type.in(ID($shift), ID($shiftx)) || !signed_a) 296 expr_a = rvalue_u(sig_a, width); 297 else 298 expr_a = stringf("resize(unsigned(%s), %d)", rvalue_s(sig_a, width_ay), width); 299 300 expr = stringf("resize(%s %s %s[%d:0], %d)", expr_a.c_str(), op.c_str(), rvalue_u(sig_b), shift_b_width-1, width_y); 301 if (shift_b_width < GetSize(sig_b)) 302 expr = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", rvalue_u(sig_b), GetSize(sig_b)-1, shift_b_width, 303 GetSize(sig_b)-shift_b_width, width_y, expr.c_str()); 304 } 305 306 definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort(ID::Y)), expr.c_str())); 307 308 continue; 309 } 310 311 if (cell->type.in(ID($not), ID($pos), ID($neg))) 312 { 313 int width = GetSize(cell->getPort(ID::Y)); 314 string expr_a, op; 315 316 if (cell->type == ID($not)) op = "!"; 317 if (cell->type == ID($pos)) op = ""; 318 if (cell->type == ID($neg)) op = "-"; 319 320 if (cell->getParam(ID::A_SIGNED).as_bool()) 321 { 322 definitions.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort(ID::Y)), 323 op.c_str(), rvalue_s(cell->getPort(ID::A), width))); 324 } 325 else 326 { 327 definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort(ID::Y)), 328 op.c_str(), rvalue_u(cell->getPort(ID::A), width))); 329 } 330 331 continue; 332 } 333 334 if (cell->type.in(ID($add), ID($sub), ID($mul), ID($and), ID($or), ID($xor), ID($xnor))) 335 { 336 int width = GetSize(cell->getPort(ID::Y)); 337 string expr_a, expr_b, op; 338 339 if (cell->type == ID($add)) op = "+"; 340 if (cell->type == ID($sub)) op = "-"; 341 if (cell->type == ID($mul)) op = "*"; 342 if (cell->type == ID($and)) op = "&"; 343 if (cell->type == ID($or)) op = "|"; 344 if (cell->type == ID($xor)) op = "xor"; 345 if (cell->type == ID($xnor)) op = "xnor"; 346 347 if (cell->getParam(ID::A_SIGNED).as_bool()) 348 { 349 definitions.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort(ID::Y)), 350 rvalue_s(cell->getPort(ID::A), width), op.c_str(), rvalue_s(cell->getPort(ID::B), width))); 351 } 352 else 353 { 354 definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort(ID::Y)), 355 rvalue_u(cell->getPort(ID::A), width), op.c_str(), rvalue_u(cell->getPort(ID::B), width))); 356 } 357 358 continue; 359 } 360 361 // SMV has a "mod" operator, but its semantics don't seem to be well-defined - to be safe, don't generate it at all 362 if (cell->type.in(ID($div)/*, ID($mod), ID($modfloor)*/)) 363 { 364 int width_y = GetSize(cell->getPort(ID::Y)); 365 int width = max(width_y, GetSize(cell->getPort(ID::A))); 366 width = max(width, GetSize(cell->getPort(ID::B))); 367 string expr_a, expr_b, op; 368 369 if (cell->type == ID($div)) op = "/"; 370 //if (cell->type == ID($mod)) op = "mod"; 371 372 if (cell->getParam(ID::A_SIGNED).as_bool()) 373 { 374 definitions.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell->getPort(ID::Y)), 375 rvalue_s(cell->getPort(ID::A), width), op.c_str(), rvalue_s(cell->getPort(ID::B), width), width_y)); 376 } 377 else 378 { 379 definitions.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell->getPort(ID::Y)), 380 rvalue_u(cell->getPort(ID::A), width), op.c_str(), rvalue_u(cell->getPort(ID::B), width), width_y)); 381 } 382 383 continue; 384 } 385 386 if (cell->type.in(ID($eq), ID($ne), ID($eqx), ID($nex), ID($lt), ID($le), ID($ge), ID($gt))) 387 { 388 int width = max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::B))); 389 string expr_a, expr_b, op; 390 391 if (cell->type == ID($eq)) op = "="; 392 if (cell->type == ID($ne)) op = "!="; 393 if (cell->type == ID($eqx)) op = "="; 394 if (cell->type == ID($nex)) op = "!="; 395 if (cell->type == ID($lt)) op = "<"; 396 if (cell->type == ID($le)) op = "<="; 397 if (cell->type == ID($ge)) op = ">="; 398 if (cell->type == ID($gt)) op = ">"; 399 400 if (cell->getParam(ID::A_SIGNED).as_bool()) 401 { 402 expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort(ID::A)), width); 403 expr_b = stringf("resize(signed(%s), %d)", rvalue(cell->getPort(ID::B)), width); 404 } 405 else 406 { 407 expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort(ID::A)), width); 408 expr_b = stringf("resize(%s, %d)", rvalue(cell->getPort(ID::B)), width); 409 } 410 411 definitions.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell->getPort(ID::Y)), 412 expr_a.c_str(), op.c_str(), expr_b.c_str(), GetSize(cell->getPort(ID::Y)))); 413 414 continue; 415 } 416 417 if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool))) 418 { 419 int width_a = GetSize(cell->getPort(ID::A)); 420 int width_y = GetSize(cell->getPort(ID::Y)); 421 const char *expr_a = rvalue(cell->getPort(ID::A)); 422 const char *expr_y = lvalue(cell->getPort(ID::Y)); 423 string expr; 424 425 if (cell->type == ID($reduce_and)) expr = stringf("%s = !0ub%d_0", expr_a, width_a); 426 if (cell->type == ID($reduce_or)) expr = stringf("%s != 0ub%d_0", expr_a, width_a); 427 if (cell->type == ID($reduce_bool)) expr = stringf("%s != 0ub%d_0", expr_a, width_a); 428 429 definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y)); 430 continue; 431 } 432 433 if (cell->type.in(ID($reduce_xor), ID($reduce_xnor))) 434 { 435 int width_y = GetSize(cell->getPort(ID::Y)); 436 const char *expr_y = lvalue(cell->getPort(ID::Y)); 437 string expr; 438 439 for (auto bit : cell->getPort(ID::A)) { 440 if (!expr.empty()) 441 expr += " xor "; 442 expr += rvalue(bit); 443 } 444 445 if (cell->type == ID($reduce_xnor)) 446 expr = "!(" + expr + ")"; 447 448 definitions.push_back(stringf("%s := resize(%s, %d);", expr_y, expr.c_str(), width_y)); 449 continue; 450 } 451 452 if (cell->type.in(ID($logic_and), ID($logic_or))) 453 { 454 int width_a = GetSize(cell->getPort(ID::A)); 455 int width_b = GetSize(cell->getPort(ID::B)); 456 int width_y = GetSize(cell->getPort(ID::Y)); 457 458 string expr_a = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort(ID::A)), width_a); 459 string expr_b = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort(ID::B)), width_b); 460 const char *expr_y = lvalue(cell->getPort(ID::Y)); 461 462 string expr; 463 if (cell->type == ID($logic_and)) expr = expr_a + " & " + expr_b; 464 if (cell->type == ID($logic_or)) expr = expr_a + " | " + expr_b; 465 466 definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y)); 467 continue; 468 } 469 470 if (cell->type.in(ID($logic_not))) 471 { 472 int width_a = GetSize(cell->getPort(ID::A)); 473 int width_y = GetSize(cell->getPort(ID::Y)); 474 475 string expr_a = stringf("(%s = 0ub%d_0)", rvalue(cell->getPort(ID::A)), width_a); 476 const char *expr_y = lvalue(cell->getPort(ID::Y)); 477 478 definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr_a.c_str(), width_y)); 479 continue; 480 } 481 482 if (cell->type.in(ID($mux), ID($pmux))) 483 { 484 int width = GetSize(cell->getPort(ID::Y)); 485 SigSpec sig_a = cell->getPort(ID::A); 486 SigSpec sig_b = cell->getPort(ID::B); 487 SigSpec sig_s = cell->getPort(ID::S); 488 489 string expr; 490 for (int i = 0; i < GetSize(sig_s); i++) 491 expr += stringf("bool(%s) ? %s : ", rvalue(sig_s[i]), rvalue(sig_b.extract(i*width, width))); 492 expr += rvalue(sig_a); 493 494 definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort(ID::Y)), expr.c_str())); 495 continue; 496 } 497 498 if (cell->type == ID($dff)) 499 { 500 vars.push_back(stringf("%s : unsigned word[%d]; -- %s", lvalue(cell->getPort(ID::Q)), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q)))); 501 assignments.push_back(stringf("next(%s) := %s;", lvalue(cell->getPort(ID::Q)), rvalue(cell->getPort(ID::D)))); 502 continue; 503 } 504 505 if (cell->type.in(ID($_BUF_), ID($_NOT_))) 506 { 507 string op = cell->type == ID($_NOT_) ? "!" : ""; 508 definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort(ID::Y)), op.c_str(), rvalue(cell->getPort(ID::A)))); 509 continue; 510 } 511 512 if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_))) 513 { 514 string op; 515 516 if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_ANDNOT_))) op = "&"; 517 if (cell->type.in(ID($_OR_), ID($_NOR_), ID($_ORNOT_))) op = "|"; 518 if (cell->type.in(ID($_XOR_))) op = "xor"; 519 if (cell->type.in(ID($_XNOR_))) op = "xnor"; 520 521 if (cell->type.in(ID($_ANDNOT_), ID($_ORNOT_))) 522 definitions.push_back(stringf("%s := %s %s (!%s);", lvalue(cell->getPort(ID::Y)), 523 rvalue(cell->getPort(ID::A)), op.c_str(), rvalue(cell->getPort(ID::B)))); 524 else 525 if (cell->type.in(ID($_NAND_), ID($_NOR_))) 526 definitions.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort(ID::Y)), 527 rvalue(cell->getPort(ID::A)), op.c_str(), rvalue(cell->getPort(ID::B)))); 528 else 529 definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort(ID::Y)), 530 rvalue(cell->getPort(ID::A)), op.c_str(), rvalue(cell->getPort(ID::B)))); 531 continue; 532 } 533 534 if (cell->type == ID($_MUX_)) 535 { 536 definitions.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell->getPort(ID::Y)), 537 rvalue(cell->getPort(ID::S)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::A)))); 538 continue; 539 } 540 541 if (cell->type == ID($_NMUX_)) 542 { 543 definitions.push_back(stringf("%s := !(bool(%s) ? %s : %s);", lvalue(cell->getPort(ID::Y)), 544 rvalue(cell->getPort(ID::S)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::A)))); 545 continue; 546 } 547 548 if (cell->type == ID($_AOI3_)) 549 { 550 definitions.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort(ID::Y)), 551 rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C)))); 552 continue; 553 } 554 555 if (cell->type == ID($_OAI3_)) 556 { 557 definitions.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort(ID::Y)), 558 rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C)))); 559 continue; 560 } 561 562 if (cell->type == ID($_AOI4_)) 563 { 564 definitions.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort(ID::Y)), 565 rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C)), rvalue(cell->getPort(ID::D)))); 566 continue; 567 } 568 569 if (cell->type == ID($_OAI4_)) 570 { 571 definitions.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort(ID::Y)), 572 rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C)), rvalue(cell->getPort(ID::D)))); 573 continue; 574 } 575 576 if (cell->type[0] == '$') { 577 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)) { 578 log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smv`.\n", 579 log_id(cell->type), log_id(module), log_id(cell)); 580 } 581 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") { 582 log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smv`.\n", 583 log_id(cell->type), log_id(module), log_id(cell)); 584 } 585 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_") { 586 log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_smv`.\n", 587 log_id(cell->type), log_id(module), log_id(cell)); 588 } 589 log_error("Unsupported cell type %s for cell %s.%s.\n", 590 log_id(cell->type), log_id(module), log_id(cell)); 591 } 592 593 // f << stringf(" %s : %s;\n", cid(cell->name), cid(cell->type)); 594 595 for (auto &conn : cell->connections()) 596 if (cell->output(conn.first)) 597 definitions.push_back(stringf("%s := %s.%s;", lvalue(conn.second), cid(cell->name), cid(conn.first))); 598 else 599 definitions.push_back(stringf("%s.%s := %s;", cid(cell->name), cid(conn.first), rvalue(conn.second))); 600 } 601 602 for (Wire *wire : partial_assignment_wires) 603 { 604 string expr; 605 606 for (int i = 0; i < wire->width; i++) 607 { 608 if (!expr.empty()) 609 expr = " :: " + expr; 610 611 if (partial_assignment_bits.count(sigmap(SigBit(wire, i)))) 612 { 613 int width = 1; 614 const auto &bit_a = partial_assignment_bits.at(sigmap(SigBit(wire, i))); 615 616 while (i+1 < wire->width) 617 { 618 SigBit next_bit = sigmap(SigBit(wire, i+1)); 619 620 if (!partial_assignment_bits.count(next_bit)) 621 break; 622 623 const auto &bit_b = partial_assignment_bits.at(next_bit); 624 if (strcmp(bit_a.first, bit_b.first)) 625 break; 626 if (bit_a.second+width != bit_b.second) 627 break; 628 629 width++, i++; 630 } 631 632 expr = stringf("%s[%d:%d]", bit_a.first, bit_a.second+width-1, bit_a.second) + expr; 633 } 634 else if (sigmap(SigBit(wire, i)).wire == nullptr) 635 { 636 string bits; 637 SigSpec sig = sigmap(SigSpec(wire, i)); 638 639 while (i+1 < wire->width) { 640 SigBit next_bit = sigmap(SigBit(wire, i+1)); 641 if (next_bit.wire != nullptr) 642 break; 643 sig.append(next_bit); 644 i++; 645 } 646 647 for (int k = GetSize(sig)-1; k >= 0; k--) 648 bits += sig[k] == State::S1 ? '1' : '0'; 649 650 expr = stringf("0ub%d_%s", GetSize(bits), bits.c_str()) + expr; 651 } 652 else if (sigmap(SigBit(wire, i)) == SigBit(wire, i)) 653 { 654 int length = 1; 655 656 while (i+1 < wire->width) { 657 if (partial_assignment_bits.count(sigmap(SigBit(wire, i+1)))) 658 break; 659 if (sigmap(SigBit(wire, i+1)) != SigBit(wire, i+1)) 660 break; 661 i++, length++; 662 } 663 664 expr = stringf("0ub%d_0", length) + expr; 665 } 666 else 667 { 668 string bits; 669 SigSpec sig = sigmap(SigSpec(wire, i)); 670 671 while (i+1 < wire->width) { 672 SigBit next_bit = sigmap(SigBit(wire, i+1)); 673 if (next_bit.wire == nullptr || partial_assignment_bits.count(next_bit)) 674 break; 675 sig.append(next_bit); 676 i++; 677 } 678 679 expr = rvalue(sig) + expr; 680 } 681 } 682 683 definitions.push_back(stringf("%s := %s;", cid(wire->name), expr.c_str())); 684 } 685 686 if (!inputvars.empty()) { 687 f << stringf(" IVAR\n"); 688 for (const string &line : inputvars) 689 f << stringf(" %s\n", line.c_str()); 690 } 691 692 if (!vars.empty()) { 693 f << stringf(" VAR\n"); 694 for (const string &line : vars) 695 f << stringf(" %s\n", line.c_str()); 696 } 697 698 if (!definitions.empty()) { 699 f << stringf(" DEFINE\n"); 700 for (const string &line : definitions) 701 f << stringf(" %s\n", line.c_str()); 702 } 703 704 if (!assignments.empty()) { 705 f << stringf(" ASSIGN\n"); 706 for (const string &line : assignments) 707 f << stringf(" %s\n", line.c_str()); 708 } 709 710 if (!invarspecs.empty()) { 711 for (const string &line : invarspecs) 712 f << stringf(" INVARSPEC %s\n", line.c_str()); 713 } 714 } 715 }; 716 717 struct SmvBackend : public Backend { SmvBackendSmvBackend718 SmvBackend() : Backend("smv", "write design to SMV file") { } helpSmvBackend719 void help() override 720 { 721 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| 722 log("\n"); 723 log(" write_smv [options] [filename]\n"); 724 log("\n"); 725 log("Write an SMV description of the current design.\n"); 726 log("\n"); 727 log(" -verbose\n"); 728 log(" this will print the recursive walk used to export the modules.\n"); 729 log("\n"); 730 log(" -tpl <template_file>\n"); 731 log(" use the given template file. the line containing only the token '%%%%'\n"); 732 log(" is replaced with the regular output of this command.\n"); 733 log("\n"); 734 log("THIS COMMAND IS UNDER CONSTRUCTION\n"); 735 log("\n"); 736 } executeSmvBackend737 void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override 738 { 739 std::ifstream template_f; 740 bool verbose = false; 741 742 log_header(design, "Executing SMV backend.\n"); 743 744 size_t argidx; 745 for (argidx = 1; argidx < args.size(); argidx++) 746 { 747 if (args[argidx] == "-tpl" && argidx+1 < args.size()) { 748 template_f.open(args[++argidx]); 749 if (template_f.fail()) 750 log_error("Can't open template file `%s'.\n", args[argidx].c_str()); 751 continue; 752 } 753 if (args[argidx] == "-verbose") { 754 verbose = true; 755 continue; 756 } 757 break; 758 } 759 extra_args(f, filename, args, argidx); 760 761 pool<Module*> modules; 762 763 for (auto module : design->modules()) 764 if (!module->get_blackbox_attribute() && !module->has_memories_warn() && !module->has_processes_warn()) 765 modules.insert(module); 766 767 if (template_f.is_open()) 768 { 769 std::string line; 770 while (std::getline(template_f, line)) 771 { 772 int indent = 0; 773 while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t')) 774 indent++; 775 776 if (line[indent] == '%') 777 { 778 vector<string> stmt = split_tokens(line); 779 780 if (GetSize(stmt) == 1 && stmt[0] == "%%") 781 break; 782 783 if (GetSize(stmt) == 2 && stmt[0] == "%module") 784 { 785 Module *module = design->module(RTLIL::escape_id(stmt[1])); 786 modules.erase(module); 787 788 if (module == nullptr) 789 log_error("Module '%s' not found.\n", stmt[1].c_str()); 790 791 *f << stringf("-- SMV description generated by %s\n", yosys_version_str); 792 793 log("Creating SMV representation of module %s.\n", log_id(module)); 794 SmvWorker worker(module, verbose, *f); 795 worker.run(); 796 797 *f << stringf("-- end of yosys output\n"); 798 continue; 799 } 800 801 log_error("Unknown template statement: '%s'", line.c_str() + indent); 802 } 803 804 *f << line << std::endl; 805 } 806 } 807 808 if (!modules.empty()) 809 { 810 *f << stringf("-- SMV description generated by %s\n", yosys_version_str); 811 812 for (auto module : modules) { 813 log("Creating SMV representation of module %s.\n", log_id(module)); 814 SmvWorker worker(module, verbose, *f); 815 worker.run(); 816 } 817 818 *f << stringf("-- end of yosys output\n"); 819 } 820 821 if (template_f.is_open()) { 822 std::string line; 823 while (std::getline(template_f, line)) 824 *f << line << std::endl; 825 } 826 } 827 } SmvBackend; 828 829 PRIVATE_NAMESPACE_END 830