kdrag.contrib.yosys

Functions

call_yosys_functional(mod_name, verilog_filename)

read_yosys_relational(filepath)

smt_metadata(filename)

Classes

SmtModInfo(inputs, outputs, registers, ...)

VerilogModule(input_sort, output_sort, ...)

Data defining a functional model of a verilog module as a (input, state) -> (output, state) function.

VerilogModuleRel(name, state_sort, trans, ...)

A relational model of a verilog module using yosys write_smt2 backend
class kdrag.contrib.yosys.SmtModInfo(inputs: set = <factory>, outputs: set = <factory>, registers: set = <factory>, memories: dict = <factory>, wires: set = <factory>, wsize: dict = <factory>, clocks: dict = <factory>, cells: dict = <factory>, asserts: dict = <factory>, assumes: dict = <factory>, covers: dict = <factory>, maximize: set = <factory>, minimize: set = <factory>, anyconsts: dict = <factory>, anyseqs: dict = <factory>, allconsts: dict = <factory>, allseqs: dict = <factory>, asize: dict = <factory>, witness: list = <factory>)

Bases: object

Parameters:

  • inputs (set)

  • outputs (set)

  • registers (set)

  • memories (dict)

  • wires (set)

  • wsize (dict)

  • clocks (dict)

  • cells (dict)

  • asserts (dict)

  • assumes (dict)

  • covers (dict)

  • maximize (set)

  • minimize (set)

  • anyconsts (dict)

  • anyseqs (dict)

  • allconsts (dict)

  • allseqs (dict)

  • asize (dict)

  • witness (list)

allconsts: dict
allseqs: dict
anyconsts: dict
anyseqs: dict
asize: dict
asserts: dict
assumes: dict
cells: dict
clocks: dict
covers: dict
inputs: set
maximize: set
memories: dict
minimize: set
outputs: set
registers: set
wires: set
witness: list
wsize: dict
class kdrag.contrib.yosys.VerilogModule(input_sort: SortRef, output_sort: SortRef, state_sort: SortRef, init_constrs: list[ExprRef], trans_fun: FuncDeclRef)

Bases: object

Data defining a functional model of a verilog module as a (input, state) -> (output, state) function. The fields of the inputs are <module_name>_Inputs_<wire_name> The output of the transition function is a pair`trans_fun(inputs,state).first` is the output Struct and trans_fun(inputs,state).second is the state Struct The fields of the outputs are <module_name>_Outputs_<wire_name>

Parameters:

  • input_sort (SortRef)

  • output_sort (SortRef)

  • state_sort (SortRef)

  • init_constrs (list[ExprRef])

  • trans_fun (FuncDeclRef)

classmethod from_file(mod_name, verilog_filename)
init_constrs: list[ExprRef]
input_sort: SortRef
output_sort: SortRef
state_sort: SortRef
trans_fun: FuncDeclRef
class kdrag.contrib.yosys.VerilogModuleRel(name: str, state_sort: SortRef, trans: FuncDeclRef, init: FuncDeclRef, init_unconstr: FuncDeclRef, asserts: FuncDeclRef, assumes: FuncDeclRef, wires: dict[str, FuncDeclRef])

Bases: object

A relational model of a verilog module using yosys write_smt2 backend

Parameters:

  • name (str)

  • state_sort (SortRef)

  • trans (FuncDeclRef)

  • init (FuncDeclRef)

  • init_unconstr (FuncDeclRef)

  • asserts (FuncDeclRef)

  • assumes (FuncDeclRef)

  • wires (dict[str, FuncDeclRef])

asserts: FuncDeclRef
assumes: FuncDeclRef
classmethod from_file(name: str, wire_names: list[str], filepath: str)
Parameters:

  • name (str)

  • wire_names (list[str])

  • filepath (str)

init: FuncDeclRef
init_unconstr: FuncDeclRef
name: str
state_sort: SortRef
trans: FuncDeclRef
wires: dict[str, FuncDeclRef]
kdrag.contrib.yosys.call_yosys_functional(mod_name, verilog_filename)
kdrag.contrib.yosys.read_yosys_relational(filepath: str) → str
Parameters:

filepath (str)

Return type:

str

kdrag.contrib.yosys.smt_metadata(filename)