yosys-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
test_abcloop.cc
Go to the documentation of this file.
1 /*
2  * yosys -- Yosys Open SYnthesis Suite
3  *
4  * Copyright (C) 2014 Clifford Wolf <clifford@clifford.at>
5  * Copyright (C) 2014 Johann Glaser <Johann.Glaser@gmx.at>
6  *
7  * Permission to use, copy, modify, and/or distribute this software for any
8  * purpose with or without fee is hereby granted, provided that the above
9  * copyright notice and this permission notice appear in all copies.
10  *
11  * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
12  * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
13  * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
14  * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
15  * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
16  * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
17  * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
18  *
19  */
20 
21 #include "kernel/yosys.h"
22 #include "kernel/satgen.h"
23 
24 USING_YOSYS_NAMESPACE
25 PRIVATE_NAMESPACE_BEGIN
26 
27 static uint32_t xorshift32_state = 123456789;
28 
29 static uint32_t xorshift32(uint32_t limit) {
30  xorshift32_state ^= xorshift32_state << 13;
31  xorshift32_state ^= xorshift32_state >> 17;
32  xorshift32_state ^= xorshift32_state << 5;
33  return xorshift32_state % limit;
34 }
35 
36 static RTLIL::Wire *getw(std::vector<RTLIL::Wire*> &wires, RTLIL::Wire *w)
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 }
44 
45 static void test_abcloop()
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 }
244 
245 struct TestAbcloopPass : public Pass {
246  TestAbcloopPass() : Pass("test_abcloop", "automatically test handling of loops in abc command") { }
247  virtual void help()
248  {
249  // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
250  log("\n");
251  log(" test_abcloop [options]\n");
252  log("\n");
253  log("Test handling of logic loops in ABC.\n");
254  log("\n");
255  log(" -n {integer}\n");
256  log(" create this number of circuits and test them (default = 100).\n");
257  log("\n");
258  log(" -s {positive_integer}\n");
259  log(" use this value as rng seed value (default = unix time).\n");
260  log("\n");
261  }
262  virtual void execute(std::vector<std::string> args, RTLIL::Design*)
263  {
264  int num_iter = 100;
265  xorshift32_state = 0;
266 
267  int argidx;
268  for (argidx = 1; argidx < GetSize(args); argidx++)
269  {
270  if (args[argidx] == "-n" && argidx+1 < GetSize(args)) {
271  num_iter = atoi(args[++argidx].c_str());
272  continue;
273  }
274  if (args[argidx] == "-s" && argidx+1 < GetSize(args)) {
275  xorshift32_state = atoi(args[++argidx].c_str());
276  continue;
277  }
278  break;
279  }
280 
281  if (xorshift32_state == 0)
282  xorshift32_state = time(NULL) & 0x7fffffff;
283 
284  for (int i = 0; i < num_iter; i++)
285  test_abcloop();
286  }
287 } TestAbcloopPass;
288 
289 PRIVATE_NAMESPACE_END
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
TestAbcloopPass
TestAbcloopPass TestAbcloopPass
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)
idx
static std::string idx(std::string str)
Definition: test_autotb.cc:57
RTLIL::Wire::port_input
bool port_input
Definition: rtlil.h:827
SatGen::importSigSpec
std::vector< int > importSigSpec(RTLIL::SigSpec sig, int timestep=-1)
Definition: satgen.h:78
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)
PRIVATE_NAMESPACE_BEGIN
#define PRIVATE_NAMESPACE_BEGIN
Definition: yosys.h:97
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
PRIVATE_NAMESPACE_END
#define PRIVATE_NAMESPACE_END
Definition: yosys.h:98
SatGen
Definition: satgen.h:34
Pass
Definition: register.h:27
TestAbcloopPass::execute
virtual void execute(std::vector< std::string > args, RTLIL::Design *)
Definition: test_abcloop.cc:262
RTLIL::Design::addModule
RTLIL::Module * addModule(RTLIL::IdString name)
Definition: rtlil.cc:270
USING_YOSYS_NAMESPACE
#define USING_YOSYS_NAMESPACE
Definition: yosys.h:102
RTLIL::Module::cells
RTLIL::ObjRange< RTLIL::Cell * > cells()
Definition: rtlil.h:641
NULL
#define NULL
Definition: NumberlikeArray.hh:6
test_abcloop
static void test_abcloop()
Definition: test_abcloop.cc:45
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)
SatGen::importCell
bool importCell(RTLIL::Cell *cell, int timestep=-1)
Definition: satgen.h:203
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
TestAbcloopPass::help
virtual void help()
Definition: test_abcloop.cc:247
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)