kdrag.printers.verilog

Functions

to_verilog(modname, ins, outs)	Produces a pure combinatorial module in Verilog.
verilog_decl(v)
verilog_of_expr(expr)	Convert an SMT-LIB expression to a Verilog expression.

kdrag.printers.verilog.to_verilog(modname: str, ins: list[ExprRef], outs: dict[ExprRef, ExprRef]) → str

Produces a pure combinatorial module in Verilog.

>>> x,y,z = smt.Consts("x y z", smt.BitVecSort(8))
>>> a,b,c = smt.Consts("a b c", smt.BoolSort())
>>> print(to_verilog("foo", [x, y], {a: smt.ULE(x + y, 17), z: x & y}))
// Generated by knuckledragger
module foo (
   input [7:0] x,
   input [7:0] y,
   output a,
   output [7:0] z
);
assign a = ((x + y) <= 8'd17);
assign z = (x & y);
endmodule

Parameters:

• modname (str)

• ins (list[ExprRef])

• outs (dict[ExprRef, ExprRef])

Return type:

str

kdrag.printers.verilog.verilog_decl(v: ExprRef) → str

Parameters:

v (ExprRef)

Return type:

str

kdrag.printers.verilog.verilog_of_expr(expr: ExprRef) → str

Convert an SMT-LIB expression to a Verilog expression.

>>> x,y,z = smt.Consts("x y z", smt.BitVecSort(8))
>>> a,b,c = smt.Consts("a b c", smt.BoolSort())
>>> verilog_of_expr(x + y + z)
'((x + y) + z)'
>>> verilog_of_expr(smt.Concat(x, y, z))
'{{x, y}, z}'
>>> verilog_of_expr(a & True)
"(a && 1'b1)"

Parameters:

expr (ExprRef)

Return type:

str

import kdrag.smt as smt

binops = {
    "bvand": "&",
    "bvor": "|",
    "bvxor": "^",
    "bvule": "<=",
    "bvult": "<",
    "bvuge": ">=",
    "bvugt": ">",
    "bvadd": "+",
    "bvsub": "-",
    # "bvudiv" : " / ", # TODO: think about this one
    "bvmul": "*",
    "=": "==",
    "distinct": "!=",
    "bvshl": "<<",
    "bvlshr": ">>",
    "bvashr": ">>>",
}


def verilog_of_expr(expr: smt.ExprRef) -> str:
    """
    Convert an SMT-LIB expression to a Verilog expression.

    >>> x,y,z = smt.Consts("x y z", smt.BitVecSort(8))
    >>> a,b,c = smt.Consts("a b c", smt.BoolSort())
    >>> verilog_of_expr(x + y + z)
    '((x + y) + z)'
    >>> verilog_of_expr(smt.Concat(x, y, z))
    '{{x, y}, z}'
    >>> verilog_of_expr(a & True)
    "(a && 1'b1)"
    """
    if isinstance(expr, smt.BitVecNumRef):
        return str(expr.size()) + "'d" + str(expr.as_long())
    elif smt.is_true(expr):
        return "1'b1"
    elif smt.is_false(expr):
        return "1'b0"
    elif smt.is_const(expr):
        return expr.decl().name()
    elif smt.is_app(expr):
        children = [verilog_of_expr(c) for c in expr.children()]
        name = expr.decl().name()
        if smt.is_select(expr):
            return f"{children[0]}[{children[1]}]"
        elif name == "ite":
            return f"({children[0]} ? {children[1]} : {children[2]})"
        elif name == "and":
            return "(" + " && ".join(children) + ")"
        elif name == "or":
            return "(" + " || ".join(children) + ")"
        elif name == "not":
            return f"(!{children[0]})"
        elif name in binops:
            assert len(children) == 2
            return f"({children[0]} {binops[name]} {children[1]})"
        elif name == "bvnot":
            assert len(children) == 1
            return f"(~{children[0]})"
        elif name == "concat":
            return f"{{{', '.join(children)}}}"
        else:
            raise Exception(f"Unknown expression: {expr}")
    else:
        raise Exception(f"Unknown expression: {expr}")


def verilog_decl(v: smt.ExprRef) -> str:
    assert smt.is_const(v)
    sort = v.sort()
    if sort == smt.BoolSort():
        return f"{v.decl().name()}"
    elif isinstance(v, smt.BitVecRef):
        return f"[{v.size() - 1}:0] {v.decl().name()}"
    else:
        raise Exception(f"Unknown sort: {sort}")


def to_verilog(
    modname: str, ins: list[smt.ExprRef], outs: dict[smt.ExprRef, smt.ExprRef]
) -> str:
    """
    Produces a pure combinatorial module in Verilog.

    >>> x,y,z = smt.Consts("x y z", smt.BitVecSort(8))
    >>> a,b,c = smt.Consts("a b c", smt.BoolSort())
    >>> print(to_verilog("foo", [x, y], {a: smt.ULE(x + y, 17), z: x & y}))
    // Generated by knuckledragger
    module foo (
       input [7:0] x,
       input [7:0] y,
       output a,
       output [7:0] z
    );
    assign a = ((x + y) <= 8'd17);
    assign z = (x & y);
    endmodule

    """
    assert len(set(ins)) == len(ins)
    assert all([v not in outs for v in ins])
    for k, v in outs.items():
        if k.sort() != v.sort():
            raise Exception(f"Output {k} and value {v} have different sorts")
    outdecls = ["output " + verilog_decl(out) for out in outs.keys()]
    indecls = ["input " + verilog_decl(in_) for in_ in ins]
    decls = ",\n   ".join(indecls + outdecls)
    assigns = "\n".join(
        [
            f"assign {out.decl().name()} = {verilog_of_expr(value)};"
            for out, value in outs.items()
        ]
    )
    return f"""\
// Generated by knuckledragger
module {modname} (
   {decls}
);
{assigns}
endmodule
"""