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

Public Member Functions

 BtorDumper (std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, BtorDumperConfig *config)
 
const char * cstr (const RTLIL::IdString id)
 
int dump_wire (RTLIL::Wire *wire)
 
int dump_memory (const RTLIL::Memory *memory)
 
int dump_const (const RTLIL::Const *data, int width, int offset)
 
int dump_sigchunk (const RTLIL::SigChunk *chunk)
 
int dump_sigspec (const RTLIL::SigSpec *sig, int expected_width)
 
int dump_cell (const RTLIL::Cell *cell)
 
const RTLIL::SigSpec * get_cell_output (RTLIL::Cell *cell)
 
void dump_property (RTLIL::Wire *wire)
 
void dump ()
 

Static Public Member Functions

static void dump (std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, BtorDumperConfig &config)
 

Data Fields

std::ostream & f
 
RTLIL::Module * module
 
RTLIL::Design * design
 
BtorDumperConfig * config
 
CellTypes ct
 
SigMap sigmap
 
std::map< RTLIL::IdString,
std::set< WireInfo,
WireInfoOrder > > 		inter_wire_map
 
std::map< RTLIL::IdString, int > line_ref
 
std::map< RTLIL::SigSpec, int > sig_ref
 
int line_num
 
std::string str
 
std::map< RTLIL::IdString, bool > basic_wires
 
RTLIL::IdString curr_cell
 
std::map< std::string,
std::string > 		cell_type_translation
 
std::map< std::string,
std::string > 		s_cell_type_translation
 
std::set< int > mem_next
 
std::vector< std::string > cstr_buf
 

Detailed Description

Definition at line 64 of file btor.cc.

Constructor & Destructor Documentation

BtorDumper::BtorDumper ( std::ostream &  f,
RTLIL::Module *  module,
RTLIL::Design *  design,
BtorDumperConfig *  config 
)
inline

Definition at line 82 of file btor.cc.

82  :
83  f(f), module(module), design(design), config(config), ct(design), sigmap(module)
84  {
85  line_num=0;
86  str.clear();
87  for(auto it=module->wires_.begin(); it!=module->wires_.end(); ++it)
88  {
89  if(it->second->port_input)
90  {
91  basic_wires[it->first]=true;
92  }
93  else
94  {
95  basic_wires[it->first]=false;
96  }
97  inter_wire_map[it->first].clear();
98  }
99  curr_cell.clear();
100  //assert
101  cell_type_translation["$assert"] = "root";
102  //unary
103  cell_type_translation["$not"] = "not";
104  cell_type_translation["$neg"] = "neg";
105  cell_type_translation["$reduce_and"] = "redand";
106  cell_type_translation["$reduce_or"] = "redor";
107  cell_type_translation["$reduce_xor"] = "redxor";
108  cell_type_translation["$reduce_bool"] = "redor";
109  //binary
110  cell_type_translation["$and"] = "and";
111  cell_type_translation["$or"] = "or";
112  cell_type_translation["$xor"] = "xor";
113  cell_type_translation["$xnor"] = "xnor";
114  cell_type_translation["$shr"] = "srl";
115  cell_type_translation["$shl"] = "sll";
116  cell_type_translation["$sshr"] = "sra";
117  cell_type_translation["$sshl"] = "sll";
118  cell_type_translation["$shift"] = "srl";
119  cell_type_translation["$shiftx"] = "srl";
120  cell_type_translation["$lt"] = "ult";
121  cell_type_translation["$le"] = "ulte";
122  cell_type_translation["$gt"] = "ugt";
123  cell_type_translation["$ge"] = "ugte";
124  cell_type_translation["$eq"] = "eq";
125  cell_type_translation["$eqx"] = "eq";
126  cell_type_translation["$ne"] = "ne";
127  cell_type_translation["$nex"] = "ne";
128  cell_type_translation["$add"] = "add";
129  cell_type_translation["$sub"] = "sub";
130  cell_type_translation["$mul"] = "mul";
131  cell_type_translation["$mod"] = "urem";
132  cell_type_translation["$div"] = "udiv";
133  //mux
134  cell_type_translation["$mux"] = "cond";
135  //reg
136  cell_type_translation["$dff"] = "next";
137  cell_type_translation["$adff"] = "next";
138  cell_type_translation["$dffsr"] = "next";
139  //memories
140  //nothing here
141  //slice
142  cell_type_translation["$slice"] = "slice";
143  //concat
144  cell_type_translation["$concat"] = "concat";
145 
146  //signed cell type translation
147  //binary
148  s_cell_type_translation["$modx"] = "srem";
149  s_cell_type_translation["$mody"] = "smod";
150  s_cell_type_translation["$div"] = "sdiv";
151  s_cell_type_translation["$lt"] = "slt";
152  s_cell_type_translation["$le"] = "slte";
153  s_cell_type_translation["$gt"] = "sgt";
154  s_cell_type_translation["$ge"] = "sgte";
155 
156  }
RTLIL::IdString::clear
void clear()
Definition: rtlil.h:223
RTLIL::Module::wires_
std::map< RTLIL::IdString, RTLIL::Wire * > wires_
Definition: rtlil.h:595
BtorDumper::ct
CellTypes ct
Definition: btor.cc:70
BtorDumper::cell_type_translation
std::map< std::string, std::string > cell_type_translation
Definition: btor.cc:80
BtorDumper::config
BtorDumperConfig * config
Definition: btor.cc:69
BtorDumper::curr_cell
RTLIL::IdString curr_cell
Definition: btor.cc:79
BtorDumper::inter_wire_map
std::map< RTLIL::IdString, std::set< WireInfo, WireInfoOrder > > inter_wire_map
Definition: btor.cc:73
BtorDumper::str
std::string str
Definition: btor.cc:77
BtorDumper::f
std::ostream & f
Definition: btor.cc:66
BtorDumper::sigmap
SigMap sigmap
Definition: btor.cc:72
BtorDumper::basic_wires
std::map< RTLIL::IdString, bool > basic_wires
Definition: btor.cc:78
BtorDumper::s_cell_type_translation
std::map< std::string, std::string > s_cell_type_translation
Definition: btor.cc:80
BtorDumper::module
RTLIL::Module * module
Definition: btor.cc:67
BtorDumper::line_num
int line_num
Definition: btor.cc:76
BtorDumper::design
RTLIL::Design * design
Definition: btor.cc:68

+ Here is the call graph for this function:

Member Function Documentation

const char* BtorDumper::cstr ( const RTLIL::IdString  id)
inline

Definition at line 160 of file btor.cc.

161  {
162  str = RTLIL::unescape_id(id);
163  for (size_t i = 0; i < str.size(); ++i)
164  if (str[i] == '#' || str[i] == '=')
165  str[i] = '?';
166  cstr_buf.push_back(str);
167  return cstr_buf.back().c_str();
168  }
BtorDumper::cstr_buf
std::vector< std::string > cstr_buf
Definition: btor.cc:158
RTLIL::unescape_id
static std::string unescape_id(std::string str)
Definition: rtlil.h:257
BtorDumper::str
std::string str
Definition: btor.cc:77

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

