yosys-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Public Member Functions | Data Fields
SatGen Struct Reference

#include <satgen.h>

+ Collaboration diagram for SatGen:

Public Member Functions

 SatGen (ezSAT *ez, SigMap *sigmap, std::string prefix=std::string())
 
void setContext (SigMap *sigmap, std::string prefix=std::string())
 
std::vector< int > importSigSpecWorker (RTLIL::SigSpec sig, std::string &pf, bool undef_mode, bool dup_undef)
 
std::vector< int > importSigSpec (RTLIL::SigSpec sig, int timestep=-1)
 
std::vector< int > importDefSigSpec (RTLIL::SigSpec sig, int timestep=-1)
 
std::vector< int > importUndefSigSpec (RTLIL::SigSpec sig, int timestep=-1)
 
int importSigBit (RTLIL::SigBit bit, int timestep=-1)
 
bool importedSigBit (RTLIL::SigBit bit, int timestep=-1)
 
void getAsserts (RTLIL::SigSpec &sig_a, RTLIL::SigSpec &sig_en, int timestep=-1)
 
int importAsserts (int timestep=-1)
 
int signals_eq (RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep_lhs=-1, int timestep_rhs=-1)
 
void extendSignalWidth (std::vector< int > &vec_a, std::vector< int > &vec_b, RTLIL::Cell *cell, size_t y_width=0, bool forced_signed=false)
 
void extendSignalWidth (std::vector< int > &vec_a, std::vector< int > &vec_b, std::vector< int > &vec_y, RTLIL::Cell *cell, bool forced_signed=false)
 
void extendSignalWidthUnary (std::vector< int > &vec_a, std::vector< int > &vec_y, RTLIL::Cell *cell, bool forced_signed=false)
 
void undefGating (std::vector< int > &vec_y, std::vector< int > &vec_yy, std::vector< int > &vec_undef)
 
void undefGating (int y, int yy, int undef)
 
bool importCell (RTLIL::Cell *cell, int timestep=-1)
 

Data Fields

ezSAT * ez
 
SigMap * sigmap
 
std::string prefix
 
SigPool initial_state
 
std::map< std::string,
RTLIL::SigSpec > 		asserts_a
 
std::map< std::string,
RTLIL::SigSpec > 		asserts_en
 
std::map< std::string,
std::map< RTLIL::SigBit, int > > 		imported_signals
 
bool ignore_div_by_zero
 
bool model_undef
 

Detailed Description

Definition at line 34 of file satgen.h.

Constructor & Destructor Documentation

SatGen::SatGen ( ezSAT *  ez,
SigMap *  sigmap,
std::string  prefix = std::string() 
)
inline

Definition at line 45 of file satgen.h.

45  :
46  ez(ez), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false)
47  {
48  }
SatGen::ez
ezSAT * ez
Definition: satgen.h:36
SatGen::ignore_div_by_zero
bool ignore_div_by_zero
Definition: satgen.h:42
SatGen::model_undef
bool model_undef
Definition: satgen.h:43
SatGen::sigmap
SigMap * sigmap
Definition: satgen.h:37
SatGen::prefix
std::string prefix
Definition: satgen.h:38

Member Function Documentation

void SatGen::extendSignalWidth ( std::vector< int > &  vec_a,
std::vector< int > &  vec_b,
RTLIL::Cell *  cell,
size_t  y_width = 0,
bool  forced_signed = false 
)
inline

Definition at line 157 of file satgen.h.

158  {
159  bool is_signed = forced_signed;
160  if (!forced_signed && cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters.count("\\B_SIGNED") > 0)
161  is_signed = cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool();
162  while (vec_a.size() < vec_b.size() || vec_a.size() < y_width)
163  vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->CONST_FALSE);
164  while (vec_b.size() < vec_a.size() || vec_b.size() < y_width)
165  vec_b.push_back(is_signed && vec_b.size() > 0 ? vec_b.back() : ez->CONST_FALSE);
166  }
SatGen::ez
ezSAT * ez
Definition: satgen.h:36
ezSAT::CONST_FALSE
static const int CONST_FALSE
Definition: ezsat.h:49
RTLIL::Cell::parameters
std::map< RTLIL::IdString, RTLIL::Const > parameters
Definition: rtlil.h:856

+ Here is the caller graph for this function:

void SatGen::extendSignalWidth ( std::vector< int > &  vec_a,
std::vector< int > &  vec_b,
std::vector< int > &  vec_y,
RTLIL::Cell *  cell,
bool  forced_signed = false 
)
inline

Definition at line 168 of file satgen.h.

169  {
170  extendSignalWidth(vec_a, vec_b, cell, vec_y.size(), forced_signed);
171  while (vec_y.size() < vec_a.size())
172  vec_y.push_back(ez->literal());
173  }
SatGen::ez
ezSAT * ez
Definition: satgen.h:36
SatGen::extendSignalWidth
void extendSignalWidth(std::vector< int > &vec_a, std::vector< int > &vec_b, RTLIL::Cell *cell, size_t y_width=0, bool forced_signed=false)
Definition: satgen.h:157
ezSAT::literal
int literal()
Definition: ezsat.cc:73

+ Here is the call graph for this function:

void SatGen::extendSignalWidthUnary ( std::vector< int > &  vec_a,
std::vector< int > &  vec_y,
RTLIL::Cell *  cell,
bool  forced_signed = false 
)
inline

Definition at line 175 of file satgen.h.

176  {
177  bool is_signed = forced_signed || (cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters["\\A_SIGNED"].as_bool());
178  while (vec_a.size() < vec_y.size())
179  vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->CONST_FALSE);
180  while (vec_y.size() < vec_a.size())
181  vec_y.push_back(ez->literal());
182  }
SatGen::ez
ezSAT * ez
Definition: satgen.h:36
ezSAT::CONST_FALSE
static const int CONST_FALSE
Definition: ezsat.h:49
RTLIL::Cell::parameters
std::map< RTLIL::IdString, RTLIL::Const > parameters
Definition: rtlil.h:856
ezSAT::literal
int literal()
Definition: ezsat.cc:73

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

void SatGen::getAsserts ( RTLIL::SigSpec &  sig_a,
RTLIL::SigSpec &  sig_en,
int  timestep = -1 
)
inline

Definition at line 113 of file satgen.h.

114  {
115  std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
116  sig_a = asserts_a[pf];
117  sig_en = asserts_en[pf];
118  }
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
SatGen::asserts_en
std::map< std::string, RTLIL::SigSpec > asserts_en
Definition: satgen.h:40
SatGen::asserts_a
std::map< std::string, RTLIL::SigSpec > asserts_a
Definition: satgen.h:40
SatGen::prefix
std::string prefix
Definition: satgen.h:38

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

int SatGen::importAsserts ( int  timestep = -1)
inline

Definition at line 120 of file satgen.h.

