mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 13:29:12 +00:00
Code Activity

write_aiger: Include $assert and $assume cells in -ywmap output

Browse source
This commit is contained in:
Jannis Harder 2024-02-07 18:39:32 +01:00
parent 639a8d83e4
commit 6469d90293
1 changed files with 17 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

17
backends/aiger/aiger.cc
View file

@ -67,6 +67,8 @@ struct AigerWriter
int initstate_ff = 0; int initstate_ff = 0;
dict<SigBit, int> ywmap_clocks; dict<SigBit, int> ywmap_clocks;
vector<Cell *> ywmap_asserts;
vector<Cell *> ywmap_assumes;
int mkgate(int a0, int a1) int mkgate(int a0, int a1)
{ {
@ -269,6 +271,7 @@ struct AigerWriter
unused_bits.erase(A); unused_bits.erase(A);
unused_bits.erase(EN); unused_bits.erase(EN);
asserts.push_back(make_pair(A, EN)); asserts.push_back(make_pair(A, EN));
ywmap_asserts.push_back(cell);
continue; continue;
} }
@ -279,6 +282,7 @@ struct AigerWriter
unused_bits.erase(A); unused_bits.erase(A);
unused_bits.erase(EN); unused_bits.erase(EN);
assumes.push_back(make_pair(A, EN)); assumes.push_back(make_pair(A, EN));
ywmap_assumes.push_back(cell);
continue; continue;
} }
@ -852,6 +856,19 @@ struct AigerWriter
for (auto &it : init_lines) for (auto &it : init_lines)
json.value(it.second); json.value(it.second);
json.end_array(); json.end_array();
json.name("asserts");
json.begin_array();
for (Cell *cell : ywmap_asserts)
json.value(witness_path(cell));
json.end_array();
json.name("assumes");
json.begin_array();
for (Cell *cell : ywmap_assumes)
json.value(witness_path(cell));
json.end_array();
json.end_object(); json.end_object();
} }