void BtorDumper::dump ( )
inline

Definition at line 888 of file btor.cc.

889  {
890  f << stringf(";module %s\n", cstr(module->name));
891 
892  log("creating intermediate wires map\n");
893  //creating map of intermediate wires as output of some cell
894  for (auto it = module->cells_.begin(); it != module->cells_.end(); ++it)
895  {
896  RTLIL::Cell *cell = it->second;
897  const RTLIL::SigSpec* output_sig = get_cell_output(cell);
898  if(output_sig==nullptr)
899  continue;
900  RTLIL::SigSpec s = sigmap(*output_sig);
901  output_sig = &s;
902  log(" - %s\n", cstr(it->second->type));
903  if (cell->type == "$memrd")
904  {
905  for(unsigned i=0; i<output_sig->chunks().size(); ++i)
906  {
907  RTLIL::Wire *w = output_sig->chunks().at(i).wire;
908  RTLIL::IdString wire_id = w->name;
909  inter_wire_map[wire_id].insert(WireInfo(cell->name,&output_sig->chunks().at(i)));
910  }
911  }
912  else if(cell->type == "$memwr")
913  {
914  continue;//nothing to do
915  }
916  else if(cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffsr")
917  {
918  RTLIL::IdString wire_id = output_sig->chunks().front().wire->name;
919  for(unsigned i=0; i<output_sig->chunks().size(); ++i)
920  {
921  RTLIL::Wire *w = output_sig->chunks().at(i).wire;
922  RTLIL::IdString wire_id = w->name;
923  inter_wire_map[wire_id].insert(WireInfo(cell->name,&output_sig->chunks().at(i)));
924  basic_wires[wire_id] = true;
925  }
926  }
927  else
928  {
929  for(unsigned i=0; i<output_sig->chunks().size(); ++i)
930  {
931  RTLIL::Wire *w = output_sig->chunks().at(i).wire;
932  RTLIL::IdString wire_id = w->name;
933  inter_wire_map[wire_id].insert(WireInfo(cell->name,&output_sig->chunks().at(i)));
934  }
935  }
936  }
937 
938  log("writing input\n");
939  std::map<int, RTLIL::Wire*> inputs, outputs;
940  std::vector<RTLIL::Wire*> safety;
941 
942  for (auto &wire_it : module->wires_) {
943  RTLIL::Wire *wire = wire_it.second;
944  if (wire->port_input)
945  inputs[wire->port_id] = wire;
946  if (wire->port_output) {
947  outputs[wire->port_id] = wire;
948  if (wire->name.str().find("safety") != std::string::npos )
949  safety.push_back(wire);
950  }
951  }
952 
953  f << stringf(";inputs\n");
954  for (auto &it : inputs) {
955  RTLIL::Wire *wire = it.second;
956  dump_wire(wire);
957  }
958  f << stringf("\n");
959 
960  log("writing memories\n");
961  for(auto mem_it = module->memories.begin(); mem_it != module->memories.end(); ++mem_it)
962  {
963  dump_memory(mem_it->second);
964  }
965 
966  log("writing output wires\n");
967  for (auto &it : outputs) {
968  RTLIL::Wire *wire = it.second;
969  dump_wire(wire);
970  }
971 
972  log("writing cells\n");
973  for(auto cell_it = module->cells_.begin(); cell_it != module->cells_.end(); ++cell_it)
974  {
975  dump_cell(cell_it->second);
976  }
977 
978  for(auto it: safety)
979  dump_property(it);
980 
981  f << stringf("\n");
982 
983  log("writing outputs info\n");
984  f << stringf(";outputs\n");
985  for (auto &it : outputs) {
986  RTLIL::Wire *wire = it.second;
987  int l = dump_wire(wire);
988  f << stringf(";%d %s", l, cstr(wire->name));
989  }
990  f << stringf("\n");
991  }
RTLIL::IdString::str
std::string str() const
Definition: rtlil.h:182
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
WireInfo
Definition: btor.cc:48
RTLIL::Module::wires_
std::map< RTLIL::IdString, RTLIL::Wire * > wires_
Definition: rtlil.h:595
RTLIL::Cell::name
RTLIL::IdString name
Definition: rtlil.h:853
RTLIL::Wire::port_input
bool port_input
Definition: rtlil.h:827
RTLIL::Module::memories
std::map< RTLIL::IdString, RTLIL::Memory * > memories
Definition: rtlil.h:601
BtorDumper::dump_wire
int dump_wire(RTLIL::Wire *wire)
Definition: btor.cc:170
RTLIL::Wire::port_id
int port_id
Definition: rtlil.h:826
RTLIL::Cell::type
RTLIL::IdString type
Definition: rtlil.h:854
BtorDumper::dump_property
void dump_property(RTLIL::Wire *wire)
Definition: btor.cc:880
BtorDumper::cstr
const char * cstr(const RTLIL::IdString id)
Definition: btor.cc:160
RTLIL::Wire::port_output
bool port_output
Definition: rtlil.h:827
BtorDumper::dump_memory
int dump_memory(const RTLIL::Memory *memory)
Definition: btor.cc:256
RTLIL::Module::name
RTLIL::IdString name
Definition: rtlil.h:599
BtorDumper::inter_wire_map
std::map< RTLIL::IdString, std::set< WireInfo, WireInfoOrder > > inter_wire_map
Definition: btor.cc:73
RTLIL::Wire::name
RTLIL::IdString name
Definition: rtlil.h:825
BtorDumper::get_cell_output
const RTLIL::SigSpec * get_cell_output(RTLIL::Cell *cell)
Definition: btor.cc:858
RTLIL::Module::cells_
std::map< RTLIL::IdString, RTLIL::Cell * > cells_
Definition: rtlil.h:596
BtorDumper::f
std::ostream & f
Definition: btor.cc:66
BtorDumper::sigmap
SigMap sigmap
Definition: btor.cc:72
log
void log(const char *format,...)
Definition: log.cc:180
BtorDumper::dump_cell
int dump_cell(const RTLIL::Cell *cell)
Definition: btor.cc:387
BtorDumper::basic_wires
std::map< RTLIL::IdString, bool > basic_wires
Definition: btor.cc:78
BtorDumper::module
RTLIL::Module * module
Definition: btor.cc:67
RTLIL::SigSpec::chunks
const std::vector< RTLIL::SigChunk > & chunks() const
Definition: rtlil.h:1016

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

static void BtorDumper::dump ( std::ostream &  f,
RTLIL::Module *  module,
RTLIL::Design *  design,
BtorDumperConfig &  config 
)
inlinestatic

Definition at line 993 of file btor.cc.

994  {
995  BtorDumper dumper(f, module, design, &config);
996  dumper.dump();
997  }
BtorDumper::f
std::ostream & f
Definition: btor.cc:66

+ Here is the call graph for this function:

int BtorDumper::dump_cell ( const RTLIL::Cell *  cell)
inline

Definition at line 387 of file btor.cc.

388  {
389  auto it = line_ref.find(cell->name);
390  if(it==std::end(line_ref))
391  {
392  curr_cell = cell->name;
393  //assert cell
394  if(cell->type == "$assert")
395  {
396  log("writing assert cell - %s\n", cstr(cell->type));
397  const RTLIL::SigSpec* expr = &cell->getPort(RTLIL::IdString("\\A"));
398  const RTLIL::SigSpec* en = &cell->getPort(RTLIL::IdString("\\EN"));
399  log_assert(expr->size() == 1);
400  log_assert(en->size() == 1);
401  int expr_line = dump_sigspec(expr, 1);
402  int en_line = dump_sigspec(en, 1);
403  int one_line = ++line_num;
404  str = stringf("%d one 1", line_num);
405  f << stringf("%s\n", str.c_str());
406  ++line_num;
407  str = stringf("%d %s %d %d %d", line_num, cell_type_translation.at("$eq").c_str(), 1, en_line, one_line);
408  f << stringf("%s\n", str.c_str());
409  ++line_num;
410  str = stringf("%d %s %d %d %d %d", line_num, cell_type_translation.at("$mux").c_str(), 1, line_num-1,
411  expr_line, one_line);
412  f << stringf("%s\n", str.c_str());
413  int cell_line = ++line_num;
414  str = stringf("%d %s %d %d", line_num, cell_type_translation.at("$assert").c_str(), 1, -1*(line_num-1));
415  //multiplying the line number with -1, which means logical negation
416  //the reason for negative sign is that the properties in btor are given as "negation of the original property"
417  //bug identified by bobosoft
418  //http://www.reddit.com/r/yosys/comments/1w3xig/btor_backend_bug/
419  f << stringf("%s\n", str.c_str());
420  line_ref[cell->name]=cell_line;
421  }
422  //unary cells
423  else if(cell->type == "$not" || cell->type == "$neg" || cell->type == "$pos" || cell->type == "$reduce_and" ||
424  cell->type == "$reduce_or" || cell->type == "$reduce_xor" || cell->type == "$reduce_bool")
425  {
426  log("writing unary cell - %s\n", cstr(cell->type));
427  int w = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
428  int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
429  w = w>output_width ? w:output_width; //padding of w
430  int l = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), w);
431  int cell_line = l;
432  if(cell->type != "$pos")
433  {
434  cell_line = ++line_num;
435  bool reduced = (cell->type == "$not" || cell->type == "$neg") ? false : true;
436  str = stringf ("%d %s %d %d", cell_line, cell_type_translation.at(cell->type.str()).c_str(), reduced?output_width:w, l);
437  f << stringf("%s\n", str.c_str());
438  }
439  if(output_width < w && (cell->type == "$not" || cell->type == "$neg" || cell->type == "$pos"))
440  {
441  ++line_num;
442  str = stringf ("%d slice %d %d %d %d;4", line_num, output_width, cell_line, output_width-1, 0);
443  f << stringf("%s\n", str.c_str());
444  cell_line = line_num;
445  }
446  line_ref[cell->name]=cell_line;
447  }
448  else if(cell->type == "$reduce_xnor" || cell->type == "$logic_not")//no direct translation in btor
449  {
450  log("writing unary cell - %s\n", cstr(cell->type));
451  int w = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
452  int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
453  log_assert(output_width == 1);
454  int l = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), w);
455  if(cell->type == "$logic_not" && w > 1)
456  {
457  ++line_num;
458  str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$reduce_or").c_str(), output_width, l);
459  f << stringf("%s\n", str.c_str());
460  }
461  else if(cell->type == "$reduce_xnor")
462  {
463  ++line_num;
464  str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$reduce_xor").c_str(), output_width, l);
465  f << stringf("%s\n", str.c_str());
466  }
467  ++line_num;
468  str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$not").c_str(), output_width, l);
469  f << stringf("%s\n", str.c_str());
470  line_ref[cell->name]=line_num;
471  }
472  //binary cells
473  else if(cell->type == "$and" || cell->type == "$or" || cell->type == "$xor" || cell->type == "$xnor" ||
474  cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" ||
475  cell->type == "$eqx" || cell->type == "$nex" || cell->type == "$ge" || cell->type == "$gt" )
476  {
477  log("writing binary cell - %s\n", cstr(cell->type));
478  int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
479  log_assert(!(cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex" ||
480  cell->type == "$ge" || cell->type == "$gt") || output_width == 1);
481  bool l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool();
482  bool l2_signed = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool();
483  int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
484  int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
485 
486  log_assert(l1_signed == l2_signed);
487  l1_width = l1_width > output_width ? l1_width : output_width;
488  l1_width = l1_width > l2_width ? l1_width : l2_width;
489  l2_width = l2_width > l1_width ? l2_width : l1_width;
490 
491  int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), l1_width);
492  int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), l2_width);
493 
494  ++line_num;
495  std::string op = cell_type_translation.at(cell->type.str());
496  if(cell->type == "$lt" || cell->type == "$le" ||
497  cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex" ||
498  cell->type == "$ge" || cell->type == "$gt")
499  {
500  if(l1_signed)
501  op = s_cell_type_translation.at(cell->type.str());
502  }
503 
504  str = stringf ("%d %s %d %d %d", line_num, op.c_str(), output_width, l1, l2);
505  f << stringf("%s\n", str.c_str());
506 
507  line_ref[cell->name]=line_num;
508  }
509  else if(cell->type == "$add" || cell->type == "$sub" || cell->type == "$mul" || cell->type == "$div" ||
510  cell->type == "$mod" )
511  {
512  //TODO: division by zero case
513  log("writing binary cell - %s\n", cstr(cell->type));
514  int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
515  bool l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool();
516  bool l2_signed = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool();
517  int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
518  int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
519 
520  log_assert(l1_signed == l2_signed);
521  l1_width = l1_width > output_width ? l1_width : output_width;
522  l1_width = l1_width > l2_width ? l1_width : l2_width;
523  l2_width = l2_width > l1_width ? l2_width : l1_width;
524 
525  int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), l1_width);
526  int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), l2_width);
527 
528  ++line_num;
529  std::string op = cell_type_translation.at(cell->type.str());
530  if(cell->type == "$div" && l1_signed)
531  op = s_cell_type_translation.at(cell->type.str());
532  else if(cell->type == "$mod")
533  {
534  if(l1_signed)
535  op = s_cell_type_translation.at("$modx");
536  else if(l2_signed)
537  op = s_cell_type_translation.at("$mody");
538  }
539  str = stringf ("%d %s %d %d %d", line_num, op.c_str(), l1_width, l1, l2);
540  f << stringf("%s\n", str.c_str());
541 
542  if(output_width < l1_width)
543  {
544  ++line_num;
545  str = stringf ("%d slice %d %d %d %d;5", line_num, output_width, line_num-1, output_width-1, 0);
546  f << stringf("%s\n", str.c_str());
547  }
548  line_ref[cell->name]=line_num;
549  }
550  else if(cell->type == "$shr" || cell->type == "$shl" || cell->type == "$sshr" || cell->type == "$sshl" || cell->type == "$shift" || cell->type == "$shiftx")
551  {
552  log("writing binary cell - %s\n", cstr(cell->type));
553  int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
554  bool l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool();
555  //bool l2_signed = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool();
556  int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
557  l1_width = pow(2, ceil(log(l1_width)/log(2)));
558  int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
559  //log_assert(l2_width <= ceil(log(l1_width)/log(2)) );
560  int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), l1_width);
561  int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), ceil(log(l1_width)/log(2)));
562  int cell_output = ++line_num;
563  str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(), l1_width, l1, l2);
564  f << stringf("%s\n", str.c_str());
565 
566  if(l2_width > ceil(log(l1_width)/log(2)))
567  {
568  int extra_width = l2_width - ceil(log(l1_width)/log(2));
569  l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), l2_width);
570  ++line_num;
571  str = stringf ("%d slice %d %d %d %d;6", line_num, extra_width, l2, l2_width-1, l2_width-extra_width);
572  f << stringf("%s\n", str.c_str());
573  ++line_num;
574  str = stringf ("%d one %d", line_num, extra_width);
575  f << stringf("%s\n", str.c_str());
576  int mux = ++line_num;
577  str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at("$gt").c_str(), 1, line_num-2, line_num-1);
578  f << stringf("%s\n", str.c_str());
579  ++line_num;
580  str = stringf("%d %s %d", line_num, l1_signed && cell->type == "$sshr" ? "ones":"zero", l1_width);
581  f << stringf("%s\n", str.c_str());
582  ++line_num;
583  str = stringf ("%d %s %d %d %d %d", line_num, cell_type_translation.at("$mux").c_str(), l1_width, mux, line_num-1, cell_output);
584  f << stringf("%s\n", str.c_str());
585  cell_output = line_num;
586  }
587 
588  if(output_width < l1_width)
589  {
590  ++line_num;
591  str = stringf ("%d slice %d %d %d %d;5", line_num, output_width, cell_output, output_width-1, 0);
592  f << stringf("%s\n", str.c_str());
593  cell_output = line_num;
594  }
595  line_ref[cell->name] = cell_output;
596  }
597  else if(cell->type == "$logic_and" || cell->type == "$logic_or")//no direct translation in btor
598  {
599  log("writing binary cell - %s\n", cstr(cell->type));
600  int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
601  log_assert(output_width == 1);
602  int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), output_width);
603  int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), output_width);
604  int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
605  int l2_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
606  if(l1_width >1)
607  {
608  ++line_num;
609  str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$reduce_or").c_str(), output_width, l1);
610  f << stringf("%s\n", str.c_str());
611  l1 = line_num;
612  }
613  if(l2_width > 1)
614  {
615  ++line_num;
616  str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$reduce_or").c_str(), output_width, l2);
617  f << stringf("%s\n", str.c_str());
618  l2 = line_num;
619  }
620  if(cell->type == "$logic_and")
621  {
622  ++line_num;
623  str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at("$and").c_str(), output_width, l1, l2);
624  }
625  else if(cell->type == "$logic_or")
626  {
627  ++line_num;
628  str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at("$or").c_str(), output_width, l1, l2);
629  }
630  f << stringf("%s\n", str.c_str());
631  line_ref[cell->name]=line_num;
632  }
633  //multiplexers
634  else if(cell->type == "$mux")
635  {
636  log("writing mux cell\n");
637  int output_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
638  int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), output_width);
639  int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), output_width);
640  int s = dump_sigspec(&cell->getPort(RTLIL::IdString("\\S")), 1);
641  ++line_num;
642  str = stringf ("%d %s %d %d %d %d",
643  line_num, cell_type_translation.at(cell->type.str()).c_str(), output_width, s, l2, l1);
644  //if s is 0 then l1, if s is 1 then l2 //according to the implementation of mux cell
645  f << stringf("%s\n", str.c_str());
646  line_ref[cell->name]=line_num;
647  }
648  else if(cell->type == "$pmux")
649  {
650  log("writing pmux cell\n");
651  int output_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
652  int select_width = cell->parameters.at(RTLIL::IdString("\\S_WIDTH")).as_int();
653  int default_case = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), output_width);
654  int cases = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), output_width*select_width);
655  int select = dump_sigspec(&cell->getPort(RTLIL::IdString("\\S")), select_width);
656  int *c = new int[select_width];
657 
658  for (int i=0; i<select_width; ++i)
659  {
660  ++line_num;
661  str = stringf ("%d slice 1 %d %d %d", line_num, select, i, i);
662  f << stringf("%s\n", str.c_str());
663  c[i] = line_num;
664  ++line_num;
665  str = stringf ("%d slice %d %d %d %d", line_num, output_width, cases, i*output_width+output_width-1,
666  i*output_width);
667  f << stringf("%s\n", str.c_str());
668  }
669 
670  ++line_num;
671  str = stringf ("%d cond %d %d %d %d", line_num, output_width, c[select_width-1], c[select_width-1]+1, default_case);
672  f << stringf("%s\n", str.c_str());
673 
674  for (int i=select_width-2; i>=0; --i)
675  {
676  ++line_num;
677  str = stringf ("%d cond %d %d %d %d", line_num, output_width, c[i], c[i]+1, line_num-1);
678  f << stringf("%s\n", str.c_str());
679  }
680 
681  line_ref[cell->name]=line_num;
682  }
683  //registers
684  else if(cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffsr")
685  {
686  //TODO: remodelling fo adff cells
687  log("writing cell - %s\n", cstr(cell->type));
688  int output_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
689  log(" - width is %d\n", output_width);
690  int cond = dump_sigspec(&cell->getPort(RTLIL::IdString("\\CLK")), 1);
691  bool polarity = cell->parameters.at(RTLIL::IdString("\\CLK_POLARITY")).as_bool();
692  const RTLIL::SigSpec* cell_output = &cell->getPort(RTLIL::IdString("\\Q"));
693  int value = dump_sigspec(&cell->getPort(RTLIL::IdString("\\D")), output_width);
694  unsigned start_bit = 0;
695  for(unsigned i=0; i<cell_output->chunks().size(); ++i)
696  {
697  output_width = cell_output->chunks().at(i).width;
698  log_assert( output_width == cell_output->chunks().at(i).wire->width);//full reg is given the next value
699  int reg = dump_wire(cell_output->chunks().at(i).wire);//register
700  int slice = value;
701  if(cell_output->chunks().size()>1)
702  {
703  start_bit+=output_width;
704  slice = ++line_num;
705  str = stringf ("%d slice %d %d %d %d;", line_num, output_width, value, start_bit-1,
706  start_bit-output_width);
707  f << stringf("%s\n", str.c_str());
708  }
709  if(cell->type == "$dffsr")
710  {
711  int sync_reset = dump_sigspec(&cell->getPort(RTLIL::IdString("\\CLR")), 1);
712  bool sync_reset_pol = cell->parameters.at(RTLIL::IdString("\\CLR_POLARITY")).as_bool();
713  int sync_reset_value = dump_sigspec(&cell->getPort(RTLIL::IdString("\\SET")),
714  output_width);
715  bool sync_reset_value_pol = cell->parameters.at(RTLIL::IdString("\\SET_POLARITY")).as_bool();
716  ++line_num;
717  str = stringf ("%d %s %d %s%d %s%d %d", line_num, cell_type_translation.at("$mux").c_str(),
718  output_width, sync_reset_pol ? "":"-", sync_reset, sync_reset_value_pol? "":"-",
719  sync_reset_value, slice);
720  f << stringf("%s\n", str.c_str());
721  slice = line_num;
722  }
723  ++line_num;
724  str = stringf ("%d %s %d %s%d %d %d", line_num, cell_type_translation.at("$mux").c_str(),
725  output_width, polarity?"":"-", cond, slice, reg);
726 
727  f << stringf("%s\n", str.c_str());
728  int next = line_num;
729  if(cell->type == "$adff")
730  {
731  int async_reset = dump_sigspec(&cell->getPort(RTLIL::IdString("\\ARST")), 1);
732  bool async_reset_pol = cell->parameters.at(RTLIL::IdString("\\ARST_POLARITY")).as_bool();
733  int async_reset_value = dump_const(&cell->parameters.at(RTLIL::IdString("\\ARST_VALUE")),
734  output_width, 0);
735  ++line_num;
736  str = stringf ("%d %s %d %s%d %d %d", line_num, cell_type_translation.at("$mux").c_str(),
737  output_width, async_reset_pol ? "":"-", async_reset, async_reset_value, next);
738  f << stringf("%s\n", str.c_str());
739  }
740  ++line_num;
741  str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(),
742  output_width, reg, next);
743  f << stringf("%s\n", str.c_str());
744  }
745  line_ref[cell->name]=line_num;
746  }
747  //memories
748  else if(cell->type == "$memrd")
749  {
750  log("writing memrd cell\n");
751  if (cell->parameters.at("\\CLK_ENABLE").as_bool() == true)
752  log_error("The btor backen does not support $memrd cells with built-in registers. Run memory_dff with -wr_only.\n");
753  str = cell->parameters.at(RTLIL::IdString("\\MEMID")).decode_string();
754  int mem = dump_memory(module->memories.at(RTLIL::IdString(str.c_str())));
755  int address_width = cell->parameters.at(RTLIL::IdString("\\ABITS")).as_int();
756  int address = dump_sigspec(&cell->getPort(RTLIL::IdString("\\ADDR")), address_width);
757  int data_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
758  ++line_num;
759  str = stringf("%d read %d %d %d", line_num, data_width, mem, address);
760  f << stringf("%s\n", str.c_str());
761  line_ref[cell->name]=line_num;
762  }
763  else if(cell->type == "$memwr")
764  {
765  log("writing memwr cell\n");
766  if (cell->parameters.at("\\CLK_ENABLE").as_bool() == false)
767  log_error("The btor backen does not support $memwr cells without built-in registers. Run memory_dff (but with -wr_only).\n");
768  int clk = dump_sigspec(&cell->getPort(RTLIL::IdString("\\CLK")), 1);
769  bool polarity = cell->parameters.at(RTLIL::IdString("\\CLK_POLARITY")).as_bool();
770  int enable = dump_sigspec(&cell->getPort(RTLIL::IdString("\\EN")), 1);
771  int address_width = cell->parameters.at(RTLIL::IdString("\\ABITS")).as_int();
772  int address = dump_sigspec(&cell->getPort(RTLIL::IdString("\\ADDR")), address_width);
773  int data_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
774  int data = dump_sigspec(&cell->getPort(RTLIL::IdString("\\DATA")), data_width);
775  str = cell->parameters.at(RTLIL::IdString("\\MEMID")).decode_string();
776  int mem = dump_memory(module->memories.at(RTLIL::IdString(str.c_str())));
777  //check if the memory has already next
778  auto it = mem_next.find(mem);
779  if(it != std::end(mem_next))
780  {
781  ++line_num;
782  str = cell->parameters.at(RTLIL::IdString("\\MEMID")).decode_string();
783  RTLIL::Memory *memory = module->memories.at(RTLIL::IdString(str.c_str()));
784  int address_bits = ceil(log(memory->size)/log(2));
785  str = stringf("%d array %d %d", line_num, memory->width, address_bits);
786  f << stringf("%s\n", str.c_str());
787  ++line_num;
788  str = stringf("%d eq 1 %d %d", line_num, mem, line_num - 1);
789  f << stringf("%s\n", str.c_str());
790  mem = line_num - 1;
791  }
792  ++line_num;
793  if(polarity)
794  str = stringf("%d one 1", line_num);
795  else
796  str = stringf("%d zero 1", line_num);
797  f << stringf("%s\n", str.c_str());
798  ++line_num;
799  str = stringf("%d eq 1 %d %d", line_num, clk, line_num-1);
800  f << stringf("%s\n", str.c_str());
801  ++line_num;
802  str = stringf("%d and 1 %d %d", line_num, line_num-1, enable);
803  f << stringf("%s\n", str.c_str());
804  ++line_num;
805  str = stringf("%d write %d %d %d %d %d", line_num, data_width, address_width, mem, address, data);
806  f << stringf("%s\n", str.c_str());
807  ++line_num;
808  str = stringf("%d acond %d %d %d %d %d", line_num, data_width, address_width, line_num-2/*enable*/, line_num-1, mem);
809  f << stringf("%s\n", str.c_str());
810  ++line_num;
811  str = stringf("%d anext %d %d %d %d", line_num, data_width, address_width, mem, line_num-1);
812  f << stringf("%s\n", str.c_str());
813  mem_next.insert(mem);
814  line_ref[cell->name]=line_num;
815  }
816  else if(cell->type == "$slice")
817  {
818  log("writing slice cell\n");
819  const RTLIL::SigSpec* input = &cell->getPort(RTLIL::IdString("\\A"));
820  int input_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
821  log_assert(input->size() == input_width);
822  int input_line = dump_sigspec(input, input_width);
823  const RTLIL::SigSpec* output = &cell->getPort(RTLIL::IdString("\\Y"));
824  int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
825  log_assert(output->size() == output_width);
826  int offset = cell->parameters.at(RTLIL::IdString("\\OFFSET")).as_int();
827  ++line_num;
828  str = stringf("%d %s %d %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(), output_width, input_line, output_width+offset-1, offset);
829  f << stringf("%s\n", str.c_str());
830  line_ref[cell->name]=line_num;
831  }
832  else if(cell->type == "$concat")
833  {
834  log("writing concat cell\n");
835  const RTLIL::SigSpec* input_a = &cell->getPort(RTLIL::IdString("\\A"));
836  int input_a_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
837  log_assert(input_a->size() == input_a_width);
838  int input_a_line = dump_sigspec(input_a, input_a_width);
839  const RTLIL::SigSpec* input_b = &cell->getPort(RTLIL::IdString("\\B"));
840  int input_b_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
841  log_assert(input_b->size() == input_b_width);
842  int input_b_line = dump_sigspec(input_b, input_b_width);
843  ++line_num;
844  str = stringf("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(), input_a_width+input_b_width,
845  input_a_line, input_b_line);
846  f << stringf("%s\n", str.c_str());
847  line_ref[cell->name]=line_num;
848  }
849  curr_cell.clear();
850  return line_num;
851  }
852  else
853  {
854  return it->second;
855  }
856  }
RTLIL::IdString::str
std::string str() const
Definition: rtlil.h:182
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
BtorDumper::line_ref
std::map< RTLIL::IdString, int > line_ref
Definition: btor.cc:74
RTLIL::IdString::clear
void clear()
Definition: rtlil.h:223
RTLIL::Cell::name
RTLIL::IdString name
Definition: rtlil.h:853
RTLIL::Module::memories
std::map< RTLIL::IdString, RTLIL::Memory * > memories
Definition: rtlil.h:601
BtorDumper::dump_wire
int dump_wire(RTLIL::Wire *wire)
Definition: btor.cc:170
log_error
void log_error(const char *format,...)
Definition: log.cc:204
RTLIL::Cell::type
RTLIL::IdString type
Definition: rtlil.h:854
RTLIL::Cell::parameters
std::map< RTLIL::IdString, RTLIL::Const > parameters
Definition: rtlil.h:856
RTLIL::Memory::size
int size
Definition: rtlil.h:836
RTLIL::SigSpec::size
int size() const
Definition: rtlil.h:1019
BtorDumper::cell_type_translation
std::map< std::string, std::string > cell_type_translation
Definition: btor.cc:80
BtorDumper::cstr
const char * cstr(const RTLIL::IdString id)
Definition: btor.cc:160
BtorDumper::curr_cell
RTLIL::IdString curr_cell
Definition: btor.cc:79
BtorDumper::dump_const
int dump_const(const RTLIL::Const *data, int width, int offset)
Definition: btor.cc:272
RTLIL::Cell::getPort
const RTLIL::SigSpec & getPort(RTLIL::IdString portname) const
Definition: rtlil.cc:1809
BtorDumper::dump_memory
int dump_memory(const RTLIL::Memory *memory)
Definition: btor.cc:256
log_assert
#define log_assert(_assert_expr_)
Definition: log.h:85
BtorDumper::dump_sigspec
int dump_sigspec(const RTLIL::SigSpec *sig, int expected_width)
Definition: btor.cc:322
BtorDumper::str
std::string str
Definition: btor.cc:77
BtorDumper::f
std::ostream & f
Definition: btor.cc:66
BtorDumper::mem_next
std::set< int > mem_next
Definition: btor.cc:81
log
void log(const char *format,...)
Definition: log.cc:180
input
static int input(void)
Definition: ilang_lexer.cc:1532
BtorDumper::s_cell_type_translation
std::map< std::string, std::string > s_cell_type_translation
Definition: btor.cc:80
RTLIL::Memory::width
int width
Definition: rtlil.h:836
BtorDumper::module
RTLIL::Module * module
Definition: btor.cc:67
BtorDumper::line_num
int line_num
Definition: btor.cc:76
RTLIL::SigSpec::chunks
const std::vector< RTLIL::SigChunk > & chunks() const
Definition: rtlil.h:1016

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