121  {
122  std::vector<int> check_bits, enable_bits;
123  std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
124  if (model_undef) {
125  check_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_a[pf], timestep)), importDefSigSpec(asserts_a[pf], timestep));
126  enable_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_en[pf], timestep)), importDefSigSpec(asserts_en[pf], timestep));
127  } else {
128  check_bits = importDefSigSpec(asserts_a[pf], timestep);
129  enable_bits = importDefSigSpec(asserts_en[pf], timestep);
130  }
131  return ez->vec_reduce_and(ez->vec_or(check_bits, ez->vec_not(enable_bits)));
132  }
SatGen::ez
ezSAT * ez
Definition: satgen.h:36
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
SatGen::asserts_en
std::map< std::string, RTLIL::SigSpec > asserts_en
Definition: satgen.h:40
ezSAT::vec_or
std::vector< int > vec_or(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:718
SatGen::model_undef
bool model_undef
Definition: satgen.h:43
SatGen::importUndefSigSpec
std::vector< int > importUndefSigSpec(RTLIL::SigSpec sig, int timestep=-1)
Definition: satgen.h:92
SatGen::importDefSigSpec
std::vector< int > importDefSigSpec(RTLIL::SigSpec sig, int timestep=-1)
Definition: satgen.h:85
ezSAT::vec_reduce_and
int vec_reduce_and(const std::vector< int > &vec1)
Definition: ezsat.cc:1139
SatGen::asserts_a
std::map< std::string, RTLIL::SigSpec > asserts_a
Definition: satgen.h:40
ezSAT::vec_not
std::vector< int > vec_not(const std::vector< int > &vec1)
Definition: ezsat.cc:701
SatGen::prefix
std::string prefix
Definition: satgen.h:38
ezSAT::vec_and
std::vector< int > vec_and(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:709

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

bool SatGen::importCell ( RTLIL::Cell *  cell,
int  timestep = -1 
)
inline

Definition at line 203 of file satgen.h.

204  {
205  bool arith_undef_handled = false;
206  bool is_arith_compare = cell->type.in("$lt", "$le", "$ge", "$gt");
207 
208  if (model_undef && (cell->type.in("$add", "$sub", "$mul", "$div", "$mod") || is_arith_compare))
209  {
210  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
211  std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
212  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
213  if (is_arith_compare)
214  extendSignalWidth(undef_a, undef_b, cell, true);
215  else
216  extendSignalWidth(undef_a, undef_b, undef_y, cell, true);
217 
218  int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
219  int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
220  int undef_y_bit = ez->OR(undef_any_a, undef_any_b);
221 
222  if (cell->type == "$div" || cell->type == "$mod") {
223  std::vector<int> b = importSigSpec(cell->getPort("\\B"), timestep);
224  undef_y_bit = ez->OR(undef_y_bit, ez->NOT(ez->expression(ezSAT::OpOr, b)));
225  }
226 
227  if (is_arith_compare) {
228  for (size_t i = 1; i < undef_y.size(); i++)
229  ez->SET(ez->CONST_FALSE, undef_y.at(i));
230  ez->SET(undef_y_bit, undef_y.at(0));
231  } else {
232  std::vector<int> undef_y_bits(undef_y.size(), undef_y_bit);
233  ez->assume(ez->vec_eq(undef_y_bits, undef_y));
234  }
235 
236  arith_undef_handled = true;
237  }
238 
239  if (cell->type.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_",
240  "$and", "$or", "$xor", "$xnor", "$add", "$sub"))
241  {
242  std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
243  std::vector<int> b = importDefSigSpec(cell->getPort("\\B"), timestep);
244  std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
245  extendSignalWidth(a, b, y, cell);
246 
247  std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
248 
249  if (cell->type == "$and" || cell->type == "$_AND_")
250  ez->assume(ez->vec_eq(ez->vec_and(a, b), yy));
251  if (cell->type == "$_NAND_")
252  ez->assume(ez->vec_eq(ez->vec_not(ez->vec_and(a, b)), yy));
253  if (cell->type == "$or" || cell->type == "$_OR_")
254  ez->assume(ez->vec_eq(ez->vec_or(a, b), yy));
255  if (cell->type == "$_NOR_")
256  ez->assume(ez->vec_eq(ez->vec_not(ez->vec_or(a, b)), yy));
257  if (cell->type == "$xor" || cell->type == "$_XOR_")
258  ez->assume(ez->vec_eq(ez->vec_xor(a, b), yy));
259  if (cell->type == "$xnor" || cell->type == "$_XNOR_")
260  ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(a, b)), yy));
261  if (cell->type == "$add")
262  ez->assume(ez->vec_eq(ez->vec_add(a, b), yy));
263  if (cell->type == "$sub")
264  ez->assume(ez->vec_eq(ez->vec_sub(a, b), yy));
265 
266  if (model_undef && !arith_undef_handled)
267  {
268  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
269  std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
270  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
271  extendSignalWidth(undef_a, undef_b, undef_y, cell, false);
272 
273  if (cell->type.in("$and", "$_AND_", "$_NAND_")) {
274  std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
275  std::vector<int> b0 = ez->vec_and(ez->vec_not(b), ez->vec_not(undef_b));
276  std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a0, b0)));
277  ez->assume(ez->vec_eq(yX, undef_y));
278  }
279  else if (cell->type.in("$or", "$_OR_", "$_NOR_")) {
280  std::vector<int> a1 = ez->vec_and(a, ez->vec_not(undef_a));
281  std::vector<int> b1 = ez->vec_and(b, ez->vec_not(undef_b));
282  std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a1, b1)));
283  ez->assume(ez->vec_eq(yX, undef_y));
284  }
285  else if (cell->type.in("$xor", "$xnor", "$_XOR_", "$_XNOR_")) {
286  std::vector<int> yX = ez->vec_or(undef_a, undef_b);
287  ez->assume(ez->vec_eq(yX, undef_y));
288  }
289  else
290  log_abort();
291 
292  undefGating(y, yy, undef_y);
293  }
294  else if (model_undef)
295  {
296  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
297  undefGating(y, yy, undef_y);
298  }
299  return true;
300  }
301 
302  if (cell->type.in("$_AOI3_", "$_OAI3_", "$_AOI4_", "$_OAI4_"))
303  {
304  bool aoi_mode = cell->type.in("$_AOI3_", "$_AOI4_");
305  bool three_mode = cell->type.in("$_AOI3_", "$_OAI3_");
306 
307  int a = importDefSigSpec(cell->getPort("\\A"), timestep).at(0);
308  int b = importDefSigSpec(cell->getPort("\\B"), timestep).at(0);
309  int c = importDefSigSpec(cell->getPort("\\C"), timestep).at(0);
310  int d = three_mode ? (aoi_mode ? ez->CONST_TRUE : ez->CONST_FALSE) : importDefSigSpec(cell->getPort("\\D"), timestep).at(0);
311  int y = importDefSigSpec(cell->getPort("\\Y"), timestep).at(0);
312  int yy = model_undef ? ez->literal() : y;
313 
314  if (cell->type.in("$_AOI3_", "$_AOI4_"))
315  ez->assume(ez->IFF(ez->NOT(ez->OR(ez->AND(a, b), ez->AND(c, d))), yy));
316  else
317  ez->assume(ez->IFF(ez->NOT(ez->AND(ez->OR(a, b), ez->OR(c, d))), yy));
318 
319  if (model_undef)
320  {
321  int undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep).at(0);
322  int undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep).at(0);
323  int undef_c = importUndefSigSpec(cell->getPort("\\C"), timestep).at(0);
324  int undef_d = three_mode ? ez->CONST_FALSE : importUndefSigSpec(cell->getPort("\\D"), timestep).at(0);
325  int undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep).at(0);
326 
327  if (aoi_mode)
328  {
329  int a0 = ez->AND(ez->NOT(a), ez->NOT(undef_a));
330  int b0 = ez->AND(ez->NOT(b), ez->NOT(undef_b));
331  int c0 = ez->AND(ez->NOT(c), ez->NOT(undef_c));
332  int d0 = ez->AND(ez->NOT(d), ez->NOT(undef_d));
333 
334  int ab = ez->AND(a, b), cd = ez->AND(c, d);
335  int undef_ab = ez->AND(ez->OR(undef_a, undef_b), ez->NOT(ez->OR(a0, b0)));
336  int undef_cd = ez->AND(ez->OR(undef_c, undef_d), ez->NOT(ez->OR(c0, d0)));
337 
338  int ab1 = ez->AND(ab, ez->NOT(undef_ab));
339  int cd1 = ez->AND(cd, ez->NOT(undef_cd));
340  int yX = ez->AND(ez->OR(undef_ab, undef_cd), ez->NOT(ez->OR(ab1, cd1)));
341 
342  ez->assume(ez->IFF(yX, undef_y));
343  }
344  else
345  {
346  int a1 = ez->AND(a, ez->NOT(undef_a));
347  int b1 = ez->AND(b, ez->NOT(undef_b));
348  int c1 = ez->AND(c, ez->NOT(undef_c));
349  int d1 = ez->AND(d, ez->NOT(undef_d));
350 
351  int ab = ez->OR(a, b), cd = ez->OR(c, d);
352  int undef_ab = ez->AND(ez->OR(undef_a, undef_b), ez->NOT(ez->OR(a1, b1)));
353  int undef_cd = ez->AND(ez->OR(undef_c, undef_d), ez->NOT(ez->OR(c1, d1)));
354 
355  int ab0 = ez->AND(ez->NOT(ab), ez->NOT(undef_ab));
356  int cd0 = ez->AND(ez->NOT(cd), ez->NOT(undef_cd));
357  int yX = ez->AND(ez->OR(undef_ab, undef_cd), ez->NOT(ez->OR(ab0, cd0)));
358 
359  ez->assume(ez->IFF(yX, undef_y));
360  }
361 
362  undefGating(y, yy, undef_y);
363  }
364 
365  return true;
366  }
367 
368  if (cell->type == "$_NOT_" || cell->type == "$not")
369  {
370  std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
371  std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
372  extendSignalWidthUnary(a, y, cell);
373 
374  std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
375  ez->assume(ez->vec_eq(ez->vec_not(a), yy));
376 
377  if (model_undef) {
378  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
379  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
380  extendSignalWidthUnary(undef_a, undef_y, cell, false);
381  ez->assume(ez->vec_eq(undef_a, undef_y));
382  undefGating(y, yy, undef_y);
383  }
384  return true;
385  }
386 
387  if (cell->type == "$_MUX_" || cell->type == "$mux")
388  {
389  std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
390  std::vector<int> b = importDefSigSpec(cell->getPort("\\B"), timestep);
391  std::vector<int> s = importDefSigSpec(cell->getPort("\\S"), timestep);
392  std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
393 
394  std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
395  ez->assume(ez->vec_eq(ez->vec_ite(s.at(0), b, a), yy));
396 
397  if (model_undef)
398  {
399  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
400  std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
401  std::vector<int> undef_s = importUndefSigSpec(cell->getPort("\\S"), timestep);
402  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
403 
404  std::vector<int> unequal_ab = ez->vec_not(ez->vec_iff(a, b));
405  std::vector<int> undef_ab = ez->vec_or(unequal_ab, ez->vec_or(undef_a, undef_b));
406  std::vector<int> yX = ez->vec_ite(undef_s.at(0), undef_ab, ez->vec_ite(s.at(0), undef_b, undef_a));
407  ez->assume(ez->vec_eq(yX, undef_y));
408  undefGating(y, yy, undef_y);
409  }
410  return true;
411  }
412 
413  if (cell->type == "$pmux")
414  {
415  std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
416  std::vector<int> b = importDefSigSpec(cell->getPort("\\B"), timestep);
417  std::vector<int> s = importDefSigSpec(cell->getPort("\\S"), timestep);
418  std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
419 
420  std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
421 
422  std::vector<int> tmp = a;
423  for (size_t i = 0; i < s.size(); i++) {
424  std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
425  tmp = ez->vec_ite(s.at(i), part_of_b, tmp);
426  }
427  ez->assume(ez->vec_eq(tmp, yy));
428 
429  if (model_undef)
430  {
431  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
432  std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
433  std::vector<int> undef_s = importUndefSigSpec(cell->getPort("\\S"), timestep);
434  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
435 
436  int maybe_one_hot = ez->CONST_FALSE;
437  int maybe_many_hot = ez->CONST_FALSE;
438 
439  int sure_one_hot = ez->CONST_FALSE;
440  int sure_many_hot = ez->CONST_FALSE;
441 
442  std::vector<int> bits_set = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
443  std::vector<int> bits_clr = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
444 
445  for (size_t i = 0; i < s.size(); i++)
446  {
447  std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
448  std::vector<int> part_of_undef_b(undef_b.begin()+i*a.size(), undef_b.begin()+(i+1)*a.size());
449 
450  int maybe_s = ez->OR(s.at(i), undef_s.at(i));
451  int sure_s = ez->AND(s.at(i), ez->NOT(undef_s.at(i)));
452 
453  maybe_one_hot = ez->OR(maybe_one_hot, maybe_s);
454  maybe_many_hot = ez->OR(maybe_many_hot, ez->AND(maybe_one_hot, maybe_s));
455 
456  sure_one_hot = ez->OR(sure_one_hot, sure_s);
457  sure_many_hot = ez->OR(sure_many_hot, ez->AND(sure_one_hot, sure_s));
458 
459  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);
460  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);
461  }
462 
463  int maybe_a = ez->NOT(maybe_one_hot);
464 
465  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);
466  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);
467 
468  ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(bits_set, bits_clr)), undef_y));
469  undefGating(y, yy, undef_y);
470  }
471  return true;
472  }
473 
474  if (cell->type == "$pos" || cell->type == "$neg")
475  {
476  std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
477  std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
478  extendSignalWidthUnary(a, y, cell);
479 
480  std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
481 
482  if (cell->type == "$pos") {
483  ez->assume(ez->vec_eq(a, yy));
484  } else {
485  std::vector<int> zero(a.size(), ez->CONST_FALSE);
486  ez->assume(ez->vec_eq(ez->vec_sub(zero, a), yy));
487  }
488 
489  if (model_undef)
490  {
491  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
492  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
493  extendSignalWidthUnary(undef_a, undef_y, cell);
494 
495  if (cell->type == "$pos") {
496  ez->assume(ez->vec_eq(undef_a, undef_y));
497  } else {
498  int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
499  std::vector<int> undef_y_bits(undef_y.size(), undef_any_a);
500  ez->assume(ez->vec_eq(undef_y_bits, undef_y));
501  }
502 
503  undefGating(y, yy, undef_y);
504  }
505  return true;
506  }
507 
508  if (cell->type == "$reduce_and" || cell->type == "$reduce_or" || cell->type == "$reduce_xor" ||
509  cell->type == "$reduce_xnor" || cell->type == "$reduce_bool" || cell->type == "$logic_not")
510  {
511  std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
512  std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
513 
514  std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
515 
516  if (cell->type == "$reduce_and")
517  ez->SET(ez->expression(ez->OpAnd, a), yy.at(0));
518  if (cell->type == "$reduce_or" || cell->type == "$reduce_bool")
519  ez->SET(ez->expression(ez->OpOr, a), yy.at(0));
520  if (cell->type == "$reduce_xor")
521  ez->SET(ez->expression(ez->OpXor, a), yy.at(0));
522  if (cell->type == "$reduce_xnor")
523  ez->SET(ez->NOT(ez->expression(ez->OpXor, a)), yy.at(0));
524  if (cell->type == "$logic_not")
525  ez->SET(ez->NOT(ez->expression(ez->OpOr, a)), yy.at(0));
526  for (size_t i = 1; i < y.size(); i++)
527  ez->SET(ez->CONST_FALSE, yy.at(i));
528 
529  if (model_undef)
530  {
531  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
532  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
533  int aX = ez->expression(ezSAT::OpOr, undef_a);
534 
535  if (cell->type == "$reduce_and") {
536  int a0 = ez->expression(ezSAT::OpOr, ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a)));
537  ez->assume(ez->IFF(ez->AND(ez->NOT(a0), aX), undef_y.at(0)));
538  }
539  else if (cell->type == "$reduce_or" || cell->type == "$reduce_bool" || cell->type == "$logic_not") {
540  int a1 = ez->expression(ezSAT::OpOr, ez->vec_and(a, ez->vec_not(undef_a)));
541  ez->assume(ez->IFF(ez->AND(ez->NOT(a1), aX), undef_y.at(0)));
542  }
543  else if (cell->type == "$reduce_xor" || cell->type == "$reduce_xnor") {
544  ez->assume(ez->IFF(aX, undef_y.at(0)));
545  } else
546  log_abort();
547 
548  for (size_t i = 1; i < undef_y.size(); i++)
549  ez->SET(ez->CONST_FALSE, undef_y.at(i));
550 
551  undefGating(y, yy, undef_y);
552  }
553  return true;
554  }
555 
556  if (cell->type == "$logic_and" || cell->type == "$logic_or")
557  {
558  std::vector<int> vec_a = importDefSigSpec(cell->getPort("\\A"), timestep);
559  std::vector<int> vec_b = importDefSigSpec(cell->getPort("\\B"), timestep);
560 
561  int a = ez->expression(ez->OpOr, vec_a);
562  int b = ez->expression(ez->OpOr, vec_b);
563  std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
564 
565  std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
566 
567  if (cell->type == "$logic_and")
568  ez->SET(ez->expression(ez->OpAnd, a, b), yy.at(0));
569  else
570  ez->SET(ez->expression(ez->OpOr, a, b), yy.at(0));
571  for (size_t i = 1; i < y.size(); i++)
572  ez->SET(ez->CONST_FALSE, yy.at(i));
573 
574  if (model_undef)
575  {
576  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
577  std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
578  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
579 
580  int a0 = ez->NOT(ez->OR(ez->expression(ezSAT::OpOr, vec_a), ez->expression(ezSAT::OpOr, undef_a)));
581  int b0 = ez->NOT(ez->OR(ez->expression(ezSAT::OpOr, vec_b), ez->expression(ezSAT::OpOr, undef_b)));
582  int a1 = ez->expression(ezSAT::OpOr, ez->vec_and(vec_a, ez->vec_not(undef_a)));
583  int b1 = ez->expression(ezSAT::OpOr, ez->vec_and(vec_b, ez->vec_not(undef_b)));
584  int aX = ez->expression(ezSAT::OpOr, undef_a);
585  int bX = ez->expression(ezSAT::OpOr, undef_b);
586 
587  if (cell->type == "$logic_and")
588  ez->SET(ez->AND(ez->OR(aX, bX), ez->NOT(ez->AND(a1, b1)), ez->NOT(a0), ez->NOT(b0)), undef_y.at(0));
589  else if (cell->type == "$logic_or")
590  ez->SET(ez->AND(ez->OR(aX, bX), ez->NOT(ez->AND(a0, b0)), ez->NOT(a1), ez->NOT(b1)), undef_y.at(0));
591  else
592  log_abort();
593 
594  for (size_t i = 1; i < undef_y.size(); i++)
595  ez->SET(ez->CONST_FALSE, undef_y.at(i));
596 
597  undefGating(y, yy, undef_y);
598  }
599  return true;
600  }
601 
602  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")
603  {
604  bool is_signed = cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool();
605  std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
606  std::vector<int> b = importDefSigSpec(cell->getPort("\\B"), timestep);
607  std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
608  extendSignalWidth(a, b, cell);
609 
610  std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
611 
612  if (model_undef && (cell->type == "$eqx" || cell->type == "$nex")) {
613  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
614  std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
615  extendSignalWidth(undef_a, undef_b, cell, true);
616  a = ez->vec_or(a, undef_a);
617  b = ez->vec_or(b, undef_b);
618  }
619 
620  if (cell->type == "$lt")
621  ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), yy.at(0));
622  if (cell->type == "$le")
623  ez->SET(is_signed ? ez->vec_le_signed(a, b) : ez->vec_le_unsigned(a, b), yy.at(0));
624  if (cell->type == "$eq" || cell->type == "$eqx")
625  ez->SET(ez->vec_eq(a, b), yy.at(0));
626  if (cell->type == "$ne" || cell->type == "$nex")
627  ez->SET(ez->vec_ne(a, b), yy.at(0));
628  if (cell->type == "$ge")
629  ez->SET(is_signed ? ez->vec_ge_signed(a, b) : ez->vec_ge_unsigned(a, b), yy.at(0));
630  if (cell->type == "$gt")
631  ez->SET(is_signed ? ez->vec_gt_signed(a, b) : ez->vec_gt_unsigned(a, b), yy.at(0));
632  for (size_t i = 1; i < y.size(); i++)
633  ez->SET(ez->CONST_FALSE, yy.at(i));
634 
635  if (model_undef && (cell->type == "$eqx" || cell->type == "$nex"))
636  {
637  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
638  std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
639  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
640  extendSignalWidth(undef_a, undef_b, cell, true);
641 
642  if (cell->type == "$eqx")
643  yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
644  else
645  yy.at(0) = ez->OR(yy.at(0), ez->vec_ne(undef_a, undef_b));
646 
647  for (size_t i = 0; i < y.size(); i++)
648  ez->SET(ez->CONST_FALSE, undef_y.at(i));
649 
650  ez->assume(ez->vec_eq(y, yy));
651  }
652  else if (model_undef && (cell->type == "$eq" || cell->type == "$ne"))
653  {
654  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
655  std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
656  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
657  extendSignalWidth(undef_a, undef_b, cell, true);
658 
659  int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
660  int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
661  int undef_any = ez->OR(undef_any_a, undef_any_b);
662 
663  std::vector<int> masked_a_bits = ez->vec_or(a, ez->vec_or(undef_a, undef_b));
664  std::vector<int> masked_b_bits = ez->vec_or(b, ez->vec_or(undef_a, undef_b));
665 
666  int masked_ne = ez->vec_ne(masked_a_bits, masked_b_bits);
667  int undef_y_bit = ez->AND(undef_any, ez->NOT(masked_ne));
668 
669  for (size_t i = 1; i < undef_y.size(); i++)
670  ez->SET(ez->CONST_FALSE, undef_y.at(i));
671  ez->SET(undef_y_bit, undef_y.at(0));
672 
673  undefGating(y, yy, undef_y);
674  }
675  else
676  {
677  if (model_undef) {
678  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
679  undefGating(y, yy, undef_y);
680  }
681  log_assert(!model_undef || arith_undef_handled);
682  }
683  return true;
684  }
685 
686  if (cell->type == "$shl" || cell->type == "$shr" || cell->type == "$sshl" || cell->type == "$sshr" || cell->type == "$shift" || cell->type == "$shiftx")
687  {
688  std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
689  std::vector<int> b = importDefSigSpec(cell->getPort("\\B"), timestep);
690  std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
691 
692  int extend_bit = ez->CONST_FALSE;
693 
694  if (!cell->type.in("$shift", "$shiftx") && cell->parameters["\\A_SIGNED"].as_bool())
695  extend_bit = a.back();
696 
697  while (y.size() < a.size())
698  y.push_back(ez->literal());
699  while (y.size() > a.size())
700  a.push_back(extend_bit);
701 
702  std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
703  std::vector<int> shifted_a;
704 
705  if (cell->type == "$shl" || cell->type == "$sshl")
706  shifted_a = ez->vec_shift_left(a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
707 
708  if (cell->type == "$shr")
709  shifted_a = ez->vec_shift_right(a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
710 
711  if (cell->type == "$sshr")
712  shifted_a = ez->vec_shift_right(a, b, false, cell->parameters["\\A_SIGNED"].as_bool() ? a.back() : ez->CONST_FALSE, ez->CONST_FALSE);
713 
714  if (cell->type == "$shift" || cell->type == "$shiftx")
715  shifted_a = ez->vec_shift_right(a, b, cell->parameters["\\B_SIGNED"].as_bool(), ez->CONST_FALSE, ez->CONST_FALSE);
716 
717  ez->assume(ez->vec_eq(shifted_a, yy));
718 
719  if (model_undef)
720  {
721  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
722  std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
723  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
724  std::vector<int> undef_a_shifted;
725 
726  extend_bit = cell->type == "$shiftx" ? ez->CONST_TRUE : ez->CONST_FALSE;
727  if (!cell->type.in("$shift", "$shiftx") && cell->parameters["\\A_SIGNED"].as_bool())
728  extend_bit = undef_a.back();
729 
730  while (undef_y.size() < undef_a.size())
731  undef_y.push_back(ez->literal());
732  while (undef_y.size() > undef_a.size())
733  undef_a.push_back(extend_bit);
734 
735  if (cell->type == "$shl" || cell->type == "$sshl")
736  undef_a_shifted = ez->vec_shift_left(undef_a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
737 
738  if (cell->type == "$shr")
739  undef_a_shifted = ez->vec_shift_right(undef_a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
740 
741  if (cell->type == "$sshr")
742  undef_a_shifted = ez->vec_shift_right(undef_a, b, false, cell->parameters["\\A_SIGNED"].as_bool() ? undef_a.back() : ez->CONST_FALSE, ez->CONST_FALSE);
743 
744  if (cell->type == "$shift")
745  undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters["\\B_SIGNED"].as_bool(), ez->CONST_FALSE, ez->CONST_FALSE);
746 
747  if (cell->type == "$shiftx")
748  undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters["\\B_SIGNED"].as_bool(), ez->CONST_TRUE, ez->CONST_TRUE);
749 
750  int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
751  std::vector<int> undef_all_y_bits(undef_y.size(), undef_any_b);
752  ez->assume(ez->vec_eq(ez->vec_or(undef_a_shifted, undef_all_y_bits), undef_y));
753  undefGating(y, yy, undef_y);
754  }
755  return true;
756  }
757 
758  if (cell->type == "$mul")
759  {
760  std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
761  std::vector<int> b = importDefSigSpec(cell->getPort("\\B"), timestep);
762  std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
763  extendSignalWidth(a, b, y, cell);
764 
765  std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
766 
767  std::vector<int> tmp(a.size(), ez->CONST_FALSE);
768  for (int i = 0; i < int(a.size()); i++)
769  {
770  std::vector<int> shifted_a(a.size(), ez->CONST_FALSE);
771  for (int j = i; j < int(a.size()); j++)
772  shifted_a.at(j) = a.at(j-i);
773  tmp = ez->vec_ite(b.at(i), ez->vec_add(tmp, shifted_a), tmp);
774  }
775  ez->assume(ez->vec_eq(tmp, yy));
776 
777  if (model_undef) {
778  log_assert(arith_undef_handled);
779  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
780  undefGating(y, yy, undef_y);
781  }
782  return true;
783  }
784 
785  if (cell->type == "$macc")
786  {
787  std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
788  std::vector<int> b = importDefSigSpec(cell->getPort("\\B"), timestep);
789  std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
790 
791  Macc macc;
792  macc.from_cell(cell);
793 
794  std::vector<int> tmp(GetSize(y), ez->CONST_FALSE);
795 
796  for (auto &port : macc.ports)
797  {
798  std::vector<int> in_a = importDefSigSpec(port.in_a, timestep);
799  std::vector<int> in_b = importDefSigSpec(port.in_b, timestep);
800 
801  while (GetSize(in_a) < GetSize(y))
802  in_a.push_back(port.is_signed && !in_a.empty() ? in_a.back() : ez->CONST_FALSE);
803  in_a.resize(GetSize(y));
804 
805  if (GetSize(in_b))
806  {
807  while (GetSize(in_b) < GetSize(y))
808  in_b.push_back(port.is_signed && !in_b.empty() ? in_b.back() : ez->CONST_FALSE);
809  in_b.resize(GetSize(y));
810 
811  for (int i = 0; i < GetSize(in_b); i++) {
812  std::vector<int> shifted_a(in_a.size(), ez->CONST_FALSE);
813  for (int j = i; j < int(in_a.size()); j++)
814  shifted_a.at(j) = in_a.at(j-i);
815  if (port.do_subtract)
816  tmp = ez->vec_ite(in_b.at(i), ez->vec_sub(tmp, shifted_a), tmp);
817  else
818  tmp = ez->vec_ite(in_b.at(i), ez->vec_add(tmp, shifted_a), tmp);
819  }
820  }
821  else
822  {
823  if (port.do_subtract)
824  tmp = ez->vec_sub(tmp, in_a);
825  else
826  tmp = ez->vec_add(tmp, in_a);
827  }
828  }
829 
830  for (int i = 0; i < GetSize(b); i++) {
831  std::vector<int> val(GetSize(y), ez->CONST_FALSE);
832  val.at(0) = b.at(i);
833  tmp = ez->vec_add(tmp, val);
834  }
835 
836  if (model_undef)
837  {
838  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
839  std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
840 
841  int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
842  int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
843 
844  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
845  ez->assume(ez->vec_eq(undef_y, std::vector<int>(GetSize(y), ez->OR(undef_any_a, undef_any_b))));
846 
847  undefGating(y, tmp, undef_y);
848  }
849  else
850  ez->assume(ez->vec_eq(y, tmp));
851 
852  return true;
853  }
854 
855  if (cell->type == "$div" || cell->type == "$mod")
856  {
857  std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
858  std::vector<int> b = importDefSigSpec(cell->getPort("\\B"), timestep);
859  std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
860  extendSignalWidth(a, b, y, cell);
861 
862  std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
863 
864  std::vector<int> a_u, b_u;
865  if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool()) {
866  a_u = ez->vec_ite(a.back(), ez->vec_neg(a), a);
867  b_u = ez->vec_ite(b.back(), ez->vec_neg(b), b);
868  } else {
869  a_u = a;
870  b_u = b;
871  }
872 
873  std::vector<int> chain_buf = a_u;
874  std::vector<int> y_u(a_u.size(), ez->CONST_FALSE);
875  for (int i = int(a.size())-1; i >= 0; i--)
876  {
877  chain_buf.insert(chain_buf.end(), chain_buf.size(), ez->CONST_FALSE);
878 
879  std::vector<int> b_shl(i, ez->CONST_FALSE);
880  b_shl.insert(b_shl.end(), b_u.begin(), b_u.end());
881  b_shl.insert(b_shl.end(), chain_buf.size()-b_shl.size(), ez->CONST_FALSE);
882 
883  y_u.at(i) = ez->vec_ge_unsigned(chain_buf, b_shl);
884  chain_buf = ez->vec_ite(y_u.at(i), ez->vec_sub(chain_buf, b_shl), chain_buf);
885 
886  chain_buf.erase(chain_buf.begin() + a_u.size(), chain_buf.end());
887  }
888 
889  std::vector<int> y_tmp = ignore_div_by_zero ? yy : ez->vec_var(y.size());
890  if (cell->type == "$div") {
891  if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
892  ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(ez->XOR(a.back(), b.back()), ez->vec_neg(y_u), y_u)));
893  else
894  ez->assume(ez->vec_eq(y_tmp, y_u));
895  } else {
896  if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
897  ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(a.back(), ez->vec_neg(chain_buf), chain_buf)));
898  else
899  ez->assume(ez->vec_eq(y_tmp, chain_buf));
900  }
901 
902  if (ignore_div_by_zero) {
903  ez->assume(ez->expression(ezSAT::OpOr, b));
904  } else {
905  std::vector<int> div_zero_result;
906  if (cell->type == "$div") {
907  if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool()) {
908  std::vector<int> all_ones(y.size(), ez->CONST_TRUE);
909  std::vector<int> only_first_one(y.size(), ez->CONST_FALSE);
910  only_first_one.at(0) = ez->CONST_TRUE;
911  div_zero_result = ez->vec_ite(a.back(), only_first_one, all_ones);
912  } else {
913  div_zero_result.insert(div_zero_result.end(), cell->getPort("\\A").size(), ez->CONST_TRUE);
914  div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
915  }
916  } else {
917  int copy_a_bits = std::min(cell->getPort("\\A").size(), cell->getPort("\\B").size());
918  div_zero_result.insert(div_zero_result.end(), a.begin(), a.begin() + copy_a_bits);
919  if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
920  div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), div_zero_result.back());
921  else
922  div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
923  }
924  ez->assume(ez->vec_eq(yy, ez->vec_ite(ez->expression(ezSAT::OpOr, b), y_tmp, div_zero_result)));
925  }
926 
927  if (model_undef) {
928  log_assert(arith_undef_handled);
929  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
930  undefGating(y, yy, undef_y);
931  }
932  return true;
933  }
934 
935  if (cell->type == "$lut")
936  {
937  std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
938  std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
939 
940  std::vector<int> lut;
941  for (auto bit : cell->getParam("\\LUT").bits)
942  lut.push_back(bit == RTLIL::S1 ? ez->CONST_TRUE : ez->CONST_FALSE);
943  while (GetSize(lut) < (1 << GetSize(a)))
944  lut.push_back(ez->CONST_FALSE);
945  lut.resize(1 << GetSize(a));
946 
947  if (model_undef)
948  {
949  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
950  std::vector<int> t(lut), u(GetSize(t), ez->CONST_FALSE);
951 
952  for (int i = GetSize(a)-1; i >= 0; i--)
953  {
954  std::vector<int> t0(t.begin(), t.begin() + GetSize(t)/2);
955  std::vector<int> t1(t.begin() + GetSize(t)/2, t.end());
956 
957  std::vector<int> u0(u.begin(), u.begin() + GetSize(u)/2);
958  std::vector<int> u1(u.begin() + GetSize(u)/2, u.end());
959 
960  t = ez->vec_ite(a[i], t1, t0);
961  u = ez->vec_ite(undef_a[i], ez->vec_or(ez->vec_xor(t0, t1), ez->vec_or(u0, u1)), ez->vec_ite(a[i], u1, u0));
962  }
963 
964  log_assert(GetSize(t) == 1);
965  log_assert(GetSize(u) == 1);
966  undefGating(y, t, u);
967  ez->assume(ez->vec_eq(importUndefSigSpec(cell->getPort("\\Y"), timestep), u));
968  }
969  else
970  {
971  std::vector<int> t = lut;
972  for (int i = GetSize(a)-1; i >= 0; i--)
973  {
974  std::vector<int> t0(t.begin(), t.begin() + GetSize(t)/2);
975  std::vector<int> t1(t.begin() + GetSize(t)/2, t.end());
976  t = ez->vec_ite(a[i], t1, t0);
977  }
978 
979  log_assert(GetSize(t) == 1);
980  ez->assume(ez->vec_eq(y, t));
981  }
982  return true;
983  }
984 
985  if (cell->type == "$fa")
986  {
987  std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
988  std::vector<int> b = importDefSigSpec(cell->getPort("\\B"), timestep);
989  std::vector<int> c = importDefSigSpec(cell->getPort("\\C"), timestep);
990  std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
991  std::vector<int> x = importDefSigSpec(cell->getPort("\\X"), timestep);
992 
993  std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
994  std::vector<int> xx = model_undef ? ez->vec_var(x.size()) : x;
995 
996  std::vector<int> t1 = ez->vec_xor(a, b);
997  ez->assume(ez->vec_eq(yy, ez->vec_xor(t1, c)));
998 
999  std::vector<int> t2 = ez->vec_and(a, b);
1000  std::vector<int> t3 = ez->vec_and(c, t1);
1001  ez->assume(ez->vec_eq(xx, ez->vec_or(t2, t3)));
1002 
1003  if (model_undef)
1004  {
1005  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
1006  std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
1007  std::vector<int> undef_c = importUndefSigSpec(cell->getPort("\\C"), timestep);
1008 
1009  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
1010  std::vector<int> undef_x = importUndefSigSpec(cell->getPort("\\X"), timestep);
1011 
1012  ez->assume(ez->vec_eq(undef_y, ez->vec_or(ez->vec_or(undef_a, undef_b), undef_c)));
1013  ez->assume(ez->vec_eq(undef_x, undef_y));
1014 
1015  undefGating(y, yy, undef_y);
1016  undefGating(x, xx, undef_x);
1017  }
1018  return true;
1019  }
1020 
1021  if (cell->type == "$lcu")
1022  {
1023  std::vector<int> p = importDefSigSpec(cell->getPort("\\P"), timestep);
1024  std::vector<int> g = importDefSigSpec(cell->getPort("\\G"), timestep);
1025  std::vector<int> ci = importDefSigSpec(cell->getPort("\\CI"), timestep);
1026  std::vector<int> co = importDefSigSpec(cell->getPort("\\CO"), timestep);
1027 
1028  std::vector<int> yy = model_undef ? ez->vec_var(co.size()) : co;
1029 
1030  for (int i = 0; i < GetSize(co); i++)
1031  ez->SET(yy[i], ez->OR(g[i], ez->AND(p[i], i ? yy[i-1] : ci[0])));
1032 
1033  if (model_undef)
1034  {
1035  std::vector<int> undef_p = importUndefSigSpec(cell->getPort("\\P"), timestep);
1036  std::vector<int> undef_g = importUndefSigSpec(cell->getPort("\\G"), timestep);
1037  std::vector<int> undef_ci = importUndefSigSpec(cell->getPort("\\CI"), timestep);
1038  std::vector<int> undef_co = importUndefSigSpec(cell->getPort("\\CO"), timestep);
1039 
1040  int undef_any_p = ez->expression(ezSAT::OpOr, undef_p);
1041  int undef_any_g = ez->expression(ezSAT::OpOr, undef_g);
1042  int undef_any_ci = ez->expression(ezSAT::OpOr, undef_ci);
1043  int undef_co_bit = ez->OR(undef_any_p, undef_any_g, undef_any_ci);
1044 
1045  std::vector<int> undef_co_bits(undef_co.size(), undef_co_bit);
1046  ez->assume(ez->vec_eq(undef_co_bits, undef_co));
1047 
1048  undefGating(co, yy, undef_co);
1049  }
1050  return true;
1051  }
1052 
1053  if (cell->type == "$alu")
1054  {
1055  std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
1056  std::vector<int> b = importDefSigSpec(cell->getPort("\\B"), timestep);
1057  std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
1058  std::vector<int> x = importDefSigSpec(cell->getPort("\\X"), timestep);
1059  std::vector<int> ci = importDefSigSpec(cell->getPort("\\CI"), timestep);
1060  std::vector<int> bi = importDefSigSpec(cell->getPort("\\BI"), timestep);
1061  std::vector<int> co = importDefSigSpec(cell->getPort("\\CO"), timestep);
1062 
1063  extendSignalWidth(a, b, y, cell);
1064  extendSignalWidth(a, b, x, cell);
1065  extendSignalWidth(a, b, co, cell);
1066 
1067  std::vector<int> def_y = model_undef ? ez->vec_var(y.size()) : y;
1068  std::vector<int> def_x = model_undef ? ez->vec_var(x.size()) : x;
1069  std::vector<int> def_co = model_undef ? ez->vec_var(co.size()) : co;
1070 
1071  log_assert(GetSize(y) == GetSize(x));
1072  log_assert(GetSize(y) == GetSize(co));
1073  log_assert(GetSize(ci) == 1);
1074  log_assert(GetSize(bi) == 1);
1075 
1076  for (int i = 0; i < GetSize(y); i++)
1077  {
1078  int s1 = a.at(i), s2 = ez->XOR(b.at(i), bi.at(0)), s3 = i ? co.at(i-1) : ci.at(0);
1079  ez->SET(def_x.at(i), ez->XOR(s1, s2));
1080  ez->SET(def_y.at(i), ez->XOR(def_x.at(i), s3));
1081  ez->SET(def_co.at(i), ez->OR(ez->AND(s1, s2), ez->AND(s1, s3), ez->AND(s2, s3)));
1082  }
1083 
1084  if (model_undef)
1085  {
1086  std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
1087  std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
1088  std::vector<int> undef_ci = importUndefSigSpec(cell->getPort("\\CI"), timestep);
1089  std::vector<int> undef_bi = importUndefSigSpec(cell->getPort("\\BI"), timestep);
1090 
1091  std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
1092  std::vector<int> undef_x = importUndefSigSpec(cell->getPort("\\X"), timestep);
1093  std::vector<int> undef_co = importUndefSigSpec(cell->getPort("\\CO"), timestep);
1094 
1095  extendSignalWidth(undef_a, undef_b, undef_y, cell);
1096  extendSignalWidth(undef_a, undef_b, undef_x, cell);
1097  extendSignalWidth(undef_a, undef_b, undef_co, cell);
1098 
1099  std::vector<int> all_inputs_undef;
1100  all_inputs_undef.insert(all_inputs_undef.end(), undef_a.begin(), undef_a.end());
1101  all_inputs_undef.insert(all_inputs_undef.end(), undef_b.begin(), undef_b.end());
1102  all_inputs_undef.insert(all_inputs_undef.end(), undef_ci.begin(), undef_ci.end());
1103  all_inputs_undef.insert(all_inputs_undef.end(), undef_bi.begin(), undef_bi.end());
1104  int undef_any = ez->expression(ezSAT::OpOr, all_inputs_undef);
1105 
1106  for (int i = 0; i < GetSize(undef_y); i++) {
1107  ez->SET(undef_y.at(i), undef_any);
1108  ez->SET(undef_x.at(i), ez->OR(undef_a.at(i), undef_b.at(i), undef_bi.at(0)));
1109  ez->SET(undef_co.at(i), undef_any);
1110  }
1111 
1112  undefGating(y, def_y, undef_y);
1113  undefGating(x, def_x, undef_x);
1114  undefGating(co, def_co, undef_co);
1115  }
1116  return true;
1117  }
1118 
1119  if (cell->type == "$slice")
1120  {
1121  RTLIL::SigSpec a = cell->getPort("\\A");
1122  RTLIL::SigSpec y = cell->getPort("\\Y");
1123  ez->assume(signals_eq(a.extract(cell->parameters.at("\\OFFSET").as_int(), y.size()), y, timestep));
1124  return true;
1125  }
1126 
1127  if (cell->type == "$concat")
1128  {
1129  RTLIL::SigSpec a = cell->getPort("\\A");
1130  RTLIL::SigSpec b = cell->getPort("\\B");
1131  RTLIL::SigSpec y = cell->getPort("\\Y");
1132 
1133  RTLIL::SigSpec ab = a;
1134  ab.append(b);
1135 
1136  ez->assume(signals_eq(ab, y, timestep));
1137  return true;
1138  }
1139 
1140  if (timestep > 0 && (cell->type == "$dff" || cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_"))
1141  {
1142  if (timestep == 1)
1143  {
1144  initial_state.add((*sigmap)(cell->getPort("\\Q")));
1145  }
1146  else
1147  {
1148  std::vector<int> d = importDefSigSpec(cell->getPort("\\D"), timestep-1);
1149  std::vector<int> q = importDefSigSpec(cell->getPort("\\Q"), timestep);
1150 
1151  std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
1152  ez->assume(ez->vec_eq(d, qq));
1153 
1154  if (model_undef)
1155  {
1156  std::vector<int> undef_d = importUndefSigSpec(cell->getPort("\\D"), timestep-1);
1157  std::vector<int> undef_q = importUndefSigSpec(cell->getPort("\\Q"), timestep);
1158 
1159  ez->assume(ez->vec_eq(undef_d, undef_q));
1160  undefGating(q, qq, undef_q);
1161  }
1162  }
1163  return true;
1164  }
1165 
1166  if (cell->type == "$assert")
1167  {
1168  std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
1169  asserts_a[pf].append((*sigmap)(cell->getPort("\\A")));
1170  asserts_en[pf].append((*sigmap)(cell->getPort("\\EN")));
1171  return true;
1172  }
1173 
1174  // Unsupported internal cell types: $pow $lut
1175  // .. and all sequential cells except $dff and $_DFF_[NP]_
1176  return false;
1177  }
SatGen::ez
ezSAT * ez
Definition: satgen.h:36
ezSAT::vec_sub
std::vector< int > vec_sub(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:843
SatGen::extendSignalWidth
void extendSignalWidth(std::vector< int > &vec_a, std::vector< int > &vec_b, RTLIL::Cell *cell, size_t y_width=0, bool forced_signed=false)
Definition: satgen.h:157
SatGen::ignore_div_by_zero
bool ignore_div_by_zero
Definition: satgen.h:42
ezSAT::vec_ge_signed
int vec_ge_signed(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:912
ezSAT::SET
void SET(_V a, _V b)
Definition: ezsat.h:221
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
Macc
Definition: macc.h:27
SatGen::initial_state
SigPool initial_state
Definition: satgen.h:39
ezSAT::vec_var
std::vector< int > vec_var(int numBits)
Definition: ezsat.cc:673
SatGen::asserts_en
std::map< std::string, RTLIL::SigSpec > asserts_en
Definition: satgen.h:40
ezSAT::CONST_FALSE
static const int CONST_FALSE
Definition: ezsat.h:49
ezSAT::vec_iff
std::vector< int > vec_iff(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:736
ezSAT::vec_le_signed
int vec_le_signed(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:905
ezSAT::NOT
int NOT(_V a)
Definition: ezsat.h:197
ezSAT::vec_lt_unsigned
int vec_lt_unsigned(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:926
SatGen::importSigSpec
std::vector< int > importSigSpec(RTLIL::SigSpec sig, int timestep=-1)
Definition: satgen.h:78
RTLIL::Cell::type
RTLIL::IdString type
Definition: rtlil.h:854
RTLIL::Cell::parameters
std::map< RTLIL::IdString, RTLIL::Const > parameters
Definition: rtlil.h:856
ezSAT::assume
void assume(int id)
Definition: ezsat.cc:388
RTLIL::SigSpec::size
int size() const
Definition: rtlil.h:1019
log_abort
#define log_abort()
Definition: log.h:84
ezSAT::AND
int AND(_V a=0, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
Definition: ezsat.h:201
ezSAT::vec_or
std::vector< int > vec_or(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:718
RTLIL::IdString::in
bool in(T first, Args...rest)
Definition: rtlil.h:241
SatGen::model_undef
bool model_undef
Definition: satgen.h:43
SatGen::importUndefSigSpec
std::vector< int > importUndefSigSpec(RTLIL::SigSpec sig, int timestep=-1)
Definition: satgen.h:92
ezSAT::vec_gt_unsigned
int vec_gt_unsigned(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:947
ezSAT::vec_neg
std::vector< int > vec_neg(const std::vector< int > &vec)
Definition: ezsat.cc:867
SatGen::importDefSigSpec
std::vector< int > importDefSigSpec(RTLIL::SigSpec sig, int timestep=-1)
Definition: satgen.h:85
ezSAT::vec_ne
int vec_ne(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:959
ezSAT::vec_shift_left
std::vector< int > vec_shift_left(const std::vector< int > &vec1, const std::vector< int > &vec2, bool vec2_signed, int extend_left, int extend_right)
Definition: ezsat.cc:1059
RTLIL::Cell::getPort
const RTLIL::SigSpec & getPort(RTLIL::IdString portname) const
Definition: rtlil.cc:1809
GetSize
int GetSize(RTLIL::Wire *wire)
Definition: yosys.cc:334
log_assert
#define log_assert(_assert_expr_)
Definition: log.h:85
ezSAT::vec_shift_right
std::vector< int > vec_shift_right(const std::vector< int > &vec1, const std::vector< int > &vec2, bool vec2_signed, int extend_left, int extend_right)
Definition: ezsat.cc:1016
Macc::from_cell
void from_cell(RTLIL::Cell *cell)
Definition: macc.h:100
SatGen::sigmap
SigMap * sigmap
Definition: satgen.h:37
ezSAT::vec_xor
std::vector< int > vec_xor(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:727
ezSAT::vec_gt_signed
int vec_gt_signed(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:919
SatGen::asserts_a
std::map< std::string, RTLIL::SigSpec > asserts_a
Definition: satgen.h:40
SigPool::add
void add(RTLIL::SigSpec sig)
Definition: sigtools.h:41
ezSAT::CONST_TRUE
static const int CONST_TRUE
Definition: ezsat.h:48
ezSAT::vec_add
std::vector< int > vec_add(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:819
ezSAT::literal
int literal()
Definition: ezsat.cc:73
ezSAT::vec_ite
std::vector< int > vec_ite(const std::vector< int > &vec1, const std::vector< int > &vec2, const std::vector< int > &vec3)
Definition: ezsat.cc:745
RTLIL::Cell::getParam
const RTLIL::Const & getParam(RTLIL::IdString paramname) const
Definition: rtlil.cc:1834
SatGen::undefGating
void undefGating(std::vector< int > &vec_y, std::vector< int > &vec_yy, std::vector< int > &vec_undef)
Definition: satgen.h:184
ezSAT::XOR
int XOR(_V a=0, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
Definition: ezsat.h:209
RTLIL::SigSpec::extract
RTLIL::SigSpec extract(const RTLIL::SigSpec &pattern, const RTLIL::SigSpec *other=NULL) const
Definition: rtlil.cc:2414
ezSAT::expression
int expression(OpId op, int a=0, int b=0, int c=0, int d=0, int e=0, int f=0)
Definition: ezsat.cc:102
RTLIL::Const::bits
std::vector< RTLIL::State > bits
Definition: rtlil.h:438
ezSAT::vec_eq
int vec_eq(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:954
ezSAT::vec_lt_signed
int vec_lt_signed(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:898
RTLIL::SigSpec::append
void append(const RTLIL::SigSpec &signal)
Definition: rtlil.cc:2523
ezSAT::OR
int OR(_V a=0, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
Definition: ezsat.h:205
ezSAT::IFF
int IFF(_V a, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
Definition: ezsat.h:213
ezSAT::vec_not
std::vector< int > vec_not(const std::vector< int > &vec1)
Definition: ezsat.cc:701
ezSAT::vec_ge_unsigned
int vec_ge_unsigned(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:940
ezSAT::vec_le_unsigned
int vec_le_unsigned(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:933
SatGen::signals_eq
int signals_eq(RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep_lhs=-1, int timestep_rhs=-1)
Definition: satgen.h:134
SatGen::prefix
std::string prefix
Definition: satgen.h:38
SatGen::extendSignalWidthUnary
void extendSignalWidthUnary(std::vector< int > &vec_a, std::vector< int > &vec_y, RTLIL::Cell *cell, bool forced_signed=false)
Definition: satgen.h:175
ezSAT::vec_and
std::vector< int > vec_and(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:709

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

std::vector<int> SatGen::importDefSigSpec ( RTLIL::SigSpec  sig,
int  timestep = -1 
)
inline

Definition at line 85 of file satgen.h.

86  {
87  log_assert(timestep != 0);
88  std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
89  return importSigSpecWorker(sig, pf, false, true);
90  }
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
SatGen::importSigSpecWorker
std::vector< int > importSigSpecWorker(RTLIL::SigSpec sig, std::string &pf, bool undef_mode, bool dup_undef)
Definition: satgen.h:56
log_assert
#define log_assert(_assert_expr_)
Definition: log.h:85
SatGen::prefix
std::string prefix
Definition: satgen.h:38

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

bool SatGen::importedSigBit ( RTLIL::SigBit  bit,
int  timestep = -1 
)
inline

Definition at line 106 of file satgen.h.

107  {
108  log_assert(timestep != 0);
109  std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
110  return imported_signals[pf].count(bit) != 0;
111  }
SatGen::imported_signals
std::map< std::string, std::map< RTLIL::SigBit, int > > imported_signals
Definition: satgen.h:41
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
log_assert
#define log_assert(_assert_expr_)
Definition: log.h:85
SatGen::prefix
std::string prefix
Definition: satgen.h:38

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

int SatGen::importSigBit ( RTLIL::SigBit  bit,
int  timestep = -1 
)
inline

Definition at line 99 of file satgen.h.

100  {
101  log_assert(timestep != 0);
102  std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
103  return importSigSpecWorker(bit, pf, false, false).front();
104  }
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
SatGen::importSigSpecWorker
std::vector< int > importSigSpecWorker(RTLIL::SigSpec sig, std::string &pf, bool undef_mode, bool dup_undef)
Definition: satgen.h:56
log_assert
#define log_assert(_assert_expr_)
Definition: log.h:85
SatGen::prefix
std::string prefix
Definition: satgen.h:38

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

std::vector<int> SatGen::importSigSpec ( RTLIL::SigSpec  sig,
int  timestep = -1 
)
inline

Definition at line 78 of file satgen.h.

79  {
80  log_assert(timestep != 0);
81  std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
82  return importSigSpecWorker(sig, pf, false, false);
83  }
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
SatGen::importSigSpecWorker
std::vector< int > importSigSpecWorker(RTLIL::SigSpec sig, std::string &pf, bool undef_mode, bool dup_undef)
Definition: satgen.h:56
log_assert
#define log_assert(_assert_expr_)
Definition: log.h:85
SatGen::prefix
std::string prefix
Definition: satgen.h:38

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

std::vector<int> SatGen::importSigSpecWorker ( RTLIL::SigSpec  sig,
std::string &  pf,
bool  undef_mode,
bool  dup_undef 
)
inline

Definition at line 56 of file satgen.h.

57  {
58  log_assert(!undef_mode || model_undef);
59  sigmap->apply(sig);
60 
61  std::vector<int> vec;
62  vec.reserve(GetSize(sig));
63 
64  for (auto &bit : sig)
65  if (bit.wire == NULL) {
66  if (model_undef && dup_undef && bit == RTLIL::State::Sx)
67  vec.push_back(ez->frozen_literal());
68  else
69  vec.push_back(bit == (undef_mode ? RTLIL::State::Sx : RTLIL::State::S1) ? ez->CONST_TRUE : ez->CONST_FALSE);
70  } else {
71  std::string name = pf + (bit.wire->width == 1 ? stringf("%s", log_id(bit.wire)) : stringf("%s [%d]", log_id(bit.wire->name), bit.offset));
72  vec.push_back(ez->frozen_literal(name));
73  imported_signals[pf][bit] = vec.back();
74  }
75  return vec;
76  }
SatGen::ez
ezSAT * ez
Definition: satgen.h:36
SatGen::imported_signals
std::map< std::string, std::map< RTLIL::SigBit, int > > imported_signals
Definition: satgen.h:41
ezSAT::frozen_literal
int frozen_literal()
Definition: ezsat.cc:88
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
ezSAT::CONST_FALSE
static const int CONST_FALSE
Definition: ezsat.h:49
SatGen::model_undef
bool model_undef
Definition: satgen.h:43
SigMap::apply
void apply(RTLIL::SigBit &bit) const
Definition: sigtools.h:383
GetSize
int GetSize(RTLIL::Wire *wire)
Definition: yosys.cc:334
log_assert
#define log_assert(_assert_expr_)
Definition: log.h:85
SatGen::sigmap
SigMap * sigmap
Definition: satgen.h:37
ezSAT::CONST_TRUE
static const int CONST_TRUE
Definition: ezsat.h:48
NULL
#define NULL
Definition: NumberlikeArray.hh:6
log_id
const char * log_id(RTLIL::IdString str)
Definition: log.cc:283

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

std::vector<int> SatGen::importUndefSigSpec ( RTLIL::SigSpec  sig,
int  timestep = -1 
)
inline

Definition at line 92 of file satgen.h.

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  }
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
SatGen::importSigSpecWorker
std::vector< int > importSigSpecWorker(RTLIL::SigSpec sig, std::string &pf, bool undef_mode, bool dup_undef)
Definition: satgen.h:56
log_assert
#define log_assert(_assert_expr_)
Definition: log.h:85
SatGen::prefix
std::string prefix
Definition: satgen.h:38

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

void SatGen::setContext ( SigMap *  sigmap,
std::string  prefix = std::string() 
)
inline

Definition at line 50 of file satgen.h.

51  {
52  this->sigmap = sigmap;
53  this->prefix = prefix;
54  }
SatGen::sigmap
SigMap * sigmap
Definition: satgen.h:37
SatGen::prefix
std::string prefix
Definition: satgen.h:38

+ Here is the caller graph for this function:

int SatGen::signals_eq ( RTLIL::SigSpec  lhs,
RTLIL::SigSpec  rhs,
int  timestep_lhs = -1,
int  timestep_rhs = -1 
)
inline

Definition at line 134 of file satgen.h.

135  {
136  if (timestep_rhs < 0)
137  timestep_rhs = timestep_lhs;
138 
139  log_assert(lhs.size() == rhs.size());
140 
141  std::vector<int> vec_lhs = importSigSpec(lhs, timestep_lhs);
142  std::vector<int> vec_rhs = importSigSpec(rhs, timestep_rhs);
143 
144  if (!model_undef)
145  return ez->vec_eq(vec_lhs, vec_rhs);
146 
147  std::vector<int> undef_lhs = importUndefSigSpec(lhs, timestep_lhs);
148  std::vector<int> undef_rhs = importUndefSigSpec(rhs, timestep_rhs);
149 
150  std::vector<int> eq_bits;
151  for (int i = 0; i < lhs.size(); i++)
152  eq_bits.push_back(ez->AND(ez->IFF(undef_lhs.at(i), undef_rhs.at(i)),
153  ez->IFF(ez->OR(vec_lhs.at(i), undef_lhs.at(i)), ez->OR(vec_rhs.at(i), undef_rhs.at(i)))));
154  return ez->expression(ezSAT::OpAnd, eq_bits);
155  }
SatGen::ez
ezSAT * ez
Definition: satgen.h:36
SatGen::importSigSpec
std::vector< int > importSigSpec(RTLIL::SigSpec sig, int timestep=-1)
Definition: satgen.h:78
RTLIL::SigSpec::size
int size() const
Definition: rtlil.h:1019
ezSAT::AND
int AND(_V a=0, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
Definition: ezsat.h:201
SatGen::model_undef
bool model_undef
Definition: satgen.h:43
SatGen::importUndefSigSpec
std::vector< int > importUndefSigSpec(RTLIL::SigSpec sig, int timestep=-1)
Definition: satgen.h:92
log_assert
#define log_assert(_assert_expr_)
Definition: log.h:85
ezSAT::expression
int expression(OpId op, int a=0, int b=0, int c=0, int d=0, int e=0, int f=0)
Definition: ezsat.cc:102
ezSAT::vec_eq
int vec_eq(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:954
ezSAT::OR
int OR(_V a=0, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
Definition: ezsat.h:205
ezSAT::IFF
int IFF(_V a, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
Definition: ezsat.h:213

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

void SatGen::undefGating ( std::vector< int > &  vec_y,
std::vector< int > &  vec_yy,
std::vector< int > &  vec_undef 
)
inline

Definition at line 184 of file satgen.h.

185  {
186  log_assert(model_undef);
187  log_assert(vec_y.size() == vec_yy.size());
188  if (vec_y.size() > vec_undef.size()) {
189  std::vector<int> trunc_y(vec_y.begin(), vec_y.begin() + vec_undef.size());
190  std::vector<int> trunc_yy(vec_yy.begin(), vec_yy.begin() + vec_undef.size());
191  ez->assume(ez->expression(ezSAT::OpAnd, ez->vec_or(vec_undef, ez->vec_iff(trunc_y, trunc_yy))));
192  } else {
193  log_assert(vec_y.size() == vec_undef.size());
194  ez->assume(ez->expression(ezSAT::OpAnd, ez->vec_or(vec_undef, ez->vec_iff(vec_y, vec_yy))));
195  }
196  }
SatGen::ez
ezSAT * ez
Definition: satgen.h:36
ezSAT::vec_iff
std::vector< int > vec_iff(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:736
ezSAT::assume
void assume(int id)
Definition: ezsat.cc:388
ezSAT::vec_or
std::vector< int > vec_or(const std::vector< int > &vec1, const std::vector< int > &vec2)
Definition: ezsat.cc:718
SatGen::model_undef
bool model_undef
Definition: satgen.h:43
log_assert
#define log_assert(_assert_expr_)
Definition: log.h:85
ezSAT::expression
int expression(OpId op, int a=0, int b=0, int c=0, int d=0, int e=0, int f=0)
Definition: ezsat.cc:102

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

void SatGen::undefGating ( int  y,
int  yy,
int  undef 
)
inline

Definition at line 198 of file satgen.h.

199  {
200  ez->assume(ez->OR(undef, ez->IFF(y, yy)));
201  }
SatGen::ez
ezSAT * ez
Definition: satgen.h:36
ezSAT::assume
void assume(int id)
Definition: ezsat.cc:388
ezSAT::OR
int OR(_V a=0, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
Definition: ezsat.h:205
ezSAT::IFF
int IFF(_V a, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
Definition: ezsat.h:213

+ Here is the call graph for this function:

Field Documentation

std::map<std::string, RTLIL::SigSpec> SatGen::asserts_a

Definition at line 40 of file satgen.h.

std::map<std::string, RTLIL::SigSpec> SatGen::asserts_en

Definition at line 40 of file satgen.h.

ezSAT* SatGen::ez

Definition at line 36 of file satgen.h.

bool SatGen::ignore_div_by_zero

Definition at line 42 of file satgen.h.

std::map<std::string, std::map<RTLIL::SigBit, int> > SatGen::imported_signals

Definition at line 41 of file satgen.h.

SigPool SatGen::initial_state

Definition at line 39 of file satgen.h.

bool SatGen::model_undef

Definition at line 43 of file satgen.h.

std::string SatGen::prefix

Definition at line 38 of file satgen.h.

SigMap* SatGen::sigmap

Definition at line 37 of file satgen.h.

The documentation for this struct was generated from the following file: