yosys-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
BruteForceEquivChecker Struct Reference
+ Collaboration diagram for BruteForceEquivChecker:

Public Member Functions

void run_checker (RTLIL::SigSpec &inputs)
 
 BruteForceEquivChecker (RTLIL::Module *mod1, RTLIL::Module *mod2, bool ignore_x_mod1)
 

Data Fields

RTLIL::Modulemod1
 
RTLIL::Modulemod2
 
RTLIL::SigSpec mod1_inputs
 
RTLIL::SigSpec mod1_outputs
 
RTLIL::SigSpec mod2_inputs
 
RTLIL::SigSpec mod2_outputs
 
int counter
 
int errors
 
bool ignore_x_mod1
 

Detailed Description

Definition at line 38 of file eval.cc.

Constructor & Destructor Documentation

BruteForceEquivChecker::BruteForceEquivChecker ( RTLIL::Module mod1,
RTLIL::Module mod2,
bool  ignore_x_mod1 
)
inline

Definition at line 87 of file eval.cc.

87  :
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  }
const char * c_str() const
Definition: rtlil.h:178
std::map< RTLIL::IdString, RTLIL::Wire * > wires_
Definition: rtlil.h:595
RTLIL::SigSpec mod1_inputs
Definition: eval.cc:41
RTLIL::Module * mod1
Definition: eval.cc:40
bool port_input
Definition: rtlil.h:827
int width
Definition: rtlil.h:826
int port_id
Definition: rtlil.h:826
void run_checker(RTLIL::SigSpec &inputs)
Definition: eval.cc:46
bool port_output
Definition: rtlil.h:827
RTLIL::IdString name
Definition: rtlil.h:599
RTLIL::IdString name
Definition: rtlil.h:825
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
void log(const char *format,...)
Definition: log.cc:180
void append(const RTLIL::SigSpec &signal)
Definition: rtlil.cc:2523
RTLIL::Module * mod2
Definition: eval.cc:40
RTLIL::SigSpec mod2_outputs
Definition: eval.cc:42

+ Here is the call graph for this function:

Member Function Documentation

void BruteForceEquivChecker::run_checker ( RTLIL::SigSpec inputs)
inline

Definition at line 46 of file eval.cc.

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  }
RTLIL::Const as_const() const
Definition: rtlil.cc:2857
RTLIL::SigSpec mod1_inputs
Definition: eval.cc:41
const char * log_signal(const RTLIL::SigSpec &sig, bool autoint)
Definition: log.cc:269
RTLIL::Module * mod1
Definition: eval.cc:40
int size() const
Definition: rtlil.h:1019
void run_checker(RTLIL::SigSpec &inputs)
Definition: eval.cc:46
int GetSize(RTLIL::Wire *wire)
Definition: yosys.cc:334
RTLIL::SigSpec mod2_inputs
Definition: eval.cc:42
RTLIL::SigSpec mod1_outputs
Definition: eval.cc:41
void log(const char *format,...)
Definition: log.cc:180
void append(const RTLIL::SigSpec &signal)
Definition: rtlil.cc:2523
RTLIL::Module * mod2
Definition: eval.cc:40
RTLIL::SigSpec mod2_outputs
Definition: eval.cc:42

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

Field Documentation

int BruteForceEquivChecker::counter

Definition at line 43 of file eval.cc.

int BruteForceEquivChecker::errors

Definition at line 43 of file eval.cc.

bool BruteForceEquivChecker::ignore_x_mod1

Definition at line 44 of file eval.cc.

RTLIL::Module* BruteForceEquivChecker::mod1

Definition at line 40 of file eval.cc.

RTLIL::SigSpec BruteForceEquivChecker::mod1_inputs

Definition at line 41 of file eval.cc.

RTLIL::SigSpec BruteForceEquivChecker::mod1_outputs

Definition at line 41 of file eval.cc.

RTLIL::Module * BruteForceEquivChecker::mod2

Definition at line 40 of file eval.cc.

RTLIL::SigSpec BruteForceEquivChecker::mod2_inputs

Definition at line 42 of file eval.cc.

RTLIL::SigSpec BruteForceEquivChecker::mod2_outputs

Definition at line 42 of file eval.cc.


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