int BtorDumper::dump_const ( const RTLIL::Const *  data,
int  width,
int  offset 
)
inline

Definition at line 272 of file btor.cc.

273  {
274  log("writing const \n");
275  if((data->flags & RTLIL::CONST_FLAG_STRING) == 0)
276  {
277  if(width<0)
278  width = data->bits.size() - offset;
279 
280  std::string data_str = data->as_string();
281  //if(offset > 0)
282  data_str = data_str.substr(offset, width);
283 
284  ++line_num;
285  str = stringf("%d const %d %s", line_num, width, data_str.c_str());
286  f << stringf("%s\n", str.c_str());
287  return line_num;
288  }
289  else
290  log("writing const error\n");
291  log_abort();
292  return -1;
293  }
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
RTLIL::Const::flags
int flags
Definition: rtlil.h:437
log_abort
#define log_abort()
Definition: log.h:84
RTLIL::Const::as_string
std::string as_string() const
Definition: rtlil.cc:116
BtorDumper::str
std::string str
Definition: btor.cc:77
BtorDumper::f
std::ostream & f
Definition: btor.cc:66
log
void log(const char *format,...)
Definition: log.cc:180
RTLIL::Const::bits
std::vector< RTLIL::State > bits
Definition: rtlil.h:438
BtorDumper::line_num
int line_num
Definition: btor.cc:76

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

