yosys-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Public Member Functions | Data Fields
VlogHammerReporter Struct Reference
+ Collaboration diagram for VlogHammerReporter:

Public Member Functions

std::vector< std::string > split (std::string text, const char *delim)
 
void sat_check (RTLIL::Module *module, RTLIL::SigSpec recorded_set_vars, RTLIL::Const recorded_set_vals, RTLIL::SigSpec expected_y, bool model_undef)
 
void run ()
 
 VlogHammerReporter (RTLIL::Design *design, std::string module_prefix, std::string module_list, std::string input_list, std::string pattern_list)
 

Data Fields

RTLIL::Design * design
 
std::vector< RTLIL::Module * > modules
 
std::vector< std::string > module_names
 
std::vector< RTLIL::IdString > inputs
 
std::vector< int > input_widths
 
std::vector< RTLIL::Const > patterns
 
int total_input_width
 

Detailed Description

Definition at line 119 of file eval.cc.

Constructor & Destructor Documentation

VlogHammerReporter::VlogHammerReporter ( RTLIL::Design *  design,
std::string  module_prefix,
std::string  module_list,
std::string  input_list,
std::string  pattern_list 
)
inline

Definition at line 306 of file eval.cc.

306  : 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  }
RTLIL::IdString::c_str
const char * c_str() const
Definition: rtlil.h:178
VlogHammerReporter::inputs
std::vector< RTLIL::IdString > inputs
Definition: eval.cc:124
VlogHammerReporter::design
RTLIL::Design * design
Definition: eval.cc:121
RTLIL::SigSpec::as_const
RTLIL::Const as_const() const
Definition: rtlil.cc:2857
RTLIL::Wire::port_input
bool port_input
Definition: rtlil.h:827
VlogHammerReporter::split
std::vector< std::string > split(std::string text, const char *delim)
Definition: eval.cc:129
RTLIL::Wire::width
int width
Definition: rtlil.h:826
VlogHammerReporter::module_names
std::vector< std::string > module_names
Definition: eval.cc:123
log_error
void log_error(const char *format,...)
Definition: log.cc:204
RTLIL::SigSpec::size
int size() const
Definition: rtlil.h:1019
RTLIL::escape_id
static std::string escape_id(std::string str)
Definition: rtlil.h:251
RTLIL::Wire::port_output
bool port_output
Definition: rtlil.h:827
RTLIL::SigSpec::is_fully_const
bool is_fully_const() const
Definition: rtlil.cc:2763
VlogHammerReporter::modules
std::vector< RTLIL::Module * > modules
Definition: eval.cc:122
RTLIL::id2cstr
static const char * id2cstr(const RTLIL::IdString &str)
Definition: rtlil.h:267
VlogHammerReporter::input_widths
std::vector< int > input_widths
Definition: eval.cc:125
RTLIL::Design::modules_
std::map< RTLIL::IdString, RTLIL::Module * > modules_
Definition: rtlil.h:507
NULL
#define NULL
Definition: NumberlikeArray.hh:6
log
void log(const char *format,...)
Definition: log.cc:180
VlogHammerReporter::total_input_width
int total_input_width
Definition: eval.cc:127
RTLIL::SigSpec::parse
static bool parse(RTLIL::SigSpec &sig, RTLIL::Module *module, std::string str)
Definition: rtlil.cc:2972
VlogHammerReporter::patterns
std::vector< RTLIL::Const > patterns
Definition: eval.cc:126

+ Here is the call graph for this function:

Member Function Documentation

void VlogHammerReporter::run ( )
inline

