mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 11:42:30 +00:00
Code Activity

Add $anyconst/$anyseq support to btor back-end

Browse source
This commit is contained in:
Clifford Wolf 2017-12-15 00:40:24 +01:00
parent 162c29bd6b
commit ad901671c5
1 changed files with 51 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

62
backends/btor/btor.cc
View file

@ -63,9 +63,9 @@ struct BtorWorker
vector<pair<int, Cell*>> ff_todo; vector<pair<int, Cell*>> ff_todo;
pool<Cell*> cell_recursion_guard; pool<Cell*> cell_recursion_guard;
pool<string> output_symbols;
vector<int> bad_properties; vector<int> bad_properties;
dict<SigBit, bool> initbits; dict<SigBit, bool> initbits;
pool<Wire*> statewires;
string indent; string indent;
void btorf(const char *fmt, ...) void btorf(const char *fmt, ...)
@ -483,20 +483,23 @@ struct BtorWorker
SigSpec sig_d = sigmap(cell->getPort("\\D")); SigSpec sig_d = sigmap(cell->getPort("\\D"));
SigSpec sig_q = sigmap(cell->getPort("\\Q")); SigSpec sig_q = sigmap(cell->getPort("\\Q"));
string symbol = log_signal(sig_q); IdString symbol;
if (symbol.find(' ') != string::npos)
symbol = log_id(cell);
if (symbol[0] == '\\') if (sig_q.is_wire()) {
symbol = symbol.substr(1); Wire *w = sig_q.as_wire();
if (w->port_id == 0) {
statewires.insert(w);
symbol = w->name;
}
}
int sid = get_bv_sid(GetSize(sig_q)); int sid = get_bv_sid(GetSize(sig_q));
int nid = next_nid++; int nid = next_nid++;
if (output_symbols.count(symbol)) if (symbol.empty())
btorf("%d state %d\n", nid, sid); btorf("%d state %d\n", nid, sid);
else else
btorf("%d state %d %s\n", nid, sid, symbol.c_str()); btorf("%d state %d %s\n", nid, sid, log_id(symbol));
Const initval; Const initval;
for (int i = 0; i < GetSize(sig_q); i++) for (int i = 0; i < GetSize(sig_q); i++)
@ -508,6 +511,7 @@ struct BtorWorker
if (!initval.is_fully_undef()) { if (!initval.is_fully_undef()) {
int nid_init_val = get_sig_nid(initval); int nid_init_val = get_sig_nid(initval);
int nid_init = next_nid++; int nid_init = next_nid++;
if (verbose)
btorf("; initval = %s\n", log_signal(initval)); btorf("; initval = %s\n", log_signal(initval));
btorf("%d init %d %d %d\n", nid_init, sid, nid, nid_init_val); btorf("%d init %d %d %d\n", nid_init, sid, nid, nid_init_val);
} }
@ -517,6 +521,24 @@ struct BtorWorker
goto okay; goto okay;
} }
if (cell->type.in("$anyconst", "$anyseq"))
{
SigSpec sig_y = sigmap(cell->getPort("\\Y"));
int sid = get_bv_sid(GetSize(sig_y));
int nid = next_nid++;
btorf("%d state %d\n", nid, sid);
if (cell->type == "$anyconst") {
int nid2 = next_nid++;
btorf("%d next %d %d %d\n", nid2, sid, nid, nid);
}
add_nid_sig(nid, sig_y);
goto okay;
}
if (cell->type == "$initstate") if (cell->type == "$initstate")
{ {
SigSpec sig_y = sigmap(cell->getPort("\\Y")); SigSpec sig_y = sigmap(cell->getPort("\\Y"));
@ -744,10 +766,6 @@ struct BtorWorker
bit_cell[bit] = cell; bit_cell[bit] = cell;
} }
for (auto wire : module->wires())
if (wire->port_output)
output_symbols.insert(log_id(wire));
for (auto wire : module->wires()) for (auto wire : module->wires())
{ {
if (!wire->port_id || !wire->port_output) if (!wire->port_id || !wire->port_output)
@ -806,6 +824,26 @@ struct BtorWorker
} }
} }
for (auto wire : module->wires())
{
if (wire->port_id || wire->name[0] == '$')
continue;
btorf_push(stringf("wire %s", log_id(wire)));
int sid = get_bv_sid(GetSize(wire));
int nid = get_sig_nid(sigmap(wire));
if (statewires.count(wire))
continue;
int this_nid = next_nid++;
btorf("%d uext %d %d %d %s\n", this_nid, sid, nid, 0, log_id(wire));
btorf_pop(stringf("wire %s", log_id(wire)));
continue;
}
while (!ff_todo.empty()) while (!ff_todo.empty())
{ {
vector<pair<int, Cell*>> todo; vector<pair<int, Cell*>> todo;