mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-07 09:55:20 +00:00
Code Activity

Improve (and fix for stbv mode) SMT2 memory API

Browse source
This commit is contained in:
Clifford Wolf 2017-02-26 10:58:34 +01:00
parent 38bf458037
commit fd1cc0c73d
3 changed files with 51 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

49
backends/smt2/smt2.cc
View file

@ -560,7 +560,7 @@ struct Smt2Worker
log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! " 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)); "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_m:%d %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
std::string read_expr = "#b"; std::string read_expr = "#b";
@ -568,14 +568,14 @@ struct Smt2Worker
read_expr += "0"; read_expr += "0";
for (int k = 0; k < mem_size; k++) for (int k = 0; k < mem_size; k++)
read_expr = stringf("(ite (= (|%s_m:%d %s| state) #b%s) ((_ extract %d %d) (|%s#%d#0| state))\n %s)", read_expr = stringf("(ite (= (|%s_m:R%dA %s| state) #b%s) ((_ extract %d %d) (|%s#%d#0| state))\n %s)",
get_id(module), i, get_id(cell), Const(k+mem_offset, abits).as_string().c_str(), get_id(module), i, get_id(cell), Const(k+mem_offset, abits).as_string().c_str(),
width*(k+1)-1, width*k, get_id(module), arrayid, read_expr.c_str()); width*(k+1)-1, width*k, get_id(module), arrayid, read_expr.c_str());
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d)\n %s) ; %s\n", decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d)\n %s) ; %s\n",
get_id(module), idcounter, get_id(module), width, read_expr.c_str(), log_signal(data_sig))); get_id(module), idcounter, get_id(module), width, read_expr.c_str(), log_signal(data_sig)));
decls.push_back(stringf("(define-fun |%s_m:%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n", decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n",
get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter)); get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter));
register_bv(data_sig, idcounter++); register_bv(data_sig, idcounter++);
@ -599,13 +599,13 @@ struct Smt2Worker
log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! " 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)); "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_m:%d %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s#%d#0| state) (|%s_m:%d %s| state))) ; %s\n", decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s#%d#0| state) (|%s_m:R%dA %s| state))) ; %s\n",
get_id(module), idcounter, get_id(module), width, get_id(module), arrayid, get_id(module), i, get_id(cell), log_signal(data_sig))); get_id(module), idcounter, get_id(module), width, get_id(module), arrayid, get_id(module), i, get_id(cell), log_signal(data_sig)));
decls.push_back(stringf("(define-fun |%s_m:%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n", decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n",
get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter)); get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter));
register_bv(data_sig, idcounter++); register_bv(data_sig, idcounter++);
@ -792,7 +792,6 @@ struct Smt2Worker
int abits = cell->getParam("\\ABITS").as_int(); int abits = cell->getParam("\\ABITS").as_int();
int width = cell->getParam("\\WIDTH").as_int(); int width = cell->getParam("\\WIDTH").as_int();
int rd_ports = cell->getParam("\\RD_PORTS").as_int();
int wr_ports = cell->getParam("\\WR_PORTS").as_int(); int wr_ports = cell->getParam("\\WR_PORTS").as_int();
if (statebv) if (statebv)
@ -810,17 +809,17 @@ struct Smt2Worker
std::string data = get_bv(data_sig); std::string data = get_bv(data_sig);
std::string mask = get_bv(mask_sig); std::string mask = get_bv(mask_sig);
decls.push_back(stringf("(define-fun |%s_m:%d %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
get_id(module), rd_ports+i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
addr = stringf("(|%s_m:%d %s| state)", get_id(module), rd_ports+i, get_id(cell)); addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell));
decls.push_back(stringf("(define-fun |%s_m:%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
get_id(module), rd_ports+i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig))); get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig)));
data = stringf("(|%s_m:%dD %s| state)", get_id(module), rd_ports+i, get_id(cell)); data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell));
decls.push_back(stringf("(define-fun |%s_m:%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
get_id(module), rd_ports+i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig))); get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig)));
mask = stringf("(|%s_m:%dM %s| state)", get_id(module), rd_ports+i, get_id(cell)); mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell));
std::string data_expr; std::string data_expr;
@ -848,17 +847,17 @@ struct Smt2Worker
std::string data = get_bv(data_sig); std::string data = get_bv(data_sig);
std::string mask = get_bv(mask_sig); std::string mask = get_bv(mask_sig);
decls.push_back(stringf("(define-fun |%s_m:%d %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
get_id(module), rd_ports+i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
addr = stringf("(|%s_m:%d %s| state)", get_id(module), rd_ports+i, get_id(cell)); addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell));
decls.push_back(stringf("(define-fun |%s_m:%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
get_id(module), rd_ports+i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig))); get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig)));
data = stringf("(|%s_m:%dD %s| state)", get_id(module), rd_ports+i, get_id(cell)); data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell));
decls.push_back(stringf("(define-fun |%s_m:%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
get_id(module), rd_ports+i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig))); get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig)));
mask = stringf("(|%s_m:%dM %s| state)", get_id(module), rd_ports+i, get_id(cell)); mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell));
data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))", data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str()); data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str());

