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