From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 4 Apr 2018 16:12:27 +0000 (+0200)
Subject: Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constants
X-Git-Tag: yosys-0.8~129
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4d6af2969ccaf5f235fffdc8f89bc5e91fff5962;p=yosys.git

Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constants

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---

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"):