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/celltypes.h"
22 #include "kernel/consteval.h"
23 #include "kernel/log.h"
24 #include "kernel/rtlil.h"
25 #include "kernel/register.h"
30 # define WIFEXITED(x) 1
31 # define WIFSIGNALED(x) 0
32 # define WIFSTOPPED(x) 0
33 # define WEXITSTATUS(x) ((x) & 0xff)
34 # define WTERMSIG(x) SIGTERM
36 # include <sys/wait.h>
40 PRIVATE_NAMESPACE_BEGIN
42 struct QbfSolutionType
{
43 std::vector
<std::string
> stdout_lines
;
44 dict
<std::string
, std::string
> hole_to_value
;
46 bool unknown
; //true if neither 'sat' nor 'unsat'
48 QbfSolutionType() : sat(false), unknown(true) {}
51 struct QbfSolveOptions
{
52 bool specialize
, specialize_from_file
, write_solution
, nocleanup
, dump_final_smt2
, assume_outputs
, assume_neg
;
53 bool nooptimize
, nobisection
;
54 bool sat
, unsat
, show_smtbmc
;
55 std::string specialize_soln_file
;
56 std::string write_soln_soln_file
;
57 std::string dump_final_smt2_file
;
59 QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false),
60 nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false),
61 nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false),
65 void recover_solution(QbfSolutionType
&sol
) {
66 YS_REGEX_TYPE sat_regex
= YS_REGEX_COMPILE("Status: PASSED");
67 YS_REGEX_TYPE unsat_regex
= YS_REGEX_COMPILE("Solver Error.*model is not available");
68 YS_REGEX_TYPE memout_regex
= YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\"");
69 YS_REGEX_TYPE hole_value_regex
= YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
71 YS_REGEX_TYPE hole_loc_regex
= YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+");
72 YS_REGEX_TYPE hole_val_regex
= YS_REGEX_COMPILE("[0-9]+");
74 YS_REGEX_MATCH_TYPE m
;
75 bool sat_regex_found
= false;
76 bool unsat_regex_found
= false;
77 dict
<std::string
, bool> hole_value_recovered
;
78 for (const std::string
&x
: sol
.stdout_lines
) {
79 if(YS_REGEX_NS::regex_search(x
, m
, hole_value_regex
)) {
80 std::string loc
= m
[1].str();
81 std::string val
= m
[2].str();
83 log_assert(YS_REGEX_NS::regex_search(loc
, hole_loc_regex
));
84 log_assert(YS_REGEX_NS::regex_search(val
, hole_val_regex
));
86 sol
.hole_to_value
[loc
] = val
;
88 else if (YS_REGEX_NS::regex_search(x
, sat_regex
))
89 sat_regex_found
= true;
90 else if (YS_REGEX_NS::regex_search(x
, unsat_regex
))
91 unsat_regex_found
= true;
92 else if (YS_REGEX_NS::regex_search(x
, memout_regex
)) {
94 log_warning("solver ran out of memory\n");
98 log_assert(!sol
.unknown
&& sol
.sat
? sat_regex_found
: true);
99 log_assert(!sol
.unknown
&& !sol
.sat
? unsat_regex_found
: true);
103 dict
<std::string
, std::string
> get_hole_loc_name_map(RTLIL::Module
*module
, const QbfSolutionType
&sol
) {
104 dict
<std::string
, std::string
> hole_loc_to_name
;
105 for (auto cell
: module
->cells()) {
106 std::string cell_src
= cell
->get_src_attribute();
107 auto pos
= sol
.hole_to_value
.find(cell_src
);
108 if (pos
!= sol
.hole_to_value
.end() && cell
->type
.in("$anyconst", "$anyseq")) {
109 log_assert(hole_loc_to_name
.find(pos
->first
) == hole_loc_to_name
.end());
110 hole_loc_to_name
[pos
->first
] = cell
->getPort(ID::Y
).as_wire()->name
.str();
114 return hole_loc_to_name
;
117 pool
<std::string
> validate_design_and_get_inputs(RTLIL::Module
*module
, const QbfSolveOptions
&opt
) {
118 bool found_input
= false;
119 bool found_hole
= false;
120 bool found_1bit_output
= false;
121 bool found_assert_assume
= false;
122 pool
<std::string
> input_wires
;
123 for (auto wire
: module
->wires()) {
124 if (wire
->port_input
) {
126 input_wires
.insert(wire
->name
.str());
128 if (wire
->port_output
&& wire
->width
== 1)
129 found_1bit_output
= true;
131 for (auto cell
: module
->cells()) {
132 if (cell
->type
== "$allconst")
134 if (cell
->type
== "$anyconst")
136 if (cell
->type
.in("$assert", "$assume"))
137 found_assert_assume
= true;
140 log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n");
142 log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n");
143 if (!found_1bit_output
&& !found_assert_assume
)
144 log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n");
145 if (!found_assert_assume
&& !opt
.assume_outputs
)
146 log_cmd_error("Did not find any $assert/$assume cells. Single-bit outputs were found, but `-assume-outputs` was not specified.\n");
151 void write_solution(RTLIL::Module
*module
, const QbfSolutionType
&sol
, const std::string
&file
) {
152 std::ofstream
fout(file
.c_str());
154 log_cmd_error("could not open solution file for writing.\n");
156 dict
<std::string
, std::string
> hole_loc_to_name
= get_hole_loc_name_map(module
, sol
);
157 for(auto &x
: sol
.hole_to_value
)
158 fout
<< hole_loc_to_name
[x
.first
] << "=" << x
.second
<< std::endl
;
161 void specialize_from_file(RTLIL::Module
*module
, const std::string
&file
) {
162 YS_REGEX_TYPE hole_assn_regex
= YS_REGEX_COMPILE_WITH_SUBS("^(.*)=([01]+)$");
163 YS_REGEX_MATCH_TYPE m
;
164 pool
<RTLIL::Cell
*> anyconsts_to_remove
;
165 dict
<std::string
, std::string
> hole_name_to_value
;
166 std::ifstream
fin(file
.c_str());
168 log_cmd_error("could not read solution file.\n");
171 while (std::getline(fin
, buf
)) {
172 log_assert(YS_REGEX_NS::regex_search(buf
, m
, hole_assn_regex
));
173 std::string hole_name
= m
[1].str();
174 std::string hole_value
= m
[2].str();
175 hole_name_to_value
[hole_name
] = hole_value
;
178 for (auto cell
: module
->cells())
179 if (cell
->type
== "$anyconst") {
180 auto anyconst_port_y
= cell
->getPort(ID::Y
).as_wire();
181 if (anyconst_port_y
== nullptr)
183 if (hole_name_to_value
.find(anyconst_port_y
->name
.str()) != hole_name_to_value
.end())
184 anyconsts_to_remove
.insert(cell
);
186 for (auto cell
: anyconsts_to_remove
)
187 module
->remove(cell
);
189 for (auto &it
: hole_name_to_value
) {
190 std::string hole_name
= it
.first
;
191 std::string hole_value
= it
.second
;
192 RTLIL::Wire
*wire
= module
->wire(hole_name
);
194 log_assert(wire
!= nullptr);
195 log_assert(wire
->width
> 0 && GetSize(hole_value
) == wire
->width
);
198 log("Specializing %s from file with %s = %d'b%s.\n", module
->name
.c_str(), hole_name
.c_str(), wire
->width
, hole_value
.c_str());
199 std::vector
<RTLIL::SigBit
> value_bv
;
200 value_bv
.reserve(wire
->width
);
201 for (char c
: hole_value
)
202 value_bv
.emplace_back(c
== '1'? RTLIL::S1
: RTLIL::S0
);
203 std::reverse(value_bv
.begin(), value_bv
.end());
204 module
->connect(wire
, value_bv
);
208 void specialize(RTLIL::Module
*module
, const QbfSolutionType
&sol
, bool quiet
= false) {
209 dict
<std::string
, std::string
> hole_loc_to_name
= get_hole_loc_name_map(module
, sol
);
210 pool
<RTLIL::Cell
*> anyconsts_to_remove
;
211 for (auto cell
: module
->cells())
212 if (cell
->type
== "$anyconst")
213 if (hole_loc_to_name
.find(cell
->get_src_attribute()) != hole_loc_to_name
.end())
214 anyconsts_to_remove
.insert(cell
);
215 for (auto cell
: anyconsts_to_remove
)
216 module
->remove(cell
);
217 for (auto &it
: sol
.hole_to_value
) {
218 std::string hole_loc
= it
.first
;
219 std::string hole_value
= it
.second
;
222 auto pos
= hole_loc_to_name
.find(hole_loc
);
223 log_assert(pos
!= hole_loc_to_name
.end());
226 std::string hole_name
= hole_loc_to_name
[hole_loc
];
227 RTLIL::Wire
*wire
= module
->wire(hole_name
);
229 log_assert(wire
!= nullptr);
230 log_assert(wire
->width
> 0 && GetSize(hole_value
) == wire
->width
);
234 log("Specializing %s with %s = %d'b%s.\n", module
->name
.c_str(), hole_name
.c_str(), wire
->width
, hole_value
.c_str());
235 std::vector
<RTLIL::SigBit
> value_bv
;
236 value_bv
.reserve(wire
->width
);
237 for (char c
: hole_value
)
238 value_bv
.emplace_back(c
== '1'? RTLIL::S1
: RTLIL::S0
);
239 std::reverse(value_bv
.begin(), value_bv
.end());
240 module
->connect(wire
, value_bv
);
244 void dump_model(RTLIL::Module
*module
, const QbfSolutionType
&sol
) {
245 log("Satisfiable model:\n");
246 dict
<std::string
, std::string
> hole_loc_to_name
= get_hole_loc_name_map(module
, sol
);
247 for (auto &it
: sol
.hole_to_value
) {
248 std::string hole_loc
= it
.first
;
249 std::string hole_value
= it
.second
;
252 auto pos
= hole_loc_to_name
.find(hole_loc
);
253 log_assert(pos
!= hole_loc_to_name
.end());
256 std::string hole_name
= hole_loc_to_name
[hole_loc
];
257 log("\t%s = %lu'b%s\n", hole_name
.c_str(), hole_value
.size(), hole_value
.c_str());
258 std::vector
<RTLIL::SigBit
> value_bv
;
259 value_bv
.reserve(hole_value
.size());
260 for (char c
: hole_value
)
261 value_bv
.emplace_back(c
== '1'? RTLIL::S1
: RTLIL::S0
);
262 std::reverse(value_bv
.begin(), value_bv
.end());
266 void allconstify_inputs(RTLIL::Module
*module
, const pool
<std::string
> &input_wires
) {
267 for (auto &n
: input_wires
) {
268 RTLIL::Wire
*input
= module
->wire(n
);
270 log_assert(input
!= nullptr);
273 RTLIL::Cell
*allconst
= module
->addCell("$allconst$" + n
, "$allconst");
274 allconst
->setParam(ID(WIDTH
), input
->width
);
275 allconst
->setPort(ID::Y
, input
);
276 allconst
->set_src_attribute(input
->get_src_attribute());
277 input
->port_input
= false;
278 log("Replaced input %s with $allconst cell.\n", n
.c_str());
280 module
->fixup_ports();
283 void assume_miter_outputs(RTLIL::Module
*module
, const QbfSolveOptions
&opt
) {
284 std::vector
<RTLIL::Wire
*> wires_to_assume
;
285 for (auto w
: module
->wires())
286 if (w
->port_output
&& w
->width
== 1)
287 wires_to_assume
.push_back(w
);
289 if (wires_to_assume
.size() == 0)
292 log("Adding $assume cell for output(s): ");
293 for (auto w
: wires_to_assume
)
294 log("\"%s\" ", w
->name
.c_str());
298 if (opt
.assume_neg
) {
299 for (unsigned int i
= 0; i
< wires_to_assume
.size(); ++i
) {
300 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());
301 wires_to_assume
[i
] = n_wire
.as_wire();
305 for (auto i
= 0; wires_to_assume
.size() > 1; ++i
) {
306 std::vector
<RTLIL::Wire
*> buf
;
307 for (auto j
= 0; j
+ 1 < GetSize(wires_to_assume
); j
+= 2) {
308 std::stringstream strstr
; strstr
<< i
<< "_" << j
;
309 RTLIL::Wire
*and_wire
= module
->addWire("\\_qbfsat_and_" + strstr
.str(), 1);
310 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());
311 buf
.push_back(and_wire
);
313 if (wires_to_assume
.size() % 2 == 1)
314 buf
.push_back(wires_to_assume
[wires_to_assume
.size() - 1]);
315 wires_to_assume
.swap(buf
);
319 log_assert(wires_to_assume
.size() == 1);
321 module
->addAssume("$assume_qbfsat_miter_outputs", wires_to_assume
[0], RTLIL::S1
);
324 QbfSolutionType
call_qbf_solver(RTLIL::Module
*mod
, const QbfSolveOptions
&opt
, const std::string
&tempdir_name
, const bool quiet
= false, const int iter_num
= 0) {
325 //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]`
327 const std::string yosys_smtbmc_exe
= proc_self_dirname() + "yosys-smtbmc";
328 const std::string smt2_command
= "write_smt2 -stbv -wires " + tempdir_name
+ "/problem" + (iter_num
!= 0? stringf("%d", iter_num
) : "") + ".smt2";
329 const std::string smtbmc_cmd
= yosys_smtbmc_exe
+ " -s z3 -t 1 -g --binary " + (opt
.dump_final_smt2
? "--dump-smt2 " + opt
.dump_final_smt2_file
+ " " : "") + tempdir_name
+ "/problem" + (iter_num
!= 0? stringf("%d", iter_num
) : "") + ".smt2 2>&1";
330 const std::string smtbmc_warning
= "z3: WARNING:";
331 const bool show_smtbmc
= opt
.show_smtbmc
;
333 Pass::call(mod
->design
, smt2_command
);
335 auto process_line
= [&ret
, &smtbmc_warning
, &show_smtbmc
, &quiet
](const std::string
&line
) {
336 ret
.stdout_lines
.push_back(line
.substr(0, line
.size()-1)); //don't include trailing newline
337 auto warning_pos
= line
.find(smtbmc_warning
);
338 if (warning_pos
!= std::string::npos
)
339 log_warning("%s", line
.substr(warning_pos
+ smtbmc_warning
.size() + 1).c_str());
341 if (show_smtbmc
&& !quiet
)
342 log("smtbmc output: %s", line
.c_str());
344 log_header(mod
->design
, "Solving QBF-SAT problem.\n");
345 if (!quiet
) log("Launching \"%s\".\n", smtbmc_cmd
.c_str());
346 int retval
= run_command(smtbmc_cmd
, process_line
);
350 } else if (retval
== 1) {
355 recover_solution(ret
);
359 QbfSolutionType
qbf_solve(RTLIL::Module
*mod
, const QbfSolveOptions
&opt
) {
360 QbfSolutionType ret
, best_soln
;
361 const std::string tempdir_name
= make_temp_dir("/tmp/yosys-z3-XXXXXX");
362 RTLIL::Module
*module
= mod
;
363 RTLIL::Design
*design
= module
->design
;
364 std::string module_name
= module
->name
.str();
365 RTLIL::Wire
*wire_to_optimize
= nullptr;
366 RTLIL::IdString wire_to_optimize_name
;
367 bool maximize
= false;
368 log_assert(module
->design
!= nullptr);
370 Pass::call(design
, "design -push-copy");
372 //Replace input wires with wires assigned $allconst cells:
373 pool
<std::string
> input_wires
= validate_design_and_get_inputs(module
, opt
);
374 allconstify_inputs(module
, input_wires
);
375 if (opt
.assume_outputs
)
376 assume_miter_outputs(module
, opt
);
378 //Find the wire to be optimized, if any:
379 for (auto wire
: module
->wires())
380 if (wire
->get_bool_attribute("\\maximize") || wire
->get_bool_attribute("\\minimize"))
381 wire_to_optimize
= wire
;
382 if (wire_to_optimize
!= nullptr) {
383 wire_to_optimize_name
= wire_to_optimize
->name
;
384 maximize
= wire_to_optimize
->get_bool_attribute("\\maximize");
387 if (opt
.nobisection
|| opt
.nooptimize
) {
388 if (wire_to_optimize
!= nullptr && opt
.nooptimize
) {
389 wire_to_optimize
->set_bool_attribute("\\maximize", false);
390 wire_to_optimize
->set_bool_attribute("\\minimize", false);
392 ret
= call_qbf_solver(module
, opt
, tempdir_name
, false, 0);
394 //Do the iterated bisection method:
395 unsigned int iter_num
= 1;
396 unsigned int success
= 0;
397 unsigned int failure
= 0;
398 unsigned int cur_thresh
= 0;
400 log_assert(wire_to_optimize
!= nullptr);
401 log("%s wire \"%s\".\n", (maximize
? "Maximizing" : "Minimizing"), log_signal(wire_to_optimize
));
403 //If maximizing, grow until we get a failure. Then bisect success and failure.
404 while (failure
== 0 || success
- failure
> 1) {
405 Pass::call(design
, "design -push-copy");
406 log_header(design
, "Preparing QBF-SAT problem.\n");
408 if (cur_thresh
!= 0) {
409 //Add thresholding logic (but not on the initial run when we don't have a sense of where to start):
410 RTLIL::SigSpec comparator
= maximize
? module
->Ge(NEW_ID
, module
->wire(wire_to_optimize_name
), RTLIL::Const(cur_thresh
), false)
411 : module
->Le(NEW_ID
, module
->wire(wire_to_optimize_name
), RTLIL::Const(cur_thresh
), false);
413 module
->addAssume(wire_to_optimize_name
.str() + "__threshold", comparator
, RTLIL::Const(1, 1));
414 log("Trying to solve with %s %s %d.\n", wire_to_optimize_name
.c_str(), (maximize
? ">=" : "<="), cur_thresh
);
417 ret
= call_qbf_solver(module
, opt
, tempdir_name
, false, iter_num
);
418 Pass::call(design
, "design -pop");
419 module
= design
->module(module_name
);
421 if (!ret
.unknown
&& ret
.sat
) {
422 Pass::call(design
, "design -push-copy");
423 specialize(module
, ret
, true);
425 RTLIL::SigSpec wire
, value
, undef
;
426 RTLIL::SigSpec::parse_sel(wire
, design
, module
, wire_to_optimize_name
.str());
428 ConstEval
ce(module
);
430 if (!ce
.eval(value
, undef
))
431 log_cmd_error("Failed to evaluate signal %s: Missing value for %s.\n", log_signal(wire
), log_signal(undef
));
432 log_assert(value
.is_fully_const());
433 success
= value
.as_const().as_int();
435 log("Problem is satisfiable with %s = %d.\n", wire_to_optimize_name
.c_str(), success
);
436 Pass::call(design
, "design -pop");
437 module
= design
->module(module_name
);
439 //sometimes this happens if we get an 'unknown' or timeout
440 if (!maximize
&& success
< failure
)
442 else if (maximize
&& success
> failure
)
445 //Treat 'unknown' as UNSAT
446 failure
= cur_thresh
;
448 log("Problem is NOT satisfiable.\n");
452 log("Problem is NOT satisfiable with %s %s %d.\n", wire_to_optimize_name
.c_str(), (maximize
? ">=" : "<="), failure
);
456 cur_thresh
= (maximize
&& failure
== 0)? 2 * success
//growth
457 : (success
+ failure
) / 2; //bisection
459 if (success
!= 0 || failure
!= 0) {
460 log("Wire %s is %s at %d.\n", wire_to_optimize_name
.c_str(), (maximize
? "maximized" : "minimized"), success
);
466 remove_directory(tempdir_name
);
468 Pass::call(design
, "design -pop");
473 QbfSolveOptions
parse_args(const std::vector
<std::string
> &args
) {
475 for (opt
.argidx
= 1; opt
.argidx
< args
.size(); opt
.argidx
++) {
476 if (args
[opt
.argidx
] == "-nocleanup") {
477 opt
.nocleanup
= true;
480 else if (args
[opt
.argidx
] == "-specialize") {
481 opt
.specialize
= true;
484 else if (args
[opt
.argidx
] == "-assume-outputs") {
485 opt
.assume_outputs
= true;
488 else if (args
[opt
.argidx
] == "-assume-negative-polarity") {
489 opt
.assume_neg
= true;
492 else if (args
[opt
.argidx
] == "-nooptimize") {
493 opt
.nooptimize
= true;
496 else if (args
[opt
.argidx
] == "-nobisection") {
497 opt
.nobisection
= true;
500 else if (args
[opt
.argidx
] == "-sat") {
504 else if (args
[opt
.argidx
] == "-unsat") {
508 else if (args
[opt
.argidx
] == "-show-smtbmc") {
509 opt
.show_smtbmc
= true;
512 else if (args
[opt
.argidx
] == "-dump-final-smt2") {
513 opt
.dump_final_smt2
= true;
514 if (args
.size() <= opt
.argidx
+ 1)
515 log_cmd_error("smt2 file not specified.\n");
517 opt
.dump_final_smt2_file
= args
[++opt
.argidx
];
520 else if (args
[opt
.argidx
] == "-specialize-from-file") {
521 opt
.specialize_from_file
= true;
522 if (args
.size() <= opt
.argidx
+ 1)
523 log_cmd_error("solution file not specified.\n");
525 opt
.specialize_soln_file
= args
[++opt
.argidx
];
528 else if (args
[opt
.argidx
] == "-write-solution") {
529 opt
.write_solution
= true;
530 if (args
.size() <= opt
.argidx
+ 1)
531 log_cmd_error("solution file not specified.\n");
533 opt
.write_soln_soln_file
= args
[++opt
.argidx
];
542 void print_proof_failed()
545 log(" ______ ___ ___ _ _ _ _ \n");
546 log(" (_____ \\ / __) / __) (_) | | | |\n");
547 log(" _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |\n");
548 log(" | ____/ ___) _ \\ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|\n");
549 log(" | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ \n");
550 log(" |_| |_| \\___/ \\___/ |_| |_| \\_____|_|\\_)_____)\\____|_|\n");
557 log(" /$$$$$$ /$$$$$$$$ /$$$$$$$ \n");
558 log(" /$$__ $$ | $$_____/ | $$__ $$ \n");
559 log(" | $$ \\ $$ | $$ | $$ \\ $$ \n");
560 log(" | $$ | $$ | $$$$$ | $$ | $$ \n");
561 log(" | $$ | $$ | $$__/ | $$ | $$ \n");
562 log(" | $$/$$ $$ | $$ | $$ | $$ \n");
563 log(" | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
564 log(" \\____ $$$|__/|________/|__/|_______/|__/\n");
569 struct QbfSatPass
: public Pass
{
570 QbfSatPass() : Pass("qbfsat", "solve a 2QBF-SAT problem in the circuit") { }
571 void help() YS_OVERRIDE
573 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
575 log(" qbfsat [options] [selection]\n");
577 log("This command solves a 2QBF-SAT problem defined over the currently selected module.\n");
578 log("Existentially-quantified variables are declared by assigning a wire \"$anyconst\".\n");
579 log("Universally-quantified variables may be explicitly declared by assigning a wire\n");
580 log("\"$allconst\", but module inputs will be treated as universally-quantified variables\n");
581 log("by default.\n");
583 log(" -nocleanup\n");
584 log(" Do not delete temporary files and directories. Useful for\n");
585 log(" debugging.\n");
587 log(" -dump-final-smt2 <file>\n");
588 log(" Pass the --dump-smt2 option to yosys-smtbmc.\n");
590 log(" -assume-outputs\n");
591 log(" Add an $assume cell for the conjunction of all one-bit module output wires.\n");
593 log(" -assume-negative-polarity\n");
594 log(" When adding $assume cells for one-bit module output wires, assume they are\n");
595 log(" negative polarity signals and should always be low, for example like the\n");
596 log(" miters created with the `miter` command.\n");
598 log(" -nooptimize\n");
599 log(" Ignore \"\\minimize\" and \"\\maximize\" attributes, do not emit \"(maximize)\" or\n");
600 log(" \"(minimize)\" in the SMTLIBv2, and generally make no attempt to optimize anything.\n");
602 log(" -nobisection\n");
603 log(" If a wire is marked with the \"\\minimize\" or \"\\maximize\" attribute, do not\n");
604 log(" attempt to optimize that value with the default iterated solving and threshold\n");
605 log(" bisection approach. Instead, have yosys-smtbmc emit a \"(minimize)\" or \"(maximize)\"\n");
606 log(" command in the SMTLIBv2 output and hope that the solver supports optimizing\n");
607 log(" quantified bitvector problems.\n");
610 log(" Generate an error if the solver does not return \"sat\".\n");
613 log(" Generate an error if the solver does not return \"unsat\".\n");
615 log(" -show-smtbmc\n");
616 log(" Print the output from yosys-smtbmc.\n");
618 log(" -specialize\n");
619 log(" Replace all \"$anyconst\" cells with constant values determined by the solver.\n");
621 log(" -specialize-from-file <solution file>\n");
622 log(" Do not run the solver, but instead only attempt to replace all \"$anyconst\"\n");
623 log(" cells in the current module with values provided by the specified file.\n");
625 log(" -write-solution <solution file>\n");
626 log(" Write the assignments discovered by the solver for all \"$anyconst\" cells\n");
627 log(" to the specified file.");
632 void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
634 log_header(design
, "Executing QBFSAT pass (solving QBF-SAT problems in the circuit).\n");
635 QbfSolveOptions opt
= parse_args(args
);
636 extra_args(args
, opt
.argidx
, design
);
638 RTLIL::Module
*module
= nullptr;
639 for (auto mod
: design
->selected_modules()) {
641 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
));
644 if (module
== nullptr)
645 log_cmd_error("Can't perform QBF-SAT on an empty selection!\n");
648 if (!opt
.specialize_from_file
) {
649 //Save the design to restore after modiyfing the current module.
650 std::string module_name
= module
->name
.str();
652 QbfSolutionType ret
= qbf_solve(module
, opt
);
653 module
= design
->module(module_name
);
655 log_warning("solver did not give an answer\n");
656 if (opt
.sat
|| opt
.unsat
)
657 log_cmd_error("expected problem to be %s\n", opt
.sat
? "SAT" : "UNSAT");
661 if (opt
.write_solution
) {
662 write_solution(module
, ret
, opt
.write_soln_soln_file
);
664 if (opt
.specialize
) {
665 specialize(module
, ret
);
667 dump_model(module
, ret
);
670 log_cmd_error("expected problem to be UNSAT\n");
673 print_proof_failed();
675 log_cmd_error("expected problem to be SAT\n");
678 specialize_from_file(module
, opt
.specialize_soln_file
);
683 PRIVATE_NAMESPACE_END