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

Public Member Functions

 FindReducedInputs (SigMap &sigmap, drivers_t &drivers)
 
int get_bits (int val)
 
void register_pi_bit (RTLIL::SigBit bit)
 
void register_cone_worker (std::set< RTLIL::SigBit > &pi, std::set< RTLIL::SigBit > &sigdone, RTLIL::SigBit out)
 
void register_cone (std::vector< RTLIL::SigBit > &pi, RTLIL::SigBit out)
 
void analyze (std::vector< RTLIL::SigBit > &reduced_inputs, RTLIL::SigBit output, int prec)
 

Data Fields

SigMap & sigmap
 
drivers_t & drivers
 
ezDefaultSAT ez
 
std::set< RTLIL::Cell * > ez_cells
 
SatGen satgen
 
std::map< RTLIL::SigBit, int > sat_pi
 
std::vector< int > sat_pi_uniq_bitvec
 

Detailed Description

Definition at line 71 of file freduce.cc.

Constructor & Destructor Documentation

FindReducedInputs::FindReducedInputs ( SigMap &  sigmap,
drivers_t &  drivers 
)
inline

Definition at line 83 of file freduce.cc.

83  :
84  sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap)
85  {
86  satgen.model_undef = true;
87  }
FindReducedInputs::ez
ezDefaultSAT ez
Definition: freduce.cc:76
SatGen::model_undef
bool model_undef
Definition: satgen.h:43
FindReducedInputs::drivers
drivers_t & drivers
Definition: freduce.cc:74
FindReducedInputs::sigmap
SigMap & sigmap
Definition: freduce.cc:73

Member Function Documentation

void FindReducedInputs::analyze ( std::vector< RTLIL::SigBit > &  reduced_inputs,
RTLIL::SigBit  output,
int  prec 
)
inline

Definition at line 168 of file freduce.cc.

169  {
170  if (verbose_level >= 1)
171  log("[%2d%%] Analyzing input cone for signal %s:\n", prec, log_signal(output));
172 
173  std::vector<RTLIL::SigBit> pi;
174  register_cone(pi, output);
175 
176  if (verbose_level >= 1)
177  log(" Found %d input signals and %d cells.\n", int(pi.size()), int(ez_cells.size()));
178 
179  satgen.setContext(&sigmap, "A");
180  int output_a = satgen.importSigSpec(output).front();
181  int output_undef_a = satgen.importUndefSigSpec(output).front();
182 
183  satgen.setContext(&sigmap, "B");
184  int output_b = satgen.importSigSpec(output).front();
185  int output_undef_b = satgen.importUndefSigSpec(output).front();
186 
187  std::set<int> unused_pi_idx;
188 
189  for (size_t i = 0; i < pi.size(); i++)
190  unused_pi_idx.insert(i);
191 
192  while (1)
193  {
194  std::vector<int> model_pi_idx;
195  std::vector<int> model_expr;
196  std::vector<bool> model;
197 
198  for (size_t i = 0; i < pi.size(); i++)
199  if (unused_pi_idx.count(i) != 0) {
200  model_pi_idx.push_back(i);
201  model_expr.push_back(sat_pi.at(pi[i]));
202  }
203 
204  if (!ez.solve(model_expr, model, ez.expression(ezSAT::OpOr, model_expr), ez.XOR(output_a, output_b), ez.NOT(output_undef_a), ez.NOT(output_undef_b)))
205  break;
206 
207  int found_count = 0;
208  for (size_t i = 0; i < model_pi_idx.size(); i++)
209  if (model[i]) {
210  if (verbose_level >= 2)
211  log(" Found relevant input: %s\n", log_signal(pi[model_pi_idx[i]]));
212  unused_pi_idx.erase(model_pi_idx[i]);
213  found_count++;
214  }
215  log_assert(found_count == 1);
216  }
217 
218  for (size_t i = 0; i < pi.size(); i++)
219  if (unused_pi_idx.count(i) == 0)
220  reduced_inputs.push_back(pi[i]);
221 
222  if (verbose_level >= 1)
223  log(" Reduced input cone contains %d inputs.\n", int(reduced_inputs.size()));
224  }
FindReducedInputs::ez
ezDefaultSAT ez
Definition: freduce.cc:76
log_signal
const char * log_signal(const RTLIL::SigSpec &sig, bool autoint)
Definition: log.cc:269
SatGen::importSigSpec
std::vector< int > importSigSpec(RTLIL::SigSpec sig, int timestep=-1)
Definition: satgen.h:78
FindReducedInputs::ez_cells
std::set< RTLIL::Cell * > ez_cells
Definition: freduce.cc:77
SatGen::importUndefSigSpec
std::vector< int > importUndefSigSpec(RTLIL::SigSpec sig, int timestep=-1)
Definition: satgen.h:92
FindReducedInputs::register_cone
void register_cone(std::vector< RTLIL::SigBit > &pi, RTLIL::SigBit out)
Definition: freduce.cc:160
log_assert
#define log_assert(_assert_expr_)
Definition: log.h:85
verbose_level
int verbose_level
Definition: freduce.cc:35
SatGen::setContext
void setContext(SigMap *sigmap, std::string prefix=std::string())
Definition: satgen.h:50
FindReducedInputs::sat_pi
std::map< RTLIL::SigBit, int > sat_pi
Definition: freduce.cc:80
log
void log(const char *format,...)
Definition: log.cc:180
FindReducedInputs::sigmap
SigMap & sigmap
Definition: freduce.cc:73

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