43
backends/smt2/smtbmc.py
View file

@ -614,24 +614,26 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
mems = sorted(smt.hiermems(topmod)) mems = sorted(smt.hiermems(topmod))
for mempath in mems: for mempath in mems:
abits, width, rports, wports = smt.mem_info(topmod, mempath) abits, width, rports, wports = smt.mem_info(topmod, mempath)
mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath)
addr_expr_list = list() addr_expr_list = list()
data_expr_list = list()
for i in range(steps_start, steps_stop): for i in range(steps_start, steps_stop):
for j in range(rports): for j in range(rports):
addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, j)) addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j))
data_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j))
addr_list = set() addr_list = smt.get_list(addr_expr_list)
for val in smt.get_list(addr_expr_list): data_list = smt.get_list(data_expr_list)
addr_list.add(smt.bv2int(val))
expr_list = list() addr_data = dict()
for i in addr_list: for addr, data in zip(addr_list, data_list):
expr_list.append("(select %s #b%s)" % (mem, format(i, "0%db" % abits))) addr = smt.bv2bin(addr)
data = smt.bv2bin(data)
if addr not in addr_data:
addr_data[addr] = data
for i, val in zip(addr_list, smt.get_list(expr_list)): for addr, data in addr_data.items():
val = smt.bv2bin(val) print(" UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath), len(addr), addr, len(data), data), file=f)
print(" UUT.%s[%d] = %d'b%s;" % (".".join(mempath), i, len(val), val), file=f)
for i in range(steps_start, steps_stop): for i in range(steps_start, steps_stop):
pi_names = [[name] for name, _ in primary_inputs if name not in clock_inputs] pi_names = [[name] for name, _ in primary_inputs if name not in clock_inputs]
@ -675,21 +677,24 @@ def write_constr_trace(steps_start, steps_stop, index):
mems = sorted(smt.hiermems(topmod)) mems = sorted(smt.hiermems(topmod))
for mempath in mems: for mempath in mems:
abits, width, rports, wports = smt.mem_info(topmod, mempath) abits, width, rports, wports = smt.mem_info(topmod, mempath)
mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath)
addr_expr_list = list() addr_expr_list = list()
data_expr_list = list()
for i in range(steps_start, steps_stop): for i in range(steps_start, steps_stop):
for j in range(rports): for j in range(rports):
addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, j)) addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j))
data_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j))
addr_list = set((smt.bv2int(val) for val in smt.get_list(addr_expr_list))) addr_list = smt.get_list(addr_expr_list)
data_list = smt.get_list(data_expr_list)
expr_list = list() addr_data = dict()
for i in addr_list: for addr, data in zip(addr_list, data_list):
expr_list.append("(select %s #b%s)" % (mem, format(i, "0%db" % abits))) if addr not in addr_data:
addr_data[addr] = data
for i, val in zip(addr_list, smt.get_list(expr_list)): for addr, data in addr_data.items():
print("assume (= (select [%s] #b%s) %s)" % (".".join(mempath), format(i, "0%db" % abits), val), file=f) print("assume (= (select [%s] %s) %s)" % (".".join(mempath), addr, data), file=f)
for k in range(steps_start, steps_stop): for k in range(steps_start, steps_stop):
print("", file=f) print("", file=f)

6
backends/smt2/smtio.py
View file

@ -596,20 +596,20 @@ class SmtIo:
if mem_path[-1] not in self.modinfo[mod].memories: return False if mem_path[-1] not in self.modinfo[mod].memories: return False
return True return True
def mem_expr(self, mod, base, path, portidx=None, infomode=False): def mem_expr(self, mod, base, path, port=None, infomode=False):
if len(path) == 1: if len(path) == 1:
assert mod in self.modinfo assert mod in self.modinfo
assert path[0] in self.modinfo[mod].memories assert path[0] in self.modinfo[mod].memories
if infomode: if infomode:
return self.modinfo[mod].memories[path[0]] return self.modinfo[mod].memories[path[0]]
return "(|%s_m%s %s| %s)" % (mod, "" if portidx is None else ":%d" % portidx, path[0], base) return "(|%s_m%s %s| %s)" % (mod, "" if port is None else ":%s" % port, path[0], base)
assert mod in self.modinfo assert mod in self.modinfo
assert path[0] in self.modinfo[mod].cells assert path[0] in self.modinfo[mod].cells
nextmod = self.modinfo[mod].cells[path[0]] nextmod = self.modinfo[mod].cells[path[0]]
nextbase = "(|%s_h %s| %s)" % (mod, path[0], base) nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
return self.mem_expr(nextmod, nextbase, path[1:], portidx=portidx, infomode=infomode) return self.mem_expr(nextmod, nextbase, path[1:], port=port, infomode=infomode)
def mem_info(self, mod, path): def mem_info(self, mod, path):
return self.mem_expr(mod, "", path, infomode=True) return self.mem_expr(mod, "", path, infomode=True)