int BtorDumper::dump_memory ( const RTLIL::Memory *  memory)
inline

Definition at line 256 of file btor.cc.

257  {
258  log("writing memory %s\n", cstr(memory->name));
259  auto it = line_ref.find(memory->name);
260  if(it==std::end(line_ref))
261  {
262  ++line_num;
263  int address_bits = ceil(log(memory->size)/log(2));
264  str = stringf("%d array %d %d", line_num, memory->width, address_bits);
265  line_ref[memory->name]=line_num;
266  f << stringf("%s\n", str.c_str());
267  return line_num;
268  }
269  else return it->second;
270  }
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
BtorDumper::line_ref
std::map< RTLIL::IdString, int > line_ref
Definition: btor.cc:74
RTLIL::Memory::size
int size
Definition: rtlil.h:836
BtorDumper::cstr
const char * cstr(const RTLIL::IdString id)
Definition: btor.cc:160
RTLIL::Memory::name
RTLIL::IdString name
Definition: rtlil.h:835
BtorDumper::str
std::string str
Definition: btor.cc:77
BtorDumper::f
std::ostream & f
Definition: btor.cc:66
log
void log(const char *format,...)
Definition: log.cc:180
RTLIL::Memory::width
int width
Definition: rtlil.h:836
BtorDumper::line_num
int line_num
Definition: btor.cc:76

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

