kdrag.contrib.yosys

Functions

call_yosys_functional(mod_name, verilog_filename)

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.
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
kdrag.contrib.yosys.call_yosys_functional(mod_name, verilog_filename)
kdrag.contrib.yosys.smt_metadata(filename)