diff options
| author | Clifford Wolf <clifford@clifford.at> | 2018-04-04 18:12:27 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2018-04-04 18:12:27 +0200 |
| commit | 4d6af2969ccaf5f235fffdc8f89bc5e91fff5962 (patch) | |
| tree | 74dc70b920347dbb8f149f74a0141027987ebb96 | |
| parent | 25a864fc7344756e1b2de7bcc3f446ab84e410a3 (diff) | |
| download | yosys-4d6af2969ccaf5f235fffdc8f89bc5e91fff5962.tar.gz yosys-4d6af2969ccaf5f235fffdc8f89bc5e91fff5962.tar.bz2 yosys-4d6af2969ccaf5f235fffdc8f89bc5e91fff5962.zip | |
Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constants
Signed-off-by: Clifford Wolf <clifford@clifford.at>
| -rw-r--r-- | backends/smt2/smtio.py | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index bf72e8916..1a8d2484c 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -737,6 +737,9 @@ class SmtIo: return h def bv2bin(self, v): + if type(v) is list and len(v) == 3 and v[0] == "_" and v[1].startswith("bv"): + x, n = int(v[1][2:]), int(v[2]) + return "".join("1" if (x & (1 << i)) else "0" for i in range(n-1, -1, -1)) if v == "true": return "1" if v == "false": return "0" if v.startswith("#b"): |