path: root/backends
diff options
authorClifford Wolf <>2015-08-09 13:35:44 +0200
committerClifford Wolf <>2015-08-09 13:35:44 +0200
commit883e09d8edcdd5152294cde530faf4c9e4ff19e0 (patch)
tree4a22febb30dd46185c5fe6ebcb9a4c0ce035dd47 /backends
parent3565e89a8b05a01b3035fc2081bad27c946f13e5 (diff)
Use MEMID as name for $mem cell
Diffstat (limited to 'backends')
1 files changed, 6 insertions, 1 deletions
diff --git a/backends/smt2/ b/backends/smt2/
index 4f3b2319..d828d658 100644
--- a/backends/smt2/
+++ b/backends/smt2/
@@ -440,6 +440,9 @@ 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("(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));
@@ -659,7 +662,9 @@ struct Smt2Backend : public Backend {
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.\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(" -tpl <template_file>\n");
log(" use the given template file. the line containing only the token '%%%%'\n");