kernel/satgen.h

   1 /*
   2  *  yosys -- Yosys Open SYnthesis Suite
   3  *
   4  *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
   5  *
   6  *  Permission to use, copy, modify, and/or distribute this software for any
   7  *  purpose with or without fee is hereby granted, provided that the above
   8  *  copyright notice and this permission notice appear in all copies.
   9  *
  10  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17  *
  18  */
  19
  20 #ifndef SATGEN_H
  21 #define SATGEN_H
  22
  23 #include "kernel/rtlil.h"
  24 #include "kernel/sigtools.h"
  25 #include "kernel/celltypes.h"
  26
  27 #ifdef YOSYS_ENABLE_MINISAT
  28 #  include "libs/ezsat/ezminisat.h"
  29 typedef ezMiniSAT ezDefaultSAT;
  30 #else
  31 #  include "libs/ezsat/ezsat.h"
  32 typedef ezSAT ezDefaultSAT;
  33 #endif
  34
  35 struct SatGen
  36 {
  37         ezSAT *ez;
  38         RTLIL::Design *design;
  39         SigMap *sigmap;
  40         std::string prefix;
  41         SigPool initial_state;
  42         bool ignore_div_by_zero;
  43
  44         SatGen(ezSAT *ez, RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string()) :
  45                         ez(ez), design(design), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false)
  46         {
  47         }
  48
  49         void setContext(RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string())
  50         {
  51                 this->design = design;
  52                 this->sigmap = sigmap;
  53                 this->prefix = prefix;
  54         }
  55
  56         std::vector<int> importSigSpec(RTLIL::SigSpec &sig, int timestep = -1)
  57         {
  58                 assert(timestep < 0 || timestep > 0);
  59                 RTLIL::SigSpec s = sig;
  60                 sigmap->apply(s);
  61                 s.expand();
  62
  63                 std::vector<int> vec;
  64                 vec.reserve(s.chunks.size());
  65
  66                 for (auto &c : s.chunks)
  67                         if (c.wire == NULL) {
  68                                 vec.push_back(c.data.as_bool() ? ez->TRUE : ez->FALSE);
  69                         } else {
  70                                 std::string name = prefix;
  71                                 name += timestep == -1 ? "" : stringf("@%d:", timestep);
  72                                 name += 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         void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell, size_t y_width = 0)
  79         {
  80                 bool is_signed = false;
  81                 if (cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters.count("\\B_SIGNED") > 0)
  82                         is_signed = cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool();
  83                 while (vec_a.size() < vec_b.size() || vec_a.size() < y_width)
  84                         vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
  85                 while (vec_b.size() < vec_a.size() || vec_b.size() < y_width)
  86                         vec_b.push_back(is_signed && vec_b.size() > 0 ? vec_b.back() : ez->FALSE);
  87         }
  88
  89         void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &vec_y, RTLIL::Cell *cell)
  90         {
  91                 extendSignalWidth(vec_a, vec_b, cell, vec_y.size());
  92                 while (vec_y.size() < vec_a.size())
  93                         vec_y.push_back(ez->literal());
  94         }
  95
  96         void extendSignalWidthUnary(std::vector<int> &vec_a, std::vector<int> &vec_y, RTLIL::Cell *cell)
  97         {
  98                 bool is_signed = cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters["\\A_SIGNED"].as_bool();
  99                 while (vec_a.size() < vec_y.size())
 100                         vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
 101                 while (vec_y.size() < vec_a.size())
 102                         vec_y.push_back(ez->literal());
 103         }
 104
 105         bool importCell(RTLIL::Cell *cell, int timestep = -1)
 106         {
 107                 if (cell->type == "$_AND_" || cell->type == "$_OR_" || cell->type == "$_XOR_" ||
 108                                 cell->type == "$and" || cell->type == "$or" || cell->type == "$xor" || cell->type == "$xnor" ||
 109                                 cell->type == "$add" || cell->type == "$sub") {
 110                         std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
 111                         std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
 112                         std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
 113                         extendSignalWidth(a, b, y, cell);
 114                         if (cell->type == "$and" || cell->type == "$_AND_")
 115                                 ez->assume(ez->vec_eq(ez->vec_and(a, b), y));
 116                         if (cell->type == "$or" || cell->type == "$_OR_")
 117                                 ez->assume(ez->vec_eq(ez->vec_or(a, b), y));
 118                         if (cell->type == "$xor" || cell->type == "$_XOR_")
 119                                 ez->assume(ez->vec_eq(ez->vec_xor(a, b), y));
 120                         if (cell->type == "$xnor")
 121                                 ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(a, b)), y));
 122                         if (cell->type == "$add")
 123                                 ez->assume(ez->vec_eq(ez->vec_add(a, b), y));
 124                         if (cell->type == "$sub")
 125                                 ez->assume(ez->vec_eq(ez->vec_sub(a, b), y));
 126                         return true;
 127                 }
 128
 129                 if (cell->type == "$_INV_" || cell->type == "$not") {
 130                         std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
 131                         std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
 132                         extendSignalWidthUnary(a, y, cell);
 133                         ez->assume(ez->vec_eq(ez->vec_not(a), y));
 134                         return true;
 135                 }
 136
 137                 if (cell->type == "$_MUX_" || cell->type == "$mux") {
 138                         std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
 139                         std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
 140                         std::vector<int> s = importSigSpec(cell->connections.at("\\S"), timestep);
 141                         std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
 142                         ez->assume(ez->vec_eq(ez->vec_ite(s.at(0), b, a), y));
 143                         return true;
 144                 }
 145
 146                 if (cell->type == "$pmux" || cell->type == "$safe_pmux") {
 147                         std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
 148                         std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
 149                         std::vector<int> s = importSigSpec(cell->connections.at("\\S"), timestep);
 150                         std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
 151                         std::vector<int> tmp = a;
 152                         for (size_t i = 0; i < s.size(); i++) {
 153                                 std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
 154                                 tmp = ez->vec_ite(s.at(i), part_of_b, tmp);
 155                         }
 156                         if (cell->type == "$safe_pmux")
 157                                 tmp = ez->vec_ite(ez->onehot(s, true), tmp, a);
 158                         ez->assume(ez->vec_eq(tmp, y));
 159                         return true;
 160                 }
 161
 162                 if (cell->type == "$pos" || cell->type == "$neg") {
 163                         std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
 164                         std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
 165                         extendSignalWidthUnary(a, y, cell);
 166                         if (cell->type == "$pos") {
 167                                 ez->assume(ez->vec_eq(a, y));
 168                         } else {
 169                                 std::vector<int> zero(a.size(), ez->FALSE);
 170                                 ez->assume(ez->vec_eq(ez->vec_sub(zero, a), y));
 171                         }
 172                         return true;
 173                 }
 174
 175                 if (cell->type == "$reduce_and" || cell->type == "$reduce_or" || cell->type == "$reduce_xor" ||
 176                                 cell->type == "$reduce_xnor" || cell->type == "$reduce_bool" || cell->type == "$logic_not") {
 177                         std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
 178                         std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
 179                         if (cell->type == "$reduce_and")
 180                                 ez->SET(ez->expression(ez->OpAnd, a), y.at(0));
 181                         if (cell->type == "$reduce_or" || cell->type == "$reduce_bool")
 182                                 ez->SET(ez->expression(ez->OpOr, a), y.at(0));
 183                         if (cell->type == "$reduce_xor")
 184                                 ez->SET(ez->expression(ez->OpXor, a), y.at(0));
 185                         if (cell->type == "$reduce_xnor")
 186                                 ez->SET(ez->NOT(ez->expression(ez->OpXor, a)), y.at(0));
 187                         if (cell->type == "$logic_not")
 188                                 ez->SET(ez->NOT(ez->expression(ez->OpOr, a)), y.at(0));
 189                         for (size_t i = 1; i < y.size(); i++)
 190                                 ez->SET(0, y.at(0));
 191                         return true;
 192                 }
 193
 194                 if (cell->type == "$logic_and" || cell->type == "$logic_or") {
 195                         int a = ez->expression(ez->OpOr, importSigSpec(cell->connections.at("\\A"), timestep));
 196                         int b = ez->expression(ez->OpOr, importSigSpec(cell->connections.at("\\B"), timestep));
 197                         std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
 198                         if (cell->type == "$logic_and")
 199                                 ez->SET(ez->expression(ez->OpAnd, a, b), y.at(0));
 200                         else
 201                                 ez->SET(ez->expression(ez->OpOr, a, b), y.at(0));
 202                         for (size_t i = 1; i < y.size(); i++)
 203                                 ez->SET(0, y.at(0));
 204                         return true;
 205                 }
 206
 207                 if (cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" || cell->type == "$ge" || cell->type == "$gt") {
 208                         bool is_signed = cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool();
 209                         std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
 210                         std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
 211                         std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
 212                         extendSignalWidth(a, b, cell);
 213                         if (cell->type == "$lt")
 214                                 ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), y.at(0));
 215                         if (cell->type == "$le")
 216                                 ez->SET(is_signed ? ez->vec_le_signed(a, b) : ez->vec_le_unsigned(a, b), y.at(0));
 217                         if (cell->type == "$eq")
 218                                 ez->SET(ez->vec_eq(a, b), y.at(0));
 219                         if (cell->type == "$ne")
 220                                 ez->SET(ez->vec_ne(a, b), y.at(0));
 221                         if (cell->type == "$ge")
 222                                 ez->SET(is_signed ? ez->vec_ge_signed(a, b) : ez->vec_ge_unsigned(a, b), y.at(0));
 223                         if (cell->type == "$gt")
 224                                 ez->SET(is_signed ? ez->vec_gt_signed(a, b) : ez->vec_gt_unsigned(a, b), y.at(0));
 225                         for (size_t i = 1; i < y.size(); i++)
 226                                 ez->SET(0, y.at(0));
 227                         return true;
 228                 }
 229
 230                 if (cell->type == "$shl" || cell->type == "$shr" || cell->type == "$sshl" || cell->type == "$sshr") {
 231                         std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
 232                         std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
 233                         std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
 234                         char shift_left = cell->type == "$shl" || cell->type == "$sshl";
 235                         bool sign_extend = cell->type == "$sshr" && cell->parameters["\\A_SIGNED"].as_bool();
 236                         while (y.size() < a.size())
 237                                 y.push_back(ez->literal());
 238                         while (y.size() > a.size())
 239                                 a.push_back(cell->parameters["\\A_SIGNED"].as_bool() ? a.back() : ez->FALSE);
 240                         std::vector<int> tmp = a;
 241                         for (size_t i = 0; i < b.size(); i++)
 242                         {
 243                                 std::vector<int> tmp_shifted(tmp.size());
 244                                 for (size_t j = 0; j < tmp.size(); j++) {
 245                                         int idx = j + (1 << (i > 30 ? 30 : i)) * (shift_left ? -1 : +1);
 246                                         tmp_shifted.at(j) = (0 <= idx && idx < int(tmp.size())) ? tmp.at(idx) : sign_extend ? tmp.back() : ez->FALSE;
 247                                 }
 248                                 tmp = ez->vec_ite(b.at(i), tmp_shifted, tmp);
 249                         }
 250                         ez->assume(ez->vec_eq(tmp, y));
 251                         return true;
 252                 }
 253
 254                 if (cell->type == "$mul") {
 255                         std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
 256                         std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
 257                         std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
 258                         extendSignalWidth(a, b, y, cell);
 259                         std::vector<int> tmp(a.size(), ez->FALSE);
 260                         for (int i = 0; i < int(a.size()); i++)
 261                         {
 262                                 std::vector<int> shifted_a(a.size(), ez->FALSE);
 263                                 for (int j = i; j < int(a.size()); j++)
 264                                         shifted_a.at(j) = a.at(j-i);
 265                                 tmp = ez->vec_ite(b.at(i), ez->vec_add(tmp, shifted_a), tmp);
 266                         }
 267                         ez->assume(ez->vec_eq(tmp, y));
 268                         return true;
 269                 }
 270
 271                 if (cell->type == "$div" || cell->type == "$mod")
 272                 {
 273                         std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
 274                         std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
 275                         std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
 276                         extendSignalWidth(a, b, y, cell);
 277
 278                         std::vector<int> a_u, b_u;
 279                         if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool()) {
 280                                 a_u = ez->vec_ite(a.back(), ez->vec_neg(a), a);
 281                                 b_u = ez->vec_ite(b.back(), ez->vec_neg(b), b);
 282                         } else {
 283                                 a_u = a;
 284                                 b_u = b;
 285                         }
 286
 287                         std::vector<int> chain_buf = a_u;
 288                         std::vector<int> y_u(a_u.size(), ez->FALSE);
 289                         for (int i = int(a.size())-1; i >= 0; i--)
 290                         {
 291                                 chain_buf.insert(chain_buf.end(), chain_buf.size(), ez->FALSE);
 292
 293                                 std::vector<int> b_shl(i, ez->FALSE);
 294                                 b_shl.insert(b_shl.end(), b_u.begin(), b_u.end());
 295                                 b_shl.insert(b_shl.end(), chain_buf.size()-b_shl.size(), ez->FALSE);
 296
 297                                 y_u.at(i) = ez->vec_ge_unsigned(chain_buf, b_shl);
 298                                 chain_buf = ez->vec_ite(y_u.at(i), ez->vec_sub(chain_buf, b_shl), chain_buf);
 299
 300                                 chain_buf.erase(chain_buf.begin() + a_u.size(), chain_buf.end());
 301                         }
 302
 303                         std::vector<int> y_tmp = ignore_div_by_zero ? y : ez->vec_var(y.size());
 304                         if (cell->type == "$div") {
 305                                 if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
 306                                         ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(ez->XOR(a.back(), b.back()), ez->vec_neg(y_u), y_u)));
 307                                 else
 308                                         ez->assume(ez->vec_eq(y_tmp, y_u));
 309                         } else {
 310                                 if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
 311                                         ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(a.back(), ez->vec_neg(chain_buf), chain_buf)));
 312                                 else
 313                                         ez->assume(ez->vec_eq(y_tmp, chain_buf));
 314                         }
 315
 316                         if (ignore_div_by_zero) {
 317                                 ez->assume(ez->expression(ezSAT::OpOr, b));
 318                         } else {
 319                                 std::vector<int> div_zero_result;
 320                                 if (cell->type == "$div") {
 321                                         if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool()) {
 322                                                 std::vector<int> all_ones(y.size(), ez->TRUE);
 323                                                 std::vector<int> only_first_one(y.size(), ez->FALSE);
 324                                                 only_first_one.at(0) = ez->TRUE;
 325                                                 div_zero_result = ez->vec_ite(a.back(), only_first_one, all_ones);
 326                                         } else {
 327                                                 div_zero_result.insert(div_zero_result.end(), cell->connections.at("\\A").width, ez->TRUE);
 328                                                 div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->FALSE);
 329                                         }
 330                                 } else {
 331                                         int copy_a_bits = std::min(cell->connections.at("\\A").width, cell->connections.at("\\B").width);
 332                                         div_zero_result.insert(div_zero_result.end(), a.begin(), a.begin() + copy_a_bits);
 333                                         if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
 334                                                 div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), div_zero_result.back());
 335                                         else
 336                                                 div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->FALSE);
 337                                 }
 338                                 ez->assume(ez->vec_eq(y, ez->vec_ite(ez->expression(ezSAT::OpOr, b), y_tmp, div_zero_result)));
 339                         }
 340
 341                         return true;
 342                 }
 343
 344                 if (timestep > 0 && (cell->type == "$dff" || cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_")) {
 345                         if (timestep == 1) {
 346                                 initial_state.add((*sigmap)(cell->connections.at("\\Q")));
 347                         } else {
 348                                 std::vector<int> d = importSigSpec(cell->connections.at("\\D"), timestep-1);
 349                                 std::vector<int> q = importSigSpec(cell->connections.at("\\Q"), timestep);
 350                                 ez->assume(ez->vec_eq(d, q));
 351                         }
 352                         return true;
 353                 }
 354
 355                 // Unsupported internal cell types: $div $mod $pow
 356                 // .. and all sequential cells except $dff and $_DFF_[NP]_
 357                 return false;
 358         }
 359 };
 360
 361 #endif
 362