kernel/satgen.h

   1 /*
   2  *  yosys -- Yosys Open SYnthesis Suite
   3  *
   4  *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
   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 #ifndef SATGEN_H
  21 #define SATGEN_H
  22
  23 #include "kernel/rtlil.h"
  24 #include "kernel/sigtools.h"
  25 #include "kernel/celltypes.h"
  26
  27 #ifdef YOSYS_ENABLE_MINISAT
  28 #  include "libs/ezsat/ezminisat.h"
  29 typedef ezMiniSAT ezDefaultSAT;
  30 #else
  31 #  include "libs/ezsat/ezsat.h"
  32 typedef ezSAT ezDefaultSAT;
  33 #endif
  34
  35 struct SatGen
  36 {
  37         ezSAT *ez;
  38         RTLIL::Design *design;
  39         SigMap *sigmap;
  40         std::string prefix;
  41         SigPool initial_state;
  42         bool ignore_div_by_zero;
  43         bool model_undef;
  44
  45         SatGen(ezSAT *ez, RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string()) :
  46                         ez(ez), design(design), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false)
  47         {
  48         }
  49
  50         void setContext(RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string())
  51         {
  52                 this->design = design;
  53                 this->sigmap = sigmap;
  54                 this->prefix = prefix;
  55         }
  56
  57         std::vector<int> importSigSpecWorker(RTLIL::SigSpec &sig, std::string &pf, bool undef_mode, bool dup_undef)
  58         {
  59                 log_assert(!undef_mode || model_undef);
  60                 sigmap->apply(sig);
  61                 sig.expand();
  62
  63                 std::vector<int> vec;
  64                 vec.reserve(sig.chunks.size());
  65
  66                 for (auto &c : sig.chunks)
  67                         if (c.wire == NULL) {
  68                                 RTLIL::State bit = c.data.bits.at(0);
  69                                 if (model_undef && dup_undef && bit == RTLIL::State::Sx)
  70                                         vec.push_back(ez->literal());
  71                                 else
  72                                         vec.push_back(bit == (undef_mode ? RTLIL::State::Sx : RTLIL::State::S1) ? ez->TRUE : ez->FALSE);
  73                         } else {
  74                                 std::string name = pf + stringf(c.wire->width == 1 ?  "%s" : "%s [%d]", RTLIL::id2cstr(c.wire->name), c.offset);
  75                                 vec.push_back(ez->literal(name));
  76                         }
  77                 return vec;
  78         }
  79
  80         std::vector<int> importSigSpec(RTLIL::SigSpec sig, int timestep = -1)
  81         {
  82                 log_assert(timestep != 0);
  83                 std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
  84                 return importSigSpecWorker(sig, pf, false, false);
  85         }
  86
  87         std::vector<int> importDefSigSpec(RTLIL::SigSpec sig, int timestep = -1)
  88         {
  89                 log_assert(timestep != 0);
  90                 std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
  91                 return importSigSpecWorker(sig, pf, false, true);
  92         }
  93
  94         std::vector<int> importUndefSigSpec(RTLIL::SigSpec sig, int timestep = -1)
  95         {
  96                 log_assert(timestep != 0);
  97                 std::string pf = "undef:" + prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
  98                 return importSigSpecWorker(sig, pf, true, false);
  99         }
 100
 101         int signals_eq(RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep_lhs = -1, int timestep_rhs = -1)
 102         {
 103                 if (timestep_rhs < 0)
 104                         timestep_rhs = timestep_lhs;
 105
 106                 assert(lhs.width == rhs.width);
 107
 108                 std::vector<int> vec_lhs = importSigSpec(lhs, timestep_lhs);
 109                 std::vector<int> vec_rhs = importSigSpec(rhs, timestep_rhs);
 110
 111                 if (!model_undef)
 112                         return ez->vec_eq(vec_lhs, vec_rhs);
 113
 114                 std::vector<int> undef_lhs = importUndefSigSpec(lhs, timestep_lhs);
 115                 std::vector<int> undef_rhs = importUndefSigSpec(rhs, timestep_rhs);
 116
 117                 std::vector<int> eq_bits;
 118                 for (int i = 0; i < lhs.width; i++)
 119                         eq_bits.push_back(ez->AND(ez->IFF(undef_lhs.at(i), undef_rhs.at(i)),
 120                                         ez->IFF(ez->OR(vec_lhs.at(i), undef_lhs.at(i)), ez->OR(vec_rhs.at(i), undef_rhs.at(i)))));
 121                 return ez->expression(ezSAT::OpAnd, eq_bits);
 122         }
 123
 124         void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell, size_t y_width = 0, bool forced_signed = false)
 125         {
 126                 bool is_signed = forced_signed;
 127                 if (!forced_signed && cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters.count("\\B_SIGNED") > 0)
 128                         is_signed = cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool();
 129                 while (vec_a.size() < vec_b.size() || vec_a.size() < y_width)
 130                         vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
 131                 while (vec_b.size() < vec_a.size() || vec_b.size() < y_width)
 132                         vec_b.push_back(is_signed && vec_b.size() > 0 ? vec_b.back() : ez->FALSE);
 133         }
 134
 135         void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &vec_y, RTLIL::Cell *cell, bool forced_signed = false)
 136         {
 137                 extendSignalWidth(vec_a, vec_b, cell, vec_y.size(), forced_signed);
 138                 while (vec_y.size() < vec_a.size())
 139                         vec_y.push_back(ez->literal());
 140         }
 141
 142         void extendSignalWidthUnary(std::vector<int> &vec_a, std::vector<int> &vec_y, RTLIL::Cell *cell, bool forced_signed = false)
 143         {
 144                 bool is_signed = forced_signed || (cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters["\\A_SIGNED"].as_bool());
 145                 while (vec_a.size() < vec_y.size())
 146                         vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
 147                 while (vec_y.size() < vec_a.size())
 148                         vec_y.push_back(ez->literal());
 149         }
 150
 151         void undefGating(std::vector<int> &vec_y, std::vector<int> &vec_yy, std::vector<int> &vec_undef)
 152         {
 153                 assert(model_undef);
 154                 ez->assume(ez->expression(ezSAT::OpAnd, ez->vec_or(vec_undef, ez->vec_iff(vec_y, vec_yy))));
 155         }
 156
 157         bool importCell(RTLIL::Cell *cell, int timestep = -1)
 158         {
 159                 bool arith_undef_handled = false;
 160                 bool is_arith_compare = cell->type == "$lt" || cell->type == "$le" || cell->type == "$ge" || cell->type == "$gt";
 161
 162                 if (model_undef && (cell->type == "$add" || cell->type == "$sub" || cell->type == "$mul" || cell->type == "$div" || cell->type == "$mod" || is_arith_compare))
 163                 {
 164                         std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 165                         std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
 166                         std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
 167                         if (is_arith_compare)
 168                                 extendSignalWidth(undef_a, undef_b, cell, true);
 169                         else
 170                                 extendSignalWidth(undef_a, undef_b, undef_y, cell, true);
 171
 172                         int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
 173                         int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
 174                         int undef_y_bit = ez->OR(undef_any_a, undef_any_b);
 175
 176                         if (cell->type == "$div" || cell->type == "$mod") {
 177                                 std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
 178                                 undef_y_bit = ez->OR(undef_y_bit, ez->NOT(ez->expression(ezSAT::OpOr, b)));
 179                         }
 180
 181                         if (is_arith_compare) {
 182                                 for (size_t i = 1; i < undef_y.size(); i++)
 183                                         ez->SET(ez->FALSE, undef_y.at(i));
 184                                 ez->SET(undef_y_bit, undef_y.at(0));
 185                         } else {
 186                                 std::vector<int> undef_y_bits(undef_y.size(), undef_y_bit);
 187                                 ez->assume(ez->vec_eq(undef_y_bits, undef_y));
 188                         }
 189
 190                         arith_undef_handled = true;
 191                 }
 192
 193                 if (cell->type == "$_AND_" || cell->type == "$_OR_" || cell->type == "$_XOR_" ||
 194                                 cell->type == "$and" || cell->type == "$or" || cell->type == "$xor" || cell->type == "$xnor" ||
 195                                 cell->type == "$add" || cell->type == "$sub")
 196                 {
 197                         std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep);
 198                         std::vector<int> b = importDefSigSpec(cell->connections.at("\\B"), timestep);
 199                         std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
 200                         extendSignalWidth(a, b, y, cell);
 201
 202                         std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
 203
 204                         if (cell->type == "$and" || cell->type == "$_AND_")
 205                                 ez->assume(ez->vec_eq(ez->vec_and(a, b), yy));
 206                         if (cell->type == "$or" || cell->type == "$_OR_")
 207                                 ez->assume(ez->vec_eq(ez->vec_or(a, b), yy));
 208                         if (cell->type == "$xor" || cell->type == "$_XOR_")
 209                                 ez->assume(ez->vec_eq(ez->vec_xor(a, b), yy));
 210                         if (cell->type == "$xnor")
 211                                 ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(a, b)), yy));
 212                         if (cell->type == "$add")
 213                                 ez->assume(ez->vec_eq(ez->vec_add(a, b), yy));
 214                         if (cell->type == "$sub")
 215                                 ez->assume(ez->vec_eq(ez->vec_sub(a, b), yy));
 216
 217                         if (model_undef && !arith_undef_handled)
 218                         {
 219                                 std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 220                                 std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
 221                                 std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
 222                                 extendSignalWidth(undef_a, undef_b, undef_y, cell, false);
 223
 224                                 if (cell->type == "$and" || cell->type == "$_AND_") {
 225                                         std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
 226                                         std::vector<int> b0 = ez->vec_and(ez->vec_not(b), ez->vec_not(undef_b));
 227                                         std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a0, b0)));
 228                                         ez->assume(ez->vec_eq(yX, undef_y));
 229                                 }
 230                                 else if (cell->type == "$or" || cell->type == "$_OR_") {
 231                                         std::vector<int> a1 = ez->vec_and(a, ez->vec_not(undef_a));
 232                                         std::vector<int> b1 = ez->vec_and(b, ez->vec_not(undef_b));
 233                                         std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a1, b1)));
 234                                         ez->assume(ez->vec_eq(yX, undef_y));
 235                                 }
 236                                 else if (cell->type == "$xor" || cell->type == "$_XOR_" || cell->type == "$xnor") {
 237                                         std::vector<int> yX = ez->vec_or(undef_a, undef_b);
 238                                         ez->assume(ez->vec_eq(yX, undef_y));
 239                                 }
 240                                 else
 241                                         log_abort();
 242
 243                                 undefGating(y, yy, undef_y);
 244                         }
 245                         else if (model_undef)
 246                         {
 247                                 std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
 248                                 undefGating(y, yy, undef_y);
 249                         }
 250                         return true;
 251                 }
 252
 253                 if (cell->type == "$_INV_" || cell->type == "$not")
 254                 {
 255                         std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep);
 256                         std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
 257                         extendSignalWidthUnary(a, y, cell);
 258
 259                         std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
 260                         ez->assume(ez->vec_eq(ez->vec_not(a), yy));
 261
 262                         if (model_undef) {
 263                                 std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 264                                 std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
 265                                 extendSignalWidthUnary(undef_a, undef_y, cell, true);
 266                                 ez->assume(ez->vec_eq(undef_a, undef_y));
 267                                 undefGating(y, yy, undef_y);
 268                         }
 269                         return true;
 270                 }
 271
 272                 if (cell->type == "$_MUX_" || cell->type == "$mux")
 273                 {
 274                         std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep);
 275                         std::vector<int> b = importDefSigSpec(cell->connections.at("\\B"), timestep);
 276                         std::vector<int> s = importDefSigSpec(cell->connections.at("\\S"), timestep);
 277                         std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
 278
 279                         std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
 280                         ez->assume(ez->vec_eq(ez->vec_ite(s.at(0), b, a), yy));
 281
 282                         if (model_undef)
 283                         {
 284                                 std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 285                                 std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
 286                                 std::vector<int> undef_s = importUndefSigSpec(cell->connections.at("\\S"), timestep);
 287                                 std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
 288
 289                                 std::vector<int> unequal_ab = ez->vec_not(ez->vec_iff(a, b));
 290                                 std::vector<int> undef_ab = ez->vec_or(unequal_ab, ez->vec_or(undef_a, undef_b));
 291                                 std::vector<int> yX = ez->vec_ite(undef_s.at(0), undef_ab, ez->vec_ite(s.at(0), undef_b, undef_a));
 292                                 ez->assume(ez->vec_eq(yX, undef_y));
 293                                 undefGating(y, yy, undef_y);
 294                         }
 295                         return true;
 296                 }
 297
 298                 if (cell->type == "$pmux" || cell->type == "$safe_pmux")
 299                 {
 300                         std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep);
 301                         std::vector<int> b = importDefSigSpec(cell->connections.at("\\B"), timestep);
 302                         std::vector<int> s = importDefSigSpec(cell->connections.at("\\S"), timestep);
 303                         std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
 304                         std::vector<int> tmp = a;
 305                         for (size_t i = 0; i < s.size(); i++) {
 306                                 std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
 307                                 tmp = ez->vec_ite(s.at(i), part_of_b, tmp);
 308                         }
 309                         if (cell->type == "$safe_pmux")
 310                                 tmp = ez->vec_ite(ez->onehot(s, true), tmp, a);
 311                         ez->assume(ez->vec_eq(tmp, y));
 312
 313                         if (model_undef) {
 314                                 log("FIXME: No SAT undef model cell type %s!\n", RTLIL::id2cstr(cell->type));
 315                                 std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
 316                                 ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_y)));
 317                         }
 318                         return true;
 319                 }
 320
 321                 if (cell->type == "$pos" || cell->type == "$neg")
 322                 {
 323                         std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep);
 324                         std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
 325                         extendSignalWidthUnary(a, y, cell);
 326
 327                         std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
 328
 329                         if (cell->type == "$pos") {
 330                                 ez->assume(ez->vec_eq(a, yy));
 331                         } else {
 332                                 std::vector<int> zero(a.size(), ez->FALSE);
 333                                 ez->assume(ez->vec_eq(ez->vec_sub(zero, a), yy));
 334                         }
 335
 336                         if (model_undef)
 337                         {
 338                                 std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 339                                 std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
 340                                 extendSignalWidthUnary(undef_a, undef_y, cell, true);
 341
 342                                 if (cell->type == "$pos") {
 343                                         ez->assume(ez->vec_eq(undef_a, undef_y));
 344                                 } else {
 345                                         int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
 346                                         std::vector<int> undef_y_bits(undef_y.size(), undef_any_a);
 347                                         ez->assume(ez->vec_eq(undef_y_bits, undef_y));
 348                                 }
 349
 350                                 undefGating(y, yy, undef_y);
 351                         }
 352                         return true;
 353                 }
 354
 355                 if (cell->type == "$reduce_and" || cell->type == "$reduce_or" || cell->type == "$reduce_xor" ||
 356                                 cell->type == "$reduce_xnor" || cell->type == "$reduce_bool" || cell->type == "$logic_not")
 357                 {
 358                         std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep);
 359                         std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
 360
 361                         std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
 362
 363                         if (cell->type == "$reduce_and")
 364                                 ez->SET(ez->expression(ez->OpAnd, a), yy.at(0));
 365                         if (cell->type == "$reduce_or" || cell->type == "$reduce_bool")
 366                                 ez->SET(ez->expression(ez->OpOr, a), yy.at(0));
 367                         if (cell->type == "$reduce_xor")
 368                                 ez->SET(ez->expression(ez->OpXor, a), yy.at(0));
 369                         if (cell->type == "$reduce_xnor")
 370                                 ez->SET(ez->NOT(ez->expression(ez->OpXor, a)), yy.at(0));
 371                         if (cell->type == "$logic_not")
 372                                 ez->SET(ez->NOT(ez->expression(ez->OpOr, a)), yy.at(0));
 373                         for (size_t i = 1; i < y.size(); i++)
 374                                 ez->SET(ez->FALSE, yy.at(i));
 375
 376                         if (model_undef)
 377                         {
 378                                 std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 379                                 std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
 380                                 int aX = ez->expression(ezSAT::OpOr, undef_a);
 381
 382                                 if (cell->type == "$reduce_and") {
 383                                         int a0 = ez->expression(ezSAT::OpOr, ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a)));
 384                                         ez->assume(ez->IFF(ez->AND(ez->NOT(a0), aX), undef_y.at(0)));
 385                                 }
 386                                 else if (cell->type == "$reduce_or" || cell->type == "$reduce_bool" || cell->type == "$logic_not") {
 387                                         int a1 = ez->expression(ezSAT::OpOr, ez->vec_and(a, ez->vec_not(undef_a)));
 388                                         ez->assume(ez->IFF(ez->AND(ez->NOT(a1), aX), undef_y.at(0)));
 389                                 }
 390                                 else if (cell->type == "$reduce_xor" || cell->type == "$reduce_xnor") {
 391                                         ez->assume(ez->IFF(aX, undef_y.at(0)));
 392                                 } else
 393                                         log_abort();
 394
 395                                 for (size_t i = 1; i < undef_y.size(); i++)
 396                                         ez->SET(ez->FALSE, undef_y.at(i));
 397
 398                                 undefGating(y, yy, undef_y);
 399                         }
 400                         return true;
 401                 }
 402
 403                 if (cell->type == "$logic_and" || cell->type == "$logic_or")
 404                 {
 405                         std::vector<int> vec_a = importDefSigSpec(cell->connections.at("\\A"), timestep);
 406                         std::vector<int> vec_b = importDefSigSpec(cell->connections.at("\\B"), timestep);
 407
 408                         int a = ez->expression(ez->OpOr, vec_a);
 409                         int b = ez->expression(ez->OpOr, vec_b);
 410                         std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
 411
 412                         std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
 413
 414                         if (cell->type == "$logic_and")
 415                                 ez->SET(ez->expression(ez->OpAnd, a, b), yy.at(0));
 416                         else
 417                                 ez->SET(ez->expression(ez->OpOr, a, b), yy.at(0));
 418                         for (size_t i = 1; i < y.size(); i++)
 419                                 ez->SET(ez->FALSE, yy.at(i));
 420
 421                         if (model_undef)
 422                         {
 423                                 std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 424                                 std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
 425                                 std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
 426
 427                                 int a0 = ez->NOT(ez->OR(ez->expression(ezSAT::OpOr, vec_a), ez->expression(ezSAT::OpOr, undef_a)));
 428                                 int b0 = ez->NOT(ez->OR(ez->expression(ezSAT::OpOr, vec_b), ez->expression(ezSAT::OpOr, undef_b)));
 429                                 int a1 = ez->expression(ezSAT::OpOr, ez->vec_and(vec_a, ez->vec_not(undef_a)));
 430                                 int b1 = ez->expression(ezSAT::OpOr, ez->vec_and(vec_b, ez->vec_not(undef_b)));
 431                                 int aX = ez->expression(ezSAT::OpOr, undef_a);
 432                                 int bX = ez->expression(ezSAT::OpOr, undef_b);
 433
 434                                 if (cell->type == "$logic_and")
 435                                         ez->SET(ez->AND(ez->OR(aX, bX), ez->NOT(ez->AND(a1, b1)), ez->NOT(a0), ez->NOT(b0)), undef_y.at(0));
 436                                 else if (cell->type == "$logic_or")
 437                                         ez->SET(ez->AND(ez->OR(aX, bX), ez->NOT(ez->AND(a0, b0)), ez->NOT(a1), ez->NOT(b1)), undef_y.at(0));
 438                                 else
 439                                         log_abort();
 440
 441                                 for (size_t i = 1; i < undef_y.size(); i++)
 442                                         ez->SET(ez->FALSE, undef_y.at(i));
 443
 444                                 undefGating(y, yy, undef_y);
 445                         }
 446                         return true;
 447                 }
 448
 449                 if (cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex" || cell->type == "$ge" || cell->type == "$gt")
 450                 {
 451                         bool is_signed = cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool();
 452                         std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep);
 453                         std::vector<int> b = importDefSigSpec(cell->connections.at("\\B"), timestep);
 454                         std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
 455                         extendSignalWidth(a, b, cell);
 456
 457                         std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
 458
 459                         if (model_undef && (cell->type == "$eqx" || cell->type == "$nex")) {
 460                                 std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 461                                 std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
 462                                 extendSignalWidth(undef_a, undef_b, cell, true);
 463                                 a = ez->vec_or(a, undef_a);
 464                                 b = ez->vec_or(b, undef_b);
 465                         }
 466
 467                         if (cell->type == "$lt")
 468                                 ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), yy.at(0));
 469                         if (cell->type == "$le")
 470                                 ez->SET(is_signed ? ez->vec_le_signed(a, b) : ez->vec_le_unsigned(a, b), yy.at(0));
 471                         if (cell->type == "$eq" || cell->type == "$eqx")
 472                                 ez->SET(ez->vec_eq(a, b), yy.at(0));
 473                         if (cell->type == "$ne" || cell->type == "$nex")
 474                                 ez->SET(ez->vec_ne(a, b), yy.at(0));
 475                         if (cell->type == "$ge")
 476                                 ez->SET(is_signed ? ez->vec_ge_signed(a, b) : ez->vec_ge_unsigned(a, b), yy.at(0));
 477                         if (cell->type == "$gt")
 478                                 ez->SET(is_signed ? ez->vec_gt_signed(a, b) : ez->vec_gt_unsigned(a, b), yy.at(0));
 479                         for (size_t i = 1; i < y.size(); i++)
 480                                 ez->SET(ez->FALSE, yy.at(i));
 481
 482                         if (model_undef && (cell->type == "$eqx" || cell->type == "$nex"))
 483                         {
 484                                 std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 485                                 std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
 486                                 std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
 487                                 extendSignalWidth(undef_a, undef_b, cell, true);
 488
 489                                 if (cell->type == "$eqx")
 490                                         yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
 491                                 else
 492                                         yy.at(0) = ez->OR(yy.at(0), ez->vec_ne(undef_a, undef_b));
 493
 494                                 for (size_t i = 0; i < y.size(); i++)
 495                                         ez->SET(ez->FALSE, undef_y.at(i));
 496
 497                                 ez->assume(ez->vec_eq(y, yy));
 498                         }
 499                         else if (model_undef && (cell->type == "$eq" || cell->type == "$ne"))
 500                         {
 501                                 std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 502                                 std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
 503                                 std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
 504                                 extendSignalWidth(undef_a, undef_b, cell, true);
 505
 506                                 int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
 507                                 int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
 508                                 int undef_any = ez->OR(undef_any_a, undef_any_b);
 509
 510                                 std::vector<int> masked_a_bits = ez->vec_or(a, ez->vec_or(undef_a, undef_b));
 511                                 std::vector<int> masked_b_bits = ez->vec_or(b, ez->vec_or(undef_a, undef_b));
 512
 513                                 int masked_ne = ez->vec_ne(masked_a_bits, masked_b_bits);
 514                                 int undef_y_bit = ez->AND(undef_any, ez->NOT(masked_ne));
 515
 516                                 for (size_t i = 1; i < undef_y.size(); i++)
 517                                         ez->SET(ez->FALSE, undef_y.at(i));
 518                                 ez->SET(undef_y_bit, undef_y.at(0));
 519
 520                                 undefGating(y, yy, undef_y);
 521                         }
 522                         else
 523                         {
 524                                 if (model_undef) {
 525                                         std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
 526                                         undefGating(y, yy, undef_y);
 527                                 }
 528                                 log_assert(!model_undef || arith_undef_handled);
 529                         }
 530                         return true;
 531                 }
 532
 533                 if (cell->type == "$shl" || cell->type == "$shr" || cell->type == "$sshl" || cell->type == "$sshr")
 534                 {
 535                         std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep);
 536                         std::vector<int> b = importDefSigSpec(cell->connections.at("\\B"), timestep);
 537                         std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
 538
 539                         char shift_left = cell->type == "$shl" || cell->type == "$sshl";
 540                         bool sign_extend = cell->type == "$sshr" && cell->parameters["\\A_SIGNED"].as_bool();
 541
 542                         while (y.size() < a.size())
 543                                 y.push_back(ez->literal());
 544                         while (y.size() > a.size())
 545                                 a.push_back(cell->parameters["\\A_SIGNED"].as_bool() ? a.back() : ez->FALSE);
 546
 547                         std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
 548
 549                         std::vector<int> tmp = a;
 550                         for (size_t i = 0; i < b.size(); i++)
 551                         {
 552                                 std::vector<int> tmp_shifted(tmp.size());
 553                                 for (size_t j = 0; j < tmp.size(); j++) {
 554                                         int idx = j + (1 << (i > 30 ? 30 : i)) * (shift_left ? -1 : +1);
 555                                         tmp_shifted.at(j) = (0 <= idx && idx < int(tmp.size())) ? tmp.at(idx) : sign_extend ? tmp.back() : ez->FALSE;
 556                                 }
 557                                 tmp = ez->vec_ite(b.at(i), tmp_shifted, tmp);
 558                         }
 559                         ez->assume(ez->vec_eq(tmp, yy));
 560
 561                         if (model_undef)
 562                         {
 563                                 std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 564                                 std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
 565                                 std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
 566
 567                                 while (undef_y.size() < undef_a.size())
 568                                         undef_y.push_back(ez->literal());
 569                                 while (undef_y.size() > undef_a.size())
 570                                         undef_a.push_back(undef_a.back());
 571
 572                                 tmp = undef_a;
 573                                 for (size_t i = 0; i < b.size(); i++)
 574                                 {
 575                                         std::vector<int> tmp_shifted(tmp.size());
 576                                         for (size_t j = 0; j < tmp.size(); j++) {
 577                                                 int idx = j + (1 << (i > 30 ? 30 : i)) * (shift_left ? -1 : +1);
 578                                                 tmp_shifted.at(j) = (0 <= idx && idx < int(tmp.size())) ? tmp.at(idx) : sign_extend ? tmp.back() : ez->FALSE;
 579                                         }
 580                                         tmp = ez->vec_ite(b.at(i), tmp_shifted, tmp);
 581                                 }
 582
 583                                 int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
 584                                 std::vector<int> undef_all_y_bits(undef_y.size(), undef_any_b);
 585                                 ez->assume(ez->vec_eq(ez->vec_or(tmp, undef_all_y_bits), undef_y));
 586                                 undefGating(y, yy, undef_y);
 587                         }
 588                         return true;
 589                 }
 590
 591                 if (cell->type == "$mul")
 592                 {
 593                         std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep);
 594                         std::vector<int> b = importDefSigSpec(cell->connections.at("\\B"), timestep);
 595                         std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
 596                         extendSignalWidth(a, b, y, cell);
 597
 598                         std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
 599
 600                         std::vector<int> tmp(a.size(), ez->FALSE);
 601                         for (int i = 0; i < int(a.size()); i++)
 602                         {
 603                                 std::vector<int> shifted_a(a.size(), ez->FALSE);
 604                                 for (int j = i; j < int(a.size()); j++)
 605                                         shifted_a.at(j) = a.at(j-i);
 606                                 tmp = ez->vec_ite(b.at(i), ez->vec_add(tmp, shifted_a), tmp);
 607                         }
 608                         ez->assume(ez->vec_eq(tmp, yy));
 609
 610                         if (model_undef) {
 611                                 log_assert(arith_undef_handled);
 612                                 std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
 613                                 undefGating(y, yy, undef_y);
 614                         }
 615                         return true;
 616                 }
 617
 618                 if (cell->type == "$div" || cell->type == "$mod")
 619                 {
 620                         std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep);
 621                         std::vector<int> b = importDefSigSpec(cell->connections.at("\\B"), timestep);
 622                         std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
 623                         extendSignalWidth(a, b, y, cell);
 624
 625                         std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
 626
 627                         std::vector<int> a_u, b_u;
 628                         if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool()) {
 629                                 a_u = ez->vec_ite(a.back(), ez->vec_neg(a), a);
 630                                 b_u = ez->vec_ite(b.back(), ez->vec_neg(b), b);
 631                         } else {
 632                                 a_u = a;
 633                                 b_u = b;
 634                         }
 635
 636                         std::vector<int> chain_buf = a_u;
 637                         std::vector<int> y_u(a_u.size(), ez->FALSE);
 638                         for (int i = int(a.size())-1; i >= 0; i--)
 639                         {
 640                                 chain_buf.insert(chain_buf.end(), chain_buf.size(), ez->FALSE);
 641
 642                                 std::vector<int> b_shl(i, ez->FALSE);
 643                                 b_shl.insert(b_shl.end(), b_u.begin(), b_u.end());
 644                                 b_shl.insert(b_shl.end(), chain_buf.size()-b_shl.size(), ez->FALSE);
 645
 646                                 y_u.at(i) = ez->vec_ge_unsigned(chain_buf, b_shl);
 647                                 chain_buf = ez->vec_ite(y_u.at(i), ez->vec_sub(chain_buf, b_shl), chain_buf);
 648
 649                                 chain_buf.erase(chain_buf.begin() + a_u.size(), chain_buf.end());
 650                         }
 651
 652                         std::vector<int> y_tmp = ignore_div_by_zero ? yy : ez->vec_var(y.size());
 653                         if (cell->type == "$div") {
 654                                 if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
 655                                         ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(ez->XOR(a.back(), b.back()), ez->vec_neg(y_u), y_u)));
 656                                 else
 657                                         ez->assume(ez->vec_eq(y_tmp, y_u));
 658                         } else {
 659                                 if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
 660                                         ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(a.back(), ez->vec_neg(chain_buf), chain_buf)));
 661                                 else
 662                                         ez->assume(ez->vec_eq(y_tmp, chain_buf));
 663                         }
 664
 665                         if (ignore_div_by_zero) {
 666                                 ez->assume(ez->expression(ezSAT::OpOr, b));
 667                         } else {
 668                                 std::vector<int> div_zero_result;
 669                                 if (cell->type == "$div") {
 670                                         if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool()) {
 671                                                 std::vector<int> all_ones(y.size(), ez->TRUE);
 672                                                 std::vector<int> only_first_one(y.size(), ez->FALSE);
 673                                                 only_first_one.at(0) = ez->TRUE;
 674                                                 div_zero_result = ez->vec_ite(a.back(), only_first_one, all_ones);
 675                                         } else {
 676                                                 div_zero_result.insert(div_zero_result.end(), cell->connections.at("\\A").width, ez->TRUE);
 677                                                 div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->FALSE);
 678                                         }
 679                                 } else {
 680                                         int copy_a_bits = std::min(cell->connections.at("\\A").width, cell->connections.at("\\B").width);
 681                                         div_zero_result.insert(div_zero_result.end(), a.begin(), a.begin() + copy_a_bits);
 682                                         if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
 683                                                 div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), div_zero_result.back());
 684                                         else
 685                                                 div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->FALSE);
 686                                 }
 687                                 ez->assume(ez->vec_eq(yy, ez->vec_ite(ez->expression(ezSAT::OpOr, b), y_tmp, div_zero_result)));
 688                         }
 689
 690                         if (model_undef) {
 691                                 log_assert(arith_undef_handled);
 692                                 std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
 693                                 undefGating(y, yy, undef_y);
 694                         }
 695                         return true;
 696                 }
 697
 698                 if (timestep > 0 && (cell->type == "$dff" || cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_"))
 699                 {
 700                         if (timestep == 1)
 701                         {
 702                                 initial_state.add((*sigmap)(cell->connections.at("\\Q")));
 703                         }
 704                         else
 705                         {
 706                                 std::vector<int> d = importDefSigSpec(cell->connections.at("\\D"), timestep-1);
 707                                 std::vector<int> q = importDefSigSpec(cell->connections.at("\\Q"), timestep);
 708
 709                                 std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
 710                                 ez->assume(ez->vec_eq(d, qq));
 711
 712                                 if (model_undef)
 713                                 {
 714                                         std::vector<int> undef_d = importUndefSigSpec(cell->connections.at("\\D"), timestep-1);
 715                                         std::vector<int> undef_q = importUndefSigSpec(cell->connections.at("\\Q"), timestep);
 716
 717                                         ez->assume(ez->vec_eq(undef_d, undef_q));
 718                                         undefGating(q, qq, undef_q);
 719                                 }
 720                         }
 721                         return true;
 722                 }
 723
 724                 // Unsupported internal cell types: $pow $lut
 725                 // .. and all sequential cells except $dff and $_DFF_[NP]_
 726                 return false;
 727         }
 728 };
 729
 730 #endif
 731