2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
6 * Permission to use, copy, modify, and/or distribute this software for any
7 * purpose with or without fee is hereby granted, provided that the above
8 * copyright notice and this permission notice appear in all copies.
10 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
11 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
12 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
13 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
14 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
15 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
16 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
20 // [[CITE]] 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
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"
37 PRIVATE_NAMESPACE_BEGIN
41 RTLIL::Design
*design
;
42 RTLIL::Module
*module
;
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
;
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
;
62 std::vector
<std::string
> shows
;
63 SigPool show_signal_pool
;
64 SigSet
<RTLIL::Cell
*> show_drivers
;
65 int max_timestep
, timeout
;
68 SatHelper(RTLIL::Design
*design
, RTLIL::Module
*module
, bool enable_undef
) :
69 design(design
), module(module
), sigmap(module
), ct(design
), satgen(ez
.get(), &sigmap
)
71 this->enable_undef
= enable_undef
;
72 satgen
.model_undef
= enable_undef
;
74 set_init_undef
= false;
75 set_init_zero
= false;
76 ignore_unknown_cells
= false;
82 void check_undef_enabled(const RTLIL::SigSpec
&sig
)
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
));
93 void setup(int timestep
= -1, bool initstate
= false)
96 log ("\nSetting up time step %d:\n", timestep
);
98 log ("\nSetting up SAT problem:\n");
101 satgen
.setInitState(timestep
);
103 if (timestep
> max_timestep
)
104 max_timestep
= timestep
;
106 RTLIL::SigSpec big_lhs
, big_rhs
;
110 RTLIL::SigSpec lhs
, rhs
;
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
));
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());
123 log("Import set-constraint: %s = %s\n", log_signal(lhs
), log_signal(rhs
));
124 big_lhs
.remove2(lhs
, &big_rhs
);
129 for (auto &s
: sets_at
[timestep
])
131 RTLIL::SigSpec lhs
, rhs
;
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
));
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());
144 log("Import set-constraint for this timestep: %s = %s\n", log_signal(lhs
), log_signal(rhs
));
145 big_lhs
.remove2(lhs
, &big_rhs
);
150 for (auto &s
: unsets_at
[timestep
])
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
));
158 log("Import unset-constraint for this timestep: %s\n", log_signal(lhs
));
159 big_lhs
.remove2(lhs
, &big_rhs
);
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
));
167 // 1 = sets_any_undef
168 // 2 = sets_all_undef
169 std::set
<RTLIL::SigSpec
> sets_def_undef
[3];
171 for (auto &s
: sets_def
) {
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
);
178 for (auto &s
: sets_any_undef
) {
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
);
185 for (auto &s
: sets_all_undef
) {
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
);
192 for (auto &s
: sets_def_at
[timestep
]) {
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
);
201 for (auto &s
: sets_any_undef_at
[timestep
]) {
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
);
210 for (auto &s
: sets_all_undef_at
[timestep
]) {
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
);
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
);
224 ez
->assume(ez
->NOT(ez
->expression(ezSAT::OpOr
, undef_sig
)));
226 ez
->assume(ez
->expression(ezSAT::OpOr
, undef_sig
));
228 ez
->assume(ez
->expression(ezSAT::OpAnd
, undef_sig
));
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
));
243 log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell
->name
), RTLIL::id2cstr(cell
->type
));
245 log("Imported %d cells to SAT database.\n", import_cell_counter
);
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
));
257 RTLIL::SigSpec big_lhs
, big_rhs
;
259 for (auto &it
: module
->wires_
)
261 if (it
.second
->attributes
.count("\\init") == 0)
264 RTLIL::SigSpec lhs
= sigmap(it
.second
);
265 RTLIL::SigSpec rhs
= it
.second
->attributes
.at("\\init");
266 log_assert(lhs
.size() == rhs
.size());
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
)
273 if (!satgen
.initial_state
.check_all(bit
)) {
274 removed_bits
.append(bit
);
281 if (removed_bits
.size())
282 log_warning("ignoring initial value on non-register: %s\n", log_signal(removed_bits
));
285 log("Import set-constraint from init attribute: %s = %s\n", log_signal(lhs
), log_signal(rhs
));
286 big_lhs
.remove2(lhs
, &big_rhs
);
292 for (auto &s
: sets_init
)
294 RTLIL::SigSpec lhs
, rhs
;
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
));
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());
307 log("Import init set-constraint: %s = %s\n", log_signal(lhs
), log_signal(rhs
));
308 big_lhs
.remove2(lhs
, &big_rhs
);
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
));
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
)));
324 if (set_init_undef
) {
325 RTLIL::SigSpec rem
= satgen
.initial_state
.export_all();
328 big_rhs
.append(RTLIL::SigSpec(RTLIL::State::Sx
, rem
.size()));
332 RTLIL::SigSpec rem
= satgen
.initial_state
.export_all();
335 big_rhs
.append(RTLIL::SigSpec(RTLIL::State::S0
, rem
.size()));
338 if (big_lhs
.size() == 0) {
339 log("No constraints for initial state found.\n\n");
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
));
349 int setup_proof(int timestep
= -1)
351 log_assert(prove
.size() || prove_x
.size() || prove_asserts
);
353 RTLIL::SigSpec big_lhs
, big_rhs
;
354 std::vector
<int> prove_bits
;
356 if (prove
.size() > 0)
358 for (auto &s
: prove
)
360 RTLIL::SigSpec lhs
, rhs
;
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
));
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());
373 log("Import proof-constraint: %s = %s\n", log_signal(lhs
), log_signal(rhs
));
374 big_lhs
.remove2(lhs
, &big_rhs
);
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
));
384 if (prove_x
.size() > 0)
386 for (auto &s
: prove_x
)
388 RTLIL::SigSpec lhs
, rhs
;
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
));
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());
401 log("Import proof-x-constraint: %s = %s\n", log_signal(lhs
), log_signal(rhs
));
402 big_lhs
.remove2(lhs
, &big_rhs
);
407 log("Final proof-x equation: %s = %s\n", log_signal(big_lhs
), log_signal(big_rhs
));
409 std::vector
<int> value_lhs
= satgen
.importDefSigSpec(big_lhs
, timestep
);
410 std::vector
<int> value_rhs
= satgen
.importDefSigSpec(big_rhs
, timestep
);
412 std::vector
<int> undef_lhs
= satgen
.importUndefSigSpec(big_lhs
, timestep
);
413 std::vector
<int> undef_rhs
= satgen
.importUndefSigSpec(big_rhs
, timestep
);
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
))))));
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
));
427 return ez
->expression(ezSAT::OpAnd
, prove_bits
);
430 void force_unique_state(int timestep_from
, int timestep_to
)
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
)));
437 bool solve(const std::vector
<int> &assumptions
)
439 log_assert(gotTimeout
== false);
440 ez
->setSolverTimeout(timeout
);
441 bool success
= ez
->solve(modelExpressions
, modelValues
, assumptions
);
442 if (ez
->getSolverTimoutStatus())
447 bool solve(int a
= 0, int b
= 0, int c
= 0, int d
= 0, int e
= 0, int f
= 0)
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())
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
;
473 std::vector
<int> modelExpressions
;
474 std::vector
<bool> modelValues
;
475 std::set
<ModelBlockInfo
> modelInfo
;
477 void maximize_undefs()
479 log_assert(enable_undef
);
480 std::vector
<bool> backupValues
;
484 std::vector
<int> must_undef
, maybe_undef
;
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
));
490 maybe_undef
.push_back(modelExpressions
.at(modelExpressions
.size()/2 + i
));
492 backupValues
.swap(modelValues
);
493 if (!solve(ez
->expression(ezSAT::OpAnd
, must_undef
), ez
->expression(ezSAT::OpOr
, maybe_undef
)))
497 backupValues
.swap(modelValues
);
500 void generate_model()
502 RTLIL::SigSpec modelSig
;
503 modelExpressions
.clear();
506 // Add "show" signals or alternatively the leaves on the input cone on all set and prove signals
508 if (shows
.size() == 0)
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
);
520 for (auto &d
: drivers
)
521 for (auto &p
: d
->connections()) {
522 if (d
->type
== "$dff" && p
.first
== "\\CLK")
524 if (d
->type
.begins_with("$_DFF_") && p
.first
== "\\C")
526 queued_signals
.add(handled_signals
.remove(sigmap(p
.second
)));
530 modelSig
= final_signals
.export_all();
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());
538 for (auto &s
: shows
) {
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
);
547 modelSig
.sort_and_unify();
548 // log("Model signals: %s\n", log_signal(modelSig));
550 std::vector
<int> modelUndefExpressions
;
552 for (auto &c
: modelSig
.chunks())
556 RTLIL::SigSpec chunksig
= c
;
557 info
.width
= chunksig
.size();
558 info
.description
= log_signal(chunksig
);
560 for (int timestep
= -1; timestep
<= max_timestep
; timestep
++)
562 if ((timestep
== -1 && max_timestep
> 0) || timestep
== 0)
565 info
.timestep
= timestep
;
566 info
.offset
= modelExpressions
.size();
567 modelInfo
.insert(info
);
569 std::vector
<int> vec
= satgen
.importSigSpec(chunksig
, timestep
);
570 modelExpressions
.insert(modelExpressions
.end(), vec
.begin(), vec
.end());
573 std::vector
<int> undef_vec
= satgen
.importUndefSigSpec(chunksig
, timestep
);
574 modelUndefExpressions
.insert(modelUndefExpressions
.end(), undef_vec
.begin(), undef_vec
.end());
579 // Add initial state signals as collected by satgen
581 modelSig
= satgen
.initial_state
.export_all();
582 for (auto &c
: modelSig
.chunks())
586 RTLIL::SigSpec chunksig
= c
;
589 info
.offset
= modelExpressions
.size();
590 info
.width
= chunksig
.size();
591 info
.description
= log_signal(chunksig
);
592 modelInfo
.insert(info
);
594 std::vector
<int> vec
= satgen
.importSigSpec(chunksig
, 1);
595 modelExpressions
.insert(modelExpressions
.end(), vec
.begin(), vec
.end());
598 std::vector
<int> undef_vec
= satgen
.importUndefSigSpec(chunksig
, 1);
599 modelUndefExpressions
.insert(modelUndefExpressions
.end(), undef_vec
.begin(), undef_vec
.end());
603 modelExpressions
.insert(modelExpressions
.end(), modelUndefExpressions
.begin(), modelUndefExpressions
.end());
608 int maxModelName
= 10;
609 int maxModelWidth
= 10;
611 for (auto &info
: modelInfo
) {
612 maxModelName
= max(maxModelName
, int(info
.description
.size()));
613 maxModelWidth
= max(maxModelWidth
, info
.width
);
618 int last_timestep
= -2;
619 for (auto &info
: modelInfo
)
622 bool found_undef
= false;
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;
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");
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
;
644 if (max_timestep
> 0) {
645 if (info
.timestep
> 0)
646 log(" %4d ", info
.timestep
);
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());
655 log("%-*s %11s %9s %*s\n", maxModelName
+5, info
.description
.c_str(), "--", "--", maxModelWidth
+3, value
.as_string().c_str());
658 if (last_timestep
== -2)
659 log(" no model variables selected for display.\n");
662 void dump_model_to_vcd(std::string vcd_file_name
)
664 rewrite_filename(vcd_file_name
);
665 FILE *f
= fopen(vcd_file_name
.c_str(), "w");
667 log_cmd_error("Can't open output file `%s' for writing: %s\n", vcd_file_name
.c_str(), strerror(errno
));
669 log("Dumping SAT model to VCD file %s\n", vcd_file_name
.c_str());
673 char stime
[128] = {};
675 now
= localtime(×tamp
);
676 strftime(stime
, sizeof(stime
), "%c", now
);
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();
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");
694 // VCD has some limits on internal (non-display) identifier names, so make legal ones
695 std::map
<std::string
, std::string
> vcdnames
;
697 fprintf(f
, "$scope module %s $end\n", module
->name
.c_str());
698 for (auto &info
: modelInfo
)
700 if (vcdnames
.find(info
.description
) != vcdnames
.end())
704 snprintf(namebuf
, sizeof(namebuf
), "v%d", static_cast<int>(vcdnames
.size()));
705 vcdnames
[info
.description
] = namebuf
;
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
) {
716 fprintf(f
, "$var wire %d %s %s $end\n", info
.width
, namebuf
, legal_desc
.c_str());
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)
724 fprintf(f
, "$upscope $end\n");
725 fprintf(f
, "$enddefinitions $end\n");
726 fprintf(f
, "$dumpvars\n");
728 static const char bitvals
[] = "01xzxx";
730 int last_timestep
= -2;
731 for (auto &info
: modelInfo
)
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
;
741 if (info
.timestep
!= last_timestep
) {
742 if(last_timestep
== 0)
743 fprintf(f
, "$end\n");
745 fprintf(f
, "#%d\n", info
.timestep
);
746 last_timestep
= info
.timestep
;
749 if(info
.width
== 1) {
750 fprintf(f
, "%c%s\n", bitvals
[value
.bits
[0]], vcdnames
[info
.description
].c_str());
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());
759 if (last_timestep
== -2)
760 log(" no model variables selected for display.\n");
765 void dump_model_to_json(std::string json_file_name
)
767 rewrite_filename(json_file_name
);
768 FILE *f
= fopen(json_file_name
.c_str(), "w");
770 log_cmd_error("Can't open output file `%s' for writing: %s\n", json_file_name
.c_str(), strerror(errno
));
772 log("Dumping SAT model to WaveJSON file '%s'.\n", json_file_name
.c_str());
774 int mintime
= 1, maxtime
= 0, maxwidth
= 0;;
775 dict
<string
, pair
<int, dict
<int, Const
>>> wavedata
;
777 for (auto &info
: modelInfo
)
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
;
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
);
793 fprintf(f
, "{ \"signal\": [");
794 bool fist_wavedata
= true;
795 for (auto &wd
: wavedata
)
797 fprintf(f
, "%s", fist_wavedata
? "\n" : ",\n");
798 fist_wavedata
= false;
801 string name
= wd
.first
.c_str();
802 while (name
.compare(0, 1, "\\") == 0)
803 name
= name
.substr(1);
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();
810 if (wd
.second
.first
== 1)
812 if (!data
.empty() && data
.back() == this_data
) {
815 data
.push_back(this_data
);
816 fprintf(f
, "%c", ch
);
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());
832 fprintf(f
, "\n ],\n");
833 fprintf(f
, " \"config\": {\n");
834 fprintf(f
, " \"hscale\": %.2f\n", maxwidth
/ 4.0);
840 void invalidate_model(bool max_undef
)
842 std::vector
<int> clause
;
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
);
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
));
857 void print_proof_failed()
860 log(" ______ ___ ___ _ _ _ _ \n");
861 log(" (_____ \\ / __) / __) (_) | | | |\n");
862 log(" _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |\n");
863 log(" | ____/ ___) _ \\ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|\n");
864 log(" | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ \n");
865 log(" |_| |_| \\___/ \\___/ |_| |_| \\_____|_|\\_)_____)\\____|_|\n");
872 log(" _____ _ _ _____ ____ _ _____\n");
873 log(" /__ __\\/ \\/ \\__/|/ __// _ \\/ \\ /\\/__ __\\\n");
874 log(" / \\ | || |\\/||| \\ | / \\|| | || / \\\n");
875 log(" | | | || | ||| /_ | \\_/|| \\_/| | |\n");
876 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");
895 struct SatPass
: public Pass
{
896 SatPass() : Pass("sat", "solve a SAT problem in the circuit") { }
897 void help() YS_OVERRIDE
899 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
901 log(" sat [options] [selection]\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");
907 log(" show all solutions to the problem (this can grow exponentially, use\n");
908 log(" -max <N> instead to get <N> solutions)\n");
911 log(" like -all, but limit number of solutions to <N>\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");
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");
921 log(" -set <signal> <value>\n");
922 log(" set the specified signal to the specified value.\n");
924 log(" -set-def <signal>\n");
925 log(" add a constraint that all bits of the given signal must be defined\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");
930 log(" -set-all-undef <signal>\n");
931 log(" add a constraint that all bits of the given signal are undefined\n");
933 log(" -set-def-inputs\n");
934 log(" add -set-def constraints for all module inputs\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");
940 log(" -show-inputs, -show-outputs, -show-ports\n");
941 log(" add all module (input/output) ports to the list of shown signals\n");
943 log(" -show-regs, -show-public, -show-all\n");
944 log(" show all registers, show signals with 'public' names, show all signals\n");
946 log(" -ignore_div_by_zero\n");
947 log(" ignore all solutions that involve a division by zero\n");
949 log(" -ignore_unknown_cells\n");
950 log(" ignore all cells that can not be matched to a SAT model\n");
952 log("The following options can be used to set up a sequential problem:\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");
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");
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");
966 log(" -set-assumes\n");
967 log(" set all assumptions provided via $assume cells\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");
974 log(" -set-init <signal> <value>\n");
975 log(" set the initial value for the register driving the signal to the value\n");
977 log(" -set-init-undef\n");
978 log(" set all initial states (not set using -set-init) to undef\n");
980 log(" -set-init-def\n");
981 log(" do not force a value for the initial state but do not allow undef\n");
983 log(" -set-init-zero\n");
984 log(" set all initial states (not set using -set-init) to zero\n");
986 log(" -dump_vcd <vcd-file-name>\n");
987 log(" dump SAT model (counter example in proof) to VCD file\n");
989 log(" -dump_json <json-file-name>\n");
990 log(" dump SAT model (counter example in proof) to a WaveJSON file.\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");
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");
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");
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");
1008 log(" -tempinduct-baseonly\n");
1009 log(" Run only the basecase half of temporal induction (requires -maxsteps)\n");
1011 log(" -tempinduct-inductonly\n");
1012 log(" Run only the induction half of temporal induction\n");
1014 log(" -tempinduct-skip <N>\n");
1015 log(" Skip the first <N> steps of the induction proof.\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");
1022 log(" -prove <signal> <value>\n");
1023 log(" Attempt to proof that <signal> is always <value>.\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");
1029 log(" -prove-asserts\n");
1030 log(" Prove that all asserts in the design hold.\n");
1032 log(" -prove-skip <N>\n");
1033 log(" Do not enforce the prove-condition for the first <N> time steps.\n");
1035 log(" -maxsteps <N>\n");
1036 log(" Set a maximum length for the induction.\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");
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");
1048 log(" -timeout <N>\n");
1049 log(" Maximum number of seconds a single SAT instance may take.\n");
1052 log(" Return an error and stop the synthesis script if the proof fails.\n");
1054 log(" -verify-no-timeout\n");
1055 log(" Like -verify but do not return an error for timeouts.\n");
1058 log(" Return an error and stop the synthesis script if the proof succeeds.\n");
1060 log(" -falsify-no-timeout\n");
1061 log(" Like -falsify but do not return an error for timeouts.\n");
1064 void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
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
;
1080 log_header(design
, "Executing SAT pass (solving SAT problems in the circuit).\n");
1083 for (argidx
= 1; argidx
< args
.size(); argidx
++) {
1084 if (args
[argidx
] == "-all") {
1088 if (args
[argidx
] == "-verify") {
1089 fail_on_timeout
= true;
1093 if (args
[argidx
] == "-verify-no-timeout") {
1097 if (args
[argidx
] == "-falsify") {
1098 fail_on_timeout
= true;
1102 if (args
[argidx
] == "-falsify-no-timeout") {
1106 if (args
[argidx
] == "-timeout" && argidx
+1 < args
.size()) {
1107 timeout
= atoi(args
[++argidx
].c_str());
1110 if (args
[argidx
] == "-max" && argidx
+1 < args
.size()) {
1111 loopcount
= atoi(args
[++argidx
].c_str());
1114 if (args
[argidx
] == "-maxsteps" && argidx
+1 < args
.size()) {
1115 maxsteps
= atoi(args
[++argidx
].c_str());
1118 if (args
[argidx
] == "-initsteps" && argidx
+1 < args
.size()) {
1119 initsteps
= atoi(args
[++argidx
].c_str());
1122 if (args
[argidx
] == "-stepsize" && argidx
+1 < args
.size()) {
1123 stepsize
= max(1, atoi(args
[++argidx
].c_str()));
1126 if (args
[argidx
] == "-ignore_div_by_zero") {
1127 ignore_div_by_zero
= true;
1130 if (args
[argidx
] == "-enable_undef") {
1131 enable_undef
= true;
1134 if (args
[argidx
] == "-max_undef") {
1135 enable_undef
= true;
1139 if (args
[argidx
] == "-set-def-inputs") {
1140 enable_undef
= true;
1141 set_def_inputs
= true;
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
));
1150 if (args
[argidx
] == "-set-def" && argidx
+1 < args
.size()) {
1151 sets_def
.push_back(args
[++argidx
]);
1152 enable_undef
= true;
1155 if (args
[argidx
] == "-set-any-undef" && argidx
+1 < args
.size()) {
1156 sets_any_undef
.push_back(args
[++argidx
]);
1157 enable_undef
= true;
1160 if (args
[argidx
] == "-set-all-undef" && argidx
+1 < args
.size()) {
1161 sets_all_undef
.push_back(args
[++argidx
]);
1162 enable_undef
= true;
1165 if (args
[argidx
] == "-set-assumes") {
1169 if (args
[argidx
] == "-tempinduct") {
1173 if (args
[argidx
] == "-tempinduct-def") {
1175 tempinduct_def
= true;
1176 enable_undef
= true;
1179 if (args
[argidx
] == "-tempinduct-baseonly") {
1181 tempinduct_baseonly
= true;
1184 if (args
[argidx
] == "-tempinduct-inductonly") {
1186 tempinduct_inductonly
= true;
1189 if (args
[argidx
] == "-tempinduct-skip" && argidx
+1 < args
.size()) {
1190 tempinduct_skip
= atoi(args
[++argidx
].c_str());
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
));
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;
1206 if (args
[argidx
] == "-prove-asserts") {
1207 prove_asserts
= true;
1210 if (args
[argidx
] == "-prove-skip" && argidx
+1 < args
.size()) {
1211 prove_skip
= atoi(args
[++argidx
].c_str());
1214 if (args
[argidx
] == "-seq" && argidx
+1 < args
.size()) {
1215 seq_len
= atoi(args
[++argidx
].c_str());
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
));
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
]);
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;
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;
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;
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
));
1254 if (args
[argidx
] == "-set-init-undef") {
1255 set_init_undef
= true;
1256 enable_undef
= true;
1259 if (args
[argidx
] == "-set-init-def") {
1260 set_init_def
= true;
1263 if (args
[argidx
] == "-set-init-zero") {
1264 set_init_zero
= true;
1267 if (args
[argidx
] == "-show" && argidx
+1 < args
.size()) {
1268 shows
.push_back(args
[++argidx
]);
1271 if (args
[argidx
] == "-show-inputs") {
1275 if (args
[argidx
] == "-show-outputs") {
1276 show_outputs
= true;
1279 if (args
[argidx
] == "-show-ports") {
1281 show_outputs
= true;
1284 if (args
[argidx
] == "-show-regs") {
1288 if (args
[argidx
] == "-show-public") {
1292 if (args
[argidx
] == "-show-all") {
1296 if (args
[argidx
] == "-ignore_unknown_cells") {
1297 ignore_unknown_cells
= true;
1300 if (args
[argidx
] == "-dump_vcd" && argidx
+1 < args
.size()) {
1301 vcd_file_name
= args
[++argidx
];
1304 if (args
[argidx
] == "-dump_json" && argidx
+1 < args
.size()) {
1305 json_file_name
= args
[++argidx
];
1308 if (args
[argidx
] == "-dump_cnf" && argidx
+1 < args
.size()) {
1309 cnf_file_name
= args
[++argidx
];
1314 extra_args(args
, argidx
, design
);
1316 RTLIL::Module
*module
= NULL
;
1317 for (auto mod
: design
->selected_modules()) {
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
));
1323 log_cmd_error("Can't perform SAT on an empty selection!\n");
1325 if (!prove
.size() && !prove_x
.size() && !prove_asserts
&& tempinduct
)
1326 log_cmd_error("Got -tempinduct but nothing to prove!\n");
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");
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");
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");
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());
1344 for (auto &it
: module
->wires_
)
1345 if (it
.second
->port_input
)
1346 shows
.push_back(it
.second
->name
.str());
1350 for (auto &it
: module
->wires_
)
1351 if (it
.second
->port_output
)
1352 shows
.push_back(it
.second
->name
.str());
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"))
1361 reg_wires
.insert(bit
.wire
);
1363 for (auto wire
: reg_wires
)
1364 shows
.push_back(wire
->name
.str());
1368 for (auto wire
: module
->wires())
1369 if (wire
->name
[0] == '\\')
1370 shows
.push_back(wire
->name
.str());
1374 for (auto wire
: module
->wires())
1375 shows
.push_back(wire
->name
.str());
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");
1383 SatHelper
basecase(design
, module
, enable_undef
);
1384 SatHelper
inductstep(design
, module
, enable_undef
);
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
;
1408 for (int timestep
= 1; timestep
<= seq_len
; timestep
++)
1409 if (!tempinduct_inductonly
)
1410 basecase
.setup(timestep
, timestep
== 1);
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
;
1425 if (!tempinduct_baseonly
) {
1426 inductstep
.setup(1);
1427 inductstep
.ez
->assume(inductstep
.setup_proof(1));
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
)));
1435 for (int inductlen
= 1; inductlen
<= maxsteps
|| maxsteps
== 0; inductlen
++)
1437 log("\n** Trying induction with length %d **\n", inductlen
);
1439 // phase 1: proving base case
1441 if (!tempinduct_inductonly
)
1443 basecase
.setup(seq_len
+ inductlen
, seq_len
+ inductlen
== 1);
1444 int property
= basecase
.setup_proof(seq_len
+ inductlen
);
1445 basecase
.generate_model();
1448 basecase
.force_unique_state(seq_len
+ 1, seq_len
+ inductlen
);
1450 if (tempinduct_skip
< inductlen
)
1452 log("\n[base case %d] Solving problem with %d variables and %d clauses..\n",
1453 inductlen
, basecase
.ez
->numCnfVariables(), basecase
.ez
->numCnfClauses());
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
);
1467 if (basecase
.gotTimeout
)
1470 log("Base case for induction length %d proven.\n", inductlen
);
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());
1479 basecase
.ez
->assume(property
);
1482 // phase 2: proving induction step
1484 if (!tempinduct_baseonly
)
1486 inductstep
.setup(inductlen
+ 1);
1487 int property
= inductstep
.setup_proof(inductlen
+ 1);
1488 inductstep
.generate_model();
1491 inductstep
.force_unique_state(1, inductlen
+ 1);
1493 if (inductlen
<= tempinduct_skip
|| inductlen
<= initsteps
|| inductlen
% stepsize
!= 0)
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
);
1510 if (!cnf_file_name
.empty())
1512 rewrite_filename(cnf_file_name
);
1513 FILE *f
= fopen(cnf_file_name
.c_str(), "w");
1515 log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name
.c_str(), strerror(errno
));
1517 log("Dumping CNF to file `%s'.\n", cnf_file_name
.c_str());
1518 cnf_file_name
.clear();
1520 inductstep
.ez
->printDIMACS(f
, false);
1524 log("\n[induction step %d] Solving problem with %d variables and %d clauses..\n",
1525 inductlen
, inductstep
.ez
->numCnfVariables(), inductstep
.ez
->numCnfClauses());
1528 if (!inductstep
.solve(inductstep
.ez
->NOT(property
))) {
1529 if (inductstep
.gotTimeout
)
1531 log("Induction step proven: SUCCESS!\n");
1536 log("Induction step failed. Incrementing induction length.\n");
1537 inductstep
.ez
->assume(property
);
1538 inductstep
.print_model();
1543 if (tempinduct_baseonly
) {
1544 log("\nReached maximum number of time steps -> proved base case for %d steps: SUCCESS!\n", maxsteps
);
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();
1558 log_error("Called with -verify and proof did fail!\n");
1565 log_error("Called with -falsify and proof did succeed!\n");
1571 log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
1573 SatHelper
sathelper(design
, module
, enable_undef
);
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
;
1599 if (sathelper
.prove
.size() || sathelper
.prove_x
.size() || sathelper
.prove_asserts
)
1600 sathelper
.ez
->assume(sathelper
.ez
->NOT(sathelper
.setup_proof()));
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
));
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
)));
1612 sathelper
.generate_model();
1614 if (!cnf_file_name
.empty())
1616 rewrite_filename(cnf_file_name
);
1617 FILE *f
= fopen(cnf_file_name
.c_str(), "w");
1619 log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name
.c_str(), strerror(errno
));
1621 log("Dumping CNF to file `%s'.\n", cnf_file_name
.c_str());
1622 cnf_file_name
.clear();
1624 sathelper
.ez
->printDIMACS(f
, false);
1628 int rerun_counter
= 0;
1631 log("\nSolving problem with %d variables and %d clauses..\n",
1632 sathelper
.ez
->numCnfVariables(), sathelper
.ez
->numCnfClauses());
1635 if (sathelper
.solve())
1638 log("SAT model found. maximizing number of undefs.\n");
1639 sathelper
.maximize_undefs();
1642 if (!prove
.size() && !prove_x
.size() && !prove_asserts
) {
1643 log("SAT solving finished - model found:\n");
1645 log("SAT proof finished - model found: FAIL!\n");
1646 print_proof_failed();
1649 sathelper
.print_model();
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
);
1656 if (loopcount
!= 0) {
1657 loopcount
--, rerun_counter
++;
1658 sathelper
.invalidate_model(max_undef
);
1662 if (!prove
.size() && !prove_x
.size() && !prove_asserts
) {
1665 log_error("Called with -falsify and found a model!\n");
1670 log_error("Called with -verify and proof did fail!\n");
1676 if (sathelper
.gotTimeout
)
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");
1684 log_error("Called with -verify and found no model!\n");
1687 log("SAT proof finished - no model found: SUCCESS!\n");
1691 log_error("Called with -falsify and proof did succeed!\n");
1696 if (!prove
.size() && !prove_x
.size() && !prove_asserts
) {
1697 if (falsify
&& rerun_counter
) {
1699 log_error("Called with -falsify and found a model!\n");
1702 if (verify
&& rerun_counter
) {
1704 log_error("Called with -verify and proof did fail!\n");
1711 log("Interrupted SAT solver: TIMEOUT!\n");
1713 if (fail_on_timeout
)
1714 log_error("Called with -verify and proof did time out!\n");
1719 PRIVATE_NAMESPACE_END