int FindReducedInputs::get_bits ( int  val)
inline

Definition at line 89 of file freduce.cc.

90  {
91  int bits = 0;
92  for (int i = 8*sizeof(int); val; i = i >> 1)
93  if (val >> (i-1)) {
94  bits += i;
95  val = val >> i;
96  }
97  return bits;
98  }

+ Here is the caller graph for this function:

void FindReducedInputs::register_cone ( std::vector< RTLIL::SigBit > &  pi,
RTLIL::SigBit  out 
)
inline

Definition at line 160 of file freduce.cc.

161  {
162  std::set<RTLIL::SigBit> pi_set, sigdone;
163  register_cone_worker(pi_set, sigdone, out);
164  pi.clear();
165  pi.insert(pi.end(), pi_set.begin(), pi_set.end());
166  }
FindReducedInputs::register_cone_worker
void register_cone_worker(std::set< RTLIL::SigBit > &pi, std::set< RTLIL::SigBit > &sigdone, RTLIL::SigBit out)
Definition: freduce.cc:133

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

void FindReducedInputs::register_cone_worker ( std::set< RTLIL::SigBit > &  pi,
std::set< RTLIL::SigBit > &  sigdone,
RTLIL::SigBit  out 
)
inline

Definition at line 133 of file freduce.cc.

134  {
135  if (out.wire == NULL)
136  return;
137  if (sigdone.count(out) != 0)
138  return;
139  sigdone.insert(out);
140 
141  if (drivers.count(out) != 0) {
142  std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> &drv = drivers.at(out);
143  if (ez_cells.count(drv.first) == 0) {
144  satgen.setContext(&sigmap, "A");
145  if (!satgen.importCell(drv.first))
146  log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(drv.first->name), RTLIL::id2cstr(drv.first->type));
147  satgen.setContext(&sigmap, "B");
148  if (!satgen.importCell(drv.first))
149  log_abort();
150  ez_cells.insert(drv.first);
151  }
152  for (auto &bit : drv.second)
153  register_cone_worker(pi, sigdone, bit);
154  } else {
155  register_pi_bit(out);
156  pi.insert(out);
157  }
158  }
RTLIL::SigBit::wire
RTLIL::Wire * wire
Definition: rtlil.h:907
log_error
void log_error(const char *format,...)
Definition: log.cc:204
log_abort
#define log_abort()
Definition: log.h:84
FindReducedInputs::drivers
drivers_t & drivers
Definition: freduce.cc:74
FindReducedInputs::ez_cells
std::set< RTLIL::Cell * > ez_cells
Definition: freduce.cc:77
FindReducedInputs::register_pi_bit
void register_pi_bit(RTLIL::SigBit bit)
Definition: freduce.cc:100
SatGen::setContext
void setContext(SigMap *sigmap, std::string prefix=std::string())
Definition: satgen.h:50
RTLIL::id2cstr
static const char * id2cstr(const RTLIL::IdString &str)
Definition: rtlil.h:267
NULL
#define NULL
Definition: NumberlikeArray.hh:6
SatGen::importCell
bool importCell(RTLIL::Cell *cell, int timestep=-1)
Definition: satgen.h:203
FindReducedInputs::sigmap
SigMap & sigmap
Definition: freduce.cc:73
FindReducedInputs::register_cone_worker
void register_cone_worker(std::set< RTLIL::SigBit > &pi, std::set< RTLIL::SigBit > &sigdone, RTLIL::SigBit out)
Definition: freduce.cc:133

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

