int sid = get_bv_sid(GetSize(sig_y));
int nid = next_nid++;
- btorf("%d state %d\n", nid, sid);
+ btorf("%d state %d%s\n", nid, sid, getinfo(cell).c_str());
if (cell->type == ID($anyconst)) {
int nid2 = next_nid++;
int one_nid = get_sig_nid(State::S1);
int zero_nid = get_sig_nid(State::S0);
initstate_nid = next_nid++;
- btorf("%d state %d\n", initstate_nid, sid);
+ btorf("%d state %d%s\n", initstate_nid, sid, getinfo(cell).c_str());
btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid);
}
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));
}
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++)
{