64 if (!ce1.eval(sig1, undef1))
65 log(
"Failed ConstEval of module 1 outputs at signal %s (input: %s = %s).\n",
67 if (!ce2.
eval(sig2, undef2))
68 log(
"Failed ConstEval of module 2 outputs at signal %s (input: %s = %s).\n",
72 for (
int i = 0; i <
GetSize(sig1); i++)
78 log(
"Found counter-example (ignore_x_mod1 = %s):\n",
ignore_x_mod1 ?
"active" :
"inactive");
88 mod1(mod1), mod2(mod2),
counter(0),
errors(0), ignore_x_mod1(ignore_x_mod1)
91 for (
auto &w : mod1->
wires_)
129 std::vector<std::string>
split(std::string text,
const char *delim)
131 std::vector<std::string> list;
132 char *p = strdup(text.c_str());
133 char *t = strtok(p, delim);
136 t = strtok(
NULL, delim);
144 log(
"Verifying SAT model (%s)..\n", model_undef ?
"with undef" :
"without undef");
148 SatGen satgen(&ez, &sigmap);
151 for (
auto &c : module->
cells_)
155 ez.assume(satgen.
signals_eq(recorded_set_vars, recorded_set_vals));
158 std::vector<bool> y_values;
162 y_vec.insert(y_vec.end(), y_undef_vec.begin(), y_undef_vec.end());
165 log(
" Created SAT problem with %d variables and %d clauses.\n",
166 ez.numCnfVariables(), ez.numCnfClauses());
168 if (!ez.solve(y_vec, y_values))
169 log_error(
"Failed to find solution to SAT problem.\n");
171 for (
int i = 0; i < expected_y.
size(); i++) {
175 if (y_values.at(expected_y.
size()+i))
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))
187 sat_bits += y_values.at(k) ?
"1" :
"0";
190 log_error(
"Found error in SAT model: y[%d] = %s, should be %s:\n SAT: %s\n RTL: %s\n %*s^\n",
192 sat_bits.c_str(), rtl_bits.c_str(), expected_y.
size()-i-1,
"");
198 std::vector<int> cmp_vars;
199 std::vector<bool> cmp_vals;
201 std::vector<bool> y_undef(y_values.begin() + expected_y.
size(), y_values.end());
203 for (
int i = 0; i < expected_y.
size(); i++)
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");
210 cmp_vars.push_back(y_vec.at(expected_y.
size() + i));
211 cmp_vals.push_back(
true);
215 cmp_vars.push_back(y_vec.at(i));
216 cmp_vals.push_back(y_values.at(i));
218 cmp_vars.push_back(y_vec.at(expected_y.
size() + i));
219 cmp_vals.push_back(
false);
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");
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");
235 log(
" SAT model verified.\n");
243 std::string input_pattern_list;
246 for (
int mod = 0; mod < int(
modules.size()); mod++)
255 for (
int i = 0; i < int(
inputs.size()); i++) {
260 recorded_set_vals.
bits.push_back(bits.back());
263 if (module ==
modules.front()) {
272 if (module->
wires_.count(
"\\y") == 0)
278 while (!ce.
eval(sig, undef)) {
284 log(
"++VAL++ %d %s %s #\n", idx, module_name.c_str(), sig.as_const().as_string().c_str());
286 if (module_name ==
"rtl") {
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())
293 for (
int i = 0; i <
GetSize(sig); i++)
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());
301 log(
"++RPT++ ----\n");
308 for (
auto name :
split(module_list,
",")) {
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());
318 for (
auto name :
split(input_list,
",")) {
322 if (mod->wires_.count(esc_name) == 0)
327 if (width >= 0 && width != port->
width)
328 log_error(
"Port %s has different sizes in the different modules!\n", name.c_str());
331 log(
"Using input port %s with width %d.\n", esc_name.
c_str(), width);
332 inputs.push_back(esc_name);
337 for (
auto pattern :
split(pattern_list,
",")) {
339 bool invert_pattern =
false;
340 if (pattern.size() > 0 && pattern[0] ==
'~') {
341 invert_pattern =
true;
342 pattern = pattern.substr(1);
345 log_error(
"Failed to parse pattern %s!\n", pattern.c_str());
347 log_error(
"Pattern %s is to short!\n", pattern.c_str());
349 if (invert_pattern) {
350 for (
auto &bit :
patterns.back().bits)
356 log(
"Using pattern %s.\n",
patterns.back().as_string().c_str());
367 log(
" eval [options] [selection]\n");
369 log(
"This command evaluates the value of a signal given the value of all required\n");
372 log(
" -set <signal> <value>\n");
373 log(
" set the specified signal to the specified value.\n");
375 log(
" -set-undef\n");
376 log(
" set all unspecified source signals to undef (x)\n");
378 log(
" -table <signal>\n");
379 log(
" create a truth table using the specified input signals\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");
388 std::vector<std::pair<std::string, std::string>> sets;
389 std::vector<std::string> shows, tables;
390 bool set_undef =
false;
392 log_header(
"Executing EVAL pass (evaluate the circuit given an input).\n");
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));
402 if (args[argidx] ==
"-set-undef") {
406 if (args[argidx] ==
"-show" && argidx+1 < args.size()) {
407 shows.push_back(args[++argidx]);
410 if (args[argidx] ==
"-table" && argidx+1 < args.size()) {
411 tables.push_back(args[++argidx]);
414 if ((args[argidx] ==
"-brute_force_equiv_checker" || args[argidx] ==
"-brute_force_equiv_checker_x") && argidx+3 == args.size()) {
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());
423 if (checker.errors > 0)
425 log(
"Verified %s = %s (using brute-force check on %d cases).\n",
426 mod1_name.c_str(), mod2_name.c_str(), checker.counter);
429 if (args[argidx] ==
"-vloghammer_report" && argidx+5 == args.size()) {
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);
444 for (
auto &mod_it : design->
modules_)
445 if (design->
selected(mod_it.second)) {
447 log_cmd_error(
"Only one module must be selected for the EVAL pass! (selected: %s and %s)\n",
449 module = mod_it.second;
452 log_cmd_error(
"Can't perform EVAL on an empty selection!\n");
456 for (
auto &it : sets) {
459 log_cmd_error(
"Failed to parse lhs set expression `%s'.\n", it.first.c_str());
461 log_cmd_error(
"Failed to parse rhs set expression `%s'.\n", it.second.c_str());
463 log_cmd_error(
"Right-hand-side set expression `%s' is not constant.\n", it.second.c_str());
465 log_cmd_error(
"Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
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());
478 for (
auto &it : shows) {
481 log_cmd_error(
"Failed to parse show expression `%s'.\n", it.c_str());
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));
491 if (!ce.
eval(value, undef))
501 std::vector<std::vector<std::string>> tab;
502 int tab_sep_colidx = 0;
504 for (
auto &it : shows) {
507 log_cmd_error(
"Failed to parse show expression `%s'.\n", it.c_str());
511 for (
auto &it : tables) {
514 log_cmd_error(
"Failed to parse table expression `%s'.\n", it.c_str());
518 std::vector<std::string> tab_line;
519 for (
auto &c : tabsigs.
chunks())
521 tab_sep_colidx = tab_line.size();
522 for (
auto &c : signal.
chunks())
524 tab.push_back(tab_line);
531 ce.
set(tabsigs, tabvals);
535 while (!ce.
eval(value, this_undef)) {
537 log(
"Failed to evaluate signal %s at %s = %s: Missing value for %s.\n",
log_signal(signal),
547 for (
auto &c : tabsigs.
chunks()) {
553 for (
auto &c : signal.
chunks()) {
558 tab.push_back(tab_line);
564 while (tabvals.as_bool());
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()));
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());
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++)
595 if (undef.
size() > 0) {
597 log(
"Assumend undef (x) value for the following singals: %s\n\n",
log_signal(undef));
const char * c_str() const
bool selected(T1 *module) const
void sat_check(RTLIL::Module *module, RTLIL::SigSpec recorded_set_vars, RTLIL::Const recorded_set_vals, RTLIL::SigSpec expected_y, bool model_undef)
std::vector< RTLIL::IdString > inputs
std::string stringf(const char *fmt,...)
void log_warning(const char *format,...)
static bool parse_sel(RTLIL::SigSpec &sig, RTLIL::Design *design, RTLIL::Module *module, std::string str)
void log_header(const char *format,...)
RTLIL::Const as_const() const
std::map< RTLIL::IdString, RTLIL::Wire * > wires_
RTLIL::SigSpec mod1_inputs
const char * log_signal(const RTLIL::SigSpec &sig, bool autoint)
static std::string idx(std::string str)
std::vector< std::string > split(std::string text, const char *delim)
bool eval(RTLIL::Cell *cell, RTLIL::SigSpec &undef)
std::vector< std::string > module_names
void log_error(const char *format,...)
virtual void execute(std::vector< std::string > args, RTLIL::Design *design)
void run_checker(RTLIL::SigSpec &inputs)
std::vector< int > importUndefSigSpec(RTLIL::SigSpec sig, int timestep=-1)
static std::string escape_id(std::string str)
YOSYS_NAMESPACE_BEGIN typedef ezMiniSAT ezDefaultSAT
std::vector< int > importDefSigSpec(RTLIL::SigSpec sig, int timestep=-1)
std::string as_string() const
VlogHammerReporter(RTLIL::Design *design, std::string module_prefix, std::string module_list, std::string input_list, std::string pattern_list)
#define PRIVATE_NAMESPACE_BEGIN
int GetSize(RTLIL::Wire *wire)
bool is_fully_const() const
std::vector< RTLIL::Module * > modules
#define PRIVATE_NAMESPACE_END
static const char * id2cstr(const RTLIL::IdString &str)
void log_cmd_error(const char *format,...)
RTLIL::SigSpec mod2_inputs
RTLIL::SigSpec mod1_outputs
std::vector< int > input_widths
#define USING_YOSYS_NAMESPACE
std::map< RTLIL::IdString, RTLIL::Module * > modules_
std::map< RTLIL::IdString, RTLIL::Cell * > cells_
void log(const char *format,...)
bool importCell(RTLIL::Cell *cell, int timestep=-1)
RTLIL::SigSpec extract(const RTLIL::SigSpec &pattern, const RTLIL::SigSpec *other=NULL) const
std::vector< RTLIL::State > bits
void append(const RTLIL::SigSpec &signal)
RTLIL::Const const_add(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
static bool parse_rhs(const RTLIL::SigSpec &lhs, RTLIL::SigSpec &sig, RTLIL::Module *module, std::string str)
BruteForceEquivChecker(RTLIL::Module *mod1, RTLIL::Module *mod2, bool ignore_x_mod1)
void extra_args(std::vector< std::string > args, size_t argidx, RTLIL::Design *design, bool select=true)
void set(RTLIL::SigSpec sig, RTLIL::Const value)
RTLIL::SigSpec mod2_outputs
static bool parse(RTLIL::SigSpec &sig, RTLIL::Module *module, std::string str)
std::vector< RTLIL::Const > patterns
int signals_eq(RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep_lhs=-1, int timestep_rhs=-1)
const std::vector< RTLIL::SigChunk > & chunks() const