yosys-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Data Structures | Functions | Variables
test_abcloop.cc File Reference
#include "kernel/yosys.h"
#include "kernel/satgen.h"
+ Include dependency graph for test_abcloop.cc:

Go to the source code of this file.

Data Structures

struct  TestAbcloopPass
 

Functions

static uint32_t xorshift32 (uint32_t limit)
 
static RTLIL::Wire * getw (std::vector< RTLIL::Wire * > &wires, RTLIL::Wire *w)
 
static void test_abcloop ()
 

Variables

USING_YOSYS_NAMESPACE static
PRIVATE_NAMESPACE_BEGIN
uint32_t 		xorshift32_state = 123456789
 
TestAbcloopPass TestAbcloopPass
 

Function Documentation

static RTLIL::Wire* getw ( std::vector< RTLIL::Wire * > &  wires,
RTLIL::Wire *  w 
)
static

Definition at line 36 of file test_abcloop.cc.

37 {
38  while (1) {
39  int idx = xorshift32(GetSize(wires));
40  if (wires[idx] != w && !wires[idx]->port_output)
41  return wires[idx];
42  }
43 }
idx
static std::string idx(std::string str)
Definition: test_autotb.cc:57
xorshift32
static uint32_t xorshift32(uint32_t limit)
Definition: test_abcloop.cc:29
GetSize
int GetSize(RTLIL::Wire *wire)
Definition: yosys.cc:334

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

static void test_abcloop ( )
static

Definition at line 45 of file test_abcloop.cc.

