diff --git a/backends/smt2/svi2smt.py b/backends/smt2/svi2smt.py
new file mode 100644
index 000000000..186186f0f
--- /dev/null
+++ b/backends/smt2/svi2smt.py
@@ -0,0 +1,316 @@
+#
+# yosys -- Yosys Open SYnthesis Suite
+#
+# Copyright (C) 2012  Claire Xenia Wolf <claire@yosyshq.com>
+#
+# Permission to use, copy, modify, and/or distribute this software for any
+# purpose with or without fee is hereby granted, provided that the above
+# copyright notice and this permission notice appear in all copies.
+#
+# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+#
+
+from collections import namedtuple
+
+Op = namedtuple("Op", ["op", "args", "tail"], defaults=[list, ""])
+
+def pp(v, indent=""):
+    if isinstance(v, Op):
+        lit = True
+        if isinstance(v.args, list):
+            for a in v.args:
+                if isinstance(a, str): continue
+                if isinstance(a, int): continue
+                lit = False
+        if lit:
+            print(indent + v.op + " " + str(v.args))
+        else:
+            print(indent + v.op + ":")
+            pp(v.args, indent=indent+"  ")
+    elif isinstance(v, list):
+        for a in v:
+            pp(a, indent=indent)
+    elif isinstance(v, str):
+        print(indent + '"' + v + '"')
+    else:
+        print(indent + "=" + str(v))
+
+class SviParserError(Exception):
+    def __init__(self, text, expected):
+        self.text = text
+        self.expected = expected
+
+def parse_str(text, s):
+    text = text.lstrip()
+    if not text.startswith(s):
+        raise SviParserError(text, s)
+    return Op("str", [s], text[len(s):])
+
+def parse_binop(text, ops, arg_parser, assoc="L"):
+    text = text.lstrip()
+    args = [arg_parser(text)]
+    opers = []
+
+    while True:
+        for op, cmd in ops:
+            try:
+                q = parse_str(args[-1].tail, op)
+                q = arg2_parser(q.tail)
+                args.append(q)
+                opers.append(cmd)
+            except SviParserError:
+                pass
+        else:
+            break
+
+    if len(opers) == 1:
+        args, opers = [Op(opers[0], args, args[-1].tail)], []
+    elif assoc == "L":
+        while len(opers) > 1:
+            args = [Op(opers[0], args[0:2], args[1].tail), *args[2:]]
+            opers = opers[1:]
+    elif assoc == "R":
+        while len(opers) > 1:
+            args = [Op(opers[-1], args[-2:], args[-1].tail), *args[0:-2]]
+            opers = opers[:-1]
+    else:
+        assert False
+
+    return args[0]
+
+def parse_int(text, label, base, digits):
+    text = text.lstrip()
+    tail = text.lstrip(digits)
+
+    if len(text) == len(tail) or text.startswith("_"):
+        raise SviParserError(text, label)
+
+    text = text[:-len(tail)].replace("_", "")
+    return Op("int", int(text, base), tail)
+
+def parse_dec(text):
+    return parse_int(text, "dec", 10, "0123456789_")
+
+def parse_hex(text):
+    return parse_int(text, "hex", 16, "0123456789abcdefABCDEF_")
+
+def parse_bin(text):
+    return parse_int(text, "bin", 2, "01_")
+
+def parse_name(text):
+    text = text.lstrip()
+
+    tail = text
+    if len(tail) and tail[0].isalpha():
+        tail = tail[1:]
+        while len(tail) and tail[0].isalnum():
+            tail = tail[1:]
+
+    if len(text) == len(tail):
+        raise SviParserError(text, "name")
+
+    return Op("name", text[:-len(tail)], tail)
+
+# const: dec
+# const: dec 'h hex
+# const: dec 'b bin
+def parse_const(text):
+    p = parse_dec(text)
+
+    try:
+        q = parse_str(p.tail, "'h")
+        q = parse_hex(q.tail)
+        return Op("const", [p.args, q.args], q.tail)
+    except SviParserError:
+        pass
+
+    try:
+        q = parse_str(p.tail, "'b")
+        q = parse_bin(q.tail)
+        return Op("const", [p.args, q.args], q.tail)
+    except SviParserError:
+        pass
+
+    return Op("const", [32, p.args], p.tail)
+
+# signal: name
+# signal: name [ idx ]
+# signal: name [ msb : lsb ]
+# signal: name [ lsb +: width ]
+def parse_signal(text):
+    p = parse_name(text)
+
+    try:
+        q = parse_str(p.tail, "[")
+        q = parse_dec(q.tail)
+
+        try:
+            r = parse_str(q.tail, ":")
+            r = parse_dec(r.tail)
+            s = parse_str(r.tail, "]")
+            return Op("signal", [p.args, r.args, q.args-r.args+1], s.tail)
+        except SviParserError:
+            pass
+
+        try:
+            r = parse_str(q.tail, "+:")
+            r = parse_dec(r.tail)
+            s = parse_str(r.tail, "]")
+            return Op("signal", [p.args, q.args, r.args], s.tail)
+        except SviParserError:
+            pass
+
+        r = parse_str(q.tail, "]")
+        return Op("signal", [p.args, q.args], r.tail)
+    except SviParserError:
+        pass
+
+    return Op("signal", [p.args], p.tail)
+
+# lvl0:
+#   "!" lvl0
+#   "~" lvl0
+#   const
+#   signal
+#   "(" expr ")"
+def parse_lvl0(text):
+    try:
+        p = parse_str(text, "!")
+        p = parse_atom(p.tail)
+        return Op("not", [p], p.tail)
+    except SviParserError:
+        pass
+
+    try:
+        return parse_const(text)
+    except SviParserError:
+        pass
+
+    try:
+        return parse_signal(text)
+    except SviParserError:
+        pass
+
+    p = parse_str(text, "(")
+    p = parse_expr(p.tail)
+    q = parse_str(p.tail, ")")
+    return p._replace(tail=q.tail)
+
+# lvl1:
+#   lvl0
+#   lvl1 + lvl0
+#   lvl1 - lvl0
+def parse_lvl1(text):
+    return parse_binop(text, [("+", "add"), ("-", "sub")], parse_lvl0)
+
+# lvl2:
+#   lvl2 "<<" lvl1
+#   lvl2 ">>" lvl1
+def parse_lvl2(text):
+    return parse_binop(text, [("<<", "shl"), (">>", "shr")], parse_lvl1)
+
+# lvl3:
+#   lvl3 ("<"|">"|"<="|">="|"=="|"!=") lvl2
+def parse_lvl3(text):
+    return parse_binop(text, [
+        ("<", "lt"),
+        (">", "gt"),
+        ("<=", "le"),
+        (">=", "ge"),
+        ("==", "eq"),
+        ("!=", "ne")
+    ], parse_lvl2)
+
+# lvl4:
+#   lvl3 op lvl3
+def parse_lvl4(text):
+    return parse_binop(text, [("&", "or")], parse_lvl3)
+
+# lvl5:
+#   lvl4 op lvl4
+def parse_lvl4(text):
+    return parse_binop(text, [("&", "or")], parse_lvl3)
+
+# lvlN:
+#   lvlN op lvlK
+def parse_lvlN(text):
+    return parse_binop(text, [("|", "or")], parse_lvlK)
+
+# term: sum
+# term: sum ^ term
+def parse_term(text):
+    return parse_binop(text, [("^", "xor")], parse_sum, parse_term)
+
+# expr: term
+# expr: term < term
+# expr: term > term
+# expr: term <= term
+# expr: term >= term
+# expr: term == term
+# expr: term != term
+def parse_expr(text):
+    return parse_binop(text, [
+        ("<", "lt"),
+        (">", "gt"),
+        ("<=", "le"),
+        (">=", "ge"),
+        ("==", "eq"),
+        ("!=", "ne")
+    ], parse_term)
+
+# conj: expr
+# conj: expr "and" conj
+def parse_conj(text):
+    return parse_binop(text, [("and", "conj")], parse_expr, parse_conj)
+
+# prop:
+#   expr "|->" conj ";"
+#   expr ";"
+def parse_prop(text):
+    p = parse_binop(text, [("|->", "impl")], parse_expr, parse_conj)
+    q = parse_str(p.tail, ";")
+    return p._replace(tail=q.tail)
+
+if __name__ == '__main__':
+    if False:
+        import fileinput
+        with fileinput.input() as f:
+            svi_text = "".join(f).rstrip()
+    else:
+        svi_text = """
+1 & S[1] |-> S[3:2] and 8'h a_B | S[2+:2] | 1 ^ 3 'b 101 == S;
+
+a
+  |-> b
+  and (c & d) == e;
+
+x |-> c > d;
+        """.strip()
+
+    print("--- Input ---")
+    print(svi_text)
+    print("-------------")
+
+    props = []
+    try:
+        while len(svi_text):
+            props.append(parse_prop(svi_text))
+            svi_text = props[-1].tail
+    except SviParserError as e:
+        print(e)
+
+    if len(props) == 1:
+        props = props[0]
+    else:
+        props = Op("conj", props, svi_text)
+
+    print()
+    print("--- Property ---")
+    pp(props)
+    print("----------------")