mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-11 03:33:36 +00:00
Code Activity

Merge 884f40df11 into 63b3ce0c77

Browse source
This commit is contained in:
KrystalDelusion 2025-04-04 04:08:16 +13:00 committed by GitHub
parent 63b3ce0c77 884f40df11
commit d657f6878a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 19 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
backends/btor/btor.cc
View file

@ -98,6 +98,8 @@ struct BtorWorker
vector<ywmap_btor_sig> ywmap_states;
dict<SigBit, int> ywmap_clock_bits;
dict<SigBit, int> ywmap_clock_inputs;
vector<Cell *> ywmap_asserts;
vector<Cell *> ywmap_assumes;
PrettyJson ywmap_json;
@ -1282,6 +1284,8 @@ struct BtorWorker
btorf("%d or %d %d %d\n", nid_a_or_not_en, sid, nid_a, nid_not_en);
btorf("%d constraint %d\n", nid, nid_a_or_not_en);
if (ywmap_json.active()) ywmap_assumes.emplace_back(cell);
btorf_pop(log_id(cell));
}
@ -1306,6 +1310,8 @@ struct BtorWorker
} else {
int nid = next_nid++;
btorf("%d bad %d%s\n", nid, nid_en_and_not_a, getinfo(cell, true).c_str());
if (ywmap_json.active()) ywmap_asserts.emplace_back(cell);
}
}
@ -1463,6 +1469,7 @@ struct BtorWorker
log_assert(cursor == 0);
log_assert(GetSize(todo) == 1);
btorf("%d bad %d\n", nid, todo[cursor]);
// What do we do with ywmap_asserts when using single_bad?
}
}
@ -1528,6 +1535,18 @@ struct BtorWorker
emit_ywmap_btor_sig(entry);
ywmap_json.end_array();
ywmap_json.name("asserts");
ywmap_json.begin_array();
for (Cell *cell : ywmap_asserts)
ywmap_json.value(witness_path(cell));
ywmap_json.end_array();
ywmap_json.name("assumes");
ywmap_json.begin_array();
for (Cell *cell : ywmap_assumes)
ywmap_json.value(witness_path(cell));
ywmap_json.end_array();
ywmap_json.end_object();
}
}