46 {
47  log("Rng seed value: %u\n", int(xorshift32_state));
48 
49  RTLIL::Design *design = new RTLIL::Design;
50  RTLIL::Module *module = nullptr;
51  RTLIL::SigSpec in_sig, out_sig;
52 
53  bool truthtab[16][4];
54  int create_cycles = 0;
55 
56  while (1)
57  {
58  module = design->addModule("\\uut");
59  create_cycles++;
60 
61  in_sig = {};
62  out_sig = {};
63 
64  std::vector<RTLIL::Wire*> wires;
65 
66  for (int i = 0; i < 4; i++) {
67  RTLIL::Wire *w = module->addWire(stringf("\\i%d", i));
68  w->port_input = true;
69  wires.push_back(w);
70  in_sig.append(w);
71  }
72 
73  for (int i = 0; i < 4; i++) {
74  RTLIL::Wire *w = module->addWire(stringf("\\o%d", i));
75  w->port_output = true;
76  wires.push_back(w);
77  out_sig.append(w);
78  }
79 
80  for (int i = 0; i < 16; i++) {
81  RTLIL::Wire *w = module->addWire(stringf("\\t%d", i));
82  wires.push_back(w);
83  }
84 
85  for (auto w : wires)
86  if (!w->port_input)
87  switch (xorshift32(12))
88  {
89  case 0:
90  module->addNotGate(w->name.str() + "g", getw(wires, w), w);
91  break;
92  case 1:
93  module->addAndGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
94  break;
95  case 2:
96  module->addNandGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
97  break;
98  case 3:
99  module->addOrGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
100  break;
101  case 4:
102  module->addNorGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
103  break;
104  case 5:
105  module->addXorGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
106  break;
107  case 6:
108  module->addXnorGate(w->name.str() + "g", getw(wires, w), getw(wires, w), w);
109  break;
110  case 7:
111  module->addMuxGate(w->name.str() + "g", getw(wires, w), getw(wires, w), getw(wires, w), w);
112  break;
113  case 8:
114  module->addAoi3Gate(w->name.str() + "g", getw(wires, w), getw(wires, w), getw(wires, w), w);
115  break;
116  case 9:
117  module->addOai3Gate(w->name.str() + "g", getw(wires, w), getw(wires, w), getw(wires, w), w);
118  break;
119  case 10:
120  module->addAoi4Gate(w->name.str() + "g", getw(wires, w), getw(wires, w), getw(wires, w), getw(wires, w), w);
121  break;
122  case 11:
123  module->addOai4Gate(w->name.str() + "g", getw(wires, w), getw(wires, w), getw(wires, w), getw(wires, w), w);
124  break;
125  }
126 
127  module->fixup_ports();
128  Pass::call(design, "clean");
129 
130  ezDefaultSAT ez;
131  SigMap sigmap(module);
132  SatGen satgen(&ez, &sigmap);
133 
134  for (auto c : module->cells()) {
135  bool ok = satgen.importCell(c);
136  log_assert(ok);
137  }
138 
139  std::vector<int> in_vec = satgen.importSigSpec(in_sig);
140  std::vector<int> inverse_in_vec = ez.vec_not(in_vec);
141 
142  std::vector<int> out_vec = satgen.importSigSpec(out_sig);
143 
144  for (int i = 0; i < 16; i++)
145  {
146  std::vector<int> assumptions;
147  for (int j = 0; j < GetSize(in_vec); j++)
148  assumptions.push_back((i & (1 << j)) ? in_vec.at(j) : inverse_in_vec.at(j));
149 
150  std::vector<bool> results;
151  if (!ez.solve(out_vec, results, assumptions)) {
152  log("No stable solution for input %d found -> recreate module.\n", i);
153  goto recreate_module;
154  }
155 
156  for (int j = 0; j < 4; j++)
157  truthtab[i][j] = results[j];
158 
159  assumptions.push_back(ez.vec_ne(out_vec, ez.vec_const(results)));
160 
161  std::vector<bool> results2;
162  if (ez.solve(out_vec, results2, assumptions)) {
163  log("Two stable solutions for input %d found -> recreate module.\n", i);
164  goto recreate_module;
165  }
166  }
167  break;
168 
169  recreate_module:
170  design->remove(module);
171  }
172 
173  log("Found viable UUT after %d cycles:\n", create_cycles);
174  Pass::call(design, "write_ilang");
175  Pass::call(design, "abc");
176 
177  log("\n");
178  log("Pre- and post-abc truth table:\n");
179 
180  ezDefaultSAT ez;
181  SigMap sigmap(module);
182  SatGen satgen(&ez, &sigmap);
183 
184  for (auto c : module->cells()) {
185  bool ok = satgen.importCell(c);
186  log_assert(ok);
187  }
188 
189  std::vector<int> in_vec = satgen.importSigSpec(in_sig);
190  std::vector<int> inverse_in_vec = ez.vec_not(in_vec);
191 
192  std::vector<int> out_vec = satgen.importSigSpec(out_sig);
193 
194  bool found_error = false;
195  bool truthtab2[16][4];
196 
197  for (int i = 0; i < 16; i++)
198  {
199  std::vector<int> assumptions;
200  for (int j = 0; j < GetSize(in_vec); j++)
201  assumptions.push_back((i & (1 << j)) ? in_vec.at(j) : inverse_in_vec.at(j));
202 
203  for (int j = 0; j < 4; j++)
204  truthtab2[i][j] = truthtab[i][j];
205 
206  std::vector<bool> results;
207  if (!ez.solve(out_vec, results, assumptions)) {
208  log("No stable solution for input %d found.\n", i);
209  found_error = true;
210  continue;
211  }
212 
213  for (int j = 0; j < 4; j++)
214  truthtab2[i][j] = results[j];
215 
216  assumptions.push_back(ez.vec_ne(out_vec, ez.vec_const(results)));
217 
218  std::vector<bool> results2;
219  if (ez.solve(out_vec, results2, assumptions)) {
220  log("Two stable solutions for input %d found -> recreate module.\n", i);
221  found_error = true;
222  }
223  }
224 
225  for (int i = 0; i < 16; i++) {
226  log("%3d ", i);
227  for (int j = 0; j < 4; j++)
228  log("%c", truthtab[i][j] ? '1' : '0');
229  log(" ");
230  for (int j = 0; j < 4; j++)
231  log("%c", truthtab2[i][j] ? '1' : '0');
232  for (int j = 0; j < 4; j++)
233  if (truthtab[i][j] != truthtab2[i][j]) {
234  found_error = true;
235  log(" !");
236  break;
237  }
238  log("\n");
239  }
240 
241  log_assert(found_error == false);
242  log("\n");
243 }
RTLIL::IdString::str
std::string str() const
Definition: rtlil.h:182
xorshift32_state
USING_YOSYS_NAMESPACE static PRIVATE_NAMESPACE_BEGIN uint32_t xorshift32_state
Definition: test_abcloop.cc:27
RTLIL::Module::addXorGate
RTLIL::Cell * addXorGate(RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_y)
stringf
std::string stringf(const char *fmt,...)
Definition: yosys.cc:58
RTLIL::Module::addNandGate
RTLIL::Cell * addNandGate(RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_y)
getw
static RTLIL::Wire * getw(std::vector< RTLIL::Wire * > &wires, RTLIL::Wire *w)
Definition: test_abcloop.cc:36
RTLIL::Module::addOai4Gate
RTLIL::Cell * addOai4Gate(RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_d, RTLIL::SigBit sig_y)
RTLIL::Module::addAoi3Gate
RTLIL::Cell * addAoi3Gate(RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_y)
ez
ezMiniSAT ez
Definition: puzzle3d.cc:31
RTLIL::Module::addNorGate
RTLIL::Cell * addNorGate(RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_y)
RTLIL::Wire::port_input
bool port_input
Definition: rtlil.h:827
module
RTLIL::Module * module
Definition: abc.cc:94
xorshift32
static uint32_t xorshift32(uint32_t limit)
Definition: test_abcloop.cc:29
RTLIL::Module::addNotGate
RTLIL::Cell * addNotGate(RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_y)
RTLIL::Wire::port_output
bool port_output
Definition: rtlil.h:827
ezDefaultSAT
YOSYS_NAMESPACE_BEGIN typedef ezMiniSAT ezDefaultSAT
Definition: satgen.h:32
RTLIL::Module::addAndGate
RTLIL::Cell * addAndGate(RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_y)
RTLIL::Module::addOrGate
RTLIL::Cell * addOrGate(RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_y)
GetSize
int GetSize(RTLIL::Wire *wire)
Definition: yosys.cc:334
RTLIL::Module::fixup_ports
void fixup_ports()
Definition: rtlil.cc:1312
log_assert
#define log_assert(_assert_expr_)
Definition: log.h:85
RTLIL::Module::addWire
RTLIL::Wire * addWire(RTLIL::IdString name, int width=1)
Definition: rtlil.cc:1331
SatGen
Definition: satgen.h:34
RTLIL::Wire::name
RTLIL::IdString name
Definition: rtlil.h:825
RTLIL::Design::addModule
RTLIL::Module * addModule(RTLIL::IdString name)
Definition: rtlil.cc:270
RTLIL::Module::cells
RTLIL::ObjRange< RTLIL::Cell * > cells()
Definition: rtlil.h:641
log
void log(const char *format,...)
Definition: log.cc:180
RTLIL::Module::addAoi4Gate
RTLIL::Cell * addAoi4Gate(RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_d, RTLIL::SigBit sig_y)
RTLIL::Module::addMuxGate
RTLIL::Cell * addMuxGate(RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_s, RTLIL::SigBit sig_y)
RTLIL::SigSpec::append
void append(const RTLIL::SigSpec &signal)
Definition: rtlil.cc:2523
RTLIL::Module::addXnorGate
RTLIL::Cell * addXnorGate(RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_y)
RTLIL::Design::remove
void remove(RTLIL::Module *module)
Definition: rtlil.cc:347
Pass::call
static void call(RTLIL::Design *design, std::string command)
Definition: register.cc:146
RTLIL::Module::addOai3Gate
RTLIL::Cell * addOai3Gate(RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_y)

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

static uint32_t xorshift32 ( uint32_t  limit)
static

Definition at line 29 of file test_abcloop.cc.

29  {
30  xorshift32_state ^= xorshift32_state << 13;
31  xorshift32_state ^= xorshift32_state >> 17;
32  xorshift32_state ^= xorshift32_state << 5;
33  return xorshift32_state % limit;
34 }
xorshift32_state
USING_YOSYS_NAMESPACE static PRIVATE_NAMESPACE_BEGIN uint32_t xorshift32_state
Definition: test_abcloop.cc:27

+ Here is the caller graph for this function:

Variable Documentation

TestAbcloopPass TestAbcloopPass
USING_YOSYS_NAMESPACE static PRIVATE_NAMESPACE_BEGIN uint32_t xorshift32_state = 123456789
static

Definition at line 27 of file test_abcloop.cc.