diff options
| author | Clifford Wolf <clifford@clifford.at> | 2015-08-04 20:05:37 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2015-08-04 20:05:37 +0200 |
| commit | c7fd3fbb68351a09575eb66e5db8de06d6ab1984 (patch) | |
| tree | d4243a7c9abb10871f70e15d683170344a00677f /backends/smv | |
| parent | 31b555ae72c37c72a27f4ffb66d38bc89420a25b (diff) | |
| download | yosys-c7fd3fbb68351a09575eb66e5db8de06d6ab1984.tar.gz yosys-c7fd3fbb68351a09575eb66e5db8de06d6ab1984.tar.bz2 yosys-c7fd3fbb68351a09575eb66e5db8de06d6ab1984.zip | |
Added $assert support to SMV back-end
Diffstat (limited to 'backends/smv')
| -rw-r--r-- | backends/smv/smv.cc | 25 |
1 files changed, 21 insertions, 4 deletions
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc index f4e8ff724..03959a4f7 100644 --- a/backends/smv/smv.cc +++ b/backends/smv/smv.cc @@ -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()); + } } }; |