diff options
author | Marcelina KoĆcielnicka <mwk@0x04.net> | 2020-10-18 03:09:45 +0200 |
---|---|---|
committer | Marcelina KoĆcielnicka <mwk@0x04.net> | 2020-10-21 17:51:20 +0200 |
commit | f272c8b407b656aedaa48a362f1e844278be3b16 (patch) | |
tree | c0c0f83f45a260d2f38a066d3035ae61eaf47d26 /backends/smt2/smt2.cc | |
parent | ec483b7c3bdd852be1cd22cbaad758c47fa61ae7 (diff) | |
download | yosys-f272c8b407b656aedaa48a362f1e844278be3b16.tar.gz yosys-f272c8b407b656aedaa48a362f1e844278be3b16.tar.bz2 yosys-f272c8b407b656aedaa48a362f1e844278be3b16.zip |
smt2: Use Mem helper.
Diffstat (limited to 'backends/smt2/smt2.cc')
-rw-r--r-- | backends/smt2/smt2.cc | 430 |
1 files changed, 244 insertions, 186 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 0b4e20ac6..a185fdd74 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -22,6 +22,7 @@ #include "kernel/sigtools.h" #include "kernel/celltypes.h" #include "kernel/log.h" +#include "kernel/mem.h" #include <string> USING_YOSYS_NAMESPACE @@ -40,12 +41,15 @@ struct Smt2Worker std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver; std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue; pool<Cell*> recursive_cells, registers; + std::vector<Mem> memories; + dict<Cell*, Mem*> mem_cells; + std::set<Mem*> memory_queue; pool<SigBit> clock_posedge, clock_negedge; vector<string> ex_state_eq, ex_input_eq; std::map<RTLIL::SigBit, std::pair<int, int>> fcache; - std::map<Cell*, int> memarrays; + std::map<Mem*, int> memarrays; std::map<int, int> bvsizes; dict<IdString, char*> ids; @@ -116,12 +120,73 @@ struct Smt2Worker makebits(stringf("%s_is", get_id(module))); + dict<IdString, Mem*> mem_dict; + memories = Mem::get_all_memories(module); + for (auto &mem : memories) + { + mem_dict[mem.memid] = &mem; + for (auto &port : mem.wr_ports) + { + if (port.clk_enable) { + SigSpec clk = sigmap(port.clk); + for (int i = 0; i < GetSize(clk); i++) + { + if (clk[i].wire == nullptr) + continue; + if (port.clk_polarity) + clock_posedge.insert(clk[i]); + else + clock_negedge.insert(clk[i]); + } + } + for (auto bit : sigmap(port.en)) + noclock.insert(bit); + for (auto bit : sigmap(port.addr)) + noclock.insert(bit); + for (auto bit : sigmap(port.data)) + noclock.insert(bit); + } + for (auto &port : mem.rd_ports) + { + if (port.clk_enable) { + SigSpec clk = sigmap(port.clk); + for (int i = 0; i < GetSize(clk); i++) + { + if (clk[i].wire == nullptr) + continue; + if (port.clk_polarity) + clock_posedge.insert(clk[i]); + else + clock_negedge.insert(clk[i]); + } + } + for (auto bit : sigmap(port.en)) + noclock.insert(bit); + for (auto bit : sigmap(port.addr)) + noclock.insert(bit); + for (auto bit : sigmap(port.data)) + noclock.insert(bit); + Cell *driver = port.cell ? port.cell : mem.cell; + for (auto bit : sigmap(port.data)) { + if (bit_driver.count(bit)) + log_error("Found multiple drivers for %s.\n", log_signal(bit)); + bit_driver[bit] = driver; + } + } + } + for (auto cell : module->cells()) for (auto &conn : cell->connections()) { if (GetSize(conn.second) == 0) continue; + // Handled above. + if (cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit))) { + mem_cells[cell] = mem_dict[cell->parameters.at(ID::MEMID).decode_string()]; + continue; + } + bool is_input = ct.cell_input(cell->type, conn.first); bool is_output = ct.cell_output(cell->type, conn.first); @@ -135,24 +200,6 @@ struct Smt2Worker log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n", log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type)); - if (cell->type.in(ID($mem)) && conn.first.in(ID::RD_CLK, ID::WR_CLK)) - { - SigSpec clk = sigmap(conn.second); - for (int i = 0; i < GetSize(clk); i++) - { - if (clk[i].wire == nullptr) - continue; - - if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_ENABLE : ID::WR_CLK_ENABLE)[i] != State::S1) - continue; - - if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_POLARITY : ID::WR_CLK_POLARITY)[i] == State::S1) - clock_posedge.insert(clk[i]); - else - clock_negedge.insert(clk[i]); - } - } - else if (cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)) && conn.first.in(ID::CLK, ID::C)) { bool posedge = (cell->type == ID($_DFF_N_)) || (cell->type == ID($dff) && cell->getParam(ID::CLK_POLARITY).as_bool()); @@ -647,27 +694,35 @@ struct Smt2Worker // FIXME: $slice $concat } - if (memmode && cell->type == ID($mem)) + if (memmode && cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit))) { + Mem *mem = mem_cells[cell]; + + if (memarrays.count(mem)) { + recursive_cells.erase(cell); + return; + } + int arrayid = idcounter++; - memarrays[cell] = arrayid; - - int abits = cell->getParam(ID::ABITS).as_int(); - int width = cell->getParam(ID::WIDTH).as_int(); - int rd_ports = cell->getParam(ID::RD_PORTS).as_int(); - int wr_ports = cell->getParam(ID::WR_PORTS).as_int(); - - bool async_read = false; - if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) { - if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero()) - log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module)); - async_read = true; + memarrays[mem] = arrayid; + + int abits = ceil_log2(mem->size); + + bool has_sync_wr = false; + bool has_async_wr = false; + for (auto &port : mem->wr_ports) { + if (port.clk_enable) + has_sync_wr = true; + else + has_async_wr = true; } + if (has_async_wr && has_sync_wr) + log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module)); - decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(cell), abits, width, rd_ports, wr_ports, async_read ? "async" : "sync")); + decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(mem->memid), abits, mem->width, GetSize(mem->rd_ports), GetSize(mem->wr_ports), has_async_wr ? "async" : "sync")); string memstate; - if (async_read) { + if (has_async_wr) { memstate = stringf("%s#%d#final", get_id(module), arrayid); } else { memstate = stringf("%s#%d#0", get_id(module), arrayid); @@ -675,80 +730,79 @@ struct Smt2Worker if (statebv) { - int mem_size = cell->getParam(ID::SIZE).as_int(); - int mem_offset = cell->getParam(ID::OFFSET).as_int(); - - makebits(memstate, width*mem_size, get_id(cell)); + makebits(memstate, mem->width*mem->size, get_id(mem->memid)); decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s| state))\n", - get_id(module), get_id(cell), get_id(module), width*mem_size, memstate.c_str())); + get_id(module), get_id(mem->memid), get_id(module), mem->width*mem->size, memstate.c_str())); - for (int i = 0; i < rd_ports; i++) + for (int i = 0; i < GetSize(mem->rd_ports); i++) { - SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits); - SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width); + auto &port = mem->rd_ports[i]; + SigSpec addr_sig = port.addr; + addr_sig.extend_u0(abits); std::string addr = get_bv(addr_sig); - if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool()) + if (port.clk_enable) 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(port.data), log_id(mem->memid), log_id(module)); 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(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); std::string read_expr = "#b"; - for (int k = 0; k < width; k++) + for (int k = 0; k < mem->width; k++) 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:R%dA %s| state) #b%s) ((_ extract %d %d) (|%s| state))\n %s)", - get_id(module), i, get_id(cell), Const(k+mem_offset, abits).as_string().c_str(), - width*(k+1)-1, width*k, memstate.c_str(), read_expr.c_str()); + get_id(module), i, get_id(mem->memid), Const(k+mem->start_offset, abits).as_string().c_str(), + mem->width*(k+1)-1, mem->width*k, memstate.c_str(), read_expr.c_str()); 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), mem->width, read_expr.c_str(), log_signal(port.data))); 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(mem->memid), get_id(module), mem->width, get_id(module), idcounter)); - register_bv(data_sig, idcounter++); + register_bv(port.data, idcounter++); } } else { if (statedt) dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", - memstate.c_str(), abits, width, get_id(cell))); + memstate.c_str(), abits, mem->width, get_id(mem->memid))); else decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", - memstate.c_str(), get_id(module), abits, width, get_id(cell))); + memstate.c_str(), get_id(module), abits, mem->width, get_id(mem->memid))); decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s| state))\n", - get_id(module), get_id(cell), get_id(module), abits, width, memstate.c_str())); + get_id(module), get_id(mem->memid), get_id(module), abits, mem->width, memstate.c_str())); - for (int i = 0; i < rd_ports; i++) + for (int i = 0; i < GetSize(mem->rd_ports); i++) { - SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits); - SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width); + auto &port = mem->rd_ports[i]; + SigSpec addr_sig = port.addr; + addr_sig.extend_u0(abits); std::string addr = get_bv(addr_sig); - if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool()) + if (port.clk_enable) 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(port.data), log_id(mem->memid), log_id(module)); 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(mem->memid), 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| state) (|%s_m:R%dA %s| state))) ; %s\n", - get_id(module), idcounter, get_id(module), width, memstate.c_str(), get_id(module), i, get_id(cell), log_signal(data_sig))); + get_id(module), idcounter, get_id(module), mem->width, memstate.c_str(), get_id(module), i, get_id(mem->memid), log_signal(port.data))); 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(mem->memid), get_id(module), mem->width, get_id(module), idcounter)); - register_bv(data_sig, idcounter++); + register_bv(port.data, idcounter++); } } - registers.insert(cell); + memory_queue.insert(mem); recursive_cells.erase(cell); return; } @@ -977,7 +1031,7 @@ struct Smt2Worker } } - for (int iter = 1; !registers.empty(); iter++) + for (int iter = 1; !registers.empty() || !memory_queue.empty(); iter++) { pool<Cell*> this_regs; this_regs.swap(registers); @@ -1010,152 +1064,156 @@ struct Smt2Worker if (cell->type == ID($anyconst)) ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Y)).c_str(), get_bv(cell->getPort(ID::Y), "other_state").c_str())); } + } - if (cell->type == ID($mem)) - { - int arrayid = memarrays.at(cell); + std::set<Mem*> this_mems; + this_mems.swap(memory_queue); + + for (auto mem : this_mems) + { + int arrayid = memarrays.at(mem); + + int abits = ceil_log2(mem->size);; - int abits = cell->getParam(ID::ABITS).as_int(); - int width = cell->getParam(ID::WIDTH).as_int(); - int wr_ports = cell->getParam(ID::WR_PORTS).as_int(); + bool has_sync_wr = false; + bool has_async_wr = false; + for (auto &port : mem->wr_ports) { + if (port.clk_enable) + has_sync_wr = true; + else + has_async_wr = true; + } - bool async_read = false; - string initial_memstate, final_memstate; + string initial_memstate, final_memstate; - if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) { - log_assert(cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero()); - async_read = true; - initial_memstate = stringf("%s#%d#0", get_id(module), arrayid); - final_memstate = stringf("%s#%d#final", get_id(module), arrayid); + if (has_async_wr) { + log_assert(!has_sync_wr); + initial_memstate = stringf("%s#%d#0", get_id(module), arrayid); + final_memstate = stringf("%s#%d#final", get_id(module), arrayid); + } + + if (statebv) + { + if (has_async_wr) { + makebits(final_memstate, mem->width*mem->size, get_id(mem->memid)); } - if (statebv) + for (int i = 0; i < GetSize(mem->wr_ports); i++) { - int mem_size = cell->getParam(ID::SIZE).as_int(); - int mem_offset = cell->getParam(ID::OFFSET).as_int(); - - if (async_read) { - makebits(final_memstate, width*mem_size, get_id(cell)); + auto &port = mem->wr_ports[i]; + SigSpec addr_sig = port.addr; + addr_sig.extend_u0(abits); + + std::string addr = get_bv(addr_sig); + std::string data = get_bv(port.data); + std::string mask = get_bv(port.en); + + decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); + addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(mem->memid)); + + decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, data.c_str(), log_signal(port.data))); + data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(mem->memid)); + + decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, mask.c_str(), log_signal(port.en))); + mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid)); + + std::string data_expr; + + for (int k = mem->size-1; k >= 0; k--) { + std::string new_data = stringf("(bvor (bvand %s %s) (bvand ((_ extract %d %d) (|%s#%d#%d| state)) (bvnot %s)))", + data.c_str(), mask.c_str(), mem->width*(k+1)-1, mem->width*k, get_id(module), arrayid, i, mask.c_str()); + data_expr += stringf("\n (ite (= %s #b%s) %s ((_ extract %d %d) (|%s#%d#%d| state)))", + addr.c_str(), Const(k+mem->start_offset, abits).as_string().c_str(), new_data.c_str(), + mem->width*(k+1)-1, mem->width*k, get_id(module), arrayid, i); } - for (int i = 0; i < wr_ports; i++) - { - SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits); - SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width); - SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width); + decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (_ BitVec %d) (concat%s)) ; %s\n", + get_id(module), arrayid, i+1, get_id(module), mem->width*mem->size, data_expr.c_str(), get_id(mem->memid))); + } + } + else + { + if (has_async_wr) { + if (statedt) + dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", + initial_memstate.c_str(), abits, mem->width, get_id(mem->memid))); + else + decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", + initial_memstate.c_str(), get_id(module), abits, mem->width, get_id(mem->memid))); + } - std::string addr = get_bv(addr_sig); - std::string data = get_bv(data_sig); - std::string mask = get_bv(mask_sig); + for (int i = 0; i < GetSize(mem->wr_ports); i++) + { + auto &port = mem->wr_ports[i]; + SigSpec addr_sig = port.addr; + addr_sig.extend_u0(abits); - decls.push_back(stringf("(define-fun |%s_m:W%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))); - addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell)); + std::string addr = get_bv(addr_sig); + std::string data = get_bv(port.data); + std::string mask = get_bv(port.en); - decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig))); - data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell)); + decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); + addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(mem->memid)); - decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig))); - mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell)); + decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, data.c_str(), log_signal(port.data))); + data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(mem->memid)); - std::string data_expr; + decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, mask.c_str(), log_signal(port.en))); + mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid)); - for (int k = mem_size-1; k >= 0; k--) { - std::string new_data = stringf("(bvor (bvand %s %s) (bvand ((_ extract %d %d) (|%s#%d#%d| state)) (bvnot %s)))", - data.c_str(), mask.c_str(), width*(k+1)-1, width*k, get_id(module), arrayid, i, mask.c_str()); - data_expr += stringf("\n (ite (= %s #b%s) %s ((_ extract %d %d) (|%s#%d#%d| state)))", - addr.c_str(), Const(k+mem_offset, abits).as_string().c_str(), new_data.c_str(), - width*(k+1)-1, width*k, get_id(module), arrayid, i); - } + 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()); - decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (_ BitVec %d) (concat%s)) ; %s\n", - get_id(module), arrayid, i+1, get_id(module), width*mem_size, data_expr.c_str(), get_id(cell))); - } + 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", + get_id(module), arrayid, i+1, get_id(module), abits, mem->width, + get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid))); } - else - { - if (async_read) { - if (statedt) - dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", - initial_memstate.c_str(), abits, width, get_id(cell))); - else - decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", - initial_memstate.c_str(), get_id(module), abits, width, get_id(cell))); - } - - for (int i = 0; i < wr_ports; i++) - { - SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits); - SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width); - SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width); + } - std::string addr = get_bv(addr_sig); - std::string data = get_bv(data_sig); - std::string mask = get_bv(mask_sig); + std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, GetSize(mem->wr_ports)); + std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid); + trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(mem->memid))); + ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid)); - decls.push_back(stringf("(define-fun |%s_m:W%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))); - addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell)); + if (has_async_wr) + hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(mem->memid))); - decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig))); - data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell)); + Const init_data = mem->get_init_data(); - decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig))); - mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell)); + for (int i = 0; i < mem->size; i++) + { + if (i*mem->width >= GetSize(init_data)) + break; - 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()); + Const initword = init_data.extract(i*mem->width, mem->width, State::Sx); + Const initmask = initword; + bool gen_init_constr = false; - 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", - get_id(module), arrayid, i+1, get_id(module), abits, width, - get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(cell))); + for (int k = 0; k < GetSize(initword); k++) { + if (initword[k] == State::S0 || initword[k] == State::S1) { + gen_init_constr = true; + initmask[k] = State::S1; + } else { + initmask[k] = State::S0; + initword[k] = State::S0; } } - std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, wr_ports); - std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid); - trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell))); - ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid)); - - if (async_read) - hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(cell))); - - Const init_data = cell->getParam(ID::INIT); - int memsize = cell->getParam(ID::SIZE).as_int(); - - for (int i = 0; i < memsize; i++) + if (gen_init_constr) { - if (i*width >= GetSize(init_data)) - break; - - Const initword = init_data.extract(i*width, width, State::Sx); - Const initmask = initword; - bool gen_init_constr = false; - - for (int k = 0; k < GetSize(initword); k++) { - if (initword[k] == State::S0 || initword[k] == State::S1) { - gen_init_constr = true; - initmask[k] = State::S1; - } else { - initmask[k] = State::S0; - initword[k] = State::S0; - } - } - - if (gen_init_constr) - { - if (statebv) - /* FIXME */; - else - init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]", - get_id(module), arrayid, Const(i, abits).as_string().c_str(), - initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i)); - } + if (statebv) + /* FIXME */; + else + init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]", + get_id(module), arrayid, Const(i, abits).as_string().c_str(), + initmask.as_string().c_str(), initword.as_string().c_str(), get_id(mem->memid), i)); } } } @@ -1586,7 +1644,7 @@ struct Smt2Backend : public Backend { for (auto module : sorted_modules) { - if (module->get_blackbox_attribute() || module->has_memories_warn() || module->has_processes_warn()) + if (module->get_blackbox_attribute() || module->has_processes_warn()) continue; log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module)); |