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