Definition at line 238 of file eval.cc.

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  }
VlogHammerReporter::sat_check
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
VlogHammerReporter::inputs
std::vector< RTLIL::IdString > inputs
Definition: eval.cc:124
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
log_warning
void log_warning(const char *format,...)
Definition: log.cc:196
RTLIL::Module::wires_
std::map< RTLIL::IdString, RTLIL::Wire * > wires_
Definition: rtlil.h:595
log_signal
const char * log_signal(const RTLIL::SigSpec &sig, bool autoint)
Definition: log.cc:269
idx
static std::string idx(std::string str)
Definition: test_autotb.cc:57
VlogHammerReporter::module_names
std::vector< std::string > module_names
Definition: eval.cc:123
log_error
void log_error(const char *format,...)
Definition: log.cc:204
module
RTLIL::Module * module
Definition: abc.cc:94
RTLIL::SigSpec::size
int size() const
Definition: rtlil.h:1019
GetSize
int GetSize(RTLIL::Wire *wire)
Definition: yosys.cc:334
RTLIL::Module::name
RTLIL::IdString name
Definition: rtlil.h:599
VlogHammerReporter::modules
std::vector< RTLIL::Module * > modules
Definition: eval.cc:122
RTLIL::id2cstr
static const char * id2cstr(const RTLIL::IdString &str)
Definition: rtlil.h:267
VlogHammerReporter::input_widths
std::vector< int > input_widths
Definition: eval.cc:125
log
void log(const char *format,...)
Definition: log.cc:180
VlogHammerReporter::total_input_width
int total_input_width
Definition: eval.cc:127
RTLIL::Const::bits
std::vector< RTLIL::State > bits
Definition: rtlil.h:438
RTLIL::SigSpec::append
void append(const RTLIL::SigSpec &signal)
Definition: rtlil.cc:2523
VlogHammerReporter::patterns
std::vector< RTLIL::Const > patterns
Definition: eval.cc:126

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

void VlogHammerReporter::sat_check ( RTLIL::Module *  module,
RTLIL::SigSpec  recorded_set_vars,
RTLIL::Const  recorded_set_vals,
RTLIL::SigSpec  expected_y,
bool  model_undef 
)
inline

Definition at line 142 of file eval.cc.

143  {
144  log("Verifying SAT model (%s)..\n", model_undef ? "with undef" : "without undef");
145 
146  ezDefaultSAT ez;
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  }
RTLIL::Module::wires_
std::map< RTLIL::IdString, RTLIL::Wire * > wires_
Definition: rtlil.h:595
log_signal
const char * log_signal(const RTLIL::SigSpec &sig, bool autoint)
Definition: log.cc:269
ez
ezMiniSAT ez
Definition: puzzle3d.cc:31
log_error
void log_error(const char *format,...)
Definition: log.cc:204
RTLIL::SigSpec::size
int size() const
Definition: rtlil.h:1019
ezDefaultSAT
YOSYS_NAMESPACE_BEGIN typedef ezMiniSAT ezDefaultSAT
Definition: satgen.h:32
SatGen
Definition: satgen.h:34
RTLIL::id2cstr
static const char * id2cstr(const RTLIL::IdString &str)
Definition: rtlil.h:267
RTLIL::Module::cells_
std::map< RTLIL::IdString, RTLIL::Cell * > cells_
Definition: rtlil.h:596
log
void log(const char *format,...)
Definition: log.cc:180
RTLIL::State
State
Definition: rtlil.h:29

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

std::vector<std::string> VlogHammerReporter::split ( std::string  text,
const char *  delim 
)
inline

Definition at line 129 of file eval.cc.

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  }
free
void free(void *)
NULL
#define NULL
Definition: NumberlikeArray.hh:6

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

Field Documentation

RTLIL::Design* VlogHammerReporter::design

Definition at line 121 of file eval.cc.

std::vector<int> VlogHammerReporter::input_widths

Definition at line 125 of file eval.cc.

std::vector<RTLIL::IdString> VlogHammerReporter::inputs

Definition at line 124 of file eval.cc.

std::vector<std::string> VlogHammerReporter::module_names

Definition at line 123 of file eval.cc.

std::vector<RTLIL::Module*> VlogHammerReporter::modules

Definition at line 122 of file eval.cc.

std::vector<RTLIL::Const> VlogHammerReporter::patterns

Definition at line 126 of file eval.cc.

int VlogHammerReporter::total_input_width

Definition at line 127 of file eval.cc.

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