void BtorDumper::dump_property ( RTLIL::Wire *  wire)
inline

Definition at line 880 of file btor.cc.

881  {
882  int l = dump_wire(wire);
883  ++line_num;
884  str = stringf("%d root 1 %d", line_num, l);
885  f << stringf("%s\n", str.c_str());
886  }
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
BtorDumper::dump_wire
int dump_wire(RTLIL::Wire *wire)
Definition: btor.cc:170
BtorDumper::str
std::string str
Definition: btor.cc:77
BtorDumper::f
std::ostream & f
Definition: btor.cc:66
BtorDumper::line_num
int line_num
Definition: btor.cc:76

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

int BtorDumper::dump_sigchunk ( const RTLIL::SigChunk *  chunk)
inline

Definition at line 295 of file btor.cc.

296  {
297  log("writing sigchunk\n");
298  int l=-1;
299  if(chunk->wire == NULL)
300  {
301  RTLIL::Const data_const(chunk->data);
302  l=dump_const(&data_const, chunk->width, chunk->offset);
303  }
304  else
305  {
306  if (chunk->width == chunk->wire->width && chunk->offset == 0)
307  l = dump_wire(chunk->wire);
308  else
309  {
310  int wire_line_num = dump_wire(chunk->wire);
311  log_assert(wire_line_num>0);
312  ++line_num;
313  str = stringf("%d slice %d %d %d %d;2", line_num, chunk->width, wire_line_num,
314  chunk->width + chunk->offset - 1, chunk->offset);
315  f << stringf("%s\n", str.c_str());
316  l = line_num;
317  }
318  }
319  return l;
320  }
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
RTLIL::Wire::width
int width
Definition: rtlil.h:826
BtorDumper::dump_wire
int dump_wire(RTLIL::Wire *wire)
Definition: btor.cc:170
BtorDumper::dump_const
int dump_const(const RTLIL::Const *data, int width, int offset)
Definition: btor.cc:272
RTLIL::SigChunk::wire
RTLIL::Wire * wire
Definition: rtlil.h:885
log_assert
#define log_assert(_assert_expr_)
Definition: log.h:85
BtorDumper::str
std::string str
Definition: btor.cc:77
NULL
#define NULL
Definition: NumberlikeArray.hh:6
BtorDumper::f
std::ostream & f
Definition: btor.cc:66
log
void log(const char *format,...)
Definition: log.cc:180
BtorDumper::line_num
int line_num
Definition: btor.cc:76
RTLIL::SigChunk::data
std::vector< RTLIL::State > data
Definition: rtlil.h:886

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

