diff options
Diffstat (limited to 'backends/btor/btor.cc')
| -rw-r--r-- | backends/btor/btor.cc | 24 |
1 files changed, 16 insertions, 8 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 692452aad..d62cc4c3d 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -1,7 +1,7 @@ /* * yosys -- Yosys Open SYnthesis Suite * - * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> + * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com> * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above @@ -18,7 +18,7 @@ */ // [[CITE]] Btor2 , BtorMC and Boolector 3.0 -// Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere +// Aina Niemetz, Mathias Preiner, C. Wolf, Armin Biere // Computer Aided Verification - 30th International Conference, CAV 2018 // https://cs.stanford.edu/people/niemetz/publication/2018/niemetzpreinerwolfbiere-cav18/ @@ -708,7 +708,7 @@ struct BtorWorker goto okay; } - if (cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit))) + if (cell->is_mem_cell()) { Mem *mem = mem_cells[cell]; @@ -728,10 +728,11 @@ struct BtorWorker log_error("Memory %s.%s has mixed async/sync write ports.\n", log_id(module), log_id(mem->memid)); - for (auto &port : mem->rd_ports) + for (auto &port : mem->rd_ports) { if (port.clk_enable) - log_error("Memory %s.%s has sync read ports.\n", + log_error("Memory %s.%s has sync read ports. Please use memory_nordff to convert them first.\n", log_id(module), log_id(mem->memid)); + } int data_sid = get_bv_sid(mem->width); int bool_sid = get_bv_sid(1); @@ -864,7 +865,7 @@ struct BtorWorker log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_btor`.\n", log_id(cell->type), log_id(module), log_id(cell)); } - if (cell->type.in(ID($adff), ID($adffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF") { + if (cell->type.in(ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF" || cell->type.str().substr(0, 7) == "$_ALDFF") { log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_btor`.\n", log_id(cell->type), log_id(module), log_id(cell)); } @@ -1080,10 +1081,12 @@ struct BtorWorker memories = Mem::get_all_memories(module); dict<IdString, Mem*> mem_dict; - for (auto &mem : memories) + for (auto &mem : memories) { + mem.narrow(); mem_dict[mem.memid] = &mem; + } for (auto cell : module->cells()) - if (cell->type.in(ID($mem), ID($memwr), ID($memrd), ID($meminit))) + if (cell->is_mem_cell()) mem_cells[cell] = mem_dict[cell->parameters.at(ID::MEMID).decode_string()]; btorf_push("inputs"); @@ -1396,6 +1399,11 @@ struct BtorBackend : public Backend { log_header(design, "Executing BTOR backend.\n"); + log_push(); + Pass::call(design, "bmuxmap"); + Pass::call(design, "demuxmap"); + log_pop(); + size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { |