kernel/satgen.h

   1 /* -*- c++ -*-
   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 #include "kernel/macc.h"
  27
  28 #include "libs/ezsat/ezminisat.h"
  29
  30 YOSYS_NAMESPACE_BEGIN
  31
  32 // defined in kernel/register.cc
  33 extern struct SatSolver *yosys_satsolver_list;
  34 extern struct SatSolver *yosys_satsolver;
  35
  36 struct SatSolver
  37 {
  38         string name;
  39         SatSolver *next;
  40         virtual ezSAT *create() = 0;
  41
  42         SatSolver(string name) : name(name) {
  43                 next = yosys_satsolver_list;
  44                 yosys_satsolver_list = this;
  45         }
  46
  47         virtual ~SatSolver() {
  48                 auto p = &yosys_satsolver_list;
  49                 while (*p) {
  50                         if (*p == this)
  51                                 *p = next;
  52                         else
  53                                 p = &(*p)->next;
  54                 }
  55                 if (yosys_satsolver == this)
  56                         yosys_satsolver = yosys_satsolver_list;
  57         }
  58 };
  59
  60 struct ezSatPtr : public std::unique_ptr<ezSAT> {
  61         ezSatPtr() : unique_ptr<ezSAT>(yosys_satsolver->create()) { }
  62 };
  63
  64 struct SatGen
  65 {
  66         ezSAT *ez;
  67         SigMap *sigmap;
  68         std::string prefix;
  69         SigPool initial_state;
  70         std::map<std::string, RTLIL::SigSpec> asserts_a, asserts_en;
  71         std::map<std::string, RTLIL::SigSpec> assumes_a, assumes_en;
  72         std::map<std::string, std::map<RTLIL::SigBit, int>> imported_signals;
  73         std::map<std::pair<std::string, int>, bool> initstates;
  74         bool ignore_div_by_zero;
  75         bool model_undef;
  76
  77         SatGen(ezSAT *ez, SigMap *sigmap, std::string prefix = std::string()) :
  78                         ez(ez), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false)
  79         {
  80         }
  81
  82         void setContext(SigMap *sigmap, std::string prefix = std::string())
  83         {
  84                 this->sigmap = sigmap;
  85                 this->prefix = prefix;
  86         }
  87
  88         std::vector<int> importSigSpecWorker(RTLIL::SigSpec sig, std::string &pf, bool undef_mode, bool dup_undef)
  89         {
  90                 log_assert(!undef_mode || model_undef);
  91                 sigmap->apply(sig);
  92
  93                 std::vector<int> vec;
  94                 vec.reserve(GetSize(sig));
  95
  96                 for (auto &bit : sig)
  97                         if (bit.wire == NULL) {
  98                                 if (model_undef && dup_undef && bit == RTLIL::State::Sx)
  99                                         vec.push_back(ez->frozen_literal());
 100                                 else
 101                                         vec.push_back(bit == (undef_mode ? RTLIL::State::Sx : RTLIL::State::S1) ? ez->CONST_TRUE : ez->CONST_FALSE);
 102                         } else {
 103                                 std::string name = pf + (bit.wire->width == 1 ? stringf("%s", log_id(bit.wire)) : stringf("%s [%d]", log_id(bit.wire->name), bit.offset));
 104                                 vec.push_back(ez->frozen_literal(name));
 105                                 imported_signals[pf][bit] = vec.back();
 106                         }
 107                 return vec;
 108         }
 109
 110         std::vector<int> importSigSpec(RTLIL::SigSpec sig, int timestep = -1)
 111         {
 112                 log_assert(timestep != 0);
 113                 std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
 114                 return importSigSpecWorker(sig, pf, false, false);
 115         }
 116
 117         std::vector<int> importDefSigSpec(RTLIL::SigSpec sig, int timestep = -1)
 118         {
 119                 log_assert(timestep != 0);
 120                 std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
 121                 return importSigSpecWorker(sig, pf, false, true);
 122         }
 123
 124         std::vector<int> importUndefSigSpec(RTLIL::SigSpec sig, int timestep = -1)
 125         {
 126                 log_assert(timestep != 0);
 127                 std::string pf = "undef:" + prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
 128                 return importSigSpecWorker(sig, pf, true, false);
 129         }
 130
 131         int importSigBit(RTLIL::SigBit bit, int timestep = -1)
 132         {
 133                 log_assert(timestep != 0);
 134                 std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
 135                 return importSigSpecWorker(bit, pf, false, false).front();
 136         }
 137
 138         int importDefSigBit(RTLIL::SigBit bit, int timestep = -1)
 139         {
 140                 log_assert(timestep != 0);
 141                 std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
 142                 return importSigSpecWorker(bit, pf, false, true).front();
 143         }
 144
 145         int importUndefSigBit(RTLIL::SigBit bit, int timestep = -1)
 146         {
 147                 log_assert(timestep != 0);
 148                 std::string pf = "undef:" + prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
 149                 return importSigSpecWorker(bit, pf, true, false).front();
 150         }
 151
 152         bool importedSigBit(RTLIL::SigBit bit, int timestep = -1)
 153         {
 154                 log_assert(timestep != 0);
 155                 std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
 156                 return imported_signals[pf].count(bit) != 0;
 157         }
 158
 159         void getAsserts(RTLIL::SigSpec &sig_a, RTLIL::SigSpec &sig_en, int timestep = -1)
 160         {
 161                 std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
 162                 sig_a = asserts_a[pf];
 163                 sig_en = asserts_en[pf];
 164         }
 165
 166         void getAssumes(RTLIL::SigSpec &sig_a, RTLIL::SigSpec &sig_en, int timestep = -1)
 167         {
 168                 std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
 169                 sig_a = assumes_a[pf];
 170                 sig_en = assumes_en[pf];
 171         }
 172
 173         int importAsserts(int timestep = -1)
 174         {
 175                 std::vector<int> check_bits, enable_bits;
 176                 std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
 177                 if (model_undef) {
 178                         check_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_a[pf], timestep)), importDefSigSpec(asserts_a[pf], timestep));
 179                         enable_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_en[pf], timestep)), importDefSigSpec(asserts_en[pf], timestep));
 180                 } else {
 181                         check_bits = importDefSigSpec(asserts_a[pf], timestep);
 182                         enable_bits = importDefSigSpec(asserts_en[pf], timestep);
 183                 }
 184                 return ez->vec_reduce_and(ez->vec_or(check_bits, ez->vec_not(enable_bits)));
 185         }
 186
 187         int importAssumes(int timestep = -1)
 188         {
 189                 std::vector<int> check_bits, enable_bits;
 190                 std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
 191                 if (model_undef) {
 192                         check_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(assumes_a[pf], timestep)), importDefSigSpec(assumes_a[pf], timestep));
 193                         enable_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(assumes_en[pf], timestep)), importDefSigSpec(assumes_en[pf], timestep));
 194                 } else {
 195                         check_bits = importDefSigSpec(assumes_a[pf], timestep);
 196                         enable_bits = importDefSigSpec(assumes_en[pf], timestep);
 197                 }
 198                 return ez->vec_reduce_and(ez->vec_or(check_bits, ez->vec_not(enable_bits)));
 199         }
 200
 201         int signals_eq(RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep_lhs = -1, int timestep_rhs = -1)
 202         {
 203                 if (timestep_rhs < 0)
 204                         timestep_rhs = timestep_lhs;
 205
 206                 log_assert(lhs.size() == rhs.size());
 207
 208                 std::vector<int> vec_lhs = importSigSpec(lhs, timestep_lhs);
 209                 std::vector<int> vec_rhs = importSigSpec(rhs, timestep_rhs);
 210
 211                 if (!model_undef)
 212                         return ez->vec_eq(vec_lhs, vec_rhs);
 213
 214                 std::vector<int> undef_lhs = importUndefSigSpec(lhs, timestep_lhs);
 215                 std::vector<int> undef_rhs = importUndefSigSpec(rhs, timestep_rhs);
 216
 217                 std::vector<int> eq_bits;
 218                 for (int i = 0; i < lhs.size(); i++)
 219                         eq_bits.push_back(ez->AND(ez->IFF(undef_lhs.at(i), undef_rhs.at(i)),
 220                                         ez->IFF(ez->OR(vec_lhs.at(i), undef_lhs.at(i)), ez->OR(vec_rhs.at(i), undef_rhs.at(i)))));
 221                 return ez->expression(ezSAT::OpAnd, eq_bits);
 222         }
 223
 224         void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell, size_t y_width = 0, bool forced_signed = false)
 225         {
 226                 bool is_signed = forced_signed;
 227                 if (!forced_signed && cell->parameters.count(ID::A_SIGNED) > 0 && cell->parameters.count(ID::B_SIGNED) > 0)
 228                         is_signed = cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool();
 229                 while (vec_a.size() < vec_b.size() || vec_a.size() < y_width)
 230                         vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->CONST_FALSE);
 231                 while (vec_b.size() < vec_a.size() || vec_b.size() < y_width)
 232                         vec_b.push_back(is_signed && vec_b.size() > 0 ? vec_b.back() : ez->CONST_FALSE);
 233         }
 234
 235         void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &vec_y, RTLIL::Cell *cell, bool forced_signed = false)
 236         {
 237                 extendSignalWidth(vec_a, vec_b, cell, vec_y.size(), forced_signed);
 238                 while (vec_y.size() < vec_a.size())
 239                         vec_y.push_back(ez->literal());
 240         }
 241
 242         void extendSignalWidthUnary(std::vector<int> &vec_a, std::vector<int> &vec_y, RTLIL::Cell *cell, bool forced_signed = false)
 243         {
 244                 bool is_signed = forced_signed || (cell->parameters.count(ID::A_SIGNED) > 0 && cell->parameters[ID::A_SIGNED].as_bool());
 245                 while (vec_a.size() < vec_y.size())
 246                         vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->CONST_FALSE);
 247                 while (vec_y.size() < vec_a.size())
 248                         vec_y.push_back(ez->literal());
 249         }
 250
 251         void undefGating(std::vector<int> &vec_y, std::vector<int> &vec_yy, std::vector<int> &vec_undef)
 252         {
 253                 log_assert(model_undef);
 254                 log_assert(vec_y.size() == vec_yy.size());
 255                 if (vec_y.size() > vec_undef.size()) {
 256                         std::vector<int> trunc_y(vec_y.begin(), vec_y.begin() + vec_undef.size());
 257                         std::vector<int> trunc_yy(vec_yy.begin(), vec_yy.begin() + vec_undef.size());
 258                         ez->assume(ez->expression(ezSAT::OpAnd, ez->vec_or(vec_undef, ez->vec_iff(trunc_y, trunc_yy))));
 259                 } else {
 260                         log_assert(vec_y.size() == vec_undef.size());
 261                         ez->assume(ez->expression(ezSAT::OpAnd, ez->vec_or(vec_undef, ez->vec_iff(vec_y, vec_yy))));
 262                 }
 263         }
 264
 265         std::pair<std::vector<int>, std::vector<int>> mux(int s, int undef_s, const std::vector<int> &a, const std::vector<int> &undef_a, const std::vector<int> &b, const std::vector<int> &undef_b) {
 266                 std::vector<int> res;
 267                 std::vector<int> undef_res;
 268                 res = ez->vec_ite(s, b, a);
 269                 if (model_undef) {
 270                         std::vector<int> unequal_ab = ez->vec_not(ez->vec_iff(a, b));
 271                         std::vector<int> undef_ab = ez->vec_or(unequal_ab, ez->vec_or(undef_a, undef_b));
 272                         undef_res = ez->vec_ite(undef_s, undef_ab, ez->vec_ite(s, undef_b, undef_a));
 273                 }
 274                 return std::make_pair(res, undef_res);
 275         }
 276
 277         void undefGating(int y, int yy, int undef)
 278         {
 279                 ez->assume(ez->OR(undef, ez->IFF(y, yy)));
 280         }
 281
 282         void setInitState(int timestep)
 283         {
 284                 auto key = make_pair(prefix, timestep);
 285                 log_assert(initstates.count(key) == 0 || initstates.at(key) == true);
 286                 initstates[key] = true;
 287         }
 288
 289         bool importCell(RTLIL::Cell *cell, int timestep = -1);
 290 };
 291
 292 YOSYS_NAMESPACE_END
 293
 294 #endif