int BtorDumper::dump_sigspec ( const RTLIL::SigSpec *  sig,
int  expected_width 
)
inline

Definition at line 322 of file btor.cc.

323  {
324  log("writing sigspec\n");
325  RTLIL::SigSpec s = sigmap(*sig);
326  int l = -1;
327  auto it = sig_ref.find(s);
328  if(it == std::end(sig_ref))
329  {
330  if (s.is_chunk())
331  {
332  l = dump_sigchunk(&s.chunks().front());
333  }
334  else
335  {
336  int l1, l2, w1, w2;
337  l1 = dump_sigchunk(&s.chunks().front());
338  log_assert(l1>0);
339  w1 = s.chunks().front().width;
340  for (unsigned i=1; i < s.chunks().size(); ++i)
341  {
342  l2 = dump_sigchunk(&s.chunks().at(i));
343  log_assert(l2>0);
344  w2 = s.chunks().at(i).width;
345  ++line_num;
346  str = stringf("%d concat %d %d %d", line_num, w1+w2, l2, l1);
347  f << stringf("%s\n", str.c_str());
348  l1=line_num;
349  w1+=w2;
350  }
351  l = line_num;
352  }
353  sig_ref[s] = l;
354  }
355  else
356  {
357  l = it->second;
358  }
359 
360  if (expected_width != s.size())
361  {
362  log(" - changing width of sigspec\n");
363  //TODO: this block may not be needed anymore, due to explicit type conversion by "splice" command
364  if(expected_width > s.size())
365  {
366  //TODO: case the signal is signed
367  ++line_num;
368  str = stringf ("%d zero %d", line_num, expected_width - s.size());
369  f << stringf("%s\n", str.c_str());
370  ++line_num;
371  str = stringf ("%d concat %d %d %d", line_num, expected_width, line_num-1, l);
372  f << stringf("%s\n", str.c_str());
373  l = line_num;
374  }
375  else if(expected_width < s.size())
376  {
377  ++line_num;
378  str = stringf ("%d slice %d %d %d %d;3", line_num, expected_width, l, expected_width-1, 0);
379  f << stringf("%s\n", str.c_str());
380  l = line_num;
381  }
382  }
383  log_assert(l>0);
384  return l;
385  }
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
RTLIL::SigSpec::size
int size() const
Definition: rtlil.h:1019
RTLIL::SigSpec::is_chunk
bool is_chunk() const
Definition: rtlil.cc:2755
log_assert
#define log_assert(_assert_expr_)
Definition: log.h:85
BtorDumper::sig_ref
std::map< RTLIL::SigSpec, int > sig_ref
Definition: btor.cc:75
BtorDumper::dump_sigchunk
int dump_sigchunk(const RTLIL::SigChunk *chunk)
Definition: btor.cc:295
BtorDumper::str
std::string str
Definition: btor.cc:77
BtorDumper::f
std::ostream & f
Definition: btor.cc:66
BtorDumper::sigmap
SigMap sigmap
Definition: btor.cc:72
log
void log(const char *format,...)
Definition: log.cc:180
BtorDumper::line_num
int line_num
Definition: btor.cc:76
RTLIL::SigSpec::chunks
const std::vector< RTLIL::SigChunk > & chunks() const
Definition: rtlil.h:1016

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

