Helpers¶

SCR requirements¶

mk_scr ¶

mk_scr(ctx, name, inputs, past_inputs, modes, past_mode)

Makes an SCR requirement

Pseudo-boolean constraints¶

pseudoboolean ¶

Routines for pseudo-boolean functions

mk_at_least_one ¶

mk_at_least_one(ctx, nets)

Computes "at least one net is true"

Args: ctx: the context to use nets: the nets to use

mk_at_most_one ¶

mk_at_most_one(ctx, nets)

Computes "at most one net is true"

Args: ctx: the context to use nets: the nets to use

mk_exactly_one ¶

mk_exactly_one(ctx, nets, name)

Computes the pseudo-boolean constraint "exactly one is true". Uses the "commander variable" encoding described in "Efficient CNF Encoding for Selecting 1 from N Objects" by Will Klieber and Gihwon Kwon.

Args: ctx: the context to use nets: the list of (Boolean) nets

Returns: a net expressing the constraint "exactly one is true"

Plotting¶

plots ¶

Implementation of plotting services for traces

plot_trace_dataframe ¶

plot_trace_dataframe(input_dataframe, only_key=None, height=5)

Draws one step plot per each signal in the trace.

Args: dataframe (DataFrame): the dataframe of the trace

plot_trace_dictionary ¶

plot_trace_dictionary(net_dict)

Draws one step plot per each signal in the trace.

Args: net_dict (Dictionary): the dictionary of the trace