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