diff options
| author | Clifford Wolf <clifford@clifford.at> | 2016-08-21 15:56:22 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2016-08-21 15:56:22 +0200 |
| commit | 7a33b9892a7a542ca1ac0b503c4368a1721a9afb (patch) | |
| tree | 54b3bc699e12b6ce3295f11b9443d0fad1755fe6 /backends/smt2/smt2.cc | |
| parent | cdd0b85e47d6c1718ec5c0d2d80c87af3e3bbc83 (diff) | |
| download | yosys-7a33b9892a7a542ca1ac0b503c4368a1721a9afb.tar.gz yosys-7a33b9892a7a542ca1ac0b503c4368a1721a9afb.tar.bz2 yosys-7a33b9892a7a542ca1ac0b503c4368a1721a9afb.zip | |
yosys-smtbmc: improved --dump-vlogtb handling of memories
Diffstat (limited to 'backends/smt2/smt2.cc')
| -rw-r--r-- | backends/smt2/smt2.cc | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 9acbfbeb8..aaafc3f9a 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -460,19 +460,23 @@ struct Smt2Worker 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))); - decls.push_back(stringf("; yosys-smt2-memory %s %d %d\n", log_id(cell), abits, width)); + decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d\n", log_id(cell), abits, width, rd_ports)); 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 addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits); SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width); + std::string addr = get_bv(addr_sig); 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_m:%d %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + log_id(module), i, log_id(cell), log_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)) ; %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++); |