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