projects / yosys.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Added sat -show-inputs and -show-outputs
[yosys.git] / passes / sat / sat.cc
1 /*
2 * yosys -- Yosys Open SYnthesis Suite
3 *
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
5 *
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.
9 *
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.
17 *
18 */
19
20 // [[CITE]] Temporal Induction by Incremental SAT Solving
21 // Niklas Een and Niklas Sörensson (2003)
22 // http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.8161
23
24 #include "kernel/register.h"
25 #include "kernel/celltypes.h"
26 #include "kernel/consteval.h"
27 #include "kernel/sigtools.h"
28 #include "kernel/log.h"
29 #include "kernel/satgen.h"
30 #include <stdlib.h>
31 #include <stdio.h>
32 #include <algorithm>
33
34 namespace {
35
36 struct SatHelper
37 {
38 RTLIL::Design *design;
39 RTLIL::Module *module;
40
41 ezDefaultSAT ez;
42 SigMap sigmap;
43 CellTypes ct;
44 SatGen satgen;
45
46 // additional constraints
47 std::vector<std::pair<std::string, std::string>> sets, prove, prove_x, sets_init;
48 std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
49 std::map<int, std::vector<std::string>> unsets_at;
50 bool prove_asserts;
51
52 // undef constraints
53 bool enable_undef, set_init_undef;
54 std::vector<std::string> sets_def, sets_any_undef, sets_all_undef;
55 std::map<int, std::vector<std::string>> sets_def_at, sets_any_undef_at, sets_all_undef_at;
56
57 // model variables
58 std::vector<std::string> shows;
59 SigPool show_signal_pool;
60 SigSet<RTLIL::Cell*> show_drivers;
61 int max_timestep, timeout;
62 bool gotTimeout;
63
64 SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) :
65 design(design), module(module), sigmap(module), ct(design), satgen(&ez, &sigmap)
66 {
67 this->enable_undef = enable_undef;
68 satgen.model_undef = enable_undef;
69 set_init_undef = false;
70 max_timestep = -1;
71 timeout = 0;
72 gotTimeout = false;
73 }
74
75 void check_undef_enabled(const RTLIL::SigSpec &sig)
76 {
77 if (enable_undef)
78 return;
79
80 std::vector<RTLIL::SigBit> sigbits = sig.to_sigbit_vector();
81 for (size_t i = 0; i < sigbits.size(); i++)
82 if (sigbits[i].wire == NULL && sigbits[i].data == RTLIL::State::Sx)
83 log_cmd_error("Bit %d of %s is undef but option -enable_undef is missing!\n", int(i), log_signal(sig));
84 }
85
86 void setup_init()
87 {
88 log ("\nSetting up initial state:\n");
89
90 RTLIL::SigSpec big_lhs, big_rhs;
91
92 for (auto &s : sets_init)
93 {
94 RTLIL::SigSpec lhs, rhs;
95
96 if (!RTLIL::SigSpec::parse(lhs, module, s.first))
97 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
98 if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
99 log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
100 show_signal_pool.add(sigmap(lhs));
101 show_signal_pool.add(sigmap(rhs));
102
103 if (lhs.width != rhs.width)
104 log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
105 s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
106
107 log("Import set-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
108 big_lhs.remove2(lhs, &big_rhs);
109 big_lhs.append(lhs);
110 big_rhs.append(rhs);
111 }
112
113 if (!satgen.initial_state.check_all(big_lhs)) {
114 RTLIL::SigSpec rem = satgen.initial_state.remove(big_lhs);
115 rem.optimize();
116 log_cmd_error("Found -set-init bits that are not part of the initial_state: %s\n", log_signal(rem));
117 }
118
119 if (set_init_undef) {
120 RTLIL::SigSpec rem = satgen.initial_state.export_all();
121 rem.remove(big_lhs);
122 big_lhs.append(rem);
123 big_rhs.append(RTLIL::SigSpec(RTLIL::State::Sx, rem.width));
124 }
125
126 if (big_lhs.width == 0) {
127 log("No constraints for initial state found.\n\n");
128 return;
129 }
130
131 log("Final constraint equation: %s = %s\n\n", log_signal(big_lhs), log_signal(big_rhs));
132 check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
133 ez.assume(satgen.signals_eq(big_lhs, big_rhs, 1));
134 }
135
136 void setup(int timestep = -1)
137 {
138 if (timestep > 0)
139 log ("\nSetting up time step %d:\n", timestep);
140 else
141 log ("\nSetting up SAT problem:\n");
142
143 if (timestep > max_timestep)
144 max_timestep = timestep;
145
146 RTLIL::SigSpec big_lhs, big_rhs;
147
148 for (auto &s : sets)
149 {
150 RTLIL::SigSpec lhs, rhs;
151
152 if (!RTLIL::SigSpec::parse(lhs, module, s.first))
153 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
154 if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
155 log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
156 show_signal_pool.add(sigmap(lhs));
157 show_signal_pool.add(sigmap(rhs));
158
159 if (lhs.width != rhs.width)
160 log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
161 s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
162
163 log("Import set-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
164 big_lhs.remove2(lhs, &big_rhs);
165 big_lhs.append(lhs);
166 big_rhs.append(rhs);
167 }
168
169 for (auto &s : sets_at[timestep])
170 {
171 RTLIL::SigSpec lhs, rhs;
172
173 if (!RTLIL::SigSpec::parse(lhs, module, s.first))
174 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
175 if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
176 log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
177 show_signal_pool.add(sigmap(lhs));
178 show_signal_pool.add(sigmap(rhs));
179
180 if (lhs.width != rhs.width)
181 log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
182 s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
183
184 log("Import set-constraint for timestep: %s = %s\n", log_signal(lhs), log_signal(rhs));
185 big_lhs.remove2(lhs, &big_rhs);
186 big_lhs.append(lhs);
187 big_rhs.append(rhs);
188 }
189
190 for (auto &s : unsets_at[timestep])
191 {
192 RTLIL::SigSpec lhs;
193
194 if (!RTLIL::SigSpec::parse(lhs, module, s))
195 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.c_str());
196 show_signal_pool.add(sigmap(lhs));
197
198 log("Import unset-constraint for timestep: %s\n", log_signal(lhs));
199 big_lhs.remove2(lhs, &big_rhs);
200 }
201
202 log("Final constraint equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
203 check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
204 ez.assume(satgen.signals_eq(big_lhs, big_rhs, timestep));
205
206 // 0 = sets_def
207 // 1 = sets_any_undef
208 // 2 = sets_all_undef
209 std::set<RTLIL::SigSpec> sets_def_undef[3];
210
211 for (auto &s : sets_def) {
212 RTLIL::SigSpec sig;
213 if (!RTLIL::SigSpec::parse(sig, module, s))
214 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
215 sets_def_undef[0].insert(sig);
216 }
217
218 for (auto &s : sets_any_undef) {
219 RTLIL::SigSpec sig;
220 if (!RTLIL::SigSpec::parse(sig, module, s))
221 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
222 sets_def_undef[1].insert(sig);
223 }
224
225 for (auto &s : sets_all_undef) {
226 RTLIL::SigSpec sig;
227 if (!RTLIL::SigSpec::parse(sig, module, s))
228 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
229 sets_def_undef[2].insert(sig);
230 }
231
232 for (auto &s : sets_def_at[timestep]) {
233 RTLIL::SigSpec sig;
234 if (!RTLIL::SigSpec::parse(sig, module, s))
235 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
236 sets_def_undef[0].insert(sig);
237 sets_def_undef[1].erase(sig);
238 sets_def_undef[2].erase(sig);
239 }
240
241 for (auto &s : sets_any_undef_at[timestep]) {
242 RTLIL::SigSpec sig;
243 if (!RTLIL::SigSpec::parse(sig, module, s))
244 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
245 sets_def_undef[0].erase(sig);
246 sets_def_undef[1].insert(sig);
247 sets_def_undef[2].erase(sig);
248 }
249
250 for (auto &s : sets_all_undef_at[timestep]) {
251 RTLIL::SigSpec sig;
252 if (!RTLIL::SigSpec::parse(sig, module, s))
253 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
254 sets_def_undef[0].erase(sig);
255 sets_def_undef[1].erase(sig);
256 sets_def_undef[2].insert(sig);
257 }
258
259 for (int t = 0; t < 3; t++)
260 for (auto &sig : sets_def_undef[t]) {
261 log("Import %s constraint for timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig));
262 std::vector<int> undef_sig = satgen.importUndefSigSpec(sig, timestep);
263 if (t == 0)
264 ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_sig)));
265 if (t == 1)
266 ez.assume(ez.expression(ezSAT::OpOr, undef_sig));
267 if (t == 2)
268 ez.assume(ez.expression(ezSAT::OpAnd, undef_sig));
269 }
270
271 int import_cell_counter = 0;
272 for (auto &c : module->cells)
273 if (design->selected(module, c.second)) {
274 // log("Import cell: %s\n", RTLIL::id2cstr(c.first));
275 if (satgen.importCell(c.second, timestep)) {
276 for (auto &p : c.second->connections)
277 if (ct.cell_output(c.second->type, p.first))
278 show_drivers.insert(sigmap(p.second), c.second);
279 import_cell_counter++;
280 } else
281 log("Warning: failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
282 }
283 log("Imported %d cells to SAT database.\n", import_cell_counter);
284 }
285
286 int setup_proof(int timestep = -1)
287 {
288 assert(prove.size() || prove_x.size() || prove_asserts);
289
290 RTLIL::SigSpec big_lhs, big_rhs;
291 std::vector<int> prove_bits;
292
293 if (prove.size() > 0)
294 {
295 for (auto &s : prove)
296 {
297 RTLIL::SigSpec lhs, rhs;
298
299 if (!RTLIL::SigSpec::parse(lhs, module, s.first))
300 log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
301 if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
302 log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str());
303 show_signal_pool.add(sigmap(lhs));
304 show_signal_pool.add(sigmap(rhs));
305
306 if (lhs.width != rhs.width)
307 log_cmd_error("Proof expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
308 s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
309
310 log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
311 big_lhs.remove2(lhs, &big_rhs);
312 big_lhs.append(lhs);
313 big_rhs.append(rhs);
314 }
315
316 log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
317 check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
318 prove_bits.push_back(satgen.signals_eq(big_lhs, big_rhs, timestep));
319 }
320
321 if (prove_x.size() > 0)
322 {
323 for (auto &s : prove_x)
324 {
325 RTLIL::SigSpec lhs, rhs;
326
327 if (!RTLIL::SigSpec::parse(lhs, module, s.first))
328 log_cmd_error("Failed to parse lhs proof-x expression `%s'.\n", s.first.c_str());
329 if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
330 log_cmd_error("Failed to parse rhs proof-x expression `%s'.\n", s.second.c_str());
331 show_signal_pool.add(sigmap(lhs));
332 show_signal_pool.add(sigmap(rhs));
333
334 if (lhs.width != rhs.width)
335 log_cmd_error("Proof-x expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
336 s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
337
338 log("Import proof-x-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
339 big_lhs.remove2(lhs, &big_rhs);
340 big_lhs.append(lhs);
341 big_rhs.append(rhs);
342 }
343
344 log("Final proof-x equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
345
346 std::vector<int> value_lhs = satgen.importDefSigSpec(big_lhs, timestep);
347 std::vector<int> value_rhs = satgen.importDefSigSpec(big_rhs, timestep);
348
349 std::vector<int> undef_lhs = satgen.importUndefSigSpec(big_lhs, timestep);
350 std::vector<int> undef_rhs = satgen.importUndefSigSpec(big_rhs, timestep);
351
352 for (size_t i = 0; i < value_lhs.size(); i++)
353 prove_bits.push_back(ez.OR(undef_lhs.at(i), ez.AND(ez.NOT(undef_rhs.at(i)), ez.NOT(ez.XOR(value_lhs.at(i), value_rhs.at(i))))));
354 }
355
356 if (prove_asserts)
357 prove_bits.push_back(satgen.importAsserts(timestep));
358
359 return ez.expression(ezSAT::OpAnd, prove_bits);
360 }
361
362 void force_unique_state(int timestep_from, int timestep_to)
363 {
364 RTLIL::SigSpec state_signals = satgen.initial_state.export_all();
365 for (int i = timestep_from; i < timestep_to; i++)
366 ez.assume(ez.NOT(satgen.signals_eq(state_signals, state_signals, i, timestep_to)));
367 }
368
369 bool solve(const std::vector<int> &assumptions)
370 {
371 log_assert(gotTimeout == false);
372 ez.setSolverTimeout(timeout);
373 bool success = ez.solve(modelExpressions, modelValues, assumptions);
374 if (ez.getSolverTimoutStatus())
375 gotTimeout = true;
376 return success;
377 }
378
379 bool solve(int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0)
380 {
381 log_assert(gotTimeout == false);
382 ez.setSolverTimeout(timeout);
383 bool success = ez.solve(modelExpressions, modelValues, a, b, c, d, e, f);
384 if (ez.getSolverTimoutStatus())
385 gotTimeout = true;
386 return success;
387 }
388
389 struct ModelBlockInfo {
390 int timestep, offset, width;
391 std::string description;
392 bool operator < (const ModelBlockInfo &other) const {
393 if (timestep != other.timestep)
394 return timestep < other.timestep;
395 if (description != other.description)
396 return description < other.description;
397 if (offset != other.offset)
398 return offset < other.offset;
399 if (width != other.width)
400 return width < other.width;
401 return false;
402 }
403 };
404
405 std::vector<int> modelExpressions;
406 std::vector<bool> modelValues;
407 std::set<ModelBlockInfo> modelInfo;
408
409 void maximize_undefs()
410 {
411 log_assert(enable_undef);
412 std::vector<bool> backupValues;
413
414 while (1)
415 {
416 std::vector<int> must_undef, maybe_undef;
417
418 for (size_t i = 0; i < modelExpressions.size()/2; i++)
419 if (modelValues.at(modelExpressions.size()/2 + i))
420 must_undef.push_back(modelExpressions.at(modelExpressions.size()/2 + i));
421 else
422 maybe_undef.push_back(modelExpressions.at(modelExpressions.size()/2 + i));
423
424 backupValues.swap(modelValues);
425 if (!solve(ez.expression(ezSAT::OpAnd, must_undef), ez.expression(ezSAT::OpOr, maybe_undef)))
426 break;
427 }
428
429 backupValues.swap(modelValues);
430 }
431
432 void generate_model()
433 {
434 RTLIL::SigSpec modelSig;
435 modelExpressions.clear();
436 modelInfo.clear();
437
438 // Add "show" signals or alternatively the leaves on the input cone on all set and prove signals
439
440 if (shows.size() == 0)
441 {
442 SigPool queued_signals, handled_signals, final_signals;
443 queued_signals = show_signal_pool;
444 while (queued_signals.size() > 0) {
445 RTLIL::SigSpec sig = queued_signals.export_one();
446 queued_signals.del(sig);
447 handled_signals.add(sig);
448 std::set<RTLIL::Cell*> drivers = show_drivers.find(sig);
449 if (drivers.size() == 0) {
450 final_signals.add(sig);
451 } else {
452 for (auto &d : drivers)
453 for (auto &p : d->connections) {
454 if (d->type == "$dff" && p.first == "\\CLK")
455 continue;
456 if (d->type.substr(0, 6) == "$_DFF_" && p.first == "\\C")
457 continue;
458 queued_signals.add(handled_signals.remove(sigmap(p.second)));
459 }
460 }
461 }
462 modelSig = final_signals.export_all();
463
464 // additionally add all set and prove signals directly
465 // (it improves user confidence if we write the constraints back ;-)
466 modelSig.append(show_signal_pool.export_all());
467 }
468 else
469 {
470 for (auto &s : shows) {
471 RTLIL::SigSpec sig;
472 if (!RTLIL::SigSpec::parse(sig, module, s))
473 log_cmd_error("Failed to parse show expression `%s'.\n", s.c_str());
474 log("Import show expression: %s\n", log_signal(sig));
475 modelSig.append(sig);
476 }
477 }
478
479 modelSig.sort_and_unify();
480 // log("Model signals: %s\n", log_signal(modelSig));
481
482 std::vector<int> modelUndefExpressions;
483
484 for (auto &c : modelSig.chunks)
485 if (c.wire != NULL)
486 {
487 ModelBlockInfo info;
488 RTLIL::SigSpec chunksig = c;
489 info.width = chunksig.width;
490 info.description = log_signal(chunksig);
491
492 for (int timestep = -1; timestep <= max_timestep; timestep++)
493 {
494 if ((timestep == -1 && max_timestep > 0) || timestep == 0)
495 continue;
496
497 info.timestep = timestep;
498 info.offset = modelExpressions.size();
499 modelInfo.insert(info);
500
501 std::vector<int> vec = satgen.importSigSpec(chunksig, timestep);
502 modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end());
503
504 if (enable_undef) {
505 std::vector<int> undef_vec = satgen.importUndefSigSpec(chunksig, timestep);
506 modelUndefExpressions.insert(modelUndefExpressions.end(), undef_vec.begin(), undef_vec.end());
507 }
508 }
509 }
510
511 // Add initial state signals as collected by satgen
512 //
513 modelSig = satgen.initial_state.export_all();
514 for (auto &c : modelSig.chunks)
515 if (c.wire != NULL)
516 {
517 ModelBlockInfo info;
518 RTLIL::SigSpec chunksig = c;
519
520 info.timestep = 0;
521 info.offset = modelExpressions.size();
522 info.width = chunksig.width;
523 info.description = log_signal(chunksig);
524 modelInfo.insert(info);
525
526 std::vector<int> vec = satgen.importSigSpec(chunksig, 1);
527 modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end());
528
529 if (enable_undef) {
530 std::vector<int> undef_vec = satgen.importUndefSigSpec(chunksig, 1);
531 modelUndefExpressions.insert(modelUndefExpressions.end(), undef_vec.begin(), undef_vec.end());
532 }
533 }
534
535 modelExpressions.insert(modelExpressions.end(), modelUndefExpressions.begin(), modelUndefExpressions.end());
536 }
537
538 void print_model()
539 {
540 int maxModelName = 10;
541 int maxModelWidth = 10;
542
543 for (auto &info : modelInfo) {
544 maxModelName = std::max(maxModelName, int(info.description.size()));
545 maxModelWidth = std::max(maxModelWidth, info.width);
546 }
547
548 log("\n");
549
550 int last_timestep = -2;
551 for (auto &info : modelInfo)
552 {
553 RTLIL::Const value;
554 bool found_undef = false;
555
556 for (int i = 0; i < info.width; i++) {
557 value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
558 if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i))
559 value.bits.back() = RTLIL::State::Sx, found_undef = true;
560 }
561
562 if (info.timestep != last_timestep) {
563 const char *hline = "---------------------------------------------------------------------------------------------------"
564 "---------------------------------------------------------------------------------------------------"
565 "---------------------------------------------------------------------------------------------------";
566 if (last_timestep == -2) {
567 log(max_timestep > 0 ? " Time " : " ");
568 log("%-*s %10s %10s %*s\n", maxModelName+10, "Signal Name", "Dec", "Hex", maxModelWidth+5, "Bin");
569 }
570 log(max_timestep > 0 ? " ---- " : " ");
571 log("%*.*s %10.10s %10.10s %*.*s\n", maxModelName+10, maxModelName+10,
572 hline, hline, hline, maxModelWidth+5, maxModelWidth+5, hline);
573 last_timestep = info.timestep;
574 }
575
576 if (max_timestep > 0) {
577 if (info.timestep > 0)
578 log(" %4d ", info.timestep);
579 else
580 log(" init ");
581 } else
582 log(" ");
583
584 if (info.width <= 32 && !found_undef)
585 log("%-*s %10d %10x %*s\n", maxModelName+10, info.description.c_str(), value.as_int(), value.as_int(), maxModelWidth+5, value.as_string().c_str());
586 else
587 log("%-*s %10s %10s %*s\n", maxModelName+10, info.description.c_str(), "--", "--", maxModelWidth+5, value.as_string().c_str());
588 }
589
590 if (last_timestep == -2)
591 log(" no model variables selected for display.\n");
592 }
593
594 void invalidate_model(bool max_undef)
595 {
596 std::vector<int> clause;
597 if (enable_undef) {
598 for (size_t i = 0; i < modelExpressions.size()/2; i++) {
599 int bit = modelExpressions.at(i), bit_undef = modelExpressions.at(modelExpressions.size()/2 + i);
600 bool val = modelValues.at(i), val_undef = modelValues.at(modelExpressions.size()/2 + i);
601 if (!max_undef || !val_undef)
602 clause.push_back(val_undef ? ez.NOT(bit_undef) : val ? ez.NOT(bit) : bit);
603 }
604 } else
605 for (size_t i = 0; i < modelExpressions.size(); i++)
606 clause.push_back(modelValues.at(i) ? ez.NOT(modelExpressions.at(i)) : modelExpressions.at(i));
607 ez.assume(ez.expression(ezSAT::OpOr, clause));
608 }
609 };
610
611 } /* namespace */
612
613 static void print_proof_failed()
614 {
615 log("\n");
616 log(" ______ ___ ___ _ _ _ _ \n");
617 log(" (_____ \\ / __) / __) (_) | | | |\n");
618 log(" _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |\n");
619 log(" | ____/ ___) _ \\ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|\n");
620 log(" | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ \n");
621 log(" |_| |_| \\___/ \\___/ |_| |_| \\_____|_|\\_)_____)\\____|_|\n");
622 log("\n");
623 }
624
625 static void print_timeout()
626 {
627 log("\n");
628 log(" _____ _ _ _____ ____ _ _____\n");
629 log(" /__ __\\/ \\/ \\__/|/ __// _ \\/ \\ /\\/__ __\\\n");
630 log(" / \\ | || |\\/||| \\ | / \\|| | || / \\\n");
631 log(" | | | || | ||| /_ | \\_/|| \\_/| | |\n");
632 log(" \\_/ \\_/\\_/ \\|\\____\\\\____/\\____/ \\_/\n");
633 log("\n");
634 }
635
636 static void print_qed()
637 {
638 log("\n");
639 log(" /$$$$$$ /$$$$$$$$ /$$$$$$$ \n");
640 log(" /$$__ $$ | $$_____/ | $$__ $$ \n");
641 log(" | $$ \\ $$ | $$ | $$ \\ $$ \n");
642 log(" | $$ | $$ | $$$$$ | $$ | $$ \n");
643 log(" | $$ | $$ | $$__/ | $$ | $$ \n");
644 log(" | $$/$$ $$ | $$ | $$ | $$ \n");
645 log(" | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
646 log(" \\____ $$$|__/|________/|__/|_______/|__/\n");
647 log(" \\__/ \n");
648 log("\n");
649 }
650
651 struct SatPass : public Pass {
652 SatPass() : Pass("sat", "solve a SAT problem in the circuit") { }
653 virtual void help()
654 {
655 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
656 log("\n");
657 log(" sat [options] [selection]\n");
658 log("\n");
659 log("This command solves a SAT problem defined over the currently selected circuit\n");
660 log("and additional constraints passed as parameters.\n");
661 log("\n");
662 log(" -all\n");
663 log(" show all solutions to the problem (this can grow exponentially, use\n");
664 log(" -max <N> instead to get <N> solutions)\n");
665 log("\n");
666 log(" -max <N>\n");
667 log(" like -all, but limit number of solutions to <N>\n");
668 log("\n");
669 log(" -enable_undef\n");
670 log(" enable modeling of undef value (aka 'x-bits')\n");
671 log(" this option is implied by -set-def, -set-undef et. cetera\n");
672 log("\n");
673 log(" -max_undef\n");
674 log(" maximize the number of undef bits in solutions, giving a better\n");
675 log(" picture of which input bits are actually vital to the solution.\n");
676 log("\n");
677 log(" -set <signal> <value>\n");
678 log(" set the specified signal to the specified value.\n");
679 log("\n");
680 log(" -set-def <signal>\n");
681 log(" add a constraint that all bits of the given signal must be defined\n");
682 log("\n");
683 log(" -set-any-undef <signal>\n");
684 log(" add a constraint that at least one bit of the given signal is undefined\n");
685 log("\n");
686 log(" -set-all-undef <signal>\n");
687 log(" add a constraint that all bits of the given signal are undefined\n");
688 log("\n");
689 log(" -set-def-inputs\n");
690 log(" add -set-def constraints for all module inputs\n");
691 log("\n");
692 log(" -show <signal>\n");
693 log(" show the model for the specified signal. if no -show option is\n");
694 log(" passed then a set of signals to be shown is automatically selected.\n");
695 log("\n");
696 log(" -show-inputs, -show-outputs\n");
697 log(" add all module input (output) ports to the list of shown signals\n");
698 log("\n");
699 log(" -ignore_div_by_zero\n");
700 log(" ignore all solutions that involve a division by zero\n");
701 log("\n");
702 log("The following options can be used to set up a sequential problem:\n");
703 log("\n");
704 log(" -seq <N>\n");
705 log(" set up a sequential problem with <N> time steps. The steps will\n");
706 log(" be numbered from 1 to N.\n");
707 log("\n");
708 log(" -set-at <N> <signal> <value>\n");
709 log(" -unset-at <N> <signal>\n");
710 log(" set or unset the specified signal to the specified value in the\n");
711 log(" given timestep. this has priority over a -set for the same signal.\n");
712 log("\n");
713 log(" -set-def-at <N> <signal>\n");
714 log(" -set-any-undef-at <N> <signal>\n");
715 log(" -set-all-undef-at <N> <signal>\n");
716 log(" add undef contraints in the given timestep.\n");
717 log("\n");
718 log(" -set-init <signal> <value>\n");
719 log(" set the initial value for the register driving the signal to the value\n");
720 log("\n");
721 log(" -set-init-undef\n");
722 log(" set all initial states (not set using -set-init) to undef\n");
723 log("\n");
724 log("The following additional options can be used to set up a proof. If also -seq\n");
725 log("is passed, a temporal induction proof is performed.\n");
726 log("\n");
727 log(" -tempinduct\n");
728 log(" Perform a temporal induction proof. In a temporalinduction proof it is\n");
729 log(" proven that the condition holds forever after the number of time steps\n");
730 log(" specified using -seq.\n");
731 log("\n");
732 log(" -prove <signal> <value>\n");
733 log(" Attempt to proof that <signal> is always <value>.\n");
734 log("\n");
735 log(" -prove-x <signal> <value>\n");
736 log(" Like -prove, but an undef (x) bit in the lhs matches any value on\n");
737 log(" the right hand side. Useful for equivialence checking.\n");
738 log("\n");
739 log(" -prove-asserts\n");
740 log(" Prove that all asserts in the design hold.\n");
741 log("\n");
742 log(" -maxsteps <N>\n");
743 log(" Set a maximum length for the induction.\n");
744 log("\n");
745 log(" -timeout <N>\n");
746 log(" Maximum number of seconds a single SAT instance may take.\n");
747 log("\n");
748 log(" -verify\n");
749 log(" Return an error and stop the synthesis script if the proof fails.\n");
750 log("\n");
751 log(" -verify-no-timeout\n");
752 log(" Like -verify but do not return an error for timeouts.\n");
753 log("\n");
754 }
755 virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
756 {
757 std::vector<std::pair<std::string, std::string>> sets, sets_init, prove, prove_x;
758 std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
759 std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
760 std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
761 int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
762 bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
763 bool ignore_div_by_zero = false, set_init_undef = false, max_undef = false;
764 bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
765
766 log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
767
768 size_t argidx;
769 for (argidx = 1; argidx < args.size(); argidx++) {
770 if (args[argidx] == "-all") {
771 loopcount = -1;
772 continue;
773 }
774 if (args[argidx] == "-verify") {
775 fail_on_timeout = true;
776 verify = true;
777 continue;
778 }
779 if (args[argidx] == "-verify-no-timeout") {
780 verify = true;
781 continue;
782 }
783 if (args[argidx] == "-timeout" && argidx+1 < args.size()) {
784 timeout = atoi(args[++argidx].c_str());
785 continue;
786 }
787 if (args[argidx] == "-max" && argidx+1 < args.size()) {
788 loopcount = atoi(args[++argidx].c_str());
789 continue;
790 }
791 if (args[argidx] == "-maxsteps" && argidx+1 < args.size()) {
792 maxsteps = atoi(args[++argidx].c_str());
793 continue;
794 }
795 if (args[argidx] == "-ignore_div_by_zero") {
796 ignore_div_by_zero = true;
797 continue;
798 }
799 if (args[argidx] == "-enable_undef") {
800 enable_undef = true;
801 continue;
802 }
803 if (args[argidx] == "-max_undef") {
804 enable_undef = true;
805 max_undef = true;
806 continue;
807 }
808 if (args[argidx] == "-set-def-inputs") {
809 enable_undef = true;
810 set_def_inputs = true;
811 continue;
812 }
813 if (args[argidx] == "-set" && argidx+2 < args.size()) {
814 std::string lhs = args[++argidx];
815 std::string rhs = args[++argidx];
816 sets.push_back(std::pair<std::string, std::string>(lhs, rhs));
817 continue;
818 }
819 if (args[argidx] == "-set-def" && argidx+1 < args.size()) {
820 sets_def.push_back(args[++argidx]);
821 enable_undef = true;
822 continue;
823 }
824 if (args[argidx] == "-set-any-undef" && argidx+1 < args.size()) {
825 sets_any_undef.push_back(args[++argidx]);
826 enable_undef = true;
827 continue;
828 }
829 if (args[argidx] == "-set-all-undef" && argidx+1 < args.size()) {
830 sets_all_undef.push_back(args[++argidx]);
831 enable_undef = true;
832 continue;
833 }
834 if (args[argidx] == "-tempinduct") {
835 tempinduct = true;
836 continue;
837 }
838 if (args[argidx] == "-prove" && argidx+2 < args.size()) {
839 std::string lhs = args[++argidx];
840 std::string rhs = args[++argidx];
841 prove.push_back(std::pair<std::string, std::string>(lhs, rhs));
842 continue;
843 }
844 if (args[argidx] == "-prove-x" && argidx+2 < args.size()) {
845 std::string lhs = args[++argidx];
846 std::string rhs = args[++argidx];
847 prove_x.push_back(std::pair<std::string, std::string>(lhs, rhs));
848 enable_undef = true;
849 continue;
850 }
851 if (args[argidx] == "-prove-asserts") {
852 prove_asserts = true;
853 continue;
854 }
855 if (args[argidx] == "-seq" && argidx+1 < args.size()) {
856 seq_len = atoi(args[++argidx].c_str());
857 continue;
858 }
859 if (args[argidx] == "-set-at" && argidx+3 < args.size()) {
860 int timestep = atoi(args[++argidx].c_str());
861 std::string lhs = args[++argidx];
862 std::string rhs = args[++argidx];
863 sets_at[timestep].push_back(std::pair<std::string, std::string>(lhs, rhs));
864 continue;
865 }
866 if (args[argidx] == "-unset-at" && argidx+2 < args.size()) {
867 int timestep = atoi(args[++argidx].c_str());
868 unsets_at[timestep].push_back(args[++argidx]);
869 continue;
870 }
871 if (args[argidx] == "-set-def-at" && argidx+2 < args.size()) {
872 int timestep = atoi(args[++argidx].c_str());
873 sets_def_at[timestep].push_back(args[++argidx]);
874 enable_undef = true;
875 continue;
876 }
877 if (args[argidx] == "-set-any-undef-at" && argidx+2 < args.size()) {
878 int timestep = atoi(args[++argidx].c_str());
879 sets_any_undef_at[timestep].push_back(args[++argidx]);
880 enable_undef = true;
881 continue;
882 }
883 if (args[argidx] == "-set-all-undef-at" && argidx+2 < args.size()) {
884 int timestep = atoi(args[++argidx].c_str());
885 sets_all_undef_at[timestep].push_back(args[++argidx]);
886 enable_undef = true;
887 continue;
888 }
889 if (args[argidx] == "-set-init" && argidx+2 < args.size()) {
890 std::string lhs = args[++argidx];
891 std::string rhs = args[++argidx];
892 sets_init.push_back(std::pair<std::string, std::string>(lhs, rhs));
893 continue;
894 }
895 if (args[argidx] == "-set-init-undef") {
896 set_init_undef = true;
897 enable_undef = true;
898 continue;
899 }
900 if (args[argidx] == "-show" && argidx+1 < args.size()) {
901 shows.push_back(args[++argidx]);
902 continue;
903 }
904 if (args[argidx] == "-show-inputs") {
905 show_inputs = true;
906 continue;
907 }
908 if (args[argidx] == "-show-outputs") {
909 show_outputs = true;
910 continue;
911 }
912 break;
913 }
914 extra_args(args, argidx, design);
915
916 RTLIL::Module *module = NULL;
917 for (auto &mod_it : design->modules)
918 if (design->selected(mod_it.second)) {
919 if (module)
920 log_cmd_error("Only one module must be selected for the SAT pass! (selected: %s and %s)\n",
921 RTLIL::id2cstr(module->name), RTLIL::id2cstr(mod_it.first));
922 module = mod_it.second;
923 }
924 if (module == NULL)
925 log_cmd_error("Can't perform SAT on an empty selection!\n");
926
927 if (!prove.size() && !prove_x.size() && !prove_asserts && verify)
928 log_cmd_error("Got -verify but nothing to prove!\n");
929
930 if (!prove.size() && !prove_x.size() && !prove_asserts && tempinduct)
931 log_cmd_error("Got -tempinduct but nothing to prove!\n");
932
933 if (seq_len == 0 && tempinduct)
934 log_cmd_error("Got -tempinduct but no -seq argument!\n");
935
936 if (set_def_inputs) {
937 for (auto &it : module->wires)
938 if (it.second->port_input)
939 sets_def.push_back(it.second->name);
940 }
941
942 if (show_inputs) {
943 for (auto &it : module->wires)
944 if (it.second->port_input)
945 shows.push_back(it.second->name);
946 }
947
948 if (show_outputs) {
949 for (auto &it : module->wires)
950 if (it.second->port_output)
951 shows.push_back(it.second->name);
952 }
953
954 if (tempinduct)
955 {
956 if (loopcount > 0 || max_undef)
957 log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
958
959 SatHelper basecase(design, module, enable_undef);
960 SatHelper inductstep(design, module, enable_undef);
961
962 basecase.sets = sets;
963 basecase.prove = prove;
964 basecase.prove_x = prove_x;
965 basecase.prove_asserts = prove_asserts;
966 basecase.sets_at = sets_at;
967 basecase.unsets_at = unsets_at;
968 basecase.shows = shows;
969 basecase.timeout = timeout;
970 basecase.sets_def = sets_def;
971 basecase.sets_any_undef = sets_any_undef;
972 basecase.sets_all_undef = sets_all_undef;
973 basecase.sets_def_at = sets_def_at;
974 basecase.sets_any_undef_at = sets_any_undef_at;
975 basecase.sets_all_undef_at = sets_all_undef_at;
976 basecase.sets_init = sets_init;
977 basecase.set_init_undef = set_init_undef;
978 basecase.satgen.ignore_div_by_zero = ignore_div_by_zero;
979
980 for (int timestep = 1; timestep <= seq_len; timestep++)
981 basecase.setup(timestep);
982 basecase.setup_init();
983
984 inductstep.sets = sets;
985 inductstep.prove = prove;
986 inductstep.prove_x = prove_x;
987 inductstep.prove_asserts = prove_asserts;
988 inductstep.shows = shows;
989 inductstep.timeout = timeout;
990 inductstep.sets_def = sets_def;
991 inductstep.sets_any_undef = sets_any_undef;
992 inductstep.sets_all_undef = sets_all_undef;
993 inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero;
994
995 inductstep.setup(1);
996 inductstep.ez.assume(inductstep.setup_proof(1));
997
998 for (int inductlen = 1; inductlen <= maxsteps || maxsteps == 0; inductlen++)
999 {
1000 log("\n** Trying induction with length %d **\n", inductlen);
1001
1002 // phase 1: proving base case
1003
1004 basecase.setup(seq_len + inductlen);
1005 int property = basecase.setup_proof(seq_len + inductlen);
1006 basecase.generate_model();
1007
1008 if (inductlen > 1)
1009 basecase.force_unique_state(seq_len + 1, seq_len + inductlen);
1010
1011 log("\n[base case] Solving problem with %d variables and %d clauses..\n",
1012 basecase.ez.numCnfVariables(), basecase.ez.numCnfClauses());
1013
1014 if (basecase.solve(basecase.ez.NOT(property))) {
1015 log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
1016 print_proof_failed();
1017 basecase.print_model();
1018 goto tip_failed;
1019 }
1020
1021 if (basecase.gotTimeout)
1022 goto timeout;
1023
1024 log("Base case for induction length %d proven.\n", inductlen);
1025 basecase.ez.assume(property);
1026
1027 // phase 2: proving induction step
1028
1029 inductstep.setup(inductlen + 1);
1030 property = inductstep.setup_proof(inductlen + 1);
1031 inductstep.generate_model();
1032
1033 if (inductlen > 1)
1034 inductstep.force_unique_state(1, inductlen + 1);
1035
1036 log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
1037 inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
1038
1039 if (!inductstep.solve(inductstep.ez.NOT(property))) {
1040 if (inductstep.gotTimeout)
1041 goto timeout;
1042 log("Induction step proven: SUCCESS!\n");
1043 print_qed();
1044 goto tip_success;
1045 }
1046
1047 log("Induction step failed. Incrementing induction length.\n");
1048 inductstep.ez.assume(property);
1049
1050 inductstep.print_model();
1051 }
1052
1053 log("\nReached maximum number of time steps -> proof failed.\n");
1054 print_proof_failed();
1055
1056 tip_failed:
1057 if (verify) {
1058 log("\n");
1059 log_error("Called with -verify and proof did fail!\n");
1060 }
1061
1062 tip_success:;
1063 }
1064 else
1065 {
1066 if (maxsteps > 0)
1067 log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
1068
1069 SatHelper sathelper(design, module, enable_undef);
1070
1071 sathelper.sets = sets;
1072 sathelper.prove = prove;
1073 sathelper.prove_x = prove_x;
1074 sathelper.prove_asserts = prove_asserts;
1075 sathelper.sets_at = sets_at;
1076 sathelper.unsets_at = unsets_at;
1077 sathelper.shows = shows;
1078 sathelper.timeout = timeout;
1079 sathelper.sets_def = sets_def;
1080 sathelper.sets_any_undef = sets_any_undef;
1081 sathelper.sets_all_undef = sets_all_undef;
1082 sathelper.sets_def_at = sets_def_at;
1083 sathelper.sets_any_undef_at = sets_any_undef_at;
1084 sathelper.sets_all_undef_at = sets_all_undef_at;
1085 sathelper.sets_init = sets_init;
1086 sathelper.set_init_undef = set_init_undef;
1087 sathelper.satgen.ignore_div_by_zero = ignore_div_by_zero;
1088
1089 if (seq_len == 0) {
1090 sathelper.setup();
1091 if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
1092 sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof()));
1093 } else {
1094 for (int timestep = 1; timestep <= seq_len; timestep++) {
1095 sathelper.setup(timestep);
1096 if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
1097 sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof(timestep)));
1098 }
1099 sathelper.setup_init();
1100 }
1101 sathelper.generate_model();
1102
1103 #if 0
1104 // print CNF for debugging
1105 sathelper.ez.printDIMACS(stdout, true);
1106 #endif
1107
1108 int rerun_counter = 0;
1109
1110 rerun_solver:
1111 log("\nSolving problem with %d variables and %d clauses..\n",
1112 sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses());
1113
1114 if (sathelper.solve())
1115 {
1116 if (max_undef) {
1117 log("SAT model found. maximizing number of undefs.\n");
1118 sathelper.maximize_undefs();
1119 }
1120
1121 if (!prove.size() && !prove_x.size() && !prove_asserts) {
1122 log("SAT solving finished - model found:\n");
1123 } else {
1124 log("SAT proof finished - model found: FAIL!\n");
1125 print_proof_failed();
1126 }
1127
1128 sathelper.print_model();
1129
1130 if (loopcount != 0) {
1131 loopcount--, rerun_counter++;
1132 sathelper.invalidate_model(max_undef);
1133 goto rerun_solver;
1134 }
1135
1136 if (verify) {
1137 log("\n");
1138 log_error("Called with -verify and proof did fail!\n");
1139 }
1140 }
1141 else
1142 {
1143 if (sathelper.gotTimeout)
1144 goto timeout;
1145 if (rerun_counter)
1146 log("SAT solving finished - no more models found (after %d distinct solutions).\n", rerun_counter);
1147 else if (!prove.size() && !prove_x.size() && !prove_asserts)
1148 log("SAT solving finished - no model found.\n");
1149 else {
1150 log("SAT proof finished - no model found: SUCCESS!\n");
1151 print_qed();
1152 }
1153 }
1154
1155 if (verify && rerun_counter) {
1156 log("\n");
1157 log_error("Called with -verify and proof did fail!\n");
1158 }
1159 }
1160
1161 if (0) {
1162 timeout:
1163 log("Interrupted SAT solver: TIMEOUT!\n");
1164 print_timeout();
1165 if (fail_on_timeout)
1166 log_error("Called with -verify and proof did time out!\n");
1167 }
1168 }
1169 } SatPass;
1170