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/log.h"
23 #include "kernel/rtlil.h"
24 #include "kernel/register.h"
28 # define WIFEXITED(x) 1
29 # define WIFSIGNALED(x) 0
30 # define WIFSTOPPED(x) 0
31 # define WEXITSTATUS(x) ((x) & 0xff)
32 # define WTERMSIG(x) SIGTERM
34 # include <sys/wait.h>
38 PRIVATE_NAMESPACE_BEGIN
40 struct QbfSolutionType
{
41 std::vector
<std::string
> stdout
;
42 std::map
<std::string
, std::string
> hole_to_value
;
44 bool unknown
; //true if neither 'sat' nor 'unsat'
45 bool success
; //true if exit code 0
47 QbfSolutionType() : sat(false), unknown(true), success(false) {}
50 struct QbfSolveOptions
{
51 bool timeout
, specialize
, specialize_from_file
, write_solution
, nocleanup
, dump_final_smt2
;
53 std::string specialize_soln_file
;
54 std::string write_soln_soln_file
;
55 std::string dump_final_smt2_file
;
56 QbfSolveOptions() : timeout(false), specialize(false), specialize_from_file(false), write_solution(false),
57 nocleanup(false), dump_final_smt2(false), timeout_sec(-1) {};
60 void recover_solution(RTLIL::Module
*mod
, QbfSolutionType
&sol
) {
61 YS_REGEX_TYPE sat_regex
= YS_REGEX_COMPILE("Status: PASSED");
62 YS_REGEX_TYPE unsat_regex
= YS_REGEX_COMPILE("Solver Error.*model is not available");
63 YS_REGEX_TYPE hole_value_regex
= YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
64 YS_REGEX_TYPE hole_loc_regex
= YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+");
65 YS_REGEX_TYPE hole_val_regex
= YS_REGEX_COMPILE("[0-9]+");
66 YS_REGEX_MATCH_TYPE m
;
67 bool sat_regex_found
= false;
68 bool unsat_regex_found
= false;
69 std::map
<std::string
, bool> hole_value_recovered
;
70 for (const std::string
&x
: sol
.stdout
) {
71 if(YS_REGEX_NS::regex_search(x
, m
, hole_value_regex
)) {
72 std::string loc
= m
[1].str();
73 std::string val
= m
[2].str();
74 log_assert(YS_REGEX_NS::regex_search(loc
, hole_loc_regex
));
75 log_assert(YS_REGEX_NS::regex_search(val
, hole_val_regex
));
76 sol
.hole_to_value
[loc
] = val
;
78 else if (YS_REGEX_NS::regex_search(x
, sat_regex
))
79 sat_regex_found
= true;
80 else if (YS_REGEX_NS::regex_search(x
, unsat_regex
))
81 unsat_regex_found
= true;
83 log_assert(!sol
.unknown
&& sol
.sat
? sat_regex_found
: true);
84 log_assert(!sol
.unknown
&& !sol
.sat
? unsat_regex_found
: true);
87 QbfSolutionType
qbf_solve(RTLIL::Module
*mod
, const QbfSolveOptions
&opt
) {
89 std::string yosys_smtbmc_exe
= proc_self_dirname() + "yosys-smtbmc";
90 std::string smtbmc_warning
= "z3: WARNING:";
92 std::string tempdir_name
= "/tmp/yosys-z3-XXXXXX";
93 tempdir_name
= make_temp_dir(tempdir_name
);
94 std::string smt2_command
= "write_smt2 -stbv -wires " + tempdir_name
+ "/problem.smt2";
95 log_assert(mod
->design
!= nullptr);
96 Pass::call(mod
->design
, smt2_command
);
98 //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g [--dump-smt2 <file>]`
101 bool keep_reading
= true;
104 char buf
[1024] = {0};
105 std::string linebuf
= "";
106 std::string cmd
= yosys_smtbmc_exe
+ " -s z3 -t 1 -g " + (opt
.dump_final_smt2
? "--dump-smt2 " + opt
.dump_final_smt2_file
+ " " : "") + tempdir_name
+ "/problem.smt2 2>&1";
107 log("Launching \"%s\".\n", cmd
.c_str());
110 FILE *f
= popen(cmd
.c_str(), "r");
112 log_cmd_error("errno %d after popen() returned NULL.\n", errno
);
113 while (keep_reading
) {
114 keep_reading
= (fgets(buf
, sizeof(buf
), f
) != nullptr);
116 memset(buf
, 0, sizeof(buf
));
118 auto pos
= linebuf
.find('\n');
119 while (pos
!= std::string::npos
) {
120 std::string line
= linebuf
.substr(0, pos
);
121 linebuf
.erase(0, pos
+ 1);
122 ret
.stdout
.push_back(line
);
123 auto warning_pos
= line
.find(smtbmc_warning
);
124 if(warning_pos
!= std::string::npos
)
125 log_warning("%s\n", line
.substr(warning_pos
+ smtbmc_warning
.size() + 1).c_str());
127 log("smtbmc output: %s\n", line
.c_str());
129 pos
= linebuf
.find('\n');
135 if(WIFEXITED(status
)) {
136 retval
= WEXITSTATUS(status
);
138 else if(WIFSIGNALED(status
)) {
139 retval
= WTERMSIG(status
);
141 else if(WIFSTOPPED(status
)) {
142 retval
= WSTOPSIG(status
);
148 } else if (retval
== 1) {
155 remove_directory(tempdir_name
);
157 recover_solution(mod
, ret
);
163 void print_proof_failed()
166 log(" ______ ___ ___ _ _ _ _ \n");
167 log(" (_____ \\ / __) / __) (_) | | | |\n");
168 log(" _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |\n");
169 log(" | ____/ ___) _ \\ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|\n");
170 log(" | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ \n");
171 log(" |_| |_| \\___/ \\___/ |_| |_| \\_____|_|\\_)_____)\\____|_|\n");
178 log(" /$$$$$$ /$$$$$$$$ /$$$$$$$ \n");
179 log(" /$$__ $$ | $$_____/ | $$__ $$ \n");
180 log(" | $$ \\ $$ | $$ | $$ \\ $$ \n");
181 log(" | $$ | $$ | $$$$$ | $$ | $$ \n");
182 log(" | $$ | $$ | $$__/ | $$ | $$ \n");
183 log(" | $$/$$ $$ | $$ | $$ | $$ \n");
184 log(" | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
185 log(" \\____ $$$|__/|________/|__/|_______/|__/\n");
190 struct QbfSatPass
: public Pass
{
191 QbfSatPass() : Pass("qbfsat", "solve a 2QBF-SAT problem in the circuit") { }
192 void help() YS_OVERRIDE
194 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
196 log(" qbfsat [options] [selection]\n");
198 log("This command solves a 2QBF-SAT problem defined over the currently selected module.\n");
199 log("Existentially-quantified variables are declared by assigning a wire \"$anyconst\".\n");
200 log("Universally-quantified variables may be explicitly declared by assigning a wire\n");
201 log("\"$allconst\", but module inputs will be treated as universally-quantified variables\n");
202 log("by default.\n");
204 log(" -timeout <seconds>\n");
205 log(" Set the solver timeout to the specified number of seconds.\n");
207 log(" -nocleanup\n");
208 log(" Do not delete temporary files and directories. Useful for\n");
209 log(" debugging.\n");
211 log(" -dump-final-smt2 <file>\n");
212 log(" Pass the --dump-smt2 option to yosys-smtbmc.\n");
214 log(" -specialize\n");
215 log(" Replace all \"$anyconst\" cells with constant values determined by the solver.\n");
217 log(" -specialize-from-file <solution file>\n");
218 log(" Do not run the solver, but instead only attempt to replace all \"$anyconst\"\n");
219 log(" cells in the current module with values provided by the specified file.\n");
221 log(" -write-solution <solution file>\n");
222 log(" Write the assignments discovered by the solver for all \"$anyconst\" cells\n");
223 log(" to the specified file.");
227 void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
230 log_header(design
, "Executing QBF-SAT pass (solving QBF-SAT problems in the circuit).\n");
233 for (argidx
= 1; argidx
< args
.size(); argidx
++) {
234 if (args
[argidx
] == "-timeout") {
236 if (args
.size() <= argidx
+ 1)
237 log_cmd_error("timeout not specified.\n");
239 opt
.timeout_sec
= atol(args
[++argidx
].c_str());
242 else if (args
[argidx
] == "-nocleanup") {
243 opt
.nocleanup
= true;
246 else if (args
[argidx
] == "-specialize") {
247 opt
.specialize
= true;
250 else if (args
[argidx
] == "-dump-final-smt2") {
251 opt
.dump_final_smt2
= true;
252 if (args
.size() <= argidx
+ 1)
253 log_cmd_error("smt2 file not specified.\n");
255 opt
.dump_final_smt2_file
= args
[++argidx
];
258 else if (args
[argidx
] == "-specialize-from-file") {
259 opt
.specialize_from_file
= true;
260 if (args
.size() <= argidx
+ 1)
261 log_cmd_error("solution file not specified.\n");
263 opt
.specialize_soln_file
= args
[++argidx
];
266 else if (args
[argidx
] == "-write-solution") {
267 opt
.write_solution
= true;
268 if (args
.size() <= argidx
+ 1)
269 log_cmd_error("solution file not specified.\n");
271 opt
.write_soln_soln_file
= args
[++argidx
];
276 extra_args(args
, argidx
, design
);
278 RTLIL::Module
*module
= NULL
;
279 for (auto mod
: design
->selected_modules()) {
281 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
));
285 log_cmd_error("Can't perform QBF-SAT on an empty selection!\n");
287 bool found_input
= false;
288 bool found_hole
= false;
289 bool found_1bit_output
= false;
290 std::set
<std::string
> input_wires
;
291 for (auto wire
: module
->wires()) {
292 if (wire
->port_input
) {
294 input_wires
.insert(wire
->name
.str());
296 if (wire
->port_output
&& wire
->width
== 1)
297 found_1bit_output
= true;
299 for (auto cell
: module
->cells()) {
300 if (cell
->type
== "$allconst")
302 if (cell
->type
== "$anyconst")
304 if (cell
->type
.in("$assert", "$assume"))
305 found_1bit_output
= true;
308 log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n");
310 log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n");
311 if (!found_1bit_output
)
312 log_cmd_error("Did not find any single-bit outputs, assert()s, or assume()s. Is this a miter circuit?\n");
314 //Save the design to restore after modiyfing the current module.
315 std::string module_name
= module
->name
.str();
316 Pass::call(design
, "design -save _qbfsat_tmp");
318 //Replace input wires with wires assigned $allconst cells.
319 for(auto &n
: input_wires
) {
320 RTLIL::Wire
*input
= module
->wire(n
);
321 log_assert(input
!= nullptr);
323 RTLIL::Cell
*allconst
= module
->addCell("$allconst$" + n
, "$allconst");
324 allconst
->setParam(ID(WIDTH
), input
->width
);
325 allconst
->setPort(ID::Y
, input
);
326 allconst
->set_src_attribute(input
->get_src_attribute());
327 input
->port_input
= false;
328 log("Replaced input %s with $allconst cell.\n", n
.c_str());
330 module
->fixup_ports();
332 QbfSolutionType ret
= qbf_solve(module
, opt
);
333 Pass::call(design
, "design -load _qbfsat_tmp");
334 module
= design
->module(module_name
);
337 log_warning("solver did not give an answer\n");
341 print_proof_failed();
343 if (opt
.specialize
) {
344 std::map
<std::string
, std::string
> hole_loc_to_name
;
345 for (auto cell
: module
->cells()) {
346 std::string cell_src
= cell
->get_src_attribute();
347 auto pos
= ret
.hole_to_value
.find(cell_src
);
348 if (pos
!= ret
.hole_to_value
.end()) {
349 log_assert(cell
->type
.in("$anyconst", "$anyseq"));
350 log_assert(cell
->hasPort(ID::Y
));
351 log_assert(cell
->getPort(ID::Y
).is_wire());
352 hole_loc_to_name
[pos
->first
] = cell
->getPort(ID::Y
).as_wire()->name
.str();
355 for (auto &it
: ret
.hole_to_value
) {
356 std::string hole_loc
= it
.first
;
357 std::string hole_value
= it
.second
;
359 auto pos
= hole_loc_to_name
.find(hole_loc
);
360 log_assert(pos
!= hole_loc_to_name
.end());
362 std::string hole_name
= hole_loc_to_name
[hole_loc
];
363 RTLIL::Wire
*wire
= module
->wire(hole_name
);
364 log_assert(wire
!= nullptr);
366 log("Specializing %s with %s = %s.\n", module
->name
.c_str(), hole_name
.c_str(), hole_value
.c_str());
367 module
->connect(wire
, hole_value
);
369 Pass::call(design
, "opt_clean");
374 PRIVATE_NAMESPACE_END