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