int BtorDumper::dump_wire ( RTLIL::Wire *  wire)
inline

Definition at line 170 of file btor.cc.

171  {
172  if(basic_wires[wire->name])
173  {
174  log("writing wire %s\n", cstr(wire->name));
175  auto it = line_ref.find(wire->name);
176  if(it==std::end(line_ref))
177  {
178  ++line_num;
179  line_ref[wire->name]=line_num;
180  str = stringf("%d var %d %s", line_num, wire->width, cstr(wire->name));
181  f << stringf("%s\n", str.c_str());
182  return line_num;
183  }
184  else return it->second;
185  }
186  else // case when the wire is not basic wire
187  {
188  log("case of non-basic wire - %s\n", cstr(wire->name));
189  auto it = line_ref.find(wire->name);
190  if(it==std::end(line_ref))
191  {
192  std::set<WireInfo, WireInfoOrder>& dep_set = inter_wire_map.at(wire->name);
193  int wire_line = 0;
194  int wire_width = 0;
195  for(auto dep_set_it=dep_set.begin(); dep_set_it!=dep_set.end(); ++dep_set_it)
196  {
197  RTLIL::IdString cell_id = dep_set_it->cell_name;
198  if(cell_id == curr_cell)
199  break;
200  log(" -- found cell %s\n", cstr(cell_id));
201  RTLIL::Cell* cell = module->cells_.at(cell_id);
202  const RTLIL::SigSpec* cell_output = get_cell_output(cell);
203  int cell_line = dump_cell(cell);
204 
205  if(dep_set.size()==1 && wire->width == cell_output->size())
206  {
207  wire_line = cell_line;
208  break;
209  }
210  else
211  {
212  int prev_wire_line=0; //previously dumped wire line
213  int start_bit=0;
214  for(unsigned j=0; j<cell_output->chunks().size(); ++j)
215  {
216  start_bit+=cell_output->chunks().at(j).width;
217  if(cell_output->chunks().at(j).wire->name == wire->name)
218  {
219  prev_wire_line = wire_line;
220  wire_line = ++line_num;
221  str = stringf("%d slice %d %d %d %d;1", line_num, cell_output->chunks().at(j).width,
222  cell_line, start_bit-1, start_bit-cell_output->chunks().at(j).width);
223  f << stringf("%s\n", str.c_str());
224  wire_width += cell_output->chunks().at(j).width;
225  if(prev_wire_line!=0)
226  {
227  ++line_num;
228  str = stringf("%d concat %d %d %d", line_num, wire_width, wire_line, prev_wire_line);
229  f << stringf("%s\n", str.c_str());
230  wire_line = line_num;
231  }
232  }
233  }
234  }
235  }
236  if(dep_set.size()==0)
237  {
238  log(" - checking sigmap\n");
239  RTLIL::SigSpec s = RTLIL::SigSpec(wire);
240  wire_line = dump_sigspec(&s, s.size());
241  line_ref[wire->name]=wire_line;
242  }
243  line_ref[wire->name]=wire_line;
244  return wire_line;
245  }
246  else
247  {
248  log(" -- already processed wire\n");
249  return it->second;
250  }
251  }
252  log_abort();
253  return -1;
254  }
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
BtorDumper::line_ref
std::map< RTLIL::IdString, int > line_ref
Definition: btor.cc:74
RTLIL::Wire::width
int width
Definition: rtlil.h:826
RTLIL::SigSpec::size
int size() const
Definition: rtlil.h:1019
log_abort
#define log_abort()
Definition: log.h:84
BtorDumper::cstr
const char * cstr(const RTLIL::IdString id)
Definition: btor.cc:160
BtorDumper::curr_cell
RTLIL::IdString curr_cell
Definition: btor.cc:79
BtorDumper::dump_sigspec
int dump_sigspec(const RTLIL::SigSpec *sig, int expected_width)
Definition: btor.cc:322
BtorDumper::inter_wire_map
std::map< RTLIL::IdString, std::set< WireInfo, WireInfoOrder > > inter_wire_map
Definition: btor.cc:73
RTLIL::Wire::name
RTLIL::IdString name
Definition: rtlil.h:825
BtorDumper::str
std::string str
Definition: btor.cc:77
BtorDumper::get_cell_output
const RTLIL::SigSpec * get_cell_output(RTLIL::Cell *cell)
Definition: btor.cc:858
RTLIL::Module::cells_
std::map< RTLIL::IdString, RTLIL::Cell * > cells_
Definition: rtlil.h:596
BtorDumper::f
std::ostream & f
Definition: btor.cc:66
log
void log(const char *format,...)
Definition: log.cc:180
BtorDumper::dump_cell
int dump_cell(const RTLIL::Cell *cell)
Definition: btor.cc:387
BtorDumper::basic_wires
std::map< RTLIL::IdString, bool > basic_wires
Definition: btor.cc:78
BtorDumper::module
RTLIL::Module * module
Definition: btor.cc:67
BtorDumper::line_num
int line_num
Definition: btor.cc:76
RTLIL::SigSpec::chunks
const std::vector< RTLIL::SigChunk > & chunks() const
Definition: rtlil.h:1016

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

