riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Add "write_btor -s" mode

This commit is contained in:
Clifford Wolf 2017-12-13 00:15:44 +01:00
parent 0881bbf2e7
commit 546de7fa4f
1 changed files with 50 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

56
backends/btor/btor.cc
View File

@ -33,6 +33,7 @@ struct BtorWorker
SigMap sigmap;
RTLIL::Module *module;
bool verbose;
bool single_bad;
int next_nid = 1;
int initstate_nid = -1;
@ -63,6 +64,7 @@ struct BtorWorker
pool<Cell*> cell_recursion_guard;
pool<string> output_symbols;
vector<int> bad_properties;
dict<SigBit, bool> initbits;
string indent;
@ -705,8 +707,8 @@ struct BtorWorker
return nid;
}
BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose) :
f(f), sigmap(module), module(module), verbose(verbose)
BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad) :
f(f), sigmap(module), module(module), verbose(verbose), single_bad(single_bad)
{
btorf_push("inputs");
@ -789,11 +791,16 @@ struct BtorWorker
int nid_en = get_sig_nid(cell->getPort("\\EN"));
int nid_not_a = next_nid++;
int nid_en_and_not_a = next_nid++;
int nid = next_nid++;
btorf("%d not %d %d\n", nid_not_a, sid, nid_a);
btorf("%d and %d %d %d\n", nid_en_and_not_a, sid, nid_en, nid_not_a);
btorf("%d bad %d\n", nid, nid_en_and_not_a);
if (single_bad) {
bad_properties.push_back(nid_en_and_not_a);
} else {
int nid = next_nid++;
btorf("%d bad %d\n", nid, nid_en_and_not_a);
}
btorf_pop(log_id(cell));
}
@ -817,6 +824,36 @@ struct BtorWorker
btorf_pop(stringf("next %s", log_id(it.second)));
}
}
while (!bad_properties.empty())
{
vector<int> todo;
bad_properties.swap(todo);
int sid = get_bv_sid(1);
int cursor = 0;
while (cursor+1 < GetSize(todo))
{
int nid_a = todo[cursor++];
int nid_b = todo[cursor++];
int nid = next_nid++;
bad_properties.push_back(nid);
btorf("%d or %d %d %d\n", nid, sid, nid_a, nid_b);
}
if (!bad_properties.empty()) {
if (cursor < GetSize(todo))
bad_properties.push_back(todo[cursor++]);
log_assert(cursor == GetSize(todo));
} else {
int nid = next_nid++;
log_assert(cursor == 0);
log_assert(GetSize(todo) == 1);
btorf("%d bad %d\n", nid, todo[cursor]);
}
}
}
};
@ -833,10 +870,13 @@ struct BtorBackend : public Backend {
log(" -v\n");
log(" Add comments and indentation to BTOR output file\n");
log("\n");
log(" -s\n");
log(" Output only a single bad property for all asserts\n");
log("\n");
}
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
{
bool verbose = false;
bool verbose = false, single_bad = false;
log_header(design, "Executing BTOR backend.\n");
@ -847,6 +887,10 @@ struct BtorBackend : public Backend {
verbose = true;
continue;
}
if (args[argidx] == "-s") {
single_bad = true;
continue;
}
break;
}
extra_args(f, filename, args, argidx);
@ -859,7 +903,7 @@ struct BtorBackend : public Backend {
*f << stringf("; BTOR description generated by %s for module %s.\n",
yosys_version_str, log_id(topmod));
BtorWorker(*f, topmod, verbose);
BtorWorker(*f, topmod, verbose, single_bad);
*f << stringf("; end of yosys output\n");
}