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

Added $assert support to SMV back-end

Browse source
This commit is contained in:
Clifford Wolf 2015-08-04 20:05:37 +02:00
parent 31b555ae72
commit c7fd3fbb68
1 changed files with 21 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

25
backends/smv/smv.cc
View file

@ -42,7 +42,7 @@ struct SmvWorker
pool<Wire*> partial_assignment_wires;
dict<SigBit, std::pair<const char*, int>> partial_assignment_bits;
vector<string> assignments;
vector<string> assignments, invarspecs;
const char *cid()
{
@ -227,6 +227,16 @@ struct SmvWorker
{
// FIXME: $slice, $concat, $mem
if (cell->type.in("$assert"))
{
SigSpec sig_a = cell->getPort("\\A");
SigSpec sig_en = cell->getPort("\\EN");
invarspecs.push_back(stringf("!bool(%s) | bool(%s);", rvalue(sig_en), rvalue(sig_a)));
continue;
}
if (cell->type.in("$shl", "$shr", "$sshl", "$sshr", "$shift", "$shiftx"))
{
SigSpec sig_a = cell->getPort("\\A");
@ -634,9 +644,16 @@ struct SmvWorker
assignments.push_back(stringf("%s := %s;", cid(wire->name), expr.c_str()));
}
f << stringf(" ASSIGN\n");
for (const string &line : assignments)
f << stringf(" %s\n", line.c_str());
if (!assignments.empty()) {
f << stringf(" ASSIGN\n");
for (const string &line : assignments)
f << stringf(" %s\n", line.c_str());
}
if (!invarspecs.empty()) {
for (const string &line : invarspecs)
f << stringf(" INVARSPEC %s\n", line.c_str());
}
}
};