const RTLIL::SigSpec* BtorDumper::get_cell_output ( RTLIL::Cell *  cell)
inline

Definition at line 858 of file btor.cc.

859  {
860  const RTLIL::SigSpec *output_sig = nullptr;
861  if (cell->type == "$memrd")
862  {
863  output_sig = &cell->getPort(RTLIL::IdString("\\DATA"));
864  }
865  else if(cell->type == "$memwr" || cell->type == "$assert")
866  {
867  //no output
868  }
869  else if(cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffsr")
870  {
871  output_sig = &cell->getPort(RTLIL::IdString("\\Q"));
872  }
873  else
874  {
875  output_sig = &cell->getPort(RTLIL::IdString("\\Y"));
876  }
877  return output_sig;
878  }
RTLIL::Cell::type
RTLIL::IdString type
Definition: rtlil.h:854
RTLIL::Cell::getPort
const RTLIL::SigSpec & getPort(RTLIL::IdString portname) const
Definition: rtlil.cc:1809

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

Field Documentation

std::map<RTLIL::IdString, bool> BtorDumper::basic_wires

Definition at line 78 of file btor.cc.

std::map<std::string, std::string> BtorDumper::cell_type_translation

Definition at line 80 of file btor.cc.

BtorDumperConfig* BtorDumper::config

Definition at line 69 of file btor.cc.

std::vector<std::string> BtorDumper::cstr_buf

Definition at line 158 of file btor.cc.

CellTypes BtorDumper::ct

Definition at line 70 of file btor.cc.

RTLIL::IdString BtorDumper::curr_cell

Definition at line 79 of file btor.cc.

RTLIL::Design* BtorDumper::design

Definition at line 68 of file btor.cc.

std::ostream& BtorDumper::f

Definition at line 66 of file btor.cc.

std::map<RTLIL::IdString, std::set<WireInfo,WireInfoOrder> > BtorDumper::inter_wire_map

Definition at line 73 of file btor.cc.

int BtorDumper::line_num

Definition at line 76 of file btor.cc.

std::map<RTLIL::IdString, int> BtorDumper::line_ref

Definition at line 74 of file btor.cc.

std::set<int> BtorDumper::mem_next

Definition at line 81 of file btor.cc.

RTLIL::Module* BtorDumper::module

Definition at line 67 of file btor.cc.

std::map<std::string, std::string> BtorDumper::s_cell_type_translation

Definition at line 80 of file btor.cc.

std::map<RTLIL::SigSpec, int> BtorDumper::sig_ref

Definition at line 75 of file btor.cc.

SigMap BtorDumper::sigmap

Definition at line 72 of file btor.cc.

std::string BtorDumper::str

Definition at line 77 of file btor.cc.

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