mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-16 12:30:35 +00:00
Code Activity

Merge pull request #4320 from YosysHQ/ywb_asserts

Browse source 
write_btor: Include `$assert` and `$assume` cells in -ywmap output
This commit is contained in:
Jannis Harder 2025-10-13 15:30:11 +02:00 • committed by GitHub
commit 84b5ec856e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 19 additions and 0 deletions
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; vector<ywmap_btor_sig> ywmap_states;
dict<SigBit, int> ywmap_clock_bits; dict<SigBit, int> ywmap_clock_bits;
dict<SigBit, int> ywmap_clock_inputs; dict<SigBit, int> ywmap_clock_inputs;
vector<Cell *> ywmap_asserts;
vector<Cell *> ywmap_assumes;
PrettyJson ywmap_json; PrettyJson ywmap_json;
@ -1280,6 +1282,8 @@ struct BtorWorker
btorf("%d or %d %d %d\n", nid_a_or_not_en, sid, nid_a, nid_not_en); 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); 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)); btorf_pop(log_id(cell));
} }
@ -1304,6 +1308,8 @@ struct BtorWorker
} else { } else {
int nid = next_nid++; int nid = next_nid++;
btorf("%d bad %d%s\n", nid, nid_en_and_not_a, getinfo(cell, true)); btorf("%d bad %d%s\n", nid, nid_en_and_not_a, getinfo(cell, true));
if (ywmap_json.active()) ywmap_asserts.emplace_back(cell);
} }
} }
@ -1461,6 +1467,7 @@ struct BtorWorker
log_assert(cursor == 0); log_assert(cursor == 0);
log_assert(GetSize(todo) == 1); log_assert(GetSize(todo) == 1);
btorf("%d bad %d\n", nid, todo[cursor]); btorf("%d bad %d\n", nid, todo[cursor]);
// What do we do with ywmap_asserts when using single_bad?
} }
} }
@ -1526,6 +1533,18 @@ struct BtorWorker
emit_ywmap_btor_sig(entry); emit_ywmap_btor_sig(entry);
ywmap_json.end_array(); 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(); ywmap_json.end_object();
} }
} }