2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2014 Clifford Wolf <clifford@clifford.at>
5 * Copyright (C) 2014 Johann Glaser <Johann.Glaser@gmx.at>
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.
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.
21 #include "kernel/yosys.h"
22 #include "kernel/satgen.h"
23 #include "kernel/consteval.h"
26 static uint32_t xorshift32_state
= 123456789;
28 static uint32_t xorshift32(uint32_t limit
) {
29 xorshift32_state
^= xorshift32_state
<< 13;
30 xorshift32_state
^= xorshift32_state
>> 17;
31 xorshift32_state
^= xorshift32_state
<< 5;
32 return xorshift32_state
% limit
;
35 static void create_gold_module(RTLIL::Design
*design
, RTLIL::IdString cell_type
, std::string cell_type_flags
)
37 RTLIL::Module
*module
= design
->addModule("\\gold");
38 RTLIL::Cell
*cell
= module
->addCell("\\UUT", cell_type
);
41 if (cell_type
== "$lut")
43 int width
= 1 + xorshift32(6);
45 wire
= module
->addWire("\\A");
47 wire
->port_input
= true;
48 cell
->setPort("\\A", wire
);
50 wire
= module
->addWire("\\Y");
51 wire
->port_output
= true;
52 cell
->setPort("\\Y", wire
);
54 RTLIL::SigSpec config
;
55 for (int i
= 0; i
< (1 << width
); i
++)
56 config
.append(xorshift32(2) ? RTLIL::S1
: RTLIL::S0
);
58 cell
->setParam("\\LUT", config
.as_const());
61 if (cell_type_flags
.find('A') != std::string::npos
) {
62 wire
= module
->addWire("\\A");
63 wire
->width
= 1 + xorshift32(8);
64 wire
->port_input
= true;
65 cell
->setPort("\\A", wire
);
68 if (cell_type_flags
.find('B') != std::string::npos
) {
69 wire
= module
->addWire("\\B");
70 if (cell_type_flags
.find('h') != std::string::npos
)
71 wire
->width
= 1 + xorshift32(6);
73 wire
->width
= 1 + xorshift32(8);
74 wire
->port_input
= true;
75 cell
->setPort("\\B", wire
);
78 if (cell_type_flags
.find('S') != std::string::npos
&& xorshift32(2)) {
79 if (cell_type_flags
.find('A') != std::string::npos
)
80 cell
->parameters
["\\A_SIGNED"] = true;
81 if (cell_type_flags
.find('B') != std::string::npos
)
82 cell
->parameters
["\\B_SIGNED"] = true;
85 if (cell_type_flags
.find('s') != std::string::npos
) {
86 if (cell_type_flags
.find('A') != std::string::npos
&& xorshift32(2))
87 cell
->parameters
["\\A_SIGNED"] = true;
88 if (cell_type_flags
.find('B') != std::string::npos
&& xorshift32(2))
89 cell
->parameters
["\\B_SIGNED"] = true;
92 if (cell_type_flags
.find('Y') != std::string::npos
) {
93 wire
= module
->addWire("\\Y");
94 wire
->width
= 1 + xorshift32(8);
95 wire
->port_output
= true;
96 cell
->setPort("\\Y", wire
);
99 if (cell_type
== "$alu")
101 wire
= module
->addWire("\\CI");
102 wire
->port_input
= true;
103 cell
->setPort("\\CI", wire
);
105 wire
= module
->addWire("\\BI");
106 wire
->port_input
= true;
107 cell
->setPort("\\BI", wire
);
109 wire
= module
->addWire("\\X");
110 wire
->width
= SIZE(cell
->getPort("\\Y"));
111 wire
->port_output
= true;
112 cell
->setPort("\\X", wire
);
114 wire
= module
->addWire("\\CO");
115 wire
->width
= SIZE(cell
->getPort("\\Y"));
116 wire
->port_output
= true;
117 cell
->setPort("\\CO", wire
);
120 module
->fixup_ports();
121 cell
->fixup_parameters();
125 static void run_eval_test(RTLIL::Design
*design
, bool verbose
)
127 log("Eval testing:%c", verbose
? '\n' : ' ');
129 RTLIL::Module
*gold_mod
= design
->module("\\gold");
130 RTLIL::Module
*gate_mod
= design
->module("\\gate");
131 ConstEval
gold_ce(gold_mod
), gate_ce(gate_mod
);
133 ezDefaultSAT ez1
, ez2
;
134 SigMap
sigmap(gold_mod
);
135 SatGen
satgen1(&ez1
, &sigmap
);
136 SatGen
satgen2(&ez2
, &sigmap
);
137 satgen2
.model_undef
= true;
139 for (auto cell
: gold_mod
->cells()) {
140 satgen1
.importCell(cell
);
141 satgen2
.importCell(cell
);
144 for (int i
= 0; i
< 64; i
++)
146 log(verbose
? "\n" : ".");
150 RTLIL::SigSpec in_sig
, in_val
;
151 RTLIL::SigSpec out_sig
, out_val
;
153 for (auto port
: gold_mod
->ports
)
155 RTLIL::Wire
*gold_wire
= gold_mod
->wire(port
);
156 RTLIL::Wire
*gate_wire
= gate_mod
->wire(port
);
158 log_assert(gold_wire
!= nullptr);
159 log_assert(gate_wire
!= nullptr);
160 log_assert(gold_wire
->port_input
== gate_wire
->port_input
);
161 log_assert(SIZE(gold_wire
) == SIZE(gate_wire
));
163 if (!gold_wire
->port_input
)
166 RTLIL::Const in_value
;
167 for (int i
= 0; i
< SIZE(gold_wire
); i
++)
168 in_value
.bits
.push_back(xorshift32(2) ? RTLIL::S1
: RTLIL::S0
);
170 if (xorshift32(4) == 0) {
171 int inv_chance
= 1 + xorshift32(8);
172 for (int i
= 0; i
< SIZE(gold_wire
); i
++)
173 if (xorshift32(inv_chance
) == 0)
174 in_value
.bits
[i
] = RTLIL::Sx
;
178 log("%s: %s\n", log_id(gold_wire
), log_signal(in_value
));
180 in_sig
.append(gold_wire
);
181 in_val
.append(in_value
);
183 gold_ce
.set(gold_wire
, in_value
);
184 gate_ce
.set(gate_wire
, in_value
);
187 for (auto port
: gold_mod
->ports
)
189 RTLIL::Wire
*gold_wire
= gold_mod
->wire(port
);
190 RTLIL::Wire
*gate_wire
= gate_mod
->wire(port
);
192 log_assert(gold_wire
!= nullptr);
193 log_assert(gate_wire
!= nullptr);
194 log_assert(gold_wire
->port_output
== gate_wire
->port_output
);
195 log_assert(SIZE(gold_wire
) == SIZE(gate_wire
));
197 if (!gold_wire
->port_output
)
200 RTLIL::SigSpec
gold_outval(gold_wire
);
201 RTLIL::SigSpec
gate_outval(gate_wire
);
203 if (!gold_ce
.eval(gold_outval
))
204 log_error("Failed to eval %s in gold module.\n", log_id(gold_wire
));
206 if (!gate_ce
.eval(gate_outval
))
207 log_error("Failed to eval %s in gate module.\n", log_id(gate_wire
));
209 bool gold_gate_mismatch
= false;
210 for (int i
= 0; i
< SIZE(gold_wire
); i
++) {
211 if (gold_outval
[i
] == RTLIL::Sx
)
213 if (gold_outval
[i
] == gate_outval
[i
])
215 gold_gate_mismatch
= true;
219 if (gold_gate_mismatch
)
220 log_error("Mismatch in output %s: gold:%s != gate:%s\n", log_id(gate_wire
), log_signal(gold_outval
), log_signal(gate_outval
));
223 log("%s: %s\n", log_id(gold_wire
), log_signal(gold_outval
));
225 out_sig
.append(gold_wire
);
226 out_val
.append(gold_outval
);
230 log("EVAL: %s\n", out_val
.as_string().c_str());
232 std::vector
<int> sat1_in_sig
= satgen1
.importSigSpec(in_sig
);
233 std::vector
<int> sat1_in_val
= satgen1
.importSigSpec(in_val
);
235 std::vector
<int> sat1_model
= satgen1
.importSigSpec(out_sig
);
236 std::vector
<bool> sat1_model_value
;
238 if (!ez1
.solve(sat1_model
, sat1_model_value
, ez1
.vec_eq(sat1_in_sig
, sat1_in_val
)))
239 log_error("Evaluating sat model 1 (no undef modeling) failed!\n");
243 for (int i
= SIZE(out_sig
)-1; i
>= 0; i
--)
244 log("%c", sat1_model_value
.at(i
) ? '1' : '0');
248 for (int i
= 0; i
< SIZE(out_sig
); i
++) {
249 if (out_val
[i
] != RTLIL::S0
&& out_val
[i
] != RTLIL::S1
)
251 if (out_val
[i
] == RTLIL::S0
&& sat1_model_value
.at(i
) == false)
253 if (out_val
[i
] == RTLIL::S1
&& sat1_model_value
.at(i
) == true)
255 log_error("Mismatch in sat model 1 (no undef modeling) output!\n");
258 std::vector
<int> sat2_in_def_sig
= satgen2
.importDefSigSpec(in_sig
);
259 std::vector
<int> sat2_in_def_val
= satgen2
.importDefSigSpec(in_val
);
261 std::vector
<int> sat2_in_undef_sig
= satgen2
.importUndefSigSpec(in_sig
);
262 std::vector
<int> sat2_in_undef_val
= satgen2
.importUndefSigSpec(in_val
);
264 std::vector
<int> sat2_model_def_sig
= satgen2
.importDefSigSpec(out_sig
);
265 std::vector
<int> sat2_model_undef_sig
= satgen2
.importUndefSigSpec(out_sig
);
267 std::vector
<int> sat2_model
;
268 sat2_model
.insert(sat2_model
.end(), sat2_model_def_sig
.begin(), sat2_model_def_sig
.end());
269 sat2_model
.insert(sat2_model
.end(), sat2_model_undef_sig
.begin(), sat2_model_undef_sig
.end());
271 std::vector
<bool> sat2_model_value
;
273 if (!ez2
.solve(sat2_model
, sat2_model_value
, ez2
.vec_eq(sat2_in_def_sig
, sat2_in_def_val
), ez2
.vec_eq(sat2_in_undef_sig
, sat2_in_undef_val
)))
274 log_error("Evaluating sat model 2 (undef modeling) failed!\n");
278 for (int i
= SIZE(out_sig
)-1; i
>= 0; i
--)
279 log("%c", sat2_model_value
.at(SIZE(out_sig
) + i
) ? 'x' : sat2_model_value
.at(i
) ? '1' : '0');
283 for (int i
= 0; i
< SIZE(out_sig
); i
++) {
284 if (sat2_model_value
.at(SIZE(out_sig
) + i
)) {
285 if (out_val
[i
] != RTLIL::S0
&& out_val
[i
] != RTLIL::S1
)
288 if (out_val
[i
] == RTLIL::S0
&& sat2_model_value
.at(i
) == false)
290 if (out_val
[i
] == RTLIL::S1
&& sat2_model_value
.at(i
) == true)
293 log_error("Mismatch in sat model 2 (undef modeling) output!\n");
301 struct TestCellPass
: public Pass
{
302 TestCellPass() : Pass("test_cell", "automatically test the implementation of a cell type") { }
305 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
307 log(" test_cell [options] {cell-types}\n");
309 log("Tests the internal implementation of the given cell type (for example '$mux')\n");
310 log("by comparing SAT solver, EVAL and TECHMAP implementations of the cell types..\n");
312 log("Run with 'all' instead of a cell type to run the test on all supported\n");
313 log("cell types.\n");
315 log(" -n {integer}\n");
316 log(" create this number of cell instances and test them (default = 100).\n");
318 log(" -s {positive_integer}\n");
319 log(" use this value as rng seed value (default = unix time).\n");
321 log(" -f {ilang_file}\n");
322 log(" don't generate circuits. instead load the specified ilang file.\n");
324 log(" -map {filename}\n");
325 log(" pass this option to techmap.\n");
328 log(" use \"techmap -map +/simlib.v -max_iter 2 -autoproc\"\n");
331 log(" print additional debug information to the console\n");
334 virtual void execute(std::vector
<std::string
> args
, RTLIL::Design
*)
337 std::string techmap_cmd
= "techmap -assert";
338 std::string ilang_file
;
339 xorshift32_state
= 0;
340 bool verbose
= false;
343 for (argidx
= 1; argidx
< SIZE(args
); argidx
++)
345 if (args
[argidx
] == "-n" && argidx
+1 < SIZE(args
)) {
346 num_iter
= atoi(args
[++argidx
].c_str());
349 if (args
[argidx
] == "-s" && argidx
+1 < SIZE(args
)) {
350 xorshift32_state
= atoi(args
[++argidx
].c_str());
353 if (args
[argidx
] == "-map" && argidx
+1 < SIZE(args
)) {
354 techmap_cmd
+= " -map " + args
[++argidx
];
357 if (args
[argidx
] == "-f" && argidx
+1 < SIZE(args
)) {
358 ilang_file
= args
[++argidx
];
362 if (args
[argidx
] == "-simlib") {
363 techmap_cmd
= "techmap -map +/simlib.v -max_iter 2 -autoproc";
366 if (args
[argidx
] == "-v") {
373 if (xorshift32_state
== 0)
374 xorshift32_state
= time(NULL
);
376 std::map
<std::string
, std::string
> cell_types
;
377 std::vector
<std::string
> selected_cell_types
;
379 cell_types
["$not"] = "ASY";
380 cell_types
["$pos"] = "ASY";
381 cell_types
["$bu0"] = "ASY";
382 cell_types
["$neg"] = "ASY";
384 cell_types
["$and"] = "ABSY";
385 cell_types
["$or"] = "ABSY";
386 cell_types
["$xor"] = "ABSY";
387 cell_types
["$xnor"] = "ABSY";
389 cell_types
["$reduce_and"] = "ASY";
390 cell_types
["$reduce_or"] = "ASY";
391 cell_types
["$reduce_xor"] = "ASY";
392 cell_types
["$reduce_xnor"] = "ASY";
393 cell_types
["$reduce_bool"] = "ASY";
395 cell_types
["$shl"] = "ABshY";
396 cell_types
["$shr"] = "ABshY";
397 cell_types
["$sshl"] = "ABshY";
398 cell_types
["$sshr"] = "ABshY";
399 cell_types
["$shift"] = "ABshY";
400 cell_types
["$shiftx"] = "ABshY";
402 cell_types
["$lt"] = "ABSY";
403 cell_types
["$le"] = "ABSY";
404 cell_types
["$eq"] = "ABSY";
405 cell_types
["$ne"] = "ABSY";
406 // cell_types["$eqx"] = "ABSY";
407 // cell_types["$nex"] = "ABSY";
408 cell_types
["$ge"] = "ABSY";
409 cell_types
["$gt"] = "ABSY";
411 cell_types
["$add"] = "ABSY";
412 cell_types
["$sub"] = "ABSY";
413 cell_types
["$mul"] = "ABSY";
414 cell_types
["$div"] = "ABSY";
415 cell_types
["$mod"] = "ABSY";
416 // cell_types["$pow"] = "ABsY";
418 cell_types
["$logic_not"] = "ASY";
419 cell_types
["$logic_and"] = "ABSY";
420 cell_types
["$logic_or"] = "ABSY";
422 // cell_types["$mux"] = "A";
423 // cell_types["$pmux"] = "A";
424 // cell_types["$slice"] = "A";
425 // cell_types["$concat"] = "A";
426 // cell_types["$assert"] = "A";
428 cell_types
["$lut"] = "*";
429 cell_types
["$alu"] = "ABSY";
431 for (; argidx
< SIZE(args
); argidx
++)
433 if (args
[argidx
].rfind("-", 0) == 0)
434 log_cmd_error("Unexpected option: %s\n", args
[argidx
].c_str());
436 if (args
[argidx
] == "all") {
437 for (auto &it
: cell_types
)
438 if (std::count(selected_cell_types
.begin(), selected_cell_types
.end(), it
.first
) == 0)
439 selected_cell_types
.push_back(it
.first
);
443 if (cell_types
.count(args
[argidx
]) == 0) {
444 std::string cell_type_list
;
446 for (auto &it
: cell_types
) {
447 if (charcount
> 60) {
448 cell_type_list
+= "\n" + it
.first
;
451 cell_type_list
+= " " + it
.first
;
452 charcount
+= SIZE(it
.first
);
454 log_cmd_error("The cell type `%s' is currently not supported. Try one of these:%s\n",
455 args
[argidx
].c_str(), cell_type_list
.c_str());
458 if (std::count(selected_cell_types
.begin(), selected_cell_types
.end(), args
[argidx
]) == 0)
459 selected_cell_types
.push_back(args
[argidx
]);
462 if (!ilang_file
.empty()) {
463 if (!selected_cell_types
.empty())
464 log_cmd_error("Do not specify any cell types when using -f.\n");
465 selected_cell_types
.push_back("ilang");
468 if (selected_cell_types
.empty())
469 log_cmd_error("No cell type to test specified.\n");
471 for (auto cell_type
: selected_cell_types
)
472 for (int i
= 0; i
< num_iter
; i
++)
474 RTLIL::Design
*design
= new RTLIL::Design
;
475 if (cell_type
== "ilang")
476 Frontend::frontend_call(design
, NULL
, std::string(), "ilang " + ilang_file
);
478 create_gold_module(design
, cell_type
, cell_types
.at(cell_type
));
479 Pass::call(design
, stringf("copy gold gate; %s gate; opt gate", techmap_cmd
.c_str()));
480 Pass::call(design
, "miter -equiv -flatten -make_outputs -ignore_gold_x gold gate miter");
482 Pass::call(design
, "dump gate");
483 Pass::call(design
, "dump gold");
484 Pass::call(design
, "sat -verify -enable_undef -prove trigger 0 -show-inputs -show-outputs miter");
485 run_eval_test(design
, verbose
);