yosys-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
eval.cc
Go to the documentation of this file.
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 // [[CITE]] VlogHammer Verilog Regression Test Suite
21 // http://www.clifford.at/yosys/vloghammer.html
22 
23 #include "kernel/register.h"
24 #include "kernel/celltypes.h"
25 #include "kernel/consteval.h"
26 #include "kernel/sigtools.h"
27 #include "kernel/satgen.h"
28 #include "kernel/log.h"
29 #include <stdlib.h>
30 #include <stdio.h>
31 #include <string.h>
32 #include <algorithm>
33 
36 
37 /* this should only be used for regression testing of ConstEval -- see vloghammer */
39 {
45 
47  {
48  if (inputs.size() < mod1_inputs.size()) {
49  RTLIL::SigSpec inputs0 = inputs, inputs1 = inputs;
50  inputs0.append(RTLIL::Const(0, 1));
51  inputs1.append(RTLIL::Const(1, 1));
52  run_checker(inputs0);
53  run_checker(inputs1);
54  return;
55  }
56 
57  ConstEval ce1(mod1), ce2(mod2);
58  ce1.set(mod1_inputs, inputs.as_const());
59  ce2.set(mod2_inputs, inputs.as_const());
60 
61  RTLIL::SigSpec sig1 = mod1_outputs, undef1;
62  RTLIL::SigSpec sig2 = mod2_outputs, undef2;
63 
64  if (!ce1.eval(sig1, undef1))
65  log("Failed ConstEval of module 1 outputs at signal %s (input: %s = %s).\n",
66  log_signal(undef1), log_signal(mod1_inputs), log_signal(inputs));
67  if (!ce2.eval(sig2, undef2))
68  log("Failed ConstEval of module 2 outputs at signal %s (input: %s = %s).\n",
69  log_signal(undef2), log_signal(mod1_inputs), log_signal(inputs));
70 
71  if (ignore_x_mod1) {
72  for (int i = 0; i < GetSize(sig1); i++)
73  if (sig1[i] == RTLIL::State::Sx)
74  sig2[i] = RTLIL::State::Sx;
75  }
76 
77  if (sig1 != sig2) {
78  log("Found counter-example (ignore_x_mod1 = %s):\n", ignore_x_mod1 ? "active" : "inactive");
79  log(" Module 1: %s = %s => %s = %s\n", log_signal(mod1_inputs), log_signal(inputs), log_signal(mod1_outputs), log_signal(sig1));
80  log(" Module 2: %s = %s => %s = %s\n", log_signal(mod2_inputs), log_signal(inputs), log_signal(mod2_outputs), log_signal(sig2));
81  errors++;
82  }
83 
84  counter++;
85  }
86 
88  mod1(mod1), mod2(mod2), counter(0), errors(0), ignore_x_mod1(ignore_x_mod1)
89  {
90  log("Checking for equivialence (brute-force): %s vs %s\n", mod1->name.c_str(), mod2->name.c_str());
91  for (auto &w : mod1->wires_)
92  {
93  RTLIL::Wire *wire1 = w.second;
94  if (wire1->port_id == 0)
95  continue;
96 
97  if (mod2->wires_.count(wire1->name) == 0)
98  log_cmd_error("Port %s in module 1 has no counterpart in module 2!\n", wire1->name.c_str());
99 
100  RTLIL::Wire *wire2 = mod2->wires_.at(wire1->name);
101  if (wire1->width != wire2->width || wire1->port_input != wire2->port_input || wire1->port_output != wire2->port_output)
102  log_cmd_error("Port %s in module 1 does not match its counterpart in module 2!\n", wire1->name.c_str());
103 
104  if (wire1->port_input) {
105  mod1_inputs.append(wire1);
106  mod2_inputs.append(wire2);
107  } else {
108  mod1_outputs.append(wire1);
109  mod2_outputs.append(wire2);
110  }
111  }
112 
113  RTLIL::SigSpec inputs;
114  run_checker(inputs);
115  }
116 };
117 
118 /* this should only be used for regression testing of ConstEval -- see vloghammer */
120 {
122  std::vector<RTLIL::Module*> modules;
123  std::vector<std::string> module_names;
124  std::vector<RTLIL::IdString> inputs;
125  std::vector<int> input_widths;
126  std::vector<RTLIL::Const> patterns;
128 
129  std::vector<std::string> split(std::string text, const char *delim)
130  {
131  std::vector<std::string> list;
132  char *p = strdup(text.c_str());
133  char *t = strtok(p, delim);
134  while (t != NULL) {
135  list.push_back(t);
136  t = strtok(NULL, delim);
137  }
138  free(p);
139  return list;
140  }
141 
142  void sat_check(RTLIL::Module *module, RTLIL::SigSpec recorded_set_vars, RTLIL::Const recorded_set_vals, RTLIL::SigSpec expected_y, bool model_undef)
143  {
144  log("Verifying SAT model (%s)..\n", model_undef ? "with undef" : "without undef");
145 
147  SigMap sigmap(module);
148  SatGen satgen(&ez, &sigmap);
149  satgen.model_undef = model_undef;
150 
151  for (auto &c : module->cells_)
152  if (!satgen.importCell(c.second))
153  log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
154 
155  ez.assume(satgen.signals_eq(recorded_set_vars, recorded_set_vals));
156 
157  std::vector<int> y_vec = satgen.importDefSigSpec(module->wires_.at("\\y"));
158  std::vector<bool> y_values;
159 
160  if (model_undef) {
161  std::vector<int> y_undef_vec = satgen.importUndefSigSpec(module->wires_.at("\\y"));
162  y_vec.insert(y_vec.end(), y_undef_vec.begin(), y_undef_vec.end());
163  }
164 
165  log(" Created SAT problem with %d variables and %d clauses.\n",
166  ez.numCnfVariables(), ez.numCnfClauses());
167 
168  if (!ez.solve(y_vec, y_values))
169  log_error("Failed to find solution to SAT problem.\n");
170 
171  for (int i = 0; i < expected_y.size(); i++) {
172  RTLIL::State solution_bit = y_values.at(i) ? RTLIL::State::S1 : RTLIL::State::S0;
173  RTLIL::State expected_bit = expected_y[i].data;
174  if (model_undef) {
175  if (y_values.at(expected_y.size()+i))
176  solution_bit = RTLIL::State::Sx;
177  } else {
178  if (expected_bit == RTLIL::State::Sx)
179  continue;
180  }
181  if (solution_bit != expected_bit) {
182  std::string sat_bits, rtl_bits;
183  for (int k = expected_y.size()-1; k >= 0; k--) {
184  if (model_undef && y_values.at(expected_y.size()+k))
185  sat_bits += "x";
186  else
187  sat_bits += y_values.at(k) ? "1" : "0";
188  rtl_bits += expected_y[k] == RTLIL::State::Sx ? "x" : expected_y[k] == RTLIL::State::S1 ? "1" : "0";
189  }
190  log_error("Found error in SAT model: y[%d] = %s, should be %s:\n SAT: %s\n RTL: %s\n %*s^\n",
191  int(i), log_signal(solution_bit), log_signal(expected_bit),
192  sat_bits.c_str(), rtl_bits.c_str(), expected_y.size()-i-1, "");
193  }
194  }
195 
196  if (model_undef)
197  {
198  std::vector<int> cmp_vars;
199  std::vector<bool> cmp_vals;
200 
201  std::vector<bool> y_undef(y_values.begin() + expected_y.size(), y_values.end());
202 
203  for (int i = 0; i < expected_y.size(); i++)
204  if (y_undef.at(i))
205  {
206  log(" Toggling undef bit %d to test undef gating.\n", i);
207  if (!ez.solve(y_vec, y_values, ez.IFF(y_vec.at(i), y_values.at(i) ? ez.CONST_FALSE : ez.CONST_TRUE)))
208  log_error("Failed to find solution with toggled bit!\n");
209 
210  cmp_vars.push_back(y_vec.at(expected_y.size() + i));
211  cmp_vals.push_back(true);
212  }
213  else
214  {
215  cmp_vars.push_back(y_vec.at(i));
216  cmp_vals.push_back(y_values.at(i));
217 
218  cmp_vars.push_back(y_vec.at(expected_y.size() + i));
219  cmp_vals.push_back(false);
220  }
221 
222  log(" Testing if SAT solution is unique.\n");
223  ez.assume(ez.vec_ne(cmp_vars, ez.vec_const(cmp_vals)));
224  if (ez.solve(y_vec, y_values))
225  log_error("Found two distinct solutions to SAT problem.\n");
226  }
227  else
228  {
229  log(" Testing if SAT solution is unique.\n");
230  ez.assume(ez.vec_ne(y_vec, ez.vec_const(y_values)));
231  if (ez.solve(y_vec, y_values))
232  log_error("Found two distinct solutions to SAT problem.\n");
233  }
234 
235  log(" SAT model verified.\n");
236  }
237 
238  void run()
239  {
240  for (int idx = 0; idx < int(patterns.size()); idx++)
241  {
242  log("Creating report for pattern %d: %s\n", idx, log_signal(patterns[idx]));
243  std::string input_pattern_list;
244  RTLIL::SigSpec rtl_sig;
245 
246  for (int mod = 0; mod < int(modules.size()); mod++)
247  {
248  RTLIL::SigSpec recorded_set_vars;
249  RTLIL::Const recorded_set_vals;
250  RTLIL::Module *module = modules[mod];
251  std::string module_name = module_names[mod].c_str();
252  ConstEval ce(module);
253 
254  std::vector<RTLIL::State> bits(patterns[idx].bits.begin(), patterns[idx].bits.begin() + total_input_width);
255  for (int i = 0; i < int(inputs.size()); i++) {
256  RTLIL::Wire *wire = module->wires_.at(inputs[i]);
257  for (int j = input_widths[i]-1; j >= 0; j--) {
258  ce.set(RTLIL::SigSpec(wire, j), bits.back());
259  recorded_set_vars.append(RTLIL::SigSpec(wire, j));
260  recorded_set_vals.bits.push_back(bits.back());
261  bits.pop_back();
262  }
263  if (module == modules.front()) {
264  RTLIL::SigSpec sig(wire);
265  if (!ce.eval(sig))
266  log_error("Can't read back value for port %s!\n", RTLIL::id2cstr(inputs[i]));
267  input_pattern_list += stringf(" %s", sig.as_const().as_string().c_str());
268  log("++PAT++ %d %s %s #\n", idx, RTLIL::id2cstr(inputs[i]), sig.as_const().as_string().c_str());
269  }
270  }
271 
272  if (module->wires_.count("\\y") == 0)
273  log_error("No output wire (y) found in module %s!\n", RTLIL::id2cstr(module->name));
274 
275  RTLIL::SigSpec sig(module->wires_.at("\\y"));
276  RTLIL::SigSpec undef;
277 
278  while (!ce.eval(sig, undef)) {
279  // log_error("Evaluation of y in module %s failed: sig=%s, undef=%s\n", RTLIL::id2cstr(module->name), log_signal(sig), log_signal(undef));
280  log_warning("Setting signal %s in module %s to undef.\n", log_signal(undef), RTLIL::id2cstr(module->name));
281  ce.set(undef, RTLIL::Const(RTLIL::State::Sx, undef.size()));
282  }
283 
284  log("++VAL++ %d %s %s #\n", idx, module_name.c_str(), sig.as_const().as_string().c_str());
285 
286  if (module_name == "rtl") {
287  rtl_sig = sig;
288  sat_check(module, recorded_set_vars, recorded_set_vals, sig, false);
289  sat_check(module, recorded_set_vars, recorded_set_vals, sig, true);
290  } else if (rtl_sig.size() > 0) {
291  if (rtl_sig.size() != sig.size())
292  log_error("Output (y) has a different width in module %s compared to rtl!\n", RTLIL::id2cstr(module->name));
293  for (int i = 0; i < GetSize(sig); i++)
294  if (rtl_sig[i] == RTLIL::State::Sx)
295  sig[i] = RTLIL::State::Sx;
296  }
297 
298  log("++RPT++ %d%s %s %s\n", idx, input_pattern_list.c_str(), sig.as_const().as_string().c_str(), module_name.c_str());
299  }
300 
301  log("++RPT++ ----\n");
302  }
303  log("++OK++\n");
304  }
305 
306  VlogHammerReporter(RTLIL::Design *design, std::string module_prefix, std::string module_list, std::string input_list, std::string pattern_list) : design(design)
307  {
308  for (auto name : split(module_list, ",")) {
309  RTLIL::IdString esc_name = RTLIL::escape_id(module_prefix + name);
310  if (design->modules_.count(esc_name) == 0)
311  log_error("Can't find module %s in current design!\n", name.c_str());
312  log("Using module %s (%s).\n", esc_name.c_str(), name.c_str());
313  modules.push_back(design->modules_.at(esc_name));
314  module_names.push_back(name);
315  }
316 
317  total_input_width = 0;
318  for (auto name : split(input_list, ",")) {
319  int width = -1;
320  RTLIL::IdString esc_name = RTLIL::escape_id(name);
321  for (auto mod : modules) {
322  if (mod->wires_.count(esc_name) == 0)
323  log_error("Can't find input %s in module %s!\n", name.c_str(), RTLIL::id2cstr(mod->name));
324  RTLIL::Wire *port = mod->wires_.at(esc_name);
325  if (!port->port_input || port->port_output)
326  log_error("Wire %s in module %s is not an input!\n", name.c_str(), RTLIL::id2cstr(mod->name));
327  if (width >= 0 && width != port->width)
328  log_error("Port %s has different sizes in the different modules!\n", name.c_str());
329  width = port->width;
330  }
331  log("Using input port %s with width %d.\n", esc_name.c_str(), width);
332  inputs.push_back(esc_name);
333  input_widths.push_back(width);
334  total_input_width += width;
335  }
336 
337  for (auto pattern : split(pattern_list, ",")) {
338  RTLIL::SigSpec sig;
339  bool invert_pattern = false;
340  if (pattern.size() > 0 && pattern[0] == '~') {
341  invert_pattern = true;
342  pattern = pattern.substr(1);
343  }
344  if (!RTLIL::SigSpec::parse(sig, NULL, pattern) || !sig.is_fully_const())
345  log_error("Failed to parse pattern %s!\n", pattern.c_str());
346  if (sig.size() < total_input_width)
347  log_error("Pattern %s is to short!\n", pattern.c_str());
348  patterns.push_back(sig.as_const());
349  if (invert_pattern) {
350  for (auto &bit : patterns.back().bits)
351  if (bit == RTLIL::State::S0)
352  bit = RTLIL::State::S1;
353  else if (bit == RTLIL::State::S1)
354  bit = RTLIL::State::S0;
355  }
356  log("Using pattern %s.\n", patterns.back().as_string().c_str());
357  }
358  }
359 };
360 
361 struct EvalPass : public Pass {
362  EvalPass() : Pass("eval", "evaluate the circuit given an input") { }
363  virtual void help()
364  {
365  // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
366  log("\n");
367  log(" eval [options] [selection]\n");
368  log("\n");
369  log("This command evaluates the value of a signal given the value of all required\n");
370  log("inputs.\n");
371  log("\n");
372  log(" -set <signal> <value>\n");
373  log(" set the specified signal to the specified value.\n");
374  log("\n");
375  log(" -set-undef\n");
376  log(" set all unspecified source signals to undef (x)\n");
377  log("\n");
378  log(" -table <signal>\n");
379  log(" create a truth table using the specified input signals\n");
380  log("\n");
381  log(" -show <signal>\n");
382  log(" show the value for the specified signal. if no -show option is passed\n");
383  log(" then all output ports of the current module are used.\n");
384  log("\n");
385  }
386  virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
387  {
388  std::vector<std::pair<std::string, std::string>> sets;
389  std::vector<std::string> shows, tables;
390  bool set_undef = false;
391 
392  log_header("Executing EVAL pass (evaluate the circuit given an input).\n");
393 
394  size_t argidx;
395  for (argidx = 1; argidx < args.size(); argidx++) {
396  if (args[argidx] == "-set" && argidx+2 < args.size()) {
397  std::string lhs = args[++argidx].c_str();
398  std::string rhs = args[++argidx].c_str();
399  sets.push_back(std::pair<std::string, std::string>(lhs, rhs));
400  continue;
401  }
402  if (args[argidx] == "-set-undef") {
403  set_undef = true;
404  continue;
405  }
406  if (args[argidx] == "-show" && argidx+1 < args.size()) {
407  shows.push_back(args[++argidx]);
408  continue;
409  }
410  if (args[argidx] == "-table" && argidx+1 < args.size()) {
411  tables.push_back(args[++argidx]);
412  continue;
413  }
414  if ((args[argidx] == "-brute_force_equiv_checker" || args[argidx] == "-brute_force_equiv_checker_x") && argidx+3 == args.size()) {
415  /* this should only be used for regression testing of ConstEval -- see vloghammer */
416  std::string mod1_name = RTLIL::escape_id(args[++argidx]);
417  std::string mod2_name = RTLIL::escape_id(args[++argidx]);
418  if (design->modules_.count(mod1_name) == 0)
419  log_error("Can't find module `%s'!\n", mod1_name.c_str());
420  if (design->modules_.count(mod2_name) == 0)
421  log_error("Can't find module `%s'!\n", mod2_name.c_str());
422  BruteForceEquivChecker checker(design->modules_.at(mod1_name), design->modules_.at(mod2_name), args[argidx-2] == "-brute_force_equiv_checker_x");
423  if (checker.errors > 0)
424  log_cmd_error("Modules are not equivialent!\n");
425  log("Verified %s = %s (using brute-force check on %d cases).\n",
426  mod1_name.c_str(), mod2_name.c_str(), checker.counter);
427  return;
428  }
429  if (args[argidx] == "-vloghammer_report" && argidx+5 == args.size()) {
430  /* this should only be used for regression testing of ConstEval -- see vloghammer */
431  std::string module_prefix = args[++argidx];
432  std::string module_list = args[++argidx];
433  std::string input_list = args[++argidx];
434  std::string pattern_list = args[++argidx];
435  VlogHammerReporter reporter(design, module_prefix, module_list, input_list, pattern_list);
436  reporter.run();
437  return;
438  }
439  break;
440  }
441  extra_args(args, argidx, design);
442 
444  for (auto &mod_it : design->modules_)
445  if (design->selected(mod_it.second)) {
446  if (module)
447  log_cmd_error("Only one module must be selected for the EVAL pass! (selected: %s and %s)\n",
448  RTLIL::id2cstr(module->name), RTLIL::id2cstr(mod_it.first));
449  module = mod_it.second;
450  }
451  if (module == NULL)
452  log_cmd_error("Can't perform EVAL on an empty selection!\n");
453 
454  ConstEval ce(module);
455 
456  for (auto &it : sets) {
457  RTLIL::SigSpec lhs, rhs;
458  if (!RTLIL::SigSpec::parse_sel(lhs, design, module, it.first))
459  log_cmd_error("Failed to parse lhs set expression `%s'.\n", it.first.c_str());
460  if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, it.second))
461  log_cmd_error("Failed to parse rhs set expression `%s'.\n", it.second.c_str());
462  if (!rhs.is_fully_const())
463  log_cmd_error("Right-hand-side set expression `%s' is not constant.\n", it.second.c_str());
464  if (lhs.size() != rhs.size())
465  log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
466  it.first.c_str(), log_signal(lhs), lhs.size(), it.second.c_str(), log_signal(rhs), rhs.size());
467  ce.set(lhs, rhs.as_const());
468  }
469 
470  if (shows.size() == 0) {
471  for (auto &it : module->wires_)
472  if (it.second->port_output)
473  shows.push_back(it.second->name.str());
474  }
475 
476  if (tables.empty())
477  {
478  for (auto &it : shows) {
479  RTLIL::SigSpec signal, value, undef;
480  if (!RTLIL::SigSpec::parse_sel(signal, design, module, it))
481  log_cmd_error("Failed to parse show expression `%s'.\n", it.c_str());
482  value = signal;
483  if (set_undef) {
484  while (!ce.eval(value, undef)) {
485  log("Failed to evaluate signal %s: Missing value for %s. -> setting to undef\n", log_signal(signal), log_signal(undef));
486  ce.set(undef, RTLIL::Const(RTLIL::State::Sx, undef.size()));
487  undef = RTLIL::SigSpec();
488  }
489  log("Eval result: %s = %s.\n", log_signal(signal), log_signal(value));
490  } else {
491  if (!ce.eval(value, undef))
492  log("Failed to evaluate signal %s: Missing value for %s.\n", log_signal(signal), log_signal(undef));
493  else
494  log("Eval result: %s = %s.\n", log_signal(signal), log_signal(value));
495  }
496  }
497  }
498  else
499  {
500  RTLIL::SigSpec tabsigs, signal, value, undef;
501  std::vector<std::vector<std::string>> tab;
502  int tab_sep_colidx = 0;
503 
504  for (auto &it : shows) {
505  RTLIL::SigSpec sig;
506  if (!RTLIL::SigSpec::parse_sel(sig, design, module, it))
507  log_cmd_error("Failed to parse show expression `%s'.\n", it.c_str());
508  signal.append(sig);
509  }
510 
511  for (auto &it : tables) {
512  RTLIL::SigSpec sig;
513  if (!RTLIL::SigSpec::parse_sel(sig, design, module, it))
514  log_cmd_error("Failed to parse table expression `%s'.\n", it.c_str());
515  tabsigs.append(sig);
516  }
517 
518  std::vector<std::string> tab_line;
519  for (auto &c : tabsigs.chunks())
520  tab_line.push_back(log_signal(c));
521  tab_sep_colidx = tab_line.size();
522  for (auto &c : signal.chunks())
523  tab_line.push_back(log_signal(c));
524  tab.push_back(tab_line);
525  tab_line.clear();
526 
527  RTLIL::Const tabvals(0, tabsigs.size());
528  do
529  {
530  ce.push();
531  ce.set(tabsigs, tabvals);
532  value = signal;
533 
534  RTLIL::SigSpec this_undef;
535  while (!ce.eval(value, this_undef)) {
536  if (!set_undef) {
537  log("Failed to evaluate signal %s at %s = %s: Missing value for %s.\n", log_signal(signal),
538  log_signal(tabsigs), log_signal(tabvals), log_signal(this_undef));
539  return;
540  }
541  ce.set(this_undef, RTLIL::Const(RTLIL::State::Sx, this_undef.size()));
542  undef.append(this_undef);
543  this_undef = RTLIL::SigSpec();
544  }
545 
546  int pos = 0;
547  for (auto &c : tabsigs.chunks()) {
548  tab_line.push_back(log_signal(RTLIL::SigSpec(tabvals).extract(pos, c.width)));
549  pos += c.width;
550  }
551 
552  pos = 0;
553  for (auto &c : signal.chunks()) {
554  tab_line.push_back(log_signal(value.extract(pos, c.width)));
555  pos += c.width;
556  }
557 
558  tab.push_back(tab_line);
559  tab_line.clear();
560  ce.pop();
561 
562  tabvals = RTLIL::const_add(tabvals, RTLIL::Const(1), false, false, tabvals.bits.size());
563  }
564  while (tabvals.as_bool());
565 
566  std::vector<int> tab_column_width;
567  for (auto &row : tab) {
568  if (tab_column_width.size() < row.size())
569  tab_column_width.resize(row.size());
570  for (size_t i = 0; i < row.size(); i++)
571  tab_column_width[i] = std::max(tab_column_width[i], int(row[i].size()));
572  }
573 
574  log("\n");
575  bool first = true;
576  for (auto &row : tab) {
577  for (size_t i = 0; i < row.size(); i++) {
578  int k = int(i) < tab_sep_colidx ? tab_sep_colidx - i - 1 : i;
579  log(" %s%*s", k == tab_sep_colidx ? "| " : "", tab_column_width[k], row[k].c_str());
580  }
581  log("\n");
582  if (first) {
583  for (size_t i = 0; i < row.size(); i++) {
584  int k = int(i) < tab_sep_colidx ? tab_sep_colidx - i - 1 : i;
585  log(" %s", k == tab_sep_colidx ? "| " : "");
586  for (int j = 0; j < tab_column_width[k]; j++)
587  log("-");
588  }
589  log("\n");
590  first = false;
591  }
592  }
593 
594  log("\n");
595  if (undef.size() > 0) {
596  undef.sort_and_unify();
597  log("Assumend undef (x) value for the following singals: %s\n\n", log_signal(undef));
598  }
599  }
600  }
601 } EvalPass;
602 
const char * c_str() const
Definition: rtlil.h:178
bool selected(T1 *module) const
Definition: rtlil.h:551
void sat_check(RTLIL::Module *module, RTLIL::SigSpec recorded_set_vars, RTLIL::Const recorded_set_vals, RTLIL::SigSpec expected_y, bool model_undef)
Definition: eval.cc:142
std::vector< RTLIL::IdString > inputs
Definition: eval.cc:124
RTLIL::Design * design
Definition: eval.cc:121
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
void log_warning(const char *format,...)
Definition: log.cc:196
void free(void *)
static bool parse_sel(RTLIL::SigSpec &sig, RTLIL::Design *design, RTLIL::Module *module, std::string str)
Definition: rtlil.cc:3058
void log_header(const char *format,...)
Definition: log.cc:188
RTLIL::Const as_const() const
Definition: rtlil.cc:2857
std::map< RTLIL::IdString, RTLIL::Wire * > wires_
Definition: rtlil.h:595
RTLIL::SigSpec mod1_inputs
Definition: eval.cc:41
const char * log_signal(const RTLIL::SigSpec &sig, bool autoint)
Definition: log.cc:269
ezMiniSAT ez
Definition: puzzle3d.cc:31
static std::string idx(std::string str)
Definition: test_autotb.cc:57
RTLIL::Module * mod1
Definition: eval.cc:40
bool port_input
Definition: rtlil.h:827
std::vector< std::string > split(std::string text, const char *delim)
Definition: eval.cc:129
bool eval(RTLIL::Cell *cell, RTLIL::SigSpec &undef)
Definition: consteval.h:89
int width
Definition: rtlil.h:826
std::vector< std::string > module_names
Definition: eval.cc:123
void log_error(const char *format,...)
Definition: log.cc:204
RTLIL::Module * module
Definition: abc.cc:94
int port_id
Definition: rtlil.h:826
int size() const
Definition: rtlil.h:1019
virtual void execute(std::vector< std::string > args, RTLIL::Design *design)
Definition: eval.cc:386
bool model_undef
Definition: satgen.h:43
void push()
Definition: consteval.h:61
EvalPass()
Definition: eval.cc:362
void run_checker(RTLIL::SigSpec &inputs)
Definition: eval.cc:46
std::vector< int > importUndefSigSpec(RTLIL::SigSpec sig, int timestep=-1)
Definition: satgen.h:92
static std::string escape_id(std::string str)
Definition: rtlil.h:251
bool port_output
Definition: rtlil.h:827
YOSYS_NAMESPACE_BEGIN typedef ezMiniSAT ezDefaultSAT
Definition: satgen.h:32
std::vector< int > importDefSigSpec(RTLIL::SigSpec sig, int timestep=-1)
Definition: satgen.h:85
std::string as_string() const
Definition: rtlil.cc:116
VlogHammerReporter(RTLIL::Design *design, std::string module_prefix, std::string module_list, std::string input_list, std::string pattern_list)
Definition: eval.cc:306
#define PRIVATE_NAMESPACE_BEGIN
Definition: yosys.h:97
EvalPass EvalPass
int GetSize(RTLIL::Wire *wire)
Definition: yosys.cc:334
bool is_fully_const() const
Definition: rtlil.cc:2763
RTLIL::IdString name
Definition: rtlil.h:599
std::vector< RTLIL::Module * > modules
Definition: eval.cc:122
#define PRIVATE_NAMESPACE_END
Definition: yosys.h:98
Definition: satgen.h:34
Definition: register.h:27
RTLIL::IdString name
Definition: rtlil.h:825
static const char * id2cstr(const RTLIL::IdString &str)
Definition: rtlil.h:267
void log_cmd_error(const char *format,...)
Definition: log.cc:211
RTLIL::SigSpec mod2_inputs
Definition: eval.cc:42
RTLIL::SigSpec mod1_outputs
Definition: eval.cc:41
std::vector< int > input_widths
Definition: eval.cc:125
#define USING_YOSYS_NAMESPACE
Definition: yosys.h:102
std::map< RTLIL::IdString, RTLIL::Module * > modules_
Definition: rtlil.h:507
void sort_and_unify()
Definition: rtlil.cc:2291
#define NULL
std::map< RTLIL::IdString, RTLIL::Cell * > cells_
Definition: rtlil.h:596
void log(const char *format,...)
Definition: log.cc:180
int total_input_width
Definition: eval.cc:127
bool importCell(RTLIL::Cell *cell, int timestep=-1)
Definition: satgen.h:203
RTLIL::SigSpec extract(const RTLIL::SigSpec &pattern, const RTLIL::SigSpec *other=NULL) const
Definition: rtlil.cc:2414
std::vector< RTLIL::State > bits
Definition: rtlil.h:438
void append(const RTLIL::SigSpec &signal)
Definition: rtlil.cc:2523
State
Definition: rtlil.h:29
RTLIL::Const const_add(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
Definition: calc.cc:464
static bool parse_rhs(const RTLIL::SigSpec &lhs, RTLIL::SigSpec &sig, RTLIL::Module *module, std::string str)
Definition: rtlil.cc:3078
BruteForceEquivChecker(RTLIL::Module *mod1, RTLIL::Module *mod2, bool ignore_x_mod1)
Definition: eval.cc:87
void extra_args(std::vector< std::string > args, size_t argidx, RTLIL::Design *design, bool select=true)
Definition: register.cc:128
RTLIL::Module * mod2
Definition: eval.cc:40
void set(RTLIL::SigSpec sig, RTLIL::Const value)
Definition: consteval.h:72
RTLIL::SigSpec mod2_outputs
Definition: eval.cc:42
static bool parse(RTLIL::SigSpec &sig, RTLIL::Module *module, std::string str)
Definition: rtlil.cc:2972
virtual void help()
Definition: eval.cc:363
std::vector< RTLIL::Const > patterns
Definition: eval.cc:126
int signals_eq(RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep_lhs=-1, int timestep_rhs=-1)
Definition: satgen.h:134
void pop()
Definition: consteval.h:66
const std::vector< RTLIL::SigChunk > & chunks() const
Definition: rtlil.h:1016