aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2
diff options
context:
space:
mode:
Diffstat (limited to 'backends/smt2')
-rw-r--r--backends/smt2/Makefile.inc13
-rw-r--r--backends/smt2/example.v11
-rw-r--r--backends/smt2/example.ys3
-rw-r--r--backends/smt2/smt2.cc465
-rw-r--r--backends/smt2/smtbmc.py225
-rw-r--r--backends/smt2/smtio.py325
6 files changed, 941 insertions, 101 deletions
diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc
index 4e0a393a8..eacda2734 100644
--- a/backends/smt2/Makefile.inc
+++ b/backends/smt2/Makefile.inc
@@ -1,3 +1,16 @@
OBJS += backends/smt2/smt2.o
+ifneq ($(CONFIG),mxe)
+ifneq ($(CONFIG),emcc)
+TARGETS += yosys-smtbmc
+
+yosys-smtbmc: backends/smt2/smtbmc.py
+ $(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(__file__) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < $< > $@.new
+ $(Q) chmod +x $@.new
+ $(Q) mv $@.new $@
+
+$(eval $(call add_share_file,share/python3,backends/smt2/smtio.py))
+endif
+endif
+
diff --git a/backends/smt2/example.v b/backends/smt2/example.v
new file mode 100644
index 000000000..b195266eb
--- /dev/null
+++ b/backends/smt2/example.v
@@ -0,0 +1,11 @@
+module main(input clk);
+ reg [3:0] counter = 0;
+ always @(posedge clk) begin
+ if (counter == 10)
+ counter <= 0;
+ else
+ counter <= counter + 1;
+ end
+ assert property (counter != 15);
+ // assert property (counter <= 10);
+endmodule
diff --git a/backends/smt2/example.ys b/backends/smt2/example.ys
new file mode 100644
index 000000000..6fccb344f
--- /dev/null
+++ b/backends/smt2/example.ys
@@ -0,0 +1,3 @@
+read_verilog -formal example.v
+hierarchy; proc; opt; memory -nordff -nomap; opt -fast
+write_smt2 -bv -mem -wires example.smt2
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 8451eff4f..e869f78cd 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -2,11 +2,11 @@
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
@@ -32,17 +32,21 @@ struct Smt2Worker
CellTypes ct;
SigMap sigmap;
RTLIL::Module *module;
- bool bvmode;
+ bool bvmode, memmode, regsmode, wiresmode, verbose;
int idcounter;
std::vector<std::string> decls, trans;
std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
std::set<RTLIL::Cell*> exported_cells;
+ pool<Cell*> recursive_cells, registers;
std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
+ std::map<Cell*, int> memarrays;
std::map<int, int> bvsizes;
- Smt2Worker(RTLIL::Module *module, bool bvmode) : ct(module->design), sigmap(module), module(module), bvmode(bvmode), idcounter(0)
+ Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool regsmode, bool wiresmode, bool verbose) :
+ ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode),
+ regsmode(regsmode), wiresmode(wiresmode), verbose(verbose), idcounter(0)
{
decls.push_back(stringf("(declare-sort |%s_s| 0)\n", log_id(module)));
@@ -64,6 +68,9 @@ struct Smt2Worker
void register_bool(RTLIL::SigBit bit, int id)
{
+ if (verbose) log("%*s-> register_bool: %s %d\n", 2+2*GetSize(recursive_cells), "",
+ log_signal(bit), id);
+
sigmap.apply(bit);
log_assert(fcache.count(bit) == 0);
fcache[bit] = std::pair<int, int>(id, -1);
@@ -71,6 +78,9 @@ struct Smt2Worker
void register_bv(RTLIL::SigSpec sig, int id)
{
+ if (verbose) log("%*s-> register_bv: %s %d\n", 2+2*GetSize(recursive_cells), "",
+ log_signal(sig), id);
+
log_assert(bvmode);
sigmap.apply(sig);
@@ -85,6 +95,9 @@ struct Smt2Worker
void register_boolvec(RTLIL::SigSpec sig, int id)
{
+ if (verbose) log("%*s-> register_boolvec: %s %d\n", 2+2*GetSize(recursive_cells), "",
+ log_signal(sig), id);
+
log_assert(bvmode);
sigmap.apply(sig);
register_bool(sig[0], id);
@@ -105,6 +118,8 @@ struct Smt2Worker
sigmap.apply(bit);
if (fcache.count(bit) == 0) {
+ if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "",
+ log_signal(bit));
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
log_id(module), idcounter, log_id(module), log_signal(bit)));
register_bool(bit, idcounter++);
@@ -118,7 +133,7 @@ struct Smt2Worker
std::string get_bool(RTLIL::SigSpec sig, const char *state_name = "state")
{
- return get_bool(sig.to_single_sigbit(), state_name);
+ return get_bool(sig.as_bit(), state_name);
}
std::string get_bv(RTLIL::SigSpec sig, const char *state_name = "state")
@@ -128,10 +143,14 @@ struct Smt2Worker
std::vector<std::string> subexpr;
- for (auto bit : sig)
- if (bit_driver.count(bit))
- export_cell(bit_driver.at(bit));
- sigmap.apply(sig);
+ SigSpec orig_sig;
+ while (orig_sig != sig) {
+ for (auto bit : sig)
+ if (bit_driver.count(bit))
+ export_cell(bit_driver.at(bit));
+ orig_sig = sig;
+ sigmap.apply(sig);
+ }
for (int i = 0, j = 1; i < GetSize(sig); i += j, j = 1)
{
@@ -161,9 +180,10 @@ struct Smt2Worker
j++;
}
if (t1.second == 0 && j == bvsizes.at(t1.first))
- subexpr.push_back(stringf("(|%s#%d| state)", log_id(module), t1.first));
+ subexpr.push_back(stringf("(|%s#%d| %s)", log_id(module), t1.first, state_name));
else
- subexpr.push_back(stringf("((_ extract %d %d) (|%s#%d| state))", t1.second + j - 1, t1.second, log_id(module), t1.first));
+ subexpr.push_back(stringf("((_ extract %d %d) (|%s#%d| %s))",
+ t1.second + j - 1, t1.second, log_id(module), t1.first, state_name));
continue;
}
@@ -171,17 +191,23 @@ struct Smt2Worker
while (i+j < GetSize(sig) && sig[i+j].wire && !fcache.count(sig[i+j]) && !seen_bits.count(sig[i+j]))
seen_bits.insert(sig[i+j]), j++;
+ if (verbose) log("%*s-> external bv: %s\n", 2+2*GetSize(recursive_cells), "",
+ log_signal(sig.extract(i, j)));
+ for (auto bit : sig.extract(i, j))
+ log_assert(bit_driver.count(bit) == 0);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
log_id(module), idcounter, log_id(module), j, log_signal(sig.extract(i, j))));
- subexpr.push_back(stringf("(|%s#%d| state)", log_id(module), idcounter));
+ subexpr.push_back(stringf("(|%s#%d| %s)", log_id(module), idcounter, state_name));
register_bv(sig.extract(i, j), idcounter++);
}
if (GetSize(subexpr) > 1) {
- std::string expr = "(concat";
- for (int i = GetSize(subexpr)-1; i >= 0; i--)
+ std::string expr = "", end_str = "";
+ for (int i = GetSize(subexpr)-1; i >= 0; i--) {
+ if (i > 0) expr += " (concat", end_str += ")";
expr += " " + subexpr[i];
- return expr + ")";
+ }
+ return expr.substr(1) + end_str;
} else {
log_assert(GetSize(subexpr) == 1);
return subexpr[0];
@@ -190,7 +216,7 @@ struct Smt2Worker
void export_gate(RTLIL::Cell *cell, std::string expr)
{
- RTLIL::SigBit bit = sigmap(cell->getPort("\\Y").to_single_sigbit());
+ RTLIL::SigBit bit = sigmap(cell->getPort("\\Y").as_bit());
std::string processed_expr;
for (char ch : expr) {
@@ -202,10 +228,12 @@ struct Smt2Worker
else processed_expr += ch;
}
+ if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
+ log_id(cell));
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(bit)));
register_bool(bit, idcounter++);
- return;
+ recursive_cells.erase(cell);
}
void export_bvop(RTLIL::Cell *cell, std::string expr, char type = 0)
@@ -216,8 +244,8 @@ struct Smt2Worker
int width = GetSize(sig_y);
if (type == 's' || type == 'd' || type == 'b') {
- width = std::max(width, GetSize(cell->getPort("\\A")));
- width = std::max(width, GetSize(cell->getPort("\\B")));
+ width = max(width, GetSize(cell->getPort("\\A")));
+ width = max(width, GetSize(cell->getPort("\\B")));
}
if (cell->hasPort("\\A")) {
@@ -243,6 +271,9 @@ struct Smt2Worker
if (width != GetSize(sig_y) && type != 'b')
processed_expr = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, processed_expr.c_str());
+ if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
+ log_id(cell));
+
if (type == 'b') {
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(sig_y)));
@@ -252,7 +283,8 @@ struct Smt2Worker
log_id(module), idcounter, log_id(module), GetSize(sig_y), processed_expr.c_str(), log_signal(sig_y)));
register_bv(sig_y, idcounter++);
}
- return;
+
+ recursive_cells.erase(cell);
}
void export_reduce(RTLIL::Cell *cell, std::string expr, bool identity_val)
@@ -270,23 +302,35 @@ struct Smt2Worker
} else
processed_expr += ch;
+ if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
+ log_id(cell));
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(sig_y)));
register_boolvec(sig_y, idcounter++);
- return;
+ recursive_cells.erase(cell);
}
void export_cell(RTLIL::Cell *cell)
{
+ if (verbose) log("%*s=> export_cell %s (%s) [%s]\n", 2+2*GetSize(recursive_cells), "",
+ log_id(cell), log_id(cell->type), exported_cells.count(cell) ? "old" : "new");
+
+ if (recursive_cells.count(cell))
+ log_error("Found logic loop in module %s! See cell %s.\n", log_id(module), log_id(cell));
+
if (exported_cells.count(cell))
return;
+
exported_cells.insert(cell);
+ recursive_cells.insert(cell);
if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
{
- std::string expr_d = get_bool(cell->getPort("\\D"));
- std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
- trans.push_back(stringf(" (= %s %s)\n", expr_d.c_str(), expr_q.c_str()));
+ registers.insert(cell);
+ decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
+ log_id(module), idcounter, log_id(module), log_signal(cell->getPort("\\Q"))));
+ register_bool(cell->getPort("\\Q"), idcounter++);
+ recursive_cells.erase(cell);
return;
}
@@ -304,94 +348,157 @@ struct Smt2Worker
if (cell->type == "$_AOI4_") return export_gate(cell, "(not (or (and A B) (and C D)))");
if (cell->type == "$_OAI4_") return export_gate(cell, "(not (and (or A B) (or C D)))");
- // FIXME: $lut $assert
-
- if (!bvmode)
- log_error("Unsupported cell type %s for cell %s.%s. (Maybe this cell type would be supported in -bv mode?)\n",
- log_id(cell->type), log_id(module), log_id(cell));
+ // FIXME: $lut
- if (cell->type == "$dff")
+ if (bvmode)
{
- std::string expr_d = get_bv(cell->getPort("\\D"));
- std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
- trans.push_back(stringf(" (= %s %s)\n", expr_d.c_str(), expr_q.c_str()));
- return;
+ if (cell->type == "$dff")
+ {
+ registers.insert(cell);
+ decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
+ log_id(module), idcounter, log_id(module), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q"))));
+ register_bv(cell->getPort("\\Q"), idcounter++);
+ recursive_cells.erase(cell);
+ return;
+ }
+
+ if (cell->type == "$and") return export_bvop(cell, "(bvand A B)");
+ if (cell->type == "$or") return export_bvop(cell, "(bvor A B)");
+ if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)");
+ if (cell->type == "$xnor") return export_bvop(cell, "(bvxnor A B)");
+
+ if (cell->type == "$shl") return export_bvop(cell, "(bvshl A B)", 's');
+ if (cell->type == "$shr") return export_bvop(cell, "(bvlshr A B)", 's');
+ if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", 's');
+ if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", 's');
+
+ // FIXME: $shift $shiftx
+
+ if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)", 'b');
+ if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)", 'b');
+ if (cell->type == "$ge") return export_bvop(cell, "(bvUge A B)", 'b');
+ if (cell->type == "$gt") return export_bvop(cell, "(bvUgt A B)", 'b');
+
+ if (cell->type == "$ne") return export_bvop(cell, "(distinct A B)", 'b');
+ if (cell->type == "$nex") return export_bvop(cell, "(distinct A B)", 'b');
+ if (cell->type == "$eq") return export_bvop(cell, "(= A B)", 'b');
+ if (cell->type == "$eqx") return export_bvop(cell, "(= A B)", 'b');
+
+ if (cell->type == "$not") return export_bvop(cell, "(bvnot A)");
+ if (cell->type == "$pos") return export_bvop(cell, "A");
+ if (cell->type == "$neg") return export_bvop(cell, "(bvneg A)");
+
+ if (cell->type == "$add") return export_bvop(cell, "(bvadd A B)");
+ if (cell->type == "$sub") return export_bvop(cell, "(bvsub A B)");
+ if (cell->type == "$mul") return export_bvop(cell, "(bvmul A B)");
+ if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)", 'd');
+ if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)", 'd');
+
+ if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true);
+ if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false);
+ if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false);
+ if (cell->type == "$reduce_xnor") return export_reduce(cell, "(not (xor A))", false);
+ if (cell->type == "$reduce_bool") return export_reduce(cell, "(or A)", false);
+
+ if (cell->type == "$logic_not") return export_reduce(cell, "(not (or A))", false);
+ if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))", false);
+ if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)", false);
+
+ if (cell->type == "$mux" || cell->type == "$pmux")
+ {
+ int width = GetSize(cell->getPort("\\Y"));
+ std::string processed_expr = get_bv(cell->getPort("\\A"));
+
+ RTLIL::SigSpec sig_b = cell->getPort("\\B");
+ RTLIL::SigSpec sig_s = cell->getPort("\\S");
+ get_bv(sig_b);
+ get_bv(sig_s);
+
+ for (int i = 0; i < GetSize(sig_s); i++)
+ processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(),
+ get_bv(sig_b.extract(i*width, width)).c_str(), processed_expr.c_str());
+
+ if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
+ log_id(cell));
+ RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y"));
+ decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+ log_id(module), idcounter, log_id(module), width, processed_expr.c_str(), log_signal(sig)));
+ register_bv(sig, idcounter++);
+ recursive_cells.erase(cell);
+ return;
+ }
+
+ // FIXME: $slice $concat
}
- if (cell->type == "$and") return export_bvop(cell, "(bvand A B)");
- if (cell->type == "$or") return export_bvop(cell, "(bvor A B)");
- if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)");
- if (cell->type == "$xnor") return export_bvop(cell, "(bvxnor A B)");
-
- if (cell->type == "$shl") return export_bvop(cell, "(bvshl A B)", 's');
- if (cell->type == "$shr") return export_bvop(cell, "(bvlshr A B)", 's');
- if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", 's');
- if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", 's');
-
- // FIXME: $shift $shiftx
-
- if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)", 'b');
- if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)", 'b');
- if (cell->type == "$ge") return export_bvop(cell, "(bvUge A B)", 'b');
- if (cell->type == "$gt") return export_bvop(cell, "(bvUgt A B)", 'b');
-
- if (cell->type == "$ne") return export_bvop(cell, "(distinct A B)", 'b');
- if (cell->type == "$nex") return export_bvop(cell, "(distinct A B)", 'b');
- if (cell->type == "$eq") return export_bvop(cell, "(= A B)", 'b');
- if (cell->type == "$eqx") return export_bvop(cell, "(= A B)", 'b');
-
- if (cell->type == "$not") return export_bvop(cell, "(bvnot A)");
- if (cell->type == "$pos") return export_bvop(cell, "A");
- if (cell->type == "$neg") return export_bvop(cell, "(bvneg A)");
-
- if (cell->type == "$add") return export_bvop(cell, "(bvadd A B)");
- if (cell->type == "$sub") return export_bvop(cell, "(bvsub A B)");
- if (cell->type == "$mul") return export_bvop(cell, "(bvmul A B)");
- if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)", 'd');
- if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)", 'd');
-
- if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true);
- if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false);
- if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false);
- if (cell->type == "$reduce_xnor") return export_reduce(cell, "(not (xor A))", false);
- if (cell->type == "$reduce_bool") return export_reduce(cell, "(or A)", false);
-
- if (cell->type == "$logic_not") return export_reduce(cell, "(not (or A))", false);
- if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))", false);
- if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)", false);
-
- if (cell->type == "$mux" || cell->type == "$pmux")
+ if (memmode && cell->type == "$mem")
{
- int width = GetSize(cell->getPort("\\Y"));
- std::string processed_expr = get_bv(cell->getPort("\\A"));
+ int arrayid = idcounter++;
+ memarrays[cell] = arrayid;
- RTLIL::SigSpec sig_b = cell->getPort("\\B");
- RTLIL::SigSpec sig_s = cell->getPort("\\S");
- get_bv(sig_b);
- get_bv(sig_s);
+ int abits = cell->getParam("\\ABITS").as_int();
+ int width = cell->getParam("\\WIDTH").as_int();
+ int rd_ports = cell->getParam("\\RD_PORTS").as_int();
- for (int i = 0; i < GetSize(sig_s); i++)
- processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(),
- get_bv(sig_b.extract(i*width, width)).c_str(), processed_expr.c_str());
+ decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
+ log_id(module), arrayid, log_id(module), abits, width, log_id(cell)));
- RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y"));
- decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
- log_id(module), idcounter, log_id(module), width, processed_expr.c_str(), log_signal(sig)));
- register_bv(sig, idcounter++);
+ decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s#%d#0| state))\n",
+ log_id(module), log_id(cell), log_id(module), abits, width, log_id(module), arrayid));
+
+ for (int i = 0; i < rd_ports; i++)
+ {
+ std::string addr = get_bv(cell->getPort("\\RD_ADDR").extract(abits*i, abits));
+ SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
+
+ if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
+ log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
+ "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
+
+ decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s#%d#0| state) %s)) ; %s\n",
+ log_id(module), idcounter, log_id(module), width, log_id(module), arrayid, addr.c_str(), log_signal(data_sig)));
+ register_bv(data_sig, idcounter++);
+ }
+
+ registers.insert(cell);
+ recursive_cells.erase(cell);
return;
}
- // FIXME: $slice $concat
-
- log_error("Unsupported cell type %s for cell %s.%s.\n",
+ log_error("Unsupported cell type %s for cell %s.%s. (Maybe this cell type would be supported in -bv or -mem mode?)\n",
log_id(cell->type), log_id(module), log_id(cell));
}
void run()
{
- for (auto wire : module->wires())
- if (wire->port_id || wire->get_bool_attribute("\\keep")) {
+ if (verbose) log("=> export logic driving outputs\n");
+
+ pool<SigBit> reg_bits;
+ if (regsmode) {
+ for (auto cell : module->cells())
+ if (cell->type.in("$_DFF_P_", "$_DFF_N_", "$dff")) {
+ // not using sigmap -- we want the net directly at the dff output
+ for (auto bit : cell->getPort("\\Q"))
+ reg_bits.insert(bit);
+ }
+ }
+
+ for (auto wire : module->wires()) {
+ bool is_register = false;
+ if (regsmode)
+ for (auto bit : SigSpec(wire))
+ if (reg_bits.count(bit))
+ is_register = true;
+ if (wire->port_id || is_register || wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) {
RTLIL::SigSpec sig = sigmap(wire);
+ if (wire->port_input)
+ decls.push_back(stringf("; yosys-smt2-input %s %d\n", log_id(wire), wire->width));
+ if (wire->port_output)
+ decls.push_back(stringf("; yosys-smt2-output %s %d\n", log_id(wire), wire->width));
+ if (is_register)
+ decls.push_back(stringf("; yosys-smt2-register %s %d\n", log_id(wire), wire->width));
+ if (wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\'))
+ decls.push_back(stringf("; yosys-smt2-wire %s %d\n", log_id(wire), wire->width));
if (bvmode && GetSize(sig) > 1) {
decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
log_id(module), log_id(wire), log_id(module), GetSize(sig), get_bv(sig).c_str()));
@@ -405,6 +512,118 @@ struct Smt2Worker
log_id(module), log_id(wire), log_id(module), get_bool(sig[i]).c_str()));
}
}
+ }
+
+ if (verbose) log("=> export logic associated with the initial state\n");
+
+ vector<string> init_list;
+ for (auto wire : module->wires())
+ if (wire->attributes.count("\\init")) {
+ RTLIL::SigSpec sig = sigmap(wire);
+ Const val = wire->attributes.at("\\init");
+ val.bits.resize(GetSize(sig));
+ if (bvmode && GetSize(sig) > 1) {
+ init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), log_id(wire)));
+ } else {
+ for (int i = 0; i < GetSize(sig); i++)
+ init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val.bits[i] == State::S1 ? "true" : "false", log_id(wire)));
+ }
+ }
+
+ if (verbose) log("=> export logic driving asserts\n");
+
+ vector<int> assert_list, assume_list;
+ for (auto cell : module->cells())
+ if (cell->type.in("$assert", "$assume")) {
+ string name_a = get_bool(cell->getPort("\\A"));
+ string name_en = get_bool(cell->getPort("\\EN"));
+ decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
+ log_id(module), idcounter, log_id(module), name_a.c_str(), name_en.c_str(), log_id(cell)));
+ if (cell->type == "$assert")
+ assert_list.push_back(idcounter++);
+ else
+ assume_list.push_back(idcounter++);
+ }
+
+ for (int iter = 1; !registers.empty(); iter++)
+ {
+ pool<Cell*> this_regs;
+ this_regs.swap(registers);
+
+ if (verbose) log("=> export logic driving registers [iteration %d]\n", iter);
+
+ for (auto cell : this_regs)
+ {
+ if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
+ {
+ std::string expr_d = get_bool(cell->getPort("\\D"));
+ std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
+ trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), log_id(cell), log_signal(cell->getPort("\\Q"))));
+ }
+
+ if (cell->type == "$dff")
+ {
+ std::string expr_d = get_bv(cell->getPort("\\D"));
+ std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
+ trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), log_id(cell), log_signal(cell->getPort("\\Q"))));
+ }
+
+ if (cell->type == "$mem")
+ {
+ int arrayid = memarrays.at(cell);
+
+ int abits = cell->getParam("\\ABITS").as_int();
+ int width = cell->getParam("\\WIDTH").as_int();
+ int wr_ports = cell->getParam("\\WR_PORTS").as_int();
+
+ for (int i = 0; i < wr_ports; i++)
+ {
+ std::string addr = get_bv(cell->getPort("\\WR_ADDR").extract(abits*i, abits));
+ std::string data = get_bv(cell->getPort("\\WR_DATA").extract(width*i, width));
+ std::string mask = get_bv(cell->getPort("\\WR_EN").extract(width*i, width));
+
+ data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
+ data.c_str(), mask.c_str(), log_id(module), arrayid, i, addr.c_str(), mask.c_str());
+
+ decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) "
+ "(store (|%s#%d#%d| state) %s %s)) ; %s\n",
+ log_id(module), arrayid, i+1, log_id(module), abits, width,
+ log_id(module), arrayid, i, addr.c_str(), data.c_str(), log_id(cell)));
+ }
+
+ std::string expr_d = stringf("(|%s#%d#%d| state)", log_id(module), arrayid, wr_ports);
+ std::string expr_q = stringf("(|%s#%d#0| next_state)", log_id(module), arrayid);
+ trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), log_id(cell)));
+ }
+ }
+ }
+
+ string assert_expr = assert_list.empty() ? "true" : "(and";
+ if (!assert_list.empty()) {
+ for (int i : assert_list)
+ assert_expr += stringf(" (|%s#%d| state)", log_id(module), i);
+ assert_expr += ")";
+ }
+ decls.push_back(stringf("(define-fun |%s_a| ((state |%s_s|)) Bool %s)\n",
+ log_id(module), log_id(module), assert_expr.c_str()));
+
+ string assume_expr = assume_list.empty() ? "true" : "(and";
+ if (!assume_list.empty()) {
+ for (int i : assume_list)
+ assume_expr += stringf(" (|%s#%d| state)", log_id(module), i);
+ assume_expr += ")";
+ }
+ decls.push_back(stringf("(define-fun |%s_u| ((state |%s_s|)) Bool %s)\n",
+ log_id(module), log_id(module), assume_expr.c_str()));
+
+ string init_expr = init_list.empty() ? "true" : "(and";
+ if (!init_list.empty()) {
+ for (auto &str : init_list)
+ init_expr += stringf("\n\t%s", str.c_str());
+ init_expr += "\n)";
+ }
+ decls.push_back(stringf("(define-fun |%s_i| ((state |%s_s|)) Bool %s)\n",
+ log_id(module), log_id(module), init_expr.c_str()));
}
void write(std::ostream &f)
@@ -412,6 +631,7 @@ struct Smt2Worker
for (auto it : decls)
f << it;
+ f << stringf("; yosys-smt2-module %s\n", log_id(module));
f << stringf("(define-fun |%s_t| ((state |%s_s|) (next_state |%s_s|)) Bool ", log_id(module), log_id(module), log_id(module));
if (GetSize(trans) > 1) {
f << "(and\n";
@@ -436,8 +656,8 @@ struct Smt2Backend : public Backend {
log(" write_smt2 [options] [filename]\n");
log("\n");
log("Write a SMT-LIBv2 [1] description of the current design. For a module with name\n");
- log("'<mod>' this will declare the sort '<mod>_s' (state of the module) and the the\n");
- log("function '<mod>_t' (state transition function).\n");
+ log("'<mod>' this will declare the sort '<mod>_s' (state of the module) and the\n");
+ log("functions operating on that state.\n");
log("\n");
log("The '<mod>_s' sort represents a module state. Additional '<mod>_n' functions\n");
log("are provided that can be used to access the values of the signals in the module.\n");
@@ -449,11 +669,37 @@ struct Smt2Backend : public Backend {
log("The '<mod>_t' function evaluates to 'true' when the given pair of states\n");
log("describes a valid state transition.\n");
log("\n");
+ log("The '<mod>_a' function evaluates to 'true' when the given state satisfies\n");
+ log("the asserts in the module.\n");
+ log("\n");
+ log("The '<mod>_u' function evaluates to 'true' when the given state satisfies\n");
+ log("the assumptions in the module.\n");
+ log("\n");
+ log("The '<mod>_i' function evaluates to 'true' when the given state conforms\n");
+ log("to the initial state.\n");
+ log("\n");
+ log(" -verbose\n");
+ log(" this will print the recursive walk used to export the modules.\n");
+ log("\n");
log(" -bv\n");
log(" enable support for BitVec (FixedSizeBitVectors theory). with this\n");
log(" option set multi-bit wires are represented using the BitVec sort and\n");
log(" support for coarse grain cells (incl. arithmetic) is enabled.\n");
log("\n");
+ log(" -mem\n");
+ log(" enable support for memories (via ArraysEx theory). this option\n");
+ log(" also implies -bv. only $mem cells without merged registers in\n");
+ log(" read ports are supported. call \"memory\" with -nordff to make sure\n");
+ log(" that no registers are merged into $mem read ports. '<mod>_m' functions\n");
+ log(" will be generated for accessing the arrays that are used to represent\n");
+ log(" memories.\n");
+ log("\n");
+ log(" -regs\n");
+ log(" also create '<mod>_n' functions for all registers.\n");
+ log("\n");
+ log(" -wires\n");
+ log(" also create '<mod>_n' functions for all public wires.\n");
+ log("\n");
log(" -tpl <template_file>\n");
log(" use the given template file. the line containing only the token '%%%%'\n");
log(" is replaced with the regular output of this command.\n");
@@ -500,7 +746,7 @@ struct Smt2Backend : public Backend {
log("The following yosys script will create a 'test.smt2' file for our proof:\n");
log("\n");
log(" read_verilog test.v\n");
- log(" hierarchy; proc; techmap; opt -fast\n");
+ log(" hierarchy -check; proc; opt; check -assert\n");
log(" write_smt2 -bv -tpl test.tpl test.smt2\n");
log("\n");
log("Running 'cvc4 test.smt2' will print 'unsat' because y can never transition\n");
@@ -510,9 +756,9 @@ struct Smt2Backend : public Backend {
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
{
std::ifstream template_f;
- bool bvmode = false;
+ bool bvmode = false, memmode = false, regsmode = false, wiresmode = false, verbose = false;
- log_header("Executing SMT2 backend.\n");
+ log_header(design, "Executing SMT2 backend.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
@@ -527,6 +773,23 @@ struct Smt2Backend : public Backend {
bvmode = true;
continue;
}
+ if (args[argidx] == "-mem") {
+ bvmode = true;
+ memmode = true;
+ continue;
+ }
+ if (args[argidx] == "-regs") {
+ regsmode = true;
+ continue;
+ }
+ if (args[argidx] == "-wires") {
+ wiresmode = true;
+ continue;
+ }
+ if (args[argidx] == "-verbose") {
+ verbose = true;
+ continue;
+ }
break;
}
extra_args(f, filename, args, argidx);
@@ -552,7 +815,7 @@ struct Smt2Backend : public Backend {
log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
- Smt2Worker worker(module, bvmode);
+ Smt2Worker worker(module, bvmode, memmode, regsmode, wiresmode, verbose);
worker.run();
worker.write(*f);
}
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
new file mode 100644
index 000000000..f2911b3e7
--- /dev/null
+++ b/backends/smt2/smtbmc.py
@@ -0,0 +1,225 @@
+#!/usr/bin/env python3
+#
+# yosys -- Yosys Open SYnthesis Suite
+#
+# Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+#
+# Permission to use, copy, modify, and/or distribute this software for any
+# purpose with or without fee is hereby granted, provided that the above
+# copyright notice and this permission notice appear in all copies.
+#
+# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+#
+
+import os, sys, getopt, re
+##yosys-sys-path##
+from smtio import smtio, smtopts, mkvcd
+
+skip_steps = 0
+step_size = 1
+num_steps = 20
+vcdfile = None
+tempind = False
+assume_skipped = None
+topmod = None
+so = smtopts()
+
+
+def usage():
+ print("""
+yosys-smtbmc [options] <yosys_smt2_output>
+
+ -t <num_steps>, -t <skip_steps>:<num_steps>
+ default: skip_steps=0, num_steps=20
+
+ -u <start_step>
+ assume asserts in skipped steps in BMC
+
+ -S <step_size>
+ proof <step_size> time steps at once
+
+ -c <vcd_filename>
+ write counter-example to this VCD file
+ (hint: use 'write_smt2 -wires' for maximum
+ coverage of signals in generated VCD file)
+
+ -i
+ instead of BMC run temporal induction
+
+ -m <module_name>
+ name of the top module
+""" + so.helpmsg())
+ sys.exit(1)
+
+
+try:
+ opts, args = getopt.getopt(sys.argv[1:], so.optstr + "t:u:S:c:im:")
+except:
+ usage()
+
+for o, a in opts:
+ if o == "-t":
+ match = re.match(r"(\d+):(.*)", a)
+ if match:
+ skip_steps = int(match.group(1))
+ num_steps = int(match.group(2))
+ else:
+ num_steps = int(a)
+ elif o == "-u":
+ assume_skipped = int(a)
+ elif o == "-S":
+ step_size = int(a)
+ elif o == "-c":
+ vcdfile = a
+ elif o == "-i":
+ tempind = True
+ elif o == "-m":
+ topmod = a
+ elif so.handle(o, a):
+ pass
+ else:
+ usage()
+
+if len(args) != 1:
+ usage()
+
+
+smt = smtio(opts=so)
+
+print("%s Solver: %s" % (smt.timestamp(), so.solver))
+smt.setup("QF_AUFBV")
+
+debug_nets = set()
+debug_nets_re = re.compile(r"^; yosys-smt2-(input|output|register|wire) (\S+) (\d+)")
+
+with open(args[0], "r") as f:
+ for line in f:
+ match = debug_nets_re.match(line)
+ if match:
+ debug_nets.add(match.group(2))
+ if line.startswith("; yosys-smt2-module") and topmod is None:
+ topmod = line.split()[2]
+ smt.write(line)
+
+assert topmod is not None
+
+
+def write_vcd_model(steps):
+ print("%s Writing model to VCD file." % smt.timestamp())
+
+ vcd = mkvcd(open(vcdfile, "w"))
+ for netname in sorted(debug_nets):
+ width = len(smt.get_net_bin(topmod, netname, "s0"))
+ vcd.add_net(netname, width)
+
+ for i in range(steps):
+ vcd.set_time(i)
+ for netname in debug_nets:
+ vcd.set_net(netname, smt.get_net_bin(topmod, netname, "s%d" % i))
+
+ vcd.set_time(steps)
+
+
+if tempind:
+ retstatus = False
+ skip_counter = step_size
+ for step in range(num_steps, -1, -1):
+ smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
+ smt.write("(assert (%s_u s%d))" % (topmod, step))
+
+ if step == num_steps:
+ smt.write("(assert (not (%s_a s%d)))" % (topmod, step))
+
+ else:
+ smt.write("(assert (%s_t s%d s%d))" % (topmod, step, step+1))
+ smt.write("(assert (%s_a s%d))" % (topmod, step))
+
+ if step > num_steps-skip_steps:
+ print("%s Skipping induction in step %d.." % (smt.timestamp(), step))
+ continue
+
+ skip_counter += 1
+ if skip_counter < step_size:
+ print("%s Skipping induction in step %d.." % (smt.timestamp(), step))
+ continue
+
+ skip_counter = 0
+ print("%s Trying induction in step %d.." % (smt.timestamp(), step))
+
+ if smt.check_sat() == "sat":
+ if step == 0:
+ print("%s Temporal induction failed!" % smt.timestamp())
+ if vcdfile is not None:
+ write_vcd_model(num_steps+1)
+
+ else:
+ print("%s Temporal induction successful." % smt.timestamp())
+ retstatus = True
+ break
+
+
+else: # not tempind
+ step = 0
+ retstatus = True
+ while step < num_steps:
+ smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
+ smt.write("(assert (%s_u s%d))" % (topmod, step))
+
+ if step == 0:
+ smt.write("(assert (%s_i s0))" % (topmod))
+
+ else:
+ smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step))
+
+ if step < skip_steps:
+ if assume_skipped is not None and step >= assume_skipped:
+ print("%s Skipping step %d (and assuming pass).." % (smt.timestamp(), step))
+ smt.write("(assert (%s_a s%d))" % (topmod, step))
+ else:
+ print("%s Skipping step %d.." % (smt.timestamp(), step))
+ step += 1
+ continue
+
+ last_check_step = step
+ for i in range(1, step_size):
+ if step+i < num_steps:
+ smt.write("(declare-fun s%d () %s_s)" % (step+i, topmod))
+ smt.write("(assert (%s_u s%d))" % (topmod, step+i))
+ smt.write("(assert (%s_t s%d s%d))" % (topmod, step+i-1, step+i))
+ last_check_step = step+i
+
+ if last_check_step == step:
+ print("%s Checking asserts in step %d.." % (smt.timestamp(), step))
+ else:
+ print("%s Checking asserts in steps %d to %d.." % (smt.timestamp(), step, last_check_step))
+ smt.write("(push 1)")
+
+ smt.write("(assert (not (and %s)))" % " ".join(["(%s_a s%d)" % (topmod, i) for i in range(step, last_check_step+1)]))
+
+ if smt.check_sat() == "sat":
+ print("%s BMC failed!" % smt.timestamp())
+ if vcdfile is not None:
+ write_vcd_model(step+step_size)
+ retstatus = False
+ break
+
+ else: # unsat
+ smt.write("(pop 1)")
+ for i in range(step, last_check_step+1):
+ smt.write("(assert (%s_a s%d))" % (topmod, i))
+
+ step += step_size
+
+
+smt.write("(exit)")
+smt.wait()
+
+print("%s Status: %s" % (smt.timestamp(), "PASSED" if retstatus else "FAILED (!)"))
+sys.exit(0 if retstatus else 1)
+
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
new file mode 100644
index 000000000..6e8bded77
--- /dev/null
+++ b/backends/smt2/smtio.py
@@ -0,0 +1,325 @@
+#!/usr/bin/env python3
+#
+# yosys -- Yosys Open SYnthesis Suite
+#
+# Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+#
+# Permission to use, copy, modify, and/or distribute this software for any
+# purpose with or without fee is hereby granted, provided that the above
+# copyright notice and this permission notice appear in all copies.
+#
+# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+#
+
+import sys
+import subprocess
+from select import select
+from time import time
+
+class smtio:
+ def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None):
+ if opts is not None:
+ self.solver = opts.solver
+ self.debug_print = opts.debug_print
+ self.debug_file = opts.debug_file
+ self.timeinfo = opts.timeinfo
+
+ else:
+ self.solver = "z3"
+ self.debug_print = False
+ self.debug_file = None
+ self.timeinfo = True
+
+ if solver is not None:
+ self.solver = solver
+
+ if debug_print is not None:
+ self.debug_print = debug_print
+
+ if debug_file is not None:
+ self.debug_file = debug_file
+
+ if timeinfo is not None:
+ self.timeinfo = timeinfo
+
+ if self.solver == "yices":
+ popen_vargs = ['yices-smt2', '--incremental']
+
+ if self.solver == "z3":
+ popen_vargs = ['z3', '-smt2', '-in']
+
+ if self.solver == "cvc4":
+ popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']
+
+ if self.solver == "mathsat":
+ popen_vargs = ['mathsat']
+
+ self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+ self.start_time = time()
+
+ def setup(self, logic="ALL", info=None):
+ self.write("(set-logic %s)" % logic)
+ if info is not None:
+ self.write("(set-info :source |%s|)" % info)
+ self.write("(set-info :smt-lib-version 2.5)")
+ self.write("(set-info :category \"industrial\")")
+
+ def timestamp(self):
+ secs = int(time() - self.start_time)
+ return "## %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
+
+ def write(self, stmt):
+ stmt = stmt.strip()
+ if self.debug_print:
+ print("> %s" % stmt)
+ if self.debug_file:
+ print(stmt, file=self.debug_file)
+ self.debug_file.flush()
+ self.p.stdin.write(bytes(stmt + "\n", "ascii"))
+ self.p.stdin.flush()
+
+ def read(self):
+ stmt = []
+ count_brackets = 0
+
+ while True:
+ line = self.p.stdout.readline().decode("ascii").strip()
+ count_brackets += line.count("(")
+ count_brackets -= line.count(")")
+ stmt.append(line)
+ if self.debug_print:
+ print("< %s" % line)
+ if count_brackets == 0:
+ break
+ if not self.p.poll():
+ print("SMT Solver terminated unexpectedly: %s" % "".join(stmt))
+ sys.exit(1)
+
+ stmt = "".join(stmt)
+ if stmt.startswith("(error"):
+ print("SMT Solver Error: %s" % stmt, file=sys.stderr)
+ sys.exit(1)
+
+ return stmt
+
+ def check_sat(self):
+ if self.debug_print:
+ print("> (check-sat)")
+ if self.debug_file:
+ print("; running check-sat..", file=self.debug_file)
+ self.debug_file.flush()
+
+ self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
+ self.p.stdin.flush()
+
+ if self.timeinfo:
+ i = 0
+ s = "/-\|"
+
+ count = 0
+ num_bs = 0
+ while select([self.p.stdout], [], [], 0.1) == ([], [], []):
+ count += 1
+
+ if count < 25:
+ continue
+
+ if count % 10 == 0 or count == 25:
+ secs = count // 10
+
+ if secs < 60:
+ m = "(%d seconds)" % secs
+ elif secs < 60*60:
+ m = "(%d seconds -- %d:%02d)" % (secs, secs // 60, secs % 60)
+ else:
+ m = "(%d seconds -- %d:%02d:%02d)" % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
+
+ print("%s %s %c" % ("\b \b" * num_bs, m, s[i]), end="", file=sys.stderr)
+ num_bs = len(m) + 3
+
+ else:
+ print("\b" + s[i], end="", file=sys.stderr)
+
+ sys.stderr.flush()
+ i = (i + 1) % len(s)
+
+ if num_bs != 0:
+ print("\b \b" * num_bs, end="", file=sys.stderr)
+ sys.stderr.flush()
+
+ result = self.read()
+ if self.debug_file:
+ print("(set-info :status %s)" % result, file=self.debug_file)
+ print("(check-sat)", file=self.debug_file)
+ self.debug_file.flush()
+ return result
+
+ def parse(self, stmt):
+ def worker(stmt):
+ if stmt[0] == '(':
+ expr = []
+ cursor = 1
+ while stmt[cursor] != ')':
+ el, le = worker(stmt[cursor:])
+ expr.append(el)
+ cursor += le
+ return expr, cursor+1
+
+ if stmt[0] == '|':
+ expr = "|"
+ cursor = 1
+ while stmt[cursor] != '|':
+ expr += stmt[cursor]
+ cursor += 1
+ expr += "|"
+ return expr, cursor+1
+
+ if stmt[0] in [" ", "\t", "\r", "\n"]:
+ el, le = worker(stmt[1:])
+ return el, le+1
+
+ expr = ""
+ cursor = 0
+ while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]:
+ expr += stmt[cursor]
+ cursor += 1
+ return expr, cursor
+ return worker(stmt)[0]
+
+ def bv2hex(self, v):
+ h = ""
+ v = bv2bin(v)
+ while len(v) > 0:
+ d = 0
+ if len(v) > 0 and v[-1] == "1": d += 1
+ if len(v) > 1 and v[-2] == "1": d += 2
+ if len(v) > 2 and v[-3] == "1": d += 4
+ if len(v) > 3 and v[-4] == "1": d += 8
+ h = hex(d)[2:] + h
+ if len(v) < 4: break
+ v = v[:-4]
+ return h
+
+ def bv2bin(self, v):
+ if v == "true": return "1"
+ if v == "false": return "0"
+ if v.startswith("#b"):
+ return v[2:]
+ if v.startswith("#x"):
+ digits = []
+ for d in v[2:]:
+ if d == "0": digits.append("0000")
+ if d == "1": digits.append("0001")
+ if d == "2": digits.append("0010")
+ if d == "3": digits.append("0011")
+ if d == "4": digits.append("0100")
+ if d == "5": digits.append("0101")
+ if d == "6": digits.append("0110")
+ if d == "7": digits.append("0111")
+ if d == "8": digits.append("1000")
+ if d == "9": digits.append("1001")
+ if d in ("a", "A"): digits.append("1010")
+ if d in ("b", "B"): digits.append("1011")
+ if d in ("c", "C"): digits.append("1100")
+ if d in ("d", "D"): digits.append("1101")
+ if d in ("e", "E"): digits.append("1110")
+ if d in ("f", "F"): digits.append("1111")
+ return "".join(digits)
+ assert False
+
+ def get(self, expr):
+ self.write("(get-value (%s))" % (expr))
+ return self.parse(self.read())[0][1]
+
+ def get_net(self, mod_name, net_name, state_name):
+ return self.get("(|%s_n %s| %s)" % (mod_name, net_name, state_name))
+
+ def get_net_bool(self, mod_name, net_name, state_name):
+ v = self.get_net(mod_name, net_name, state_name)
+ assert v in ["true", "false"]
+ return 1 if v == "true" else 0
+
+ def get_net_hex(self, mod_name, net_name, state_name):
+ return self.bv2hex(self.get_net(mod_name, net_name, state_name))
+
+ def get_net_bin(self, mod_name, net_name, state_name):
+ return self.bv2bin(self.get_net(mod_name, net_name, state_name))
+
+ def wait(self):
+ self.p.wait()
+
+
+class smtopts:
+ def __init__(self):
+ self.optstr = "s:d:vp"
+ self.solver = "z3"
+ self.debug_print = False
+ self.debug_file = None
+ self.timeinfo = True
+
+ def handle(self, o, a):
+ if o == "-s":
+ self.solver = a
+ elif o == "-v":
+ self.debug_print = True
+ elif o == "-p":
+ self.timeinfo = True
+ elif o == "-d":
+ self.debug_file = open(a, "w")
+ else:
+ return False
+ return True
+
+ def helpmsg(self):
+ return """
+ -s <solver>
+ set SMT solver: z3, cvc4, yices, mathsat
+ default: z3
+
+ -v
+ enable debug output
+
+ -p
+ disable timer display during solving
+
+ -d <filename>
+ write smt2 statements to file
+"""
+
+
+class mkvcd:
+ def __init__(self, f):
+ self.f = f
+ self.t = -1
+ self.nets = dict()
+
+ def add_net(self, name, width):
+ assert self.t == -1
+ key = "n%d" % len(self.nets)
+ self.nets[name] = (key, width)
+
+ def set_net(self, name, bits):
+ assert name in self.nets
+ assert self.t >= 0
+ print("b%s %s" % (bits, self.nets[name][0]), file=self.f)
+
+ def set_time(self, t):
+ assert t >= self.t
+ if t != self.t:
+ if self.t == -1:
+ print("$var event 1 ! smt_clock $end", file=self.f)
+ for name in sorted(self.nets):
+ key, width = self.nets[name]
+ print("$var wire %d %s %s $end" % (width, key, name), file=self.f)
+ print("$enddefinitions $end", file=self.f)
+ self.t = t
+ assert self.t >= 0
+ print("#%d" % self.t, file=self.f)
+ print("1!", file=self.f)
+
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-25 14:14:42 +0000