2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2020 Alberto Gonzalez <boqwxp@airmail.cc>
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 #include "kernel/yosys.h"
21 #include "kernel/consteval.h"
25 PRIVATE_NAMESPACE_BEGIN
27 static inline unsigned int difference(unsigned int a
, unsigned int b
) {
34 pool
<std::string
> validate_design_and_get_inputs(RTLIL::Module
*module
, bool assume_outputs
) {
35 bool found_input
= false;
36 bool found_hole
= false;
37 bool found_1bit_output
= false;
38 bool found_assert_assume
= false;
39 pool
<std::string
> input_wires
;
40 for (auto wire
: module
->wires()) {
41 if (wire
->port_input
) {
43 input_wires
.insert(wire
->name
.str());
45 if (wire
->port_output
&& wire
->width
== 1)
46 found_1bit_output
= true;
48 for (auto cell
: module
->cells()) {
49 if (cell
->type
== "$allconst")
51 if (cell
->type
== "$anyconst")
53 if (cell
->type
.in("$assert", "$assume"))
54 found_assert_assume
= true;
57 log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n");
59 log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n");
60 if (!found_1bit_output
&& !found_assert_assume
)
61 log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n");
62 if (!found_assert_assume
&& !assume_outputs
)
63 log_cmd_error("Did not find any $assert/$assume cells. Single-bit outputs were found, but `-assume-outputs` was not specified.\n");
68 void specialize_from_file(RTLIL::Module
*module
, const std::string
&file
) {
69 YS_REGEX_TYPE hole_bit_assn_regex
= YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) \\[([0-9]+)] = ([01])$");
70 YS_REGEX_TYPE hole_assn_regex
= YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) = ([01])$"); //if no index specified
71 YS_REGEX_MATCH_TYPE bit_m
, m
;
72 //(hole_loc, hole_bit, hole_name, hole_offset) -> (value, found)
73 dict
<pool
<std::string
>, RTLIL::Cell
*> anyconst_loc_to_cell
;
74 dict
<RTLIL::SigBit
, RTLIL::State
> hole_assignments
;
76 for (auto cell
: module
->cells())
77 if (cell
->type
== "$anyconst")
78 anyconst_loc_to_cell
[cell
->get_strpool_attribute(ID::src
)] = cell
;
80 std::ifstream
fin(file
.c_str());
82 log_cmd_error("could not read solution file.\n");
85 while (std::getline(fin
, buf
)) {
87 if (!YS_REGEX_NS::regex_search(buf
, bit_m
, hole_bit_assn_regex
)) {
89 if (!YS_REGEX_NS::regex_search(buf
, m
, hole_assn_regex
))
90 log_cmd_error("solution file is not formatted correctly: \"%s\"\n", buf
.c_str());
93 std::string hole_loc
= bit_assn
? bit_m
[1].str() : m
[1].str();
94 unsigned int hole_bit
= bit_assn
? atoi(bit_m
[2].str().c_str()) : atoi(m
[2].str().c_str());
95 std::string hole_name
= bit_assn
? bit_m
[3].str() : m
[3].str();
96 unsigned int hole_offset
= bit_assn
? atoi(bit_m
[4].str().c_str()) : 0;
97 RTLIL::State hole_value
= bit_assn
? (atoi(bit_m
[5].str().c_str()) == 1? RTLIL::State::S1
: RTLIL::State::S0
)
98 : (atoi(m
[4].str().c_str()) == 1? RTLIL::State::S1
: RTLIL::State::S0
);
100 //We have two options to identify holes. First, try to match wire names. If we can't find a matching wire,
101 //then try to find a cell with a matching location.
102 RTLIL::SigBit hole_sigbit
;
103 if (module
->wire(hole_name
) != nullptr) {
104 RTLIL::Wire
*hole_wire
= module
->wire(hole_name
);
105 hole_sigbit
= RTLIL::SigSpec(hole_wire
)[hole_offset
];
107 auto locs
= split_tokens(hole_loc
, "|");
108 pool
<std::string
> hole_loc_pool(locs
.begin(), locs
.end());
109 auto hole_cell_it
= anyconst_loc_to_cell
.find(hole_loc_pool
);
110 if (hole_cell_it
== anyconst_loc_to_cell
.end())
111 log_cmd_error("cannot find matching wire name or $anyconst cell location for hole spec \"%s\"\n", buf
.c_str());
113 RTLIL::Cell
*hole_cell
= hole_cell_it
->second
;
114 hole_sigbit
= hole_cell
->getPort(ID::Y
)[hole_bit
];
116 hole_assignments
[hole_sigbit
] = hole_value
;
119 for (auto &it
: anyconst_loc_to_cell
)
120 module
->remove(it
.second
);
122 for (auto &it
: hole_assignments
) {
123 RTLIL::SigSpec
lhs(it
.first
);
124 RTLIL::SigSpec
rhs(it
.second
);
125 log("Specializing %s from file with %s = %d.\n", module
->name
.c_str(), log_signal(it
.first
), it
.second
== RTLIL::State::S1
? 1 : 0);
126 module
->connect(lhs
, rhs
);
130 void specialize(RTLIL::Module
*module
, const QbfSolutionType
&sol
, bool quiet
= false) {
131 auto hole_loc_idx_to_sigbit
= sol
.get_hole_loc_idx_sigbit_map(module
);
132 pool
<RTLIL::Cell
*> anyconsts_to_remove
;
133 for (auto cell
: module
->cells())
134 if (cell
->type
== "$anyconst")
135 if (hole_loc_idx_to_sigbit
.find(std::make_pair(cell
->get_strpool_attribute(ID::src
), 0)) != hole_loc_idx_to_sigbit
.end())
136 anyconsts_to_remove
.insert(cell
);
137 for (auto cell
: anyconsts_to_remove
)
138 module
->remove(cell
);
139 for (auto &it
: sol
.hole_to_value
) {
140 pool
<std::string
> hole_loc
= it
.first
;
141 std::string hole_value
= it
.second
;
143 for (unsigned int i
= 0; i
< hole_value
.size(); ++i
) {
144 int bit_idx
= GetSize(hole_value
) - 1 - i
;
145 auto it
= hole_loc_idx_to_sigbit
.find(std::make_pair(hole_loc
, i
));
146 log_assert(it
!= hole_loc_idx_to_sigbit
.end());
148 RTLIL::SigBit hole_sigbit
= it
->second
;
149 log_assert(hole_sigbit
.wire
!= nullptr);
150 log_assert(hole_value
[bit_idx
] == '0' || hole_value
[bit_idx
] == '1');
151 RTLIL::SigSpec
lhs(hole_sigbit
.wire
, hole_sigbit
.offset
, 1);
152 RTLIL::State hole_bit_val
= hole_value
[bit_idx
] == '1'? RTLIL::State::S1
: RTLIL::State::S0
;
154 log("Specializing %s with %s = %d.\n", module
->name
.c_str(), log_signal(hole_sigbit
), hole_bit_val
== RTLIL::State::S0
? 0 : 1)
156 module
->connect(lhs
, hole_bit_val
);
161 void allconstify_inputs(RTLIL::Module
*module
, const pool
<std::string
> &input_wires
) {
162 for (auto &n
: input_wires
) {
163 RTLIL::Wire
*input
= module
->wire(n
);
165 log_assert(input
!= nullptr);
168 RTLIL::Cell
*allconst
= module
->addCell("$allconst$" + n
, "$allconst");
169 allconst
->setParam(ID(WIDTH
), input
->width
);
170 allconst
->setPort(ID::Y
, input
);
171 allconst
->set_src_attribute(input
->get_src_attribute());
172 input
->port_input
= false;
173 log("Replaced input %s with $allconst cell.\n", n
.c_str());
175 module
->fixup_ports();
178 void assume_miter_outputs(RTLIL::Module
*module
, bool assume_neg
) {
179 std::vector
<RTLIL::Wire
*> wires_to_assume
;
180 for (auto w
: module
->wires())
181 if (w
->port_output
&& w
->width
== 1)
182 wires_to_assume
.push_back(w
);
184 if (wires_to_assume
.size() == 0)
187 log("Adding $assume cell for output(s): ");
188 for (auto w
: wires_to_assume
)
189 log("\"%s\" ", w
->name
.c_str());
194 for (unsigned int i
= 0; i
< wires_to_assume
.size(); ++i
) {
195 RTLIL::SigSpec n_wire
= module
->LogicNot(wires_to_assume
[i
]->name
.str() + "__n__qbfsat", wires_to_assume
[i
], false, wires_to_assume
[i
]->get_src_attribute());
196 wires_to_assume
[i
] = n_wire
.as_wire();
200 for (auto i
= 0; wires_to_assume
.size() > 1; ++i
) {
201 std::vector
<RTLIL::Wire
*> buf
;
202 for (auto j
= 0; j
+ 1 < GetSize(wires_to_assume
); j
+= 2) {
203 std::stringstream strstr
; strstr
<< i
<< "_" << j
;
204 RTLIL::Wire
*and_wire
= module
->addWire("\\_qbfsat_and_" + strstr
.str(), 1);
205 module
->addLogicAnd("$_qbfsat_and_" + strstr
.str(), wires_to_assume
[j
], wires_to_assume
[j
+1], and_wire
, false, wires_to_assume
[j
]->get_src_attribute());
206 buf
.push_back(and_wire
);
208 if (wires_to_assume
.size() % 2 == 1)
209 buf
.push_back(wires_to_assume
[wires_to_assume
.size() - 1]);
210 wires_to_assume
.swap(buf
);
214 log_assert(wires_to_assume
.size() == 1);
216 module
->addAssume("$assume_qbfsat_miter_outputs", wires_to_assume
[0], RTLIL::S1
);
219 QbfSolutionType
call_qbf_solver(RTLIL::Module
*mod
, const QbfSolveOptions
&opt
, const std::string
&tempdir_name
, const bool quiet
= false, const int iter_num
= 0) {
220 //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]`
222 const std::string yosys_smtbmc_exe
= proc_self_dirname() + "yosys-smtbmc";
223 const std::string smt2_command
= stringf("write_smt2 -stbv -wires %s/problem%d.smt2", tempdir_name
.c_str(), iter_num
);
224 const std::string smtbmc_warning
= "z3: WARNING:";
225 const std::string smtbmc_cmd
= stringf("%s -s %s %s -t 1 -g --binary %s %s/problem%d.smt2 2>&1",
226 yosys_smtbmc_exe
.c_str(), opt
.get_solver_name().c_str(),
227 (opt
.timeout
!= 0? stringf("--timeout %d", opt
.timeout
) : "").c_str(),
228 (opt
.dump_final_smt2
? "--dump-smt2 " + opt
.dump_final_smt2_file
: "").c_str(),
229 tempdir_name
.c_str(), iter_num
);
231 Pass::call(mod
->design
, smt2_command
);
233 auto process_line
= [&ret
, &smtbmc_warning
, &opt
, &quiet
](const std::string
&line
) {
234 ret
.stdout_lines
.push_back(line
.substr(0, line
.size()-1)); //don't include trailing newline
235 auto warning_pos
= line
.find(smtbmc_warning
);
236 if (warning_pos
!= std::string::npos
)
237 log_warning("%s", line
.substr(warning_pos
+ smtbmc_warning
.size() + 1).c_str());
239 if (opt
.show_smtbmc
&& !quiet
)
240 log("smtbmc output: %s", line
.c_str());
242 log_header(mod
->design
, "Solving QBF-SAT problem.\n");
243 if (!quiet
) log("Launching \"%s\".\n", smtbmc_cmd
.c_str());
244 int64_t begin
= PerformanceTimer::query();
245 run_command(smtbmc_cmd
, process_line
);
246 int64_t end
= PerformanceTimer::query();
247 ret
.solver_time
= (end
- begin
) / 1e9f
;
248 if (!quiet
) log("Solver finished in %.3f seconds.\n", ret
.solver_time
);
250 ret
.recover_solution();
254 QbfSolutionType
qbf_solve(RTLIL::Module
*mod
, const QbfSolveOptions
&opt
) {
255 QbfSolutionType ret
, best_soln
;
256 const std::string tempdir_name
= make_temp_dir("/tmp/yosys-qbfsat-XXXXXX");
257 RTLIL::Module
*module
= mod
;
258 RTLIL::Design
*design
= module
->design
;
259 std::string module_name
= module
->name
.str();
260 RTLIL::IdString wire_to_optimize_name
= "";
261 bool maximize
= false;
262 log_assert(module
->design
!= nullptr);
264 Pass::call(design
, "design -push-copy");
266 //Replace input wires with wires assigned $allconst cells:
267 pool
<std::string
> input_wires
= validate_design_and_get_inputs(module
, opt
.assume_outputs
);
268 allconstify_inputs(module
, input_wires
);
269 if (opt
.assume_outputs
)
270 assume_miter_outputs(module
, opt
.assume_neg
);
272 //Find the wire to be optimized, if any:
273 for (auto wire
: module
->wires()) {
274 if (wire
->get_bool_attribute("\\maximize") || wire
->get_bool_attribute("\\minimize")) {
275 wire_to_optimize_name
= wire
->name
;
276 maximize
= wire
->get_bool_attribute("\\maximize");
277 if (opt
.nooptimize
) {
279 wire
->set_bool_attribute("\\maximize", false);
281 wire
->set_bool_attribute("\\minimize", false);
286 //If -O1 or -O2 was specified, use ABC to simplify the problem:
287 if (opt
.oflag
== opt
.OptimizationLevel::O1
)
288 Pass::call(module
->design
, "abc -g AND,NAND,OR,NOR,XOR,XNOR,MUX,NMUX -script +print_stats;strash;print_stats;drwsat;print_stats;fraig;print_stats;refactor,-N,10,-lz;print_stats;&get,-n;&dch,-pem;&nf;&put " + mod
->name
.str());
289 else if (opt
.oflag
== opt
.OptimizationLevel::O2
)
290 Pass::call(module
->design
, "abc -g AND,NAND,OR,NOR,XOR,XNOR,MUX,NMUX -script +print_stats;strash;print_stats;drwsat;print_stats;dch,-S,1000000,-C,100000,-p;print_stats;fraig;print_stats;refactor,-N,15,-lz;print_stats;dc2,-pbl;print_stats;drwsat;print_stats;&get,-n;&dch,-pem;&nf;&put " + mod
->name
.str());
291 if (opt
.oflag
!= opt
.OptimizationLevel::O0
) {
292 Pass::call(module
->design
, "techmap");
293 Pass::call(module
->design
, "opt");
296 if (opt
.nobisection
|| opt
.nooptimize
|| wire_to_optimize_name
== "") {
297 ret
= call_qbf_solver(module
, opt
, tempdir_name
, false, 0);
299 //Do the iterated bisection method:
300 unsigned int iter_num
= 1;
301 unsigned int success
= 0;
302 unsigned int failure
= 0;
303 unsigned int cur_thresh
= 0;
305 log_assert(wire_to_optimize_name
!= "");
306 log_assert(module
->wire(wire_to_optimize_name
) != nullptr);
307 log("%s wire \"%s\".\n", (maximize
? "Maximizing" : "Minimizing"), wire_to_optimize_name
.c_str());
309 //If maximizing, grow until we get a failure. Then bisect success and failure.
310 while (failure
== 0 || difference(success
, failure
) > 1) {
311 Pass::call(design
, "design -push-copy");
312 log_header(design
, "Preparing QBF-SAT problem.\n");
314 if (cur_thresh
!= 0) {
315 //Add thresholding logic (but not on the initial run when we don't have a sense of where to start):
316 RTLIL::SigSpec comparator
= maximize
? module
->Ge(NEW_ID
, module
->wire(wire_to_optimize_name
), RTLIL::Const(cur_thresh
), false)
317 : module
->Le(NEW_ID
, module
->wire(wire_to_optimize_name
), RTLIL::Const(cur_thresh
), false);
319 module
->addAssume(wire_to_optimize_name
.str() + "__threshold", comparator
, RTLIL::Const(1, 1));
320 log("Trying to solve with %s %s %d.\n", wire_to_optimize_name
.c_str(), (maximize
? ">=" : "<="), cur_thresh
);
323 ret
= call_qbf_solver(module
, opt
, tempdir_name
, false, iter_num
);
324 Pass::call(design
, "design -pop");
325 module
= design
->module(module_name
);
327 if (!ret
.unknown
&& ret
.sat
) {
328 Pass::call(design
, "design -push-copy");
329 specialize(module
, ret
, true);
331 RTLIL::SigSpec wire
, value
, undef
;
332 RTLIL::SigSpec::parse_sel(wire
, design
, module
, wire_to_optimize_name
.str());
334 ConstEval
ce(module
);
336 if (!ce
.eval(value
, undef
))
337 log_cmd_error("Failed to evaluate signal %s: Missing value for %s.\n", log_signal(wire
), log_signal(undef
));
338 log_assert(value
.is_fully_const());
339 success
= value
.as_const().as_int();
341 log("Problem is satisfiable with %s = %d.\n", wire_to_optimize_name
.c_str(), success
);
342 Pass::call(design
, "design -pop");
343 module
= design
->module(module_name
);
345 //sometimes this happens if we get an 'unknown' or timeout
346 if (!maximize
&& success
< failure
)
348 else if (maximize
&& failure
!= 0 && success
> failure
)
352 //Treat 'unknown' as UNSAT
353 failure
= cur_thresh
;
355 log("Problem is NOT satisfiable.\n");
359 log("Problem is NOT satisfiable with %s %s %d.\n", wire_to_optimize_name
.c_str(), (maximize
? ">=" : "<="), failure
);
363 if (maximize
&& failure
== 0 && success
== 0)
365 else if (maximize
&& failure
== 0)
366 cur_thresh
= 2 * success
; //growth
367 else //if (!maximize || failure != 0)
368 cur_thresh
= (success
+ failure
) / 2; //bisection
370 if (success
!= 0 || failure
!= 0) {
371 log("Wire %s is %s at %d.\n", wire_to_optimize_name
.c_str(), (maximize
? "maximized" : "minimized"), success
);
377 remove_directory(tempdir_name
);
379 Pass::call(design
, "design -pop");
384 QbfSolveOptions
parse_args(const std::vector
<std::string
> &args
) {
386 for (opt
.argidx
= 1; opt
.argidx
< args
.size(); opt
.argidx
++) {
387 if (args
[opt
.argidx
] == "-nocleanup") {
388 opt
.nocleanup
= true;
391 else if (args
[opt
.argidx
] == "-specialize") {
392 opt
.specialize
= true;
395 else if (args
[opt
.argidx
] == "-assume-outputs") {
396 opt
.assume_outputs
= true;
399 else if (args
[opt
.argidx
] == "-assume-negative-polarity") {
400 opt
.assume_neg
= true;
403 else if (args
[opt
.argidx
] == "-nooptimize") {
404 opt
.nooptimize
= true;
407 else if (args
[opt
.argidx
] == "-nobisection") {
408 opt
.nobisection
= true;
411 else if (args
[opt
.argidx
] == "-solver") {
412 if (args
.size() <= opt
.argidx
+ 1)
413 log_cmd_error("solver not specified.\n");
415 if (args
[opt
.argidx
+1] == "z3")
416 opt
.solver
= opt
.Solver::Z3
;
417 else if (args
[opt
.argidx
+1] == "yices")
418 opt
.solver
= opt
.Solver::Yices
;
419 else if (args
[opt
.argidx
+1] == "cvc4")
420 opt
.solver
= opt
.Solver::CVC4
;
422 log_cmd_error("Unknown solver \"%s\".\n", args
[opt
.argidx
+1].c_str());
427 else if (args
[opt
.argidx
] == "-timeout") {
428 if (args
.size() <= opt
.argidx
+ 1)
429 log_cmd_error("timeout not specified.\n");
431 int timeout
= atoi(args
[opt
.argidx
+1].c_str());
433 opt
.timeout
= timeout
;
435 log_cmd_error("timeout must be greater than 0.\n");
440 else if (args
[opt
.argidx
].substr(0, 2) == "-O" && args
[opt
.argidx
].size() == 3) {
441 switch (args
[opt
.argidx
][2]) {
443 opt
.oflag
= opt
.OptimizationLevel::O0
;
446 opt
.oflag
= opt
.OptimizationLevel::O1
;
449 opt
.oflag
= opt
.OptimizationLevel::O2
;
452 log_cmd_error("unknown argument %s\n", args
[opt
.argidx
].c_str());
456 else if (args
[opt
.argidx
] == "-sat") {
460 else if (args
[opt
.argidx
] == "-unsat") {
464 else if (args
[opt
.argidx
] == "-show-smtbmc") {
465 opt
.show_smtbmc
= true;
468 else if (args
[opt
.argidx
] == "-dump-final-smt2") {
469 opt
.dump_final_smt2
= true;
470 if (args
.size() <= opt
.argidx
+ 1)
471 log_cmd_error("smt2 file not specified.\n");
473 opt
.dump_final_smt2_file
= args
[++opt
.argidx
];
476 else if (args
[opt
.argidx
] == "-specialize-from-file") {
477 opt
.specialize_from_file
= true;
478 if (args
.size() <= opt
.argidx
+ 1)
479 log_cmd_error("solution file not specified.\n");
481 opt
.specialize_soln_file
= args
[++opt
.argidx
];
484 else if (args
[opt
.argidx
] == "-write-solution") {
485 opt
.write_solution
= true;
486 if (args
.size() <= opt
.argidx
+ 1)
487 log_cmd_error("solution file not specified.\n");
489 opt
.write_soln_soln_file
= args
[++opt
.argidx
];
498 struct QbfSatPass
: public Pass
{
499 QbfSatPass() : Pass("qbfsat", "solve a 2QBF-SAT problem in the circuit") { }
502 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
504 log(" qbfsat [options] [selection]\n");
506 log("This command solves an \"exists-forall\" 2QBF-SAT problem defined over the currently\n");
507 log("selected module. Existentially-quantified variables are declared by assigning a wire\n");
508 log("\"$anyconst\". Universally-quantified variables may be explicitly declared by assigning\n");
509 log("a wire \"$allconst\", but module inputs will be treated as universally-quantified\n");
510 log("variables by default.\n");
512 log(" -nocleanup\n");
513 log(" Do not delete temporary files and directories. Useful for debugging.\n");
515 log(" -dump-final-smt2 <file>\n");
516 log(" Pass the --dump-smt2 option to yosys-smtbmc.\n");
518 log(" -assume-outputs\n");
519 log(" Add an \"$assume\" cell for the conjunction of all one-bit module output wires.\n");
521 log(" -assume-negative-polarity\n");
522 log(" When adding $assume cells for one-bit module output wires, assume they are\n");
523 log(" negative polarity signals and should always be low, for example like the\n");
524 log(" miters created with the `miter` command.\n");
526 log(" -nooptimize\n");
527 log(" Ignore \"\\minimize\" and \"\\maximize\" attributes, do not emit \"(maximize)\" or\n");
528 log(" \"(minimize)\" in the SMT-LIBv2, and generally make no attempt to optimize anything.\n");
530 log(" -nobisection\n");
531 log(" If a wire is marked with the \"\\minimize\" or \"\\maximize\" attribute, do not\n");
532 log(" attempt to optimize that value with the default iterated solving and threshold\n");
533 log(" bisection approach. Instead, have yosys-smtbmc emit a \"(minimize)\" or \"(maximize)\"\n");
534 log(" command in the SMT-LIBv2 output and hope that the solver supports optimizing\n");
535 log(" quantified bitvector problems.\n");
537 log(" -solver <solver>\n");
538 log(" Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n");
539 log(" (default: yices)\n");
541 log(" -timeout <value>\n");
542 log(" Set the per-iteration timeout in seconds.\n");
543 log(" (default: no timeout)\n");
545 log(" -O0, -O1, -O2\n");
546 log(" Control the use of ABC to simplify the QBF-SAT problem before solving.\n");
549 log(" Generate an error if the solver does not return \"sat\".\n");
552 log(" Generate an error if the solver does not return \"unsat\".\n");
554 log(" -show-smtbmc\n");
555 log(" Print the output from yosys-smtbmc.\n");
557 log(" -specialize\n");
558 log(" If the problem is satisfiable, replace each \"$anyconst\" cell with its\n");
559 log(" corresponding constant value from the model produced by the solver.\n");
561 log(" -specialize-from-file <solution file>\n");
562 log(" Do not run the solver, but instead only attempt to replace each \"$anyconst\"\n");
563 log(" cell in the current module with a constant value provided by the specified file.\n");
565 log(" -write-solution <solution file>\n");
566 log(" If the problem is satisfiable, write the corresponding constant value for each\n");
567 log(" \"$anyconst\" cell from the model produced by the solver to the specified file.");
572 void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
) override
574 log_header(design
, "Executing QBFSAT pass (solving QBF-SAT problems in the circuit).\n");
575 QbfSolveOptions opt
= parse_args(args
);
576 extra_args(args
, opt
.argidx
, design
);
578 RTLIL::Module
*module
= nullptr;
579 for (auto mod
: design
->selected_modules()) {
581 log_cmd_error("Only one module must be selected for the QBF-SAT pass! (selected: %s and %s)\n", log_id(module
), log_id(mod
));
584 if (module
== nullptr)
585 log_cmd_error("Can't perform QBF-SAT on an empty selection!\n");
588 if (!opt
.specialize_from_file
) {
589 //Save the design to restore after modiyfing the current module.
590 std::string module_name
= module
->name
.str();
592 QbfSolutionType ret
= qbf_solve(module
, opt
);
593 module
= design
->module(module_name
);
595 if (opt
.sat
|| opt
.unsat
)
596 log_cmd_error("expected problem to be %s\n", opt
.sat
? "SAT" : "UNSAT");
600 if (opt
.write_solution
) {
601 ret
.write_solution(module
, opt
.write_soln_soln_file
);
603 if (opt
.specialize
) {
604 specialize(module
, ret
);
606 ret
.dump_model(module
);
609 log_cmd_error("expected problem to be UNSAT\n");
612 print_proof_failed();
614 log_cmd_error("expected problem to be SAT\n");
617 specialize_from_file(module
, opt
.specialize_soln_file
);
622 PRIVATE_NAMESPACE_END