void FindReducedInputs::register_pi_bit ( RTLIL::SigBit  bit)
inline

Definition at line 100 of file freduce.cc.

101  {
102  if (sat_pi.count(bit) != 0)
103  return;
104 
105  satgen.setContext(&sigmap, "A");
106  int sat_a = satgen.importSigSpec(bit).front();
107  ez.assume(ez.NOT(satgen.importUndefSigSpec(bit).front()));
108 
109  satgen.setContext(&sigmap, "B");
110  int sat_b = satgen.importSigSpec(bit).front();
111  ez.assume(ez.NOT(satgen.importUndefSigSpec(bit).front()));
112 
113  int idx = sat_pi.size();
114  size_t idx_bits = get_bits(idx);
115 
116  if (sat_pi_uniq_bitvec.size() != idx_bits) {
117  sat_pi_uniq_bitvec.push_back(ez.frozen_literal(stringf("uniq_%d", int(idx_bits)-1)));
118  for (auto &it : sat_pi)
119  ez.assume(ez.OR(ez.NOT(it.second), ez.NOT(sat_pi_uniq_bitvec.back())));
120  }
121  log_assert(sat_pi_uniq_bitvec.size() == idx_bits);
122 
123  sat_pi[bit] = ez.frozen_literal(stringf("p, falsei_%s", log_signal(bit)));
124  ez.assume(ez.IFF(ez.XOR(sat_a, sat_b), sat_pi[bit]));
125 
126  for (size_t i = 0; i < idx_bits; i++)
127  if ((idx & (1 << i)) == 0)
128  ez.assume(ez.OR(ez.NOT(sat_pi[bit]), ez.NOT(sat_pi_uniq_bitvec[i])));
129  else
130  ez.assume(ez.OR(ez.NOT(sat_pi[bit]), sat_pi_uniq_bitvec[i]));
131  }
FindReducedInputs::ez
ezDefaultSAT ez
Definition: freduce.cc:76
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
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
SatGen::importSigSpec
std::vector< int > importSigSpec(RTLIL::SigSpec sig, int timestep=-1)
Definition: satgen.h:78
FindReducedInputs::get_bits
int get_bits(int val)
Definition: freduce.cc:89
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
SatGen::setContext
void setContext(SigMap *sigmap, std::string prefix=std::string())
Definition: satgen.h:50
FindReducedInputs::sat_pi
std::map< RTLIL::SigBit, int > sat_pi
Definition: freduce.cc:80
FindReducedInputs::sat_pi_uniq_bitvec
std::vector< int > sat_pi_uniq_bitvec
Definition: freduce.cc:81
FindReducedInputs::sigmap
SigMap & sigmap
Definition: freduce.cc:73

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

Field Documentation

drivers_t& FindReducedInputs::drivers

Definition at line 74 of file freduce.cc.

ezDefaultSAT FindReducedInputs::ez

Definition at line 76 of file freduce.cc.

std::set<RTLIL::Cell*> FindReducedInputs::ez_cells

Definition at line 77 of file freduce.cc.

std::map<RTLIL::SigBit, int> FindReducedInputs::sat_pi

Definition at line 80 of file freduce.cc.

std::vector<int> FindReducedInputs::sat_pi_uniq_bitvec

Definition at line 81 of file freduce.cc.

SatGen FindReducedInputs::satgen

Definition at line 78 of file freduce.cc.

SigMap& FindReducedInputs::sigmap

Definition at line 73 of file freduce.cc.

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