2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
6 * Permission to use, copy, modify, and/or distribute this software for any
7 * purpose with or without fee is hereby granted, provided that the above
8 * copyright notice and this permission notice appear in all copies.
10 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
11 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
12 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
13 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
14 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
15 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
16 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
20 // [[CITE]] VlogHammer Verilog Regression Test Suite
21 // https://yosyshq.net/yosys/vloghammer.html
23 #include "kernel/register.h"
24 #include "kernel/celltypes.h"
25 #include "kernel/consteval.h"
26 #include "kernel/sigtools.h"
27 #include "kernel/satgen.h"
28 #include "kernel/log.h"
35 PRIVATE_NAMESPACE_BEGIN
37 /* this should only be used for regression testing of ConstEval -- see vloghammer */
38 struct BruteForceEquivChecker
40 RTLIL::Module
*mod1
, *mod2
;
41 RTLIL::SigSpec mod1_inputs
, mod1_outputs
;
42 RTLIL::SigSpec mod2_inputs
, mod2_outputs
;
46 void run_checker(RTLIL::SigSpec
&inputs
)
48 if (inputs
.size() < mod1_inputs
.size()) {
49 RTLIL::SigSpec inputs0
= inputs
, inputs1
= inputs
;
50 inputs0
.append(State::S0
);
51 inputs1
.append(State::S1
);
57 ConstEval
ce1(mod1
), ce2(mod2
);
58 ce1
.set(mod1_inputs
, inputs
.as_const());
59 ce2
.set(mod2_inputs
, inputs
.as_const());
61 RTLIL::SigSpec sig1
= mod1_outputs
, undef1
;
62 RTLIL::SigSpec sig2
= mod2_outputs
, undef2
;
64 if (!ce1
.eval(sig1
, undef1
))
65 log("Failed ConstEval of module 1 outputs at signal %s (input: %s = %s).\n",
66 log_signal(undef1
), log_signal(mod1_inputs
), log_signal(inputs
));
67 if (!ce2
.eval(sig2
, undef2
))
68 log("Failed ConstEval of module 2 outputs at signal %s (input: %s = %s).\n",
69 log_signal(undef2
), log_signal(mod1_inputs
), log_signal(inputs
));
72 for (int i
= 0; i
< GetSize(sig1
); i
++)
73 if (sig1
[i
] == RTLIL::State::Sx
)
74 sig2
[i
] = RTLIL::State::Sx
;
78 log("Found counter-example (ignore_x_mod1 = %s):\n", ignore_x_mod1
? "active" : "inactive");
79 log(" Module 1: %s = %s => %s = %s\n", log_signal(mod1_inputs
), log_signal(inputs
), log_signal(mod1_outputs
), log_signal(sig1
));
80 log(" Module 2: %s = %s => %s = %s\n", log_signal(mod2_inputs
), log_signal(inputs
), log_signal(mod2_outputs
), log_signal(sig2
));
87 BruteForceEquivChecker(RTLIL::Module
*mod1
, RTLIL::Module
*mod2
, bool ignore_x_mod1
) :
88 mod1(mod1
), mod2(mod2
), counter(0), errors(0), ignore_x_mod1(ignore_x_mod1
)
90 log("Checking for equivalence (brute-force): %s vs %s\n", mod1
->name
.c_str(), mod2
->name
.c_str());
91 for (auto w
: mod1
->wires())
96 if (mod2
->wire(w
->name
) == nullptr)
97 log_cmd_error("Port %s in module 1 has no counterpart in module 2!\n", w
->name
.c_str());
99 RTLIL::Wire
*w2
= mod2
->wire(w
->name
);
100 if (w
->width
!= w2
->width
|| w
->port_input
!= w2
->port_input
|| w
->port_output
!= w2
->port_output
)
101 log_cmd_error("Port %s in module 1 does not match its counterpart in module 2!\n", w
->name
.c_str());
104 mod1_inputs
.append(w
);
105 mod2_inputs
.append(w2
);
107 mod1_outputs
.append(w
);
108 mod2_outputs
.append(w2
);
112 RTLIL::SigSpec inputs
;
117 /* this should only be used for regression testing of ConstEval -- see vloghammer */
118 struct VlogHammerReporter
120 RTLIL::Design
*design
;
121 std::vector
<RTLIL::Module
*> modules
;
122 std::vector
<std::string
> module_names
;
123 std::vector
<RTLIL::IdString
> inputs
;
124 std::vector
<int> input_widths
;
125 std::vector
<RTLIL::Const
> patterns
;
126 int total_input_width
;
128 std::vector
<std::string
> split(std::string text
, const char *delim
)
130 std::vector
<std::string
> list
;
131 char *p
= strdup(text
.c_str());
132 char *t
= strtok(p
, delim
);
135 t
= strtok(NULL
, delim
);
141 void sat_check(RTLIL::Module
*module
, RTLIL::SigSpec recorded_set_vars
, RTLIL::Const recorded_set_vals
, RTLIL::SigSpec expected_y
, bool model_undef
)
143 log("Verifying SAT model (%s)..\n", model_undef
? "with undef" : "without undef");
146 SigMap
sigmap(module
);
147 SatGen
satgen(ez
.get(), &sigmap
);
148 satgen
.model_undef
= model_undef
;
150 for (auto c
: module
->cells())
151 if (!satgen
.importCell(c
))
152 log_error("Failed to import cell %s (type %s) to SAT database.\n", log_id(c
->name
), log_id(c
->type
));
154 ez
->assume(satgen
.signals_eq(recorded_set_vars
, recorded_set_vals
));
156 std::vector
<int> y_vec
= satgen
.importDefSigSpec(module
->wire(ID(y
)));
157 std::vector
<bool> y_values
;
160 std::vector
<int> y_undef_vec
= satgen
.importUndefSigSpec(module
->wire(ID(y
)));
161 y_vec
.insert(y_vec
.end(), y_undef_vec
.begin(), y_undef_vec
.end());
164 log(" Created SAT problem with %d variables and %d clauses.\n",
165 ez
->numCnfVariables(), ez
->numCnfClauses());
167 if (!ez
->solve(y_vec
, y_values
))
168 log_error("Failed to find solution to SAT problem.\n");
170 for (int i
= 0; i
< expected_y
.size(); i
++) {
171 RTLIL::State solution_bit
= y_values
.at(i
) ? RTLIL::State::S1
: RTLIL::State::S0
;
172 RTLIL::State expected_bit
= expected_y
[i
].data
;
174 if (y_values
.at(expected_y
.size()+i
))
175 solution_bit
= RTLIL::State::Sx
;
177 if (expected_bit
== RTLIL::State::Sx
)
180 if (solution_bit
!= expected_bit
) {
181 std::string sat_bits
, rtl_bits
;
182 for (int k
= expected_y
.size()-1; k
>= 0; k
--) {
183 if (model_undef
&& y_values
.at(expected_y
.size()+k
))
186 sat_bits
+= y_values
.at(k
) ? "1" : "0";
187 rtl_bits
+= expected_y
[k
] == RTLIL::State::Sx
? "x" : expected_y
[k
] == RTLIL::State::S1
? "1" : "0";
189 log_error("Found error in SAT model: y[%d] = %s, should be %s:\n SAT: %s\n RTL: %s\n %*s^\n",
190 int(i
), log_signal(solution_bit
), log_signal(expected_bit
),
191 sat_bits
.c_str(), rtl_bits
.c_str(), expected_y
.size()-i
-1, "");
197 std::vector
<int> cmp_vars
;
198 std::vector
<bool> cmp_vals
;
200 std::vector
<bool> y_undef(y_values
.begin() + expected_y
.size(), y_values
.end());
202 for (int i
= 0; i
< expected_y
.size(); i
++)
205 log(" Toggling undef bit %d to test undef gating.\n", i
);
206 if (!ez
->solve(y_vec
, y_values
, ez
->IFF(y_vec
.at(i
), y_values
.at(i
) ? ez
->CONST_FALSE
: ez
->CONST_TRUE
)))
207 log_error("Failed to find solution with toggled bit!\n");
209 cmp_vars
.push_back(y_vec
.at(expected_y
.size() + i
));
210 cmp_vals
.push_back(true);
214 cmp_vars
.push_back(y_vec
.at(i
));
215 cmp_vals
.push_back(y_values
.at(i
));
217 cmp_vars
.push_back(y_vec
.at(expected_y
.size() + i
));
218 cmp_vals
.push_back(false);
221 log(" Testing if SAT solution is unique.\n");
222 ez
->assume(ez
->vec_ne(cmp_vars
, ez
->vec_const(cmp_vals
)));
223 if (ez
->solve(y_vec
, y_values
))
224 log_error("Found two distinct solutions to SAT problem.\n");
228 log(" Testing if SAT solution is unique.\n");
229 ez
->assume(ez
->vec_ne(y_vec
, ez
->vec_const(y_values
)));
230 if (ez
->solve(y_vec
, y_values
))
231 log_error("Found two distinct solutions to SAT problem.\n");
234 log(" SAT model verified.\n");
239 for (int idx
= 0; idx
< int(patterns
.size()); idx
++)
241 log("Creating report for pattern %d: %s\n", idx
, log_signal(patterns
[idx
]));
242 std::string input_pattern_list
;
243 RTLIL::SigSpec rtl_sig
;
245 for (int mod
= 0; mod
< int(modules
.size()); mod
++)
247 RTLIL::SigSpec recorded_set_vars
;
248 RTLIL::Const recorded_set_vals
;
249 RTLIL::Module
*module
= modules
[mod
];
250 std::string module_name
= module_names
[mod
].c_str();
251 ConstEval
ce(module
);
253 std::vector
<RTLIL::State
> bits(patterns
[idx
].bits
.begin(), patterns
[idx
].bits
.begin() + total_input_width
);
254 for (int i
= 0; i
< int(inputs
.size()); i
++) {
255 RTLIL::Wire
*wire
= module
->wire(inputs
[i
]);
256 for (int j
= input_widths
[i
]-1; j
>= 0; j
--) {
257 ce
.set(RTLIL::SigSpec(wire
, j
), bits
.back());
258 recorded_set_vars
.append(RTLIL::SigSpec(wire
, j
));
259 recorded_set_vals
.bits
.push_back(bits
.back());
262 if (module
== modules
.front()) {
263 RTLIL::SigSpec
sig(wire
);
265 log_error("Can't read back value for port %s!\n", log_id(inputs
[i
]));
266 input_pattern_list
+= stringf(" %s", sig
.as_const().as_string().c_str());
267 log("++PAT++ %d %s %s #\n", idx
, log_id(inputs
[i
]), sig
.as_const().as_string().c_str());
271 if (module
->wire(ID(y
)) == nullptr)
272 log_error("No output wire (y) found in module %s!\n", log_id(module
->name
));
274 RTLIL::SigSpec
sig(module
->wire(ID(y
)));
275 RTLIL::SigSpec undef
;
277 while (!ce
.eval(sig
, undef
)) {
278 // log_error("Evaluation of y in module %s failed: sig=%s, undef=%s\n", log_id(module->name), log_signal(sig), log_signal(undef));
279 log_warning("Setting signal %s in module %s to undef.\n", log_signal(undef
), log_id(module
->name
));
280 ce
.set(undef
, RTLIL::Const(RTLIL::State::Sx
, undef
.size()));
283 log("++VAL++ %d %s %s #\n", idx
, module_name
.c_str(), sig
.as_const().as_string().c_str());
285 if (module_name
== "rtl") {
287 sat_check(module
, recorded_set_vars
, recorded_set_vals
, sig
, false);
288 sat_check(module
, recorded_set_vars
, recorded_set_vals
, sig
, true);
289 } else if (rtl_sig
.size() > 0) {
290 if (rtl_sig
.size() != sig
.size())
291 log_error("Output (y) has a different width in module %s compared to rtl!\n", log_id(module
->name
));
292 for (int i
= 0; i
< GetSize(sig
); i
++)
293 if (rtl_sig
[i
] == RTLIL::State::Sx
)
294 sig
[i
] = RTLIL::State::Sx
;
297 log("++RPT++ %d%s %s %s\n", idx
, input_pattern_list
.c_str(), sig
.as_const().as_string().c_str(), module_name
.c_str());
300 log("++RPT++ ----\n");
305 VlogHammerReporter(RTLIL::Design
*design
, std::string module_prefix
, std::string module_list
, std::string input_list
, std::string pattern_list
) : design(design
)
307 for (auto name
: split(module_list
, ",")) {
308 RTLIL::IdString esc_name
= RTLIL::escape_id(module_prefix
+ name
);
309 if (design
->module(esc_name
) == nullptr)
310 log_error("Can't find module %s in current design!\n", name
.c_str());
311 log("Using module %s (%s).\n", esc_name
.c_str(), name
.c_str());
312 modules
.push_back(design
->module(esc_name
));
313 module_names
.push_back(name
);
316 total_input_width
= 0;
317 for (auto name
: split(input_list
, ",")) {
319 RTLIL::IdString esc_name
= RTLIL::escape_id(name
);
320 for (auto mod
: modules
) {
321 if (mod
->wire(esc_name
) == nullptr)
322 log_error("Can't find input %s in module %s!\n", name
.c_str(), log_id(mod
->name
));
323 RTLIL::Wire
*port
= mod
->wire(esc_name
);
324 if (!port
->port_input
|| port
->port_output
)
325 log_error("Wire %s in module %s is not an input!\n", name
.c_str(), log_id(mod
->name
));
326 if (width
>= 0 && width
!= port
->width
)
327 log_error("Port %s has different sizes in the different modules!\n", name
.c_str());
330 log("Using input port %s with width %d.\n", esc_name
.c_str(), width
);
331 inputs
.push_back(esc_name
);
332 input_widths
.push_back(width
);
333 total_input_width
+= width
;
336 for (auto pattern
: split(pattern_list
, ",")) {
338 bool invert_pattern
= false;
339 if (pattern
.size() > 0 && pattern
[0] == '~') {
340 invert_pattern
= true;
341 pattern
= pattern
.substr(1);
343 if (!RTLIL::SigSpec::parse(sig
, NULL
, pattern
) || !sig
.is_fully_const())
344 log_error("Failed to parse pattern %s!\n", pattern
.c_str());
345 if (sig
.size() < total_input_width
)
346 log_error("Pattern %s is to short!\n", pattern
.c_str());
347 patterns
.push_back(sig
.as_const());
348 if (invert_pattern
) {
349 for (auto &bit
: patterns
.back().bits
)
350 if (bit
== RTLIL::State::S0
)
351 bit
= RTLIL::State::S1
;
352 else if (bit
== RTLIL::State::S1
)
353 bit
= RTLIL::State::S0
;
355 log("Using pattern %s.\n", patterns
.back().as_string().c_str());
360 struct EvalPass
: public Pass
{
361 EvalPass() : Pass("eval", "evaluate the circuit given an input") { }
364 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
366 log(" eval [options] [selection]\n");
368 log("This command evaluates the value of a signal given the value of all required\n");
371 log(" -set <signal> <value>\n");
372 log(" set the specified signal to the specified value.\n");
374 log(" -set-undef\n");
375 log(" set all unspecified source signals to undef (x)\n");
377 log(" -table <signal>\n");
378 log(" create a truth table using the specified input signals\n");
380 log(" -show <signal>\n");
381 log(" show the value for the specified signal. if no -show option is passed\n");
382 log(" then all output ports of the current module are used.\n");
385 void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
) override
387 std::vector
<std::pair
<std::string
, std::string
>> sets
;
388 std::vector
<std::string
> shows
, tables
;
389 bool set_undef
= false;
391 log_header(design
, "Executing EVAL pass (evaluate the circuit given an input).\n");
394 for (argidx
= 1; argidx
< args
.size(); argidx
++) {
395 if (args
[argidx
] == "-set" && argidx
+2 < args
.size()) {
396 std::string lhs
= args
[++argidx
].c_str();
397 std::string rhs
= args
[++argidx
].c_str();
398 sets
.push_back(std::pair
<std::string
, std::string
>(lhs
, rhs
));
401 if (args
[argidx
] == "-set-undef") {
405 if (args
[argidx
] == "-show" && argidx
+1 < args
.size()) {
406 shows
.push_back(args
[++argidx
]);
409 if (args
[argidx
] == "-table" && argidx
+1 < args
.size()) {
410 tables
.push_back(args
[++argidx
]);
413 if ((args
[argidx
] == "-brute_force_equiv_checker" || args
[argidx
] == "-brute_force_equiv_checker_x") && argidx
+3 == args
.size()) {
414 /* this should only be used for regression testing of ConstEval -- see vloghammer */
415 std::string mod1_name
= RTLIL::escape_id(args
[++argidx
]);
416 std::string mod2_name
= RTLIL::escape_id(args
[++argidx
]);
417 if (design
->module(mod1_name
) == nullptr)
418 log_error("Can't find module `%s'!\n", mod1_name
.c_str());
419 if (design
->module(mod2_name
) == nullptr)
420 log_error("Can't find module `%s'!\n", mod2_name
.c_str());
421 BruteForceEquivChecker
checker(design
->module(mod1_name
), design
->module(mod2_name
), args
[argidx
-2] == "-brute_force_equiv_checker_x");
422 if (checker
.errors
> 0)
423 log_cmd_error("Modules are not equivalent!\n");
424 log("Verified %s = %s (using brute-force check on %d cases).\n",
425 mod1_name
.c_str(), mod2_name
.c_str(), checker
.counter
);
428 if (args
[argidx
] == "-vloghammer_report" && argidx
+5 == args
.size()) {
429 /* this should only be used for regression testing of ConstEval -- see vloghammer */
430 std::string module_prefix
= args
[++argidx
];
431 std::string module_list
= args
[++argidx
];
432 std::string input_list
= args
[++argidx
];
433 std::string pattern_list
= args
[++argidx
];
434 VlogHammerReporter
reporter(design
, module_prefix
, module_list
, input_list
, pattern_list
);
440 extra_args(args
, argidx
, design
);
442 RTLIL::Module
*module
= NULL
;
443 for (auto mod
: design
->selected_modules()) {
445 log_cmd_error("Only one module must be selected for the EVAL pass! (selected: %s and %s)\n",
446 log_id(module
->name
), log_id(mod
->name
));
450 log_cmd_error("Can't perform EVAL on an empty selection!\n");
452 ConstEval
ce(module
);
454 for (auto &it
: sets
) {
455 RTLIL::SigSpec lhs
, rhs
;
456 if (!RTLIL::SigSpec::parse_sel(lhs
, design
, module
, it
.first
))
457 log_cmd_error("Failed to parse lhs set expression `%s'.\n", it
.first
.c_str());
458 if (!RTLIL::SigSpec::parse_rhs(lhs
, rhs
, module
, it
.second
))
459 log_cmd_error("Failed to parse rhs set expression `%s'.\n", it
.second
.c_str());
460 if (!rhs
.is_fully_const())
461 log_cmd_error("Right-hand-side set expression `%s' is not constant.\n", it
.second
.c_str());
462 if (lhs
.size() != rhs
.size())
463 log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
464 it
.first
.c_str(), log_signal(lhs
), lhs
.size(), it
.second
.c_str(), log_signal(rhs
), rhs
.size());
465 ce
.set(lhs
, rhs
.as_const());
468 if (shows
.size() == 0) {
469 for (auto w
: module
->wires())
471 shows
.push_back(w
->name
.str());
476 for (auto &it
: shows
) {
477 RTLIL::SigSpec signal
, value
, undef
;
478 if (!RTLIL::SigSpec::parse_sel(signal
, design
, module
, it
))
479 log_cmd_error("Failed to parse show expression `%s'.\n", it
.c_str());
482 while (!ce
.eval(value
, undef
)) {
483 log("Failed to evaluate signal %s: Missing value for %s. -> setting to undef\n", log_signal(signal
), log_signal(undef
));
484 ce
.set(undef
, RTLIL::Const(RTLIL::State::Sx
, undef
.size()));
485 undef
= RTLIL::SigSpec();
487 log("Eval result: %s = %s.\n", log_signal(signal
), log_signal(value
));
489 if (!ce
.eval(value
, undef
))
490 log("Failed to evaluate signal %s: Missing value for %s.\n", log_signal(signal
), log_signal(undef
));
492 log("Eval result: %s = %s.\n", log_signal(signal
), log_signal(value
));
498 RTLIL::SigSpec tabsigs
, signal
, value
, undef
;
499 std::vector
<std::vector
<std::string
>> tab
;
500 int tab_sep_colidx
= 0;
502 for (auto &it
: shows
) {
504 if (!RTLIL::SigSpec::parse_sel(sig
, design
, module
, it
))
505 log_cmd_error("Failed to parse show expression `%s'.\n", it
.c_str());
509 for (auto &it
: tables
) {
511 if (!RTLIL::SigSpec::parse_sel(sig
, design
, module
, it
))
512 log_cmd_error("Failed to parse table expression `%s'.\n", it
.c_str());
516 std::vector
<std::string
> tab_line
;
517 for (auto &c
: tabsigs
.chunks())
518 tab_line
.push_back(log_signal(c
));
519 tab_sep_colidx
= tab_line
.size();
520 for (auto &c
: signal
.chunks())
521 tab_line
.push_back(log_signal(c
));
522 tab
.push_back(tab_line
);
525 RTLIL::Const
tabvals(0, tabsigs
.size());
529 ce
.set(tabsigs
, tabvals
);
532 RTLIL::SigSpec this_undef
;
533 while (!ce
.eval(value
, this_undef
)) {
535 log("Failed to evaluate signal %s at %s = %s: Missing value for %s.\n", log_signal(signal
),
536 log_signal(tabsigs
), log_signal(tabvals
), log_signal(this_undef
));
539 ce
.set(this_undef
, RTLIL::Const(RTLIL::State::Sx
, this_undef
.size()));
540 undef
.append(this_undef
);
541 this_undef
= RTLIL::SigSpec();
545 for (auto &c
: tabsigs
.chunks()) {
546 tab_line
.push_back(log_signal(RTLIL::SigSpec(tabvals
).extract(pos
, c
.width
)));
551 for (auto &c
: signal
.chunks()) {
552 tab_line
.push_back(log_signal(value
.extract(pos
, c
.width
)));
556 tab
.push_back(tab_line
);
560 tabvals
= RTLIL::const_add(tabvals
, RTLIL::Const(1), false, false, tabvals
.bits
.size());
562 while (tabvals
.as_bool());
564 std::vector
<int> tab_column_width
;
565 for (auto &row
: tab
) {
566 if (tab_column_width
.size() < row
.size())
567 tab_column_width
.resize(row
.size());
568 for (size_t i
= 0; i
< row
.size(); i
++)
569 tab_column_width
[i
] = max(tab_column_width
[i
], int(row
[i
].size()));
574 for (auto &row
: tab
) {
575 for (size_t i
= 0; i
< row
.size(); i
++) {
576 int k
= int(i
) < tab_sep_colidx
? tab_sep_colidx
- i
- 1 : i
;
577 log(" %s%*s", k
== tab_sep_colidx
? "| " : "", tab_column_width
[k
], row
[k
].c_str());
581 for (size_t i
= 0; i
< row
.size(); i
++) {
582 int k
= int(i
) < tab_sep_colidx
? tab_sep_colidx
- i
- 1 : i
;
583 log(" %s", k
== tab_sep_colidx
? "| " : "");
584 for (int j
= 0; j
< tab_column_width
[k
]; j
++)
593 if (undef
.size() > 0) {
594 undef
.sort_and_unify();
595 log("Assumed undef (x) value for the following signals: %s\n\n", log_signal(undef
));
601 PRIVATE_NAMESPACE_END