projects / yosys.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Renamed RTLIL::{Module,Cell}::connections to connections_
[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 #include <errno.h>
34 #include <string.h>
35
36 namespace {
37
38 struct SatHelper
39 {
40 RTLIL::Design *design;
41 RTLIL::Module *module;
42
43 ezDefaultSAT ez;
44 SigMap sigmap;
45 CellTypes ct;
46 SatGen satgen;
47
48 // additional constraints
49 std::vector<std::pair<std::string, std::string>> sets, prove, prove_x, sets_init;
50 std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
51 std::map<int, std::vector<std::string>> unsets_at;
52 bool prove_asserts;
53
54 // undef constraints
55 bool enable_undef, set_init_def, set_init_undef, set_init_zero, ignore_unknown_cells;
56 std::vector<std::string> sets_def, sets_any_undef, sets_all_undef;
57 std::map<int, std::vector<std::string>> sets_def_at, sets_any_undef_at, sets_all_undef_at;
58
59 // model variables
60 std::vector<std::string> shows;
61 SigPool show_signal_pool;
62 SigSet<RTLIL::Cell*> show_drivers;
63 int max_timestep, timeout;
64 bool gotTimeout;
65
66 SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) :
67 design(design), module(module), sigmap(module), ct(design), satgen(&ez, &sigmap)
68 {
69 this->enable_undef = enable_undef;
70 satgen.model_undef = enable_undef;
71 set_init_def = false;
72 set_init_undef = false;
73 set_init_zero = false;
74 ignore_unknown_cells = false;
75 max_timestep = -1;
76 timeout = 0;
77 gotTimeout = false;
78 }
79
80 void check_undef_enabled(const RTLIL::SigSpec &sig)
81 {
82 if (enable_undef)
83 return;
84
85 std::vector<RTLIL::SigBit> sigbits = sig.to_sigbit_vector();
86 for (size_t i = 0; i < sigbits.size(); i++)
87 if (sigbits[i].wire == NULL && sigbits[i].data == RTLIL::State::Sx)
88 log_cmd_error("Bit %d of %s is undef but option -enable_undef is missing!\n", int(i), log_signal(sig));
89 }
90
91 void setup_init()
92 {
93 log ("\nSetting up initial state:\n");
94
95 RTLIL::SigSpec big_lhs, big_rhs;
96
97 for (auto &it : module->wires)
98 {
99 if (it.second->attributes.count("\\init") == 0)
100 continue;
101
102 RTLIL::SigSpec lhs = sigmap(it.second);
103 RTLIL::SigSpec rhs = it.second->attributes.at("\\init");
104 log_assert(lhs.size() == rhs.size());
105
106 RTLIL::SigSpec removed_bits;
107 for (int i = 0; i < lhs.size(); i++) {
108 RTLIL::SigSpec bit = lhs.extract(i, 1);
109 if (!satgen.initial_state.check_all(bit)) {
110 removed_bits.append(bit);
111 lhs.remove(i, 1);
112 rhs.remove(i, 1);
113 i--;
114 }
115 }
116
117 if (removed_bits.size())
118 log("Warning: ignoring initial value on non-register: %s\n", log_signal(removed_bits));
119
120 if (lhs.size()) {
121 log("Import set-constraint from init attribute: %s = %s\n", log_signal(lhs), log_signal(rhs));
122 big_lhs.remove2(lhs, &big_rhs);
123 big_lhs.append(lhs);
124 big_rhs.append(rhs);
125 }
126 }
127
128 for (auto &s : sets_init)
129 {
130 RTLIL::SigSpec lhs, rhs;
131
132 if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
133 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
134 if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
135 log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
136 show_signal_pool.add(sigmap(lhs));
137 show_signal_pool.add(sigmap(rhs));
138
139 if (lhs.size() != rhs.size())
140 log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
141 s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
142
143 log("Import set-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
144 big_lhs.remove2(lhs, &big_rhs);
145 big_lhs.append(lhs);
146 big_rhs.append(rhs);
147 }
148
149 if (!satgen.initial_state.check_all(big_lhs)) {
150 RTLIL::SigSpec rem = satgen.initial_state.remove(big_lhs);
151 log_cmd_error("Found -set-init bits that are not part of the initial_state: %s\n", log_signal(rem));
152 }
153
154 if (set_init_def) {
155 RTLIL::SigSpec rem = satgen.initial_state.export_all();
156 std::vector<int> undef_rem = satgen.importUndefSigSpec(rem, 1);
157 ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_rem)));
158 }
159
160 if (set_init_undef) {
161 RTLIL::SigSpec rem = satgen.initial_state.export_all();
162 rem.remove(big_lhs);
163 big_lhs.append(rem);
164 big_rhs.append(RTLIL::SigSpec(RTLIL::State::Sx, rem.size()));
165 }
166
167 if (set_init_zero) {
168 RTLIL::SigSpec rem = satgen.initial_state.export_all();
169 rem.remove(big_lhs);
170 big_lhs.append(rem);
171 big_rhs.append(RTLIL::SigSpec(RTLIL::State::S0, rem.size()));
172 }
173
174 if (big_lhs.size() == 0) {
175 log("No constraints for initial state found.\n\n");
176 return;
177 }
178
179 log("Final constraint equation: %s = %s\n\n", log_signal(big_lhs), log_signal(big_rhs));
180 check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
181 ez.assume(satgen.signals_eq(big_lhs, big_rhs, 1));
182 }
183
184 void setup(int timestep = -1)
185 {
186 if (timestep > 0)
187 log ("\nSetting up time step %d:\n", timestep);
188 else
189 log ("\nSetting up SAT problem:\n");
190
191 if (timestep > max_timestep)
192 max_timestep = timestep;
193
194 RTLIL::SigSpec big_lhs, big_rhs;
195
196 for (auto &s : sets)
197 {
198 RTLIL::SigSpec lhs, rhs;
199
200 if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
201 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
202 if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
203 log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
204 show_signal_pool.add(sigmap(lhs));
205 show_signal_pool.add(sigmap(rhs));
206
207 if (lhs.size() != rhs.size())
208 log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
209 s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
210
211 log("Import set-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
212 big_lhs.remove2(lhs, &big_rhs);
213 big_lhs.append(lhs);
214 big_rhs.append(rhs);
215 }
216
217 for (auto &s : sets_at[timestep])
218 {
219 RTLIL::SigSpec lhs, rhs;
220
221 if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
222 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
223 if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
224 log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
225 show_signal_pool.add(sigmap(lhs));
226 show_signal_pool.add(sigmap(rhs));
227
228 if (lhs.size() != rhs.size())
229 log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
230 s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
231
232 log("Import set-constraint for this timestep: %s = %s\n", log_signal(lhs), log_signal(rhs));
233 big_lhs.remove2(lhs, &big_rhs);
234 big_lhs.append(lhs);
235 big_rhs.append(rhs);
236 }
237
238 for (auto &s : unsets_at[timestep])
239 {
240 RTLIL::SigSpec lhs;
241
242 if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s))
243 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.c_str());
244 show_signal_pool.add(sigmap(lhs));
245
246 log("Import unset-constraint for this timestep: %s\n", log_signal(lhs));
247 big_lhs.remove2(lhs, &big_rhs);
248 }
249
250 log("Final constraint equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
251 check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
252 ez.assume(satgen.signals_eq(big_lhs, big_rhs, timestep));
253
254 // 0 = sets_def
255 // 1 = sets_any_undef
256 // 2 = sets_all_undef
257 std::set<RTLIL::SigSpec> sets_def_undef[3];
258
259 for (auto &s : sets_def) {
260 RTLIL::SigSpec sig;
261 if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
262 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
263 sets_def_undef[0].insert(sig);
264 }
265
266 for (auto &s : sets_any_undef) {
267 RTLIL::SigSpec sig;
268 if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
269 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
270 sets_def_undef[1].insert(sig);
271 }
272
273 for (auto &s : sets_all_undef) {
274 RTLIL::SigSpec sig;
275 if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
276 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
277 sets_def_undef[2].insert(sig);
278 }
279
280 for (auto &s : sets_def_at[timestep]) {
281 RTLIL::SigSpec sig;
282 if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
283 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
284 sets_def_undef[0].insert(sig);
285 sets_def_undef[1].erase(sig);
286 sets_def_undef[2].erase(sig);
287 }
288
289 for (auto &s : sets_any_undef_at[timestep]) {
290 RTLIL::SigSpec sig;
291 if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
292 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
293 sets_def_undef[0].erase(sig);
294 sets_def_undef[1].insert(sig);
295 sets_def_undef[2].erase(sig);
296 }
297
298 for (auto &s : sets_all_undef_at[timestep]) {
299 RTLIL::SigSpec sig;
300 if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
301 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
302 sets_def_undef[0].erase(sig);
303 sets_def_undef[1].erase(sig);
304 sets_def_undef[2].insert(sig);
305 }
306
307 for (int t = 0; t < 3; t++)
308 for (auto &sig : sets_def_undef[t]) {
309 log("Import %s constraint for this timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig));
310 std::vector<int> undef_sig = satgen.importUndefSigSpec(sig, timestep);
311 if (t == 0)
312 ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_sig)));
313 if (t == 1)
314 ez.assume(ez.expression(ezSAT::OpOr, undef_sig));
315 if (t == 2)
316 ez.assume(ez.expression(ezSAT::OpAnd, undef_sig));
317 }
318
319 int import_cell_counter = 0;
320 for (auto &c : module->cells)
321 if (design->selected(module, c.second)) {
322 // log("Import cell: %s\n", RTLIL::id2cstr(c.first));
323 if (satgen.importCell(c.second, timestep)) {
324 for (auto &p : c.second->connections_)
325 if (ct.cell_output(c.second->type, p.first))
326 show_drivers.insert(sigmap(p.second), c.second);
327 import_cell_counter++;
328 } else if (ignore_unknown_cells)
329 log("Warning: Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
330 else
331 log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
332 }
333 log("Imported %d cells to SAT database.\n", import_cell_counter);
334 }
335
336 int setup_proof(int timestep = -1)
337 {
338 assert(prove.size() || prove_x.size() || prove_asserts);
339
340 RTLIL::SigSpec big_lhs, big_rhs;
341 std::vector<int> prove_bits;
342
343 if (prove.size() > 0)
344 {
345 for (auto &s : prove)
346 {
347 RTLIL::SigSpec lhs, rhs;
348
349 if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
350 log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
351 if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
352 log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str());
353 show_signal_pool.add(sigmap(lhs));
354 show_signal_pool.add(sigmap(rhs));
355
356 if (lhs.size() != rhs.size())
357 log_cmd_error("Proof expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
358 s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
359
360 log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
361 big_lhs.remove2(lhs, &big_rhs);
362 big_lhs.append(lhs);
363 big_rhs.append(rhs);
364 }
365
366 log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
367 check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
368 prove_bits.push_back(satgen.signals_eq(big_lhs, big_rhs, timestep));
369 }
370
371 if (prove_x.size() > 0)
372 {
373 for (auto &s : prove_x)
374 {
375 RTLIL::SigSpec lhs, rhs;
376
377 if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
378 log_cmd_error("Failed to parse lhs proof-x expression `%s'.\n", s.first.c_str());
379 if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
380 log_cmd_error("Failed to parse rhs proof-x expression `%s'.\n", s.second.c_str());
381 show_signal_pool.add(sigmap(lhs));
382 show_signal_pool.add(sigmap(rhs));
383
384 if (lhs.size() != rhs.size())
385 log_cmd_error("Proof-x expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
386 s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
387
388 log("Import proof-x-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
389 big_lhs.remove2(lhs, &big_rhs);
390 big_lhs.append(lhs);
391 big_rhs.append(rhs);
392 }
393
394 log("Final proof-x equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
395
396 std::vector<int> value_lhs = satgen.importDefSigSpec(big_lhs, timestep);
397 std::vector<int> value_rhs = satgen.importDefSigSpec(big_rhs, timestep);
398
399 std::vector<int> undef_lhs = satgen.importUndefSigSpec(big_lhs, timestep);
400 std::vector<int> undef_rhs = satgen.importUndefSigSpec(big_rhs, timestep);
401
402 for (size_t i = 0; i < value_lhs.size(); i++)
403 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))))));
404 }
405
406 if (prove_asserts) {
407 RTLIL::SigSpec asserts_a, asserts_en;
408 satgen.getAsserts(asserts_a, asserts_en, timestep);
409 for (int i = 0; i < SIZE(asserts_a); i++)
410 log("Import proof for assert: %s when %s.\n", log_signal(asserts_a[i]), log_signal(asserts_en[i]));
411 prove_bits.push_back(satgen.importAsserts(timestep));
412 }
413
414 return ez.expression(ezSAT::OpAnd, prove_bits);
415 }
416
417 void force_unique_state(int timestep_from, int timestep_to)
418 {
419 RTLIL::SigSpec state_signals = satgen.initial_state.export_all();
420 for (int i = timestep_from; i < timestep_to; i++)
421 ez.assume(ez.NOT(satgen.signals_eq(state_signals, state_signals, i, timestep_to)));
422 }
423
424 bool solve(const std::vector<int> &assumptions)
425 {
426 log_assert(gotTimeout == false);
427 ez.setSolverTimeout(timeout);
428 bool success = ez.solve(modelExpressions, modelValues, assumptions);
429 if (ez.getSolverTimoutStatus())
430 gotTimeout = true;
431 return success;
432 }
433
434 bool solve(int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0)
435 {
436 log_assert(gotTimeout == false);
437 ez.setSolverTimeout(timeout);
438 bool success = ez.solve(modelExpressions, modelValues, a, b, c, d, e, f);
439 if (ez.getSolverTimoutStatus())
440 gotTimeout = true;
441 return success;
442 }
443
444 struct ModelBlockInfo {
445 int timestep, offset, width;
446 std::string description;
447 bool operator < (const ModelBlockInfo &other) const {
448 if (timestep != other.timestep)
449 return timestep < other.timestep;
450 if (description != other.description)
451 return description < other.description;
452 if (offset != other.offset)
453 return offset < other.offset;
454 if (width != other.width)
455 return width < other.width;
456 return false;
457 }
458 };
459
460 std::vector<int> modelExpressions;
461 std::vector<bool> modelValues;
462 std::set<ModelBlockInfo> modelInfo;
463
464 void maximize_undefs()
465 {
466 log_assert(enable_undef);
467 std::vector<bool> backupValues;
468
469 while (1)
470 {
471 std::vector<int> must_undef, maybe_undef;
472
473 for (size_t i = 0; i < modelExpressions.size()/2; i++)
474 if (modelValues.at(modelExpressions.size()/2 + i))
475 must_undef.push_back(modelExpressions.at(modelExpressions.size()/2 + i));
476 else
477 maybe_undef.push_back(modelExpressions.at(modelExpressions.size()/2 + i));
478
479 backupValues.swap(modelValues);
480 if (!solve(ez.expression(ezSAT::OpAnd, must_undef), ez.expression(ezSAT::OpOr, maybe_undef)))
481 break;
482 }
483
484 backupValues.swap(modelValues);
485 }
486
487 void generate_model()
488 {
489 RTLIL::SigSpec modelSig;
490 modelExpressions.clear();
491 modelInfo.clear();
492
493 // Add "show" signals or alternatively the leaves on the input cone on all set and prove signals
494
495 if (shows.size() == 0)
496 {
497 SigPool queued_signals, handled_signals, final_signals;
498 queued_signals = show_signal_pool;
499 while (queued_signals.size() > 0) {
500 RTLIL::SigSpec sig = queued_signals.export_one();
501 queued_signals.del(sig);
502 handled_signals.add(sig);
503 std::set<RTLIL::Cell*> drivers = show_drivers.find(sig);
504 if (drivers.size() == 0) {
505 final_signals.add(sig);
506 } else {
507 for (auto &d : drivers)
508 for (auto &p : d->connections_) {
509 if (d->type == "$dff" && p.first == "\\CLK")
510 continue;
511 if (d->type.substr(0, 6) == "$_DFF_" && p.first == "\\C")
512 continue;
513 queued_signals.add(handled_signals.remove(sigmap(p.second)));
514 }
515 }
516 }
517 modelSig = final_signals.export_all();
518
519 // additionally add all set and prove signals directly
520 // (it improves user confidence if we write the constraints back ;-)
521 modelSig.append(show_signal_pool.export_all());
522 }
523 else
524 {
525 for (auto &s : shows) {
526 RTLIL::SigSpec sig;
527 if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
528 log_cmd_error("Failed to parse show expression `%s'.\n", s.c_str());
529 log("Import show expression: %s\n", log_signal(sig));
530 modelSig.append(sig);
531 }
532 }
533
534 modelSig.sort_and_unify();
535 // log("Model signals: %s\n", log_signal(modelSig));
536
537 std::vector<int> modelUndefExpressions;
538
539 for (auto &c : modelSig.chunks())
540 if (c.wire != NULL)
541 {
542 ModelBlockInfo info;
543 RTLIL::SigSpec chunksig = c;
544 info.width = chunksig.size();
545 info.description = log_signal(chunksig);
546
547 for (int timestep = -1; timestep <= max_timestep; timestep++)
548 {
549 if ((timestep == -1 && max_timestep > 0) || timestep == 0)
550 continue;
551
552 info.timestep = timestep;
553 info.offset = modelExpressions.size();
554 modelInfo.insert(info);
555
556 std::vector<int> vec = satgen.importSigSpec(chunksig, timestep);
557 modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end());
558
559 if (enable_undef) {
560 std::vector<int> undef_vec = satgen.importUndefSigSpec(chunksig, timestep);
561 modelUndefExpressions.insert(modelUndefExpressions.end(), undef_vec.begin(), undef_vec.end());
562 }
563 }
564 }
565
566 // Add initial state signals as collected by satgen
567 //
568 modelSig = satgen.initial_state.export_all();
569 for (auto &c : modelSig.chunks())
570 if (c.wire != NULL)
571 {
572 ModelBlockInfo info;
573 RTLIL::SigSpec chunksig = c;
574
575 info.timestep = 0;
576 info.offset = modelExpressions.size();
577 info.width = chunksig.size();
578 info.description = log_signal(chunksig);
579 modelInfo.insert(info);
580
581 std::vector<int> vec = satgen.importSigSpec(chunksig, 1);
582 modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end());
583
584 if (enable_undef) {
585 std::vector<int> undef_vec = satgen.importUndefSigSpec(chunksig, 1);
586 modelUndefExpressions.insert(modelUndefExpressions.end(), undef_vec.begin(), undef_vec.end());
587 }
588 }
589
590 modelExpressions.insert(modelExpressions.end(), modelUndefExpressions.begin(), modelUndefExpressions.end());
591 }
592
593 void print_model()
594 {
595 int maxModelName = 10;
596 int maxModelWidth = 10;
597
598 for (auto &info : modelInfo) {
599 maxModelName = std::max(maxModelName, int(info.description.size()));
600 maxModelWidth = std::max(maxModelWidth, info.width);
601 }
602
603 log("\n");
604
605 int last_timestep = -2;
606 for (auto &info : modelInfo)
607 {
608 RTLIL::Const value;
609 bool found_undef = false;
610
611 for (int i = 0; i < info.width; i++) {
612 value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
613 if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i))
614 value.bits.back() = RTLIL::State::Sx, found_undef = true;
615 }
616
617 if (info.timestep != last_timestep) {
618 const char *hline = "---------------------------------------------------------------------------------------------------"
619 "---------------------------------------------------------------------------------------------------"
620 "---------------------------------------------------------------------------------------------------";
621 if (last_timestep == -2) {
622 log(max_timestep > 0 ? " Time " : " ");
623 log("%-*s %10s %10s %*s\n", maxModelName+10, "Signal Name", "Dec", "Hex", maxModelWidth+5, "Bin");
624 }
625 log(max_timestep > 0 ? " ---- " : " ");
626 log("%*.*s %10.10s %10.10s %*.*s\n", maxModelName+10, maxModelName+10,
627 hline, hline, hline, maxModelWidth+5, maxModelWidth+5, hline);
628 last_timestep = info.timestep;
629 }
630
631 if (max_timestep > 0) {
632 if (info.timestep > 0)
633 log(" %4d ", info.timestep);
634 else
635 log(" init ");
636 } else
637 log(" ");
638
639 if (info.width <= 32 && !found_undef)
640 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());
641 else
642 log("%-*s %10s %10s %*s\n", maxModelName+10, info.description.c_str(), "--", "--", maxModelWidth+5, value.as_string().c_str());
643 }
644
645 if (last_timestep == -2)
646 log(" no model variables selected for display.\n");
647 }
648
649 void dump_model_to_vcd(std::string vcd_file_name)
650 {
651 FILE *f = fopen(vcd_file_name.c_str(), "w");
652 if (!f)
653 log_cmd_error("Can't open output file `%s' for writing: %s\n", vcd_file_name.c_str(), strerror(errno));
654
655 log("Dumping SAT model to VCD file %s\n", vcd_file_name.c_str());
656
657 time_t timestamp;
658 struct tm* now;
659 char stime[128] = {};
660 time(&timestamp);
661 now = localtime(&timestamp);
662 strftime(stime, sizeof(stime), "%c", now);
663
664 std::string module_fname = "unknown";
665 auto apos = module->attributes.find("\\src");
666 if(apos != module->attributes.end())
667 module_fname = module->attributes["\\src"].decode_string();
668
669 fprintf(f, "$date\n");
670 fprintf(f, " %s\n", stime);
671 fprintf(f, "$end\n");
672 fprintf(f, "$version\n");
673 fprintf(f, " Generated by %s\n", yosys_version_str);
674 fprintf(f, "$end\n");
675 fprintf(f, "$comment\n");
676 fprintf(f, " Generated from SAT problem in module %s (declared at %s)\n",
677 module->name.c_str(), module_fname.c_str());
678 fprintf(f, "$end\n");
679
680 // VCD has some limits on internal (non-display) identifier names, so make legal ones
681 std::map<std::string, std::string> vcdnames;
682
683 fprintf(f, "$timescale 1ns\n"); // arbitrary time scale since actual clock period is unknown/unimportant
684 fprintf(f, "$scope module %s $end\n", module->name.c_str());
685 for (auto &info : modelInfo)
686 {
687 if (vcdnames.find(info.description) != vcdnames.end())
688 continue;
689
690 char namebuf[16];
691 snprintf(namebuf, sizeof(namebuf), "v%d", static_cast<int>(vcdnames.size()));
692 vcdnames[info.description] = namebuf;
693
694 // Even display identifiers can't use some special characters
695 std::string legal_desc = info.description.c_str();
696 for (auto &c : legal_desc) {
697 if(c == '$')
698 c = '_';
699 if(c == ':')
700 c = '_';
701 }
702
703 fprintf(f, "$var wire %d %s %s $end\n", info.width, namebuf, legal_desc.c_str());
704
705 // Need to look at first *two* cycles!
706 // We need to put a name on all variables but those without an initialization clause
707 // have no value at timestep 0
708 if(info.timestep > 1)
709 break;
710 }
711 fprintf(f, "$upscope $end\n");
712 fprintf(f, "$enddefinitions $end\n");
713 fprintf(f, "$dumpvars\n");
714
715 static const char bitvals[] = "01xzxx";
716
717 int last_timestep = -2;
718 for (auto &info : modelInfo)
719 {
720 RTLIL::Const value;
721
722 for (int i = 0; i < info.width; i++) {
723 value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
724 if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i))
725 value.bits.back() = RTLIL::State::Sx;
726 }
727
728 if (info.timestep != last_timestep) {
729 if(last_timestep == 0)
730 fprintf(f, "$end\n");
731 else
732 fprintf(f, "#%d\n", info.timestep);
733 last_timestep = info.timestep;
734 }
735
736 if(info.width == 1) {
737 fprintf(f, "%c%s\n", bitvals[value.bits[0]], vcdnames[info.description].c_str());
738 } else {
739 fprintf(f, "b");
740 for(int k=info.width-1; k >= 0; k --) //need to flip bit ordering for VCD
741 fprintf(f, "%c", bitvals[value.bits[k]]);
742 fprintf(f, " %s\n", vcdnames[info.description].c_str());
743 }
744 }
745
746 if (last_timestep == -2)
747 log(" no model variables selected for display.\n");
748
749 fclose(f);
750 }
751
752 void invalidate_model(bool max_undef)
753 {
754 std::vector<int> clause;
755 if (enable_undef) {
756 for (size_t i = 0; i < modelExpressions.size()/2; i++) {
757 int bit = modelExpressions.at(i), bit_undef = modelExpressions.at(modelExpressions.size()/2 + i);
758 bool val = modelValues.at(i), val_undef = modelValues.at(modelExpressions.size()/2 + i);
759 if (!max_undef || !val_undef)
760 clause.push_back(val_undef ? ez.NOT(bit_undef) : val ? ez.NOT(bit) : bit);
761 }
762 } else
763 for (size_t i = 0; i < modelExpressions.size(); i++)
764 clause.push_back(modelValues.at(i) ? ez.NOT(modelExpressions.at(i)) : modelExpressions.at(i));
765 ez.assume(ez.expression(ezSAT::OpOr, clause));
766 }
767 };
768
769 } /* namespace */
770
771 static void print_proof_failed()
772 {
773 log("\n");
774 log(" ______ ___ ___ _ _ _ _ \n");
775 log(" (_____ \\ / __) / __) (_) | | | |\n");
776 log(" _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |\n");
777 log(" | ____/ ___) _ \\ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|\n");
778 log(" | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ \n");
779 log(" |_| |_| \\___/ \\___/ |_| |_| \\_____|_|\\_)_____)\\____|_|\n");
780 log("\n");
781 }
782
783 static void print_timeout()
784 {
785 log("\n");
786 log(" _____ _ _ _____ ____ _ _____\n");
787 log(" /__ __\\/ \\/ \\__/|/ __// _ \\/ \\ /\\/__ __\\\n");
788 log(" / \\ | || |\\/||| \\ | / \\|| | || / \\\n");
789 log(" | | | || | ||| /_ | \\_/|| \\_/| | |\n");
790 log(" \\_/ \\_/\\_/ \\|\\____\\\\____/\\____/ \\_/\n");
791 log("\n");
792 }
793
794 static void print_qed()
795 {
796 log("\n");
797 log(" /$$$$$$ /$$$$$$$$ /$$$$$$$ \n");
798 log(" /$$__ $$ | $$_____/ | $$__ $$ \n");
799 log(" | $$ \\ $$ | $$ | $$ \\ $$ \n");
800 log(" | $$ | $$ | $$$$$ | $$ | $$ \n");
801 log(" | $$ | $$ | $$__/ | $$ | $$ \n");
802 log(" | $$/$$ $$ | $$ | $$ | $$ \n");
803 log(" | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
804 log(" \\____ $$$|__/|________/|__/|_______/|__/\n");
805 log(" \\__/ \n");
806 log("\n");
807 }
808
809 struct SatPass : public Pass {
810 SatPass() : Pass("sat", "solve a SAT problem in the circuit") { }
811 virtual void help()
812 {
813 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
814 log("\n");
815 log(" sat [options] [selection]\n");
816 log("\n");
817 log("This command solves a SAT problem defined over the currently selected circuit\n");
818 log("and additional constraints passed as parameters.\n");
819 log("\n");
820 log(" -all\n");
821 log(" show all solutions to the problem (this can grow exponentially, use\n");
822 log(" -max <N> instead to get <N> solutions)\n");
823 log("\n");
824 log(" -max <N>\n");
825 log(" like -all, but limit number of solutions to <N>\n");
826 log("\n");
827 log(" -enable_undef\n");
828 log(" enable modeling of undef value (aka 'x-bits')\n");
829 log(" this option is implied by -set-def, -set-undef et. cetera\n");
830 log("\n");
831 log(" -max_undef\n");
832 log(" maximize the number of undef bits in solutions, giving a better\n");
833 log(" picture of which input bits are actually vital to the solution.\n");
834 log("\n");
835 log(" -set <signal> <value>\n");
836 log(" set the specified signal to the specified value.\n");
837 log("\n");
838 log(" -set-def <signal>\n");
839 log(" add a constraint that all bits of the given signal must be defined\n");
840 log("\n");
841 log(" -set-any-undef <signal>\n");
842 log(" add a constraint that at least one bit of the given signal is undefined\n");
843 log("\n");
844 log(" -set-all-undef <signal>\n");
845 log(" add a constraint that all bits of the given signal are undefined\n");
846 log("\n");
847 log(" -set-def-inputs\n");
848 log(" add -set-def constraints for all module inputs\n");
849 log("\n");
850 log(" -show <signal>\n");
851 log(" show the model for the specified signal. if no -show option is\n");
852 log(" passed then a set of signals to be shown is automatically selected.\n");
853 log("\n");
854 log(" -show-inputs, -show-outputs\n");
855 log(" add all module input (output) ports to the list of shown signals\n");
856 log("\n");
857 log(" -ignore_div_by_zero\n");
858 log(" ignore all solutions that involve a division by zero\n");
859 log("\n");
860 log(" -ignore_unknown_cells\n");
861 log(" ignore all cells that can not be matched to a SAT model\n");
862 log("\n");
863 log("The following options can be used to set up a sequential problem:\n");
864 log("\n");
865 log(" -seq <N>\n");
866 log(" set up a sequential problem with <N> time steps. The steps will\n");
867 log(" be numbered from 1 to N.\n");
868 log("\n");
869 log(" -set-at <N> <signal> <value>\n");
870 log(" -unset-at <N> <signal>\n");
871 log(" set or unset the specified signal to the specified value in the\n");
872 log(" given timestep. this has priority over a -set for the same signal.\n");
873 log("\n");
874 log(" -set-def-at <N> <signal>\n");
875 log(" -set-any-undef-at <N> <signal>\n");
876 log(" -set-all-undef-at <N> <signal>\n");
877 log(" add undef contraints in the given timestep.\n");
878 log("\n");
879 log(" -set-init <signal> <value>\n");
880 log(" set the initial value for the register driving the signal to the value\n");
881 log("\n");
882 log(" -set-init-undef\n");
883 log(" set all initial states (not set using -set-init) to undef\n");
884 log("\n");
885 log(" -set-init-def\n");
886 log(" do not force a value for the initial state but do not allow undef\n");
887 log("\n");
888 log(" -set-init-zero\n");
889 log(" set all initial states (not set using -set-init) to zero\n");
890 log("\n");
891 log(" -dump_vcd <vcd-file-name>\n");
892 log(" dump SAT model (counter example in proof) to VCD file\n");
893 log("\n");
894 log(" -dump_cnf <cnf-file-name>\n");
895 log(" dump CNF of SAT problem (in DIMACS format). in temporal induction\n");
896 log(" proofs this is the CNF of the first induction step.\n");
897 log("\n");
898 log("The following additional options can be used to set up a proof. If also -seq\n");
899 log("is passed, a temporal induction proof is performed.\n");
900 log("\n");
901 log(" -tempinduct\n");
902 log(" Perform a temporal induction proof. In a temporalinduction proof it is\n");
903 log(" proven that the condition holds forever after the number of time steps\n");
904 log(" specified using -seq.\n");
905 log("\n");
906 log(" -tempinduct-def\n");
907 log(" Perform a temporal induction proof. Assume an initial state with all\n");
908 log(" registers set to defined values for the induction step.\n");
909 log("\n");
910 log(" -prove <signal> <value>\n");
911 log(" Attempt to proof that <signal> is always <value>.\n");
912 log("\n");
913 log(" -prove-x <signal> <value>\n");
914 log(" Like -prove, but an undef (x) bit in the lhs matches any value on\n");
915 log(" the right hand side. Useful for equivialence checking.\n");
916 log("\n");
917 log(" -prove-asserts\n");
918 log(" Prove that all asserts in the design hold.\n");
919 log("\n");
920 log(" -maxsteps <N>\n");
921 log(" Set a maximum length for the induction.\n");
922 log("\n");
923 log(" -initsteps <N>\n");
924 log(" Set initial length for the induction.\n");
925 log("\n");
926 log(" -timeout <N>\n");
927 log(" Maximum number of seconds a single SAT instance may take.\n");
928 log("\n");
929 log(" -verify\n");
930 log(" Return an error and stop the synthesis script if the proof fails.\n");
931 log("\n");
932 log(" -verify-no-timeout\n");
933 log(" Like -verify but do not return an error for timeouts.\n");
934 log("\n");
935 log(" -falsify\n");
936 log(" Return an error and stop the synthesis script if the proof succeeds.\n");
937 log("\n");
938 log(" -falsify-no-timeout\n");
939 log(" Like -falsify but do not return an error for timeouts.\n");
940 log("\n");
941 }
942 virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
943 {
944 std::vector<std::pair<std::string, std::string>> sets, sets_init, prove, prove_x;
945 std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
946 std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
947 std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
948 int loopcount = 0, seq_len = 0, maxsteps = 0, initsteps = 0, timeout = 0;
949 bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
950 bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false;
951 bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
952 bool ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false;
953 std::string vcd_file_name, cnf_file_name;
954
955 log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
956
957 size_t argidx;
958 for (argidx = 1; argidx < args.size(); argidx++) {
959 if (args[argidx] == "-all") {
960 loopcount = -1;
961 continue;
962 }
963 if (args[argidx] == "-verify") {
964 fail_on_timeout = true;
965 verify = true;
966 continue;
967 }
968 if (args[argidx] == "-verify-no-timeout") {
969 verify = true;
970 continue;
971 }
972 if (args[argidx] == "-falsify") {
973 fail_on_timeout = true;
974 falsify = true;
975 continue;
976 }
977 if (args[argidx] == "-falsify-no-timeout") {
978 falsify = true;
979 continue;
980 }
981 if (args[argidx] == "-timeout" && argidx+1 < args.size()) {
982 timeout = atoi(args[++argidx].c_str());
983 continue;
984 }
985 if (args[argidx] == "-max" && argidx+1 < args.size()) {
986 loopcount = atoi(args[++argidx].c_str());
987 continue;
988 }
989 if (args[argidx] == "-maxsteps" && argidx+1 < args.size()) {
990 maxsteps = atoi(args[++argidx].c_str());
991 continue;
992 }
993 if (args[argidx] == "-initsteps" && argidx+1 < args.size()) {
994 initsteps = atoi(args[++argidx].c_str());
995 continue;
996 }
997 if (args[argidx] == "-ignore_div_by_zero") {
998 ignore_div_by_zero = true;
999 continue;
1000 }
1001 if (args[argidx] == "-enable_undef") {
1002 enable_undef = true;
1003 continue;
1004 }
1005 if (args[argidx] == "-max_undef") {
1006 enable_undef = true;
1007 max_undef = true;
1008 continue;
1009 }
1010 if (args[argidx] == "-set-def-inputs") {
1011 enable_undef = true;
1012 set_def_inputs = true;
1013 continue;
1014 }
1015 if (args[argidx] == "-set" && argidx+2 < args.size()) {
1016 std::string lhs = args[++argidx];
1017 std::string rhs = args[++argidx];
1018 sets.push_back(std::pair<std::string, std::string>(lhs, rhs));
1019 continue;
1020 }
1021 if (args[argidx] == "-set-def" && argidx+1 < args.size()) {
1022 sets_def.push_back(args[++argidx]);
1023 enable_undef = true;
1024 continue;
1025 }
1026 if (args[argidx] == "-set-any-undef" && argidx+1 < args.size()) {
1027 sets_any_undef.push_back(args[++argidx]);
1028 enable_undef = true;
1029 continue;
1030 }
1031 if (args[argidx] == "-set-all-undef" && argidx+1 < args.size()) {
1032 sets_all_undef.push_back(args[++argidx]);
1033 enable_undef = true;
1034 continue;
1035 }
1036 if (args[argidx] == "-tempinduct") {
1037 tempinduct = true;
1038 continue;
1039 }
1040 if (args[argidx] == "-tempinduct-def") {
1041 tempinduct = true;
1042 tempinduct_def = true;
1043 continue;
1044 }
1045 if (args[argidx] == "-prove" && argidx+2 < args.size()) {
1046 std::string lhs = args[++argidx];
1047 std::string rhs = args[++argidx];
1048 prove.push_back(std::pair<std::string, std::string>(lhs, rhs));
1049 continue;
1050 }
1051 if (args[argidx] == "-prove-x" && argidx+2 < args.size()) {
1052 std::string lhs = args[++argidx];
1053 std::string rhs = args[++argidx];
1054 prove_x.push_back(std::pair<std::string, std::string>(lhs, rhs));
1055 enable_undef = true;
1056 continue;
1057 }
1058 if (args[argidx] == "-prove-asserts") {
1059 prove_asserts = true;
1060 continue;
1061 }
1062 if (args[argidx] == "-seq" && argidx+1 < args.size()) {
1063 seq_len = atoi(args[++argidx].c_str());
1064 continue;
1065 }
1066 if (args[argidx] == "-set-at" && argidx+3 < args.size()) {
1067 int timestep = atoi(args[++argidx].c_str());
1068 std::string lhs = args[++argidx];
1069 std::string rhs = args[++argidx];
1070 sets_at[timestep].push_back(std::pair<std::string, std::string>(lhs, rhs));
1071 continue;
1072 }
1073 if (args[argidx] == "-unset-at" && argidx+2 < args.size()) {
1074 int timestep = atoi(args[++argidx].c_str());
1075 unsets_at[timestep].push_back(args[++argidx]);
1076 continue;
1077 }
1078 if (args[argidx] == "-set-def-at" && argidx+2 < args.size()) {
1079 int timestep = atoi(args[++argidx].c_str());
1080 sets_def_at[timestep].push_back(args[++argidx]);
1081 enable_undef = true;
1082 continue;
1083 }
1084 if (args[argidx] == "-set-any-undef-at" && argidx+2 < args.size()) {
1085 int timestep = atoi(args[++argidx].c_str());
1086 sets_any_undef_at[timestep].push_back(args[++argidx]);
1087 enable_undef = true;
1088 continue;
1089 }
1090 if (args[argidx] == "-set-all-undef-at" && argidx+2 < args.size()) {
1091 int timestep = atoi(args[++argidx].c_str());
1092 sets_all_undef_at[timestep].push_back(args[++argidx]);
1093 enable_undef = true;
1094 continue;
1095 }
1096 if (args[argidx] == "-set-init" && argidx+2 < args.size()) {
1097 std::string lhs = args[++argidx];
1098 std::string rhs = args[++argidx];
1099 sets_init.push_back(std::pair<std::string, std::string>(lhs, rhs));
1100 continue;
1101 }
1102 if (args[argidx] == "-set-init-undef") {
1103 set_init_undef = true;
1104 enable_undef = true;
1105 continue;
1106 }
1107 if (args[argidx] == "-set-init-def") {
1108 set_init_def = true;
1109 continue;
1110 }
1111 if (args[argidx] == "-set-init-zero") {
1112 set_init_zero = true;
1113 continue;
1114 }
1115 if (args[argidx] == "-show" && argidx+1 < args.size()) {
1116 shows.push_back(args[++argidx]);
1117 continue;
1118 }
1119 if (args[argidx] == "-show-inputs") {
1120 show_inputs = true;
1121 continue;
1122 }
1123 if (args[argidx] == "-show-outputs") {
1124 show_outputs = true;
1125 continue;
1126 }
1127 if (args[argidx] == "-ignore_unknown_cells") {
1128 ignore_unknown_cells = true;
1129 continue;
1130 }
1131 if (args[argidx] == "-dump_vcd" && argidx+1 < args.size()) {
1132 vcd_file_name = args[++argidx];
1133 continue;
1134 }
1135 if (args[argidx] == "-dump_cnf" && argidx+1 < args.size()) {
1136 cnf_file_name = args[++argidx];
1137 continue;
1138 }
1139 break;
1140 }
1141 extra_args(args, argidx, design);
1142
1143 RTLIL::Module *module = NULL;
1144 for (auto &mod_it : design->modules)
1145 if (design->selected(mod_it.second)) {
1146 if (module)
1147 log_cmd_error("Only one module must be selected for the SAT pass! (selected: %s and %s)\n",
1148 RTLIL::id2cstr(module->name), RTLIL::id2cstr(mod_it.first));
1149 module = mod_it.second;
1150 }
1151 if (module == NULL)
1152 log_cmd_error("Can't perform SAT on an empty selection!\n");
1153
1154 if (!prove.size() && !prove_x.size() && !prove_asserts && tempinduct)
1155 log_cmd_error("Got -tempinduct but nothing to prove!\n");
1156
1157 if (set_init_undef + set_init_zero + set_init_def > 1)
1158 log_cmd_error("The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!\n");
1159
1160 if (set_def_inputs) {
1161 for (auto &it : module->wires)
1162 if (it.second->port_input)
1163 sets_def.push_back(it.second->name);
1164 }
1165
1166 if (show_inputs) {
1167 for (auto &it : module->wires)
1168 if (it.second->port_input)
1169 shows.push_back(it.second->name);
1170 }
1171
1172 if (show_outputs) {
1173 for (auto &it : module->wires)
1174 if (it.second->port_output)
1175 shows.push_back(it.second->name);
1176 }
1177
1178 if (tempinduct)
1179 {
1180 if (loopcount > 0 || max_undef)
1181 log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
1182
1183 SatHelper basecase(design, module, enable_undef);
1184 SatHelper inductstep(design, module, enable_undef);
1185
1186 basecase.sets = sets;
1187 basecase.prove = prove;
1188 basecase.prove_x = prove_x;
1189 basecase.prove_asserts = prove_asserts;
1190 basecase.sets_at = sets_at;
1191 basecase.unsets_at = unsets_at;
1192 basecase.shows = shows;
1193 basecase.timeout = timeout;
1194 basecase.sets_def = sets_def;
1195 basecase.sets_any_undef = sets_any_undef;
1196 basecase.sets_all_undef = sets_all_undef;
1197 basecase.sets_def_at = sets_def_at;
1198 basecase.sets_any_undef_at = sets_any_undef_at;
1199 basecase.sets_all_undef_at = sets_all_undef_at;
1200 basecase.sets_init = sets_init;
1201 basecase.set_init_def = set_init_def;
1202 basecase.set_init_undef = set_init_undef;
1203 basecase.set_init_zero = set_init_zero;
1204 basecase.satgen.ignore_div_by_zero = ignore_div_by_zero;
1205 basecase.ignore_unknown_cells = ignore_unknown_cells;
1206
1207 for (int timestep = 1; timestep <= seq_len; timestep++)
1208 basecase.setup(timestep);
1209 basecase.setup_init();
1210
1211 inductstep.sets = sets;
1212 inductstep.prove = prove;
1213 inductstep.prove_x = prove_x;
1214 inductstep.prove_asserts = prove_asserts;
1215 inductstep.shows = shows;
1216 inductstep.timeout = timeout;
1217 inductstep.sets_def = sets_def;
1218 inductstep.sets_any_undef = sets_any_undef;
1219 inductstep.sets_all_undef = sets_all_undef;
1220 inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero;
1221 inductstep.ignore_unknown_cells = ignore_unknown_cells;
1222
1223 inductstep.setup(1);
1224 inductstep.ez.assume(inductstep.setup_proof(1));
1225
1226 if (tempinduct_def) {
1227 std::vector<int> undef_state = inductstep.satgen.importUndefSigSpec(inductstep.satgen.initial_state.export_all(), 1);
1228 inductstep.ez.assume(inductstep.ez.NOT(inductstep.ez.expression(ezSAT::OpOr, undef_state)));
1229 }
1230
1231 for (int inductlen = 1; inductlen <= maxsteps || maxsteps == 0; inductlen++)
1232 {
1233 log("\n** Trying induction with length %d **\n", inductlen);
1234
1235 // phase 1: proving base case
1236
1237 basecase.setup(seq_len + inductlen);
1238 int property = basecase.setup_proof(seq_len + inductlen);
1239 basecase.generate_model();
1240
1241 if (inductlen > 1)
1242 basecase.force_unique_state(seq_len + 1, seq_len + inductlen);
1243
1244 log("\n[base case] Solving problem with %d variables and %d clauses..\n",
1245 basecase.ez.numCnfVariables(), basecase.ez.numCnfClauses());
1246
1247 if (basecase.solve(basecase.ez.NOT(property))) {
1248 log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
1249 print_proof_failed();
1250 basecase.print_model();
1251 if(!vcd_file_name.empty())
1252 basecase.dump_model_to_vcd(vcd_file_name);
1253 goto tip_failed;
1254 }
1255
1256 if (basecase.gotTimeout)
1257 goto timeout;
1258
1259 log("Base case for induction length %d proven.\n", inductlen);
1260 basecase.ez.assume(property);
1261
1262 // phase 2: proving induction step
1263
1264 inductstep.setup(inductlen + 1);
1265 property = inductstep.setup_proof(inductlen + 1);
1266 inductstep.generate_model();
1267
1268 if (inductlen > 1)
1269 inductstep.force_unique_state(1, inductlen + 1);
1270
1271 if (inductlen < initsteps)
1272 {
1273 log("\n[induction step] Skipping problem with %d variables and %d clauses (below initsteps).\n",
1274 inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
1275 inductstep.ez.assume(property);
1276 }
1277 else
1278 {
1279 if (!cnf_file_name.empty())
1280 {
1281 FILE *f = fopen(cnf_file_name.c_str(), "w");
1282 if (!f)
1283 log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
1284
1285 log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
1286 cnf_file_name.clear();
1287
1288 inductstep.ez.printDIMACS(f, false);
1289 fclose(f);
1290 }
1291
1292 log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
1293 inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
1294
1295 if (!inductstep.solve(inductstep.ez.NOT(property))) {
1296 if (inductstep.gotTimeout)
1297 goto timeout;
1298 log("Induction step proven: SUCCESS!\n");
1299 print_qed();
1300 goto tip_success;
1301 }
1302
1303 log("Induction step failed. Incrementing induction length.\n");
1304 inductstep.ez.assume(property);
1305 inductstep.print_model();
1306 }
1307 }
1308
1309 log("\nReached maximum number of time steps -> proof failed.\n");
1310 print_proof_failed();
1311
1312 tip_failed:
1313 if (verify) {
1314 log("\n");
1315 log_error("Called with -verify and proof did fail!\n");
1316 }
1317
1318 if (0)
1319 tip_success:
1320 if (falsify) {
1321 log("\n");
1322 log_error("Called with -falsify and proof did succeed!\n");
1323 }
1324 }
1325 else
1326 {
1327 if (maxsteps > 0)
1328 log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
1329
1330 SatHelper sathelper(design, module, enable_undef);
1331
1332 sathelper.sets = sets;
1333 sathelper.prove = prove;
1334 sathelper.prove_x = prove_x;
1335 sathelper.prove_asserts = prove_asserts;
1336 sathelper.sets_at = sets_at;
1337 sathelper.unsets_at = unsets_at;
1338 sathelper.shows = shows;
1339 sathelper.timeout = timeout;
1340 sathelper.sets_def = sets_def;
1341 sathelper.sets_any_undef = sets_any_undef;
1342 sathelper.sets_all_undef = sets_all_undef;
1343 sathelper.sets_def_at = sets_def_at;
1344 sathelper.sets_any_undef_at = sets_any_undef_at;
1345 sathelper.sets_all_undef_at = sets_all_undef_at;
1346 sathelper.sets_init = sets_init;
1347 sathelper.set_init_def = set_init_def;
1348 sathelper.set_init_undef = set_init_undef;
1349 sathelper.set_init_zero = set_init_zero;
1350 sathelper.satgen.ignore_div_by_zero = ignore_div_by_zero;
1351 sathelper.ignore_unknown_cells = ignore_unknown_cells;
1352
1353 if (seq_len == 0) {
1354 sathelper.setup();
1355 if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
1356 sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof()));
1357 } else {
1358 std::vector<int> prove_bits;
1359 for (int timestep = 1; timestep <= seq_len; timestep++) {
1360 sathelper.setup(timestep);
1361 if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
1362 prove_bits.push_back(sathelper.setup_proof(timestep));
1363 }
1364 if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
1365 sathelper.ez.assume(sathelper.ez.NOT(sathelper.ez.expression(ezSAT::OpAnd, prove_bits)));
1366 sathelper.setup_init();
1367 }
1368 sathelper.generate_model();
1369
1370 if (!cnf_file_name.empty())
1371 {
1372 FILE *f = fopen(cnf_file_name.c_str(), "w");
1373 if (!f)
1374 log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
1375
1376 log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
1377 cnf_file_name.clear();
1378
1379 sathelper.ez.printDIMACS(f, false);
1380 fclose(f);
1381 }
1382
1383 int rerun_counter = 0;
1384
1385 rerun_solver:
1386 log("\nSolving problem with %d variables and %d clauses..\n",
1387 sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses());
1388
1389 if (sathelper.solve())
1390 {
1391 if (max_undef) {
1392 log("SAT model found. maximizing number of undefs.\n");
1393 sathelper.maximize_undefs();
1394 }
1395
1396 if (!prove.size() && !prove_x.size() && !prove_asserts) {
1397 log("SAT solving finished - model found:\n");
1398 } else {
1399 log("SAT proof finished - model found: FAIL!\n");
1400 print_proof_failed();
1401 }
1402
1403 sathelper.print_model();
1404
1405 if(!vcd_file_name.empty())
1406 sathelper.dump_model_to_vcd(vcd_file_name);
1407
1408 if (loopcount != 0) {
1409 loopcount--, rerun_counter++;
1410 sathelper.invalidate_model(max_undef);
1411 goto rerun_solver;
1412 }
1413
1414 if (!prove.size() && !prove_x.size() && !prove_asserts) {
1415 if (falsify) {
1416 log("\n");
1417 log_error("Called with -falsify and found a model!\n");
1418 }
1419 } else {
1420 if (verify) {
1421 log("\n");
1422 log_error("Called with -verify and proof did fail!\n");
1423 }
1424 }
1425 }
1426 else
1427 {
1428 if (sathelper.gotTimeout)
1429 goto timeout;
1430 if (rerun_counter)
1431 log("SAT solving finished - no more models found (after %d distinct solutions).\n", rerun_counter);
1432 else if (!prove.size() && !prove_x.size() && !prove_asserts) {
1433 log("SAT solving finished - no model found.\n");
1434 if (verify) {
1435 log("\n");
1436 log_error("Called with -verify and found no model!\n");
1437 }
1438 } else {
1439 log("SAT proof finished - no model found: SUCCESS!\n");
1440 print_qed();
1441 if (falsify) {
1442 log("\n");
1443 log_error("Called with -falsify and proof did succeed!\n");
1444 }
1445 }
1446 }
1447
1448 if (!prove.size() && !prove_x.size() && !prove_asserts) {
1449 if (falsify && rerun_counter) {
1450 log("\n");
1451 log_error("Called with -falsify and found a model!\n");
1452 }
1453 } else {
1454 if (verify && rerun_counter) {
1455 log("\n");
1456 log_error("Called with -verify and proof did fail!\n");
1457 }
1458 }
1459 }
1460
1461 if (0) {
1462 timeout:
1463 log("Interrupted SAT solver: TIMEOUT!\n");
1464 print_timeout();
1465 if (fail_on_timeout)
1466 log_error("Called with -verify and proof did time out!\n");
1467 }
1468 }
1469 } SatPass;
1470