pycaliper.per package

Submodules

pycaliper.per.expr module

PyCaliper

Author: Adwait Godbole, UC Berkeley

File: per/expr.py

Expression base class, and Expr operator classes

This module provides the base class for expression abstract syntax trees (AST) with overloaded operators. Supports operations like addition, subtraction, logical operations, etc.

For licensing information, please refer to the LICENSE file.

class pycaliper.per.expr.Add

Bases: Op

Represents the addition operation.

class pycaliper.per.expr.ArithmeticShiftLeft

Bases: Op

Represents the arithmetic shift left operation.

class pycaliper.per.expr.ArithmeticShiftRight

Bases: Op

Represents the arithmetic shift right operation.

class pycaliper.per.expr.BinaryAnd

Bases: Op

Represents the binary AND operation.

class pycaliper.per.expr.BinaryNor

Bases: Op

Represents the binary NOR operation.

class pycaliper.per.expr.BinaryOr

Bases: Op

Represents the binary OR operation.

class pycaliper.per.expr.BinaryXnor

Bases: Op

Represents the binary XNOR operation.

class pycaliper.per.expr.BinaryXor

Bases: Op

Represents the binary XOR operation.

class pycaliper.per.expr.CaseEquality

Bases: Op

Represents the case equality operation.

class pycaliper.per.expr.CaseInequality

Bases: Op

Represents the case inequality operation.

class pycaliper.per.expr.Concat

Bases: Op

Represents the concatenation operation.

class pycaliper.per.expr.Const(val, width=-1)

Bases: Expr

A constant value with an optional width.

Parameters:

val (int) – The constant value.
width (int, optional) – The width of the constant. Defaults to -1.

get_sva(pref='a')

Return type:: str

class pycaliper.per.expr.Div

Bases: Op

Represents the division operation.

class pycaliper.per.expr.Equality

Bases: Op

Represents the equality operation.

class pycaliper.per.expr.Expr

Bases: object

Base class for expression abstract syntax trees (AST) with overloaded operators. Supports operations like addition, subtraction, logical operations, etc.

eand(other)

eneg()

eor(other)

get_sva(pref='a')

Return type:: str

class pycaliper.per.expr.Extract

Bases: Op

Represents the extract operation.

class pycaliper.per.expr.GreaterThan

Bases: Op

Represents the greater than operation.

class pycaliper.per.expr.GreaterThanEqual

Bases: Op

Represents the greater than or equal operation.

class pycaliper.per.expr.ITE

Bases: Op

Represents the if-then-else operation.

class pycaliper.per.expr.Inequality

Bases: Op

Represents the inequality operation.

class pycaliper.per.expr.LessThan

Bases: Op

Represents the less than operation.

class pycaliper.per.expr.LessThanEqual

Bases: Op

Represents the less than or equal operation.

class pycaliper.per.expr.LogicalAnd

Bases: Op

Represents the logical AND operation.

class pycaliper.per.expr.LogicalEquivalence

Bases: Op

Represents the logical equivalence operation.

class pycaliper.per.expr.LogicalImplication

Bases: Op

Represents the logical implication operation.

class pycaliper.per.expr.LogicalOr

Bases: Op

Represents the logical OR operation.

class pycaliper.per.expr.LogicalShiftLeft

Bases: Op

Represents the logical shift left operation.

class pycaliper.per.expr.LogicalShiftRight

Bases: Op

Represents the logical shift right operation.

class pycaliper.per.expr.Mod

Bases: Op

Represents the modulus operation.

class pycaliper.per.expr.Mul

Bases: Op

Represents the multiplication operation.

class pycaliper.per.expr.Op(opstring, fixity, reprstring)

Bases: object

Represents an operator with a string representation, fixity, and a representation string.

opstring

The operator string.

Type:: str

fixity

The fixity of the operator.

Type:: Fixity

reprstring

The string for creating a representation.

Type:: str

class Fixity(value)

Bases: Enum

Fixity of the operator; used during SVA compilation.

CONCAT = 3

EXTRACT = 2

INFIX = 0

ITE = 4

PREFIX = 1

class pycaliper.per.expr.OpApply(op, args)

Bases: Expr

Apply an operator to a list of arguments.

Parameters:

op (Op) – Operator
args (list) – List of arguments.

get_sva(pref='a')

Get the SVA representation of the operator application.

Return type:: str
Parameters:: pref (str, optional) – Prefix that signals are nested under. Defaults to ‘a’.
Raises:: ValueError – If the fixity of the operator is unknown.
Returns:: SVA representation of the operator application.
Return type:: str

class pycaliper.per.expr.Power

Bases: Op

Represents the power operation.

class pycaliper.per.expr.Sub

Bases: Op

Represents the subtraction operation.

class pycaliper.per.expr.UnaryBitwiseAnd

Bases: Op

Represents the unary bitwise AND operation.

class pycaliper.per.expr.UnaryBitwiseNand

Bases: Op

Represents the unary bitwise NAND operation.

class pycaliper.per.expr.UnaryBitwiseNor

Bases: Op

Represents the unary bitwise NOR operation.

class pycaliper.per.expr.UnaryBitwiseNot

Bases: Op

Represents the unary bitwise NOT operation.

class pycaliper.per.expr.UnaryBitwiseOr

Bases: Op

Represents the unary bitwise OR operation.

class pycaliper.per.expr.UnaryBitwiseXnor

Bases: Op

Represents the unary bitwise XNOR operation.

class pycaliper.per.expr.UnaryBitwiseXor

Bases: Op

Represents the unary bitwise XOR operation.

class pycaliper.per.expr.UnaryLogicalNot

Bases: Op

Represents the unary logical NOT operation.

class pycaliper.per.expr.UnaryMinus

Bases: Op

Represents the unary minus operation.

class pycaliper.per.expr.UnaryPlus

Bases: Op

Represents the unary plus operation.

class pycaliper.per.expr.WildcardEquality

Bases: Op

Represents the wildcard equality operation.

class pycaliper.per.expr.WildcardInequality

Bases: Op

Represents the wildcard inequality operation.

pycaliper.per.per module

PyCaliper

Author: Adwait Godbole, UC Berkeley

File: per/per.py

Internal representation classes for PyCaliper:

PER (Partial Equivalence Relations):

A partial equivalence relation defined through equality and: conditional equality assertions.

Logic:

Single bitvectors

Struct:

Support for SystemVerilog structs

SpecModule:

A module in the specification hierarchy, what else can it be?

This module provides internal representation classes for PyCaliper, including PER, Logic, Struct, and SpecModule.

For licensing information, please refer to the LICENSE file.

class pycaliper.per.per.AuxModule(portmapping, name='', tt=False, **kwargs)

Bases: SpecModule

get_instance_str(bindinstance)

Return type:: str

instantiate(root=Path(path=[], slicelow=-1, slicehigh=-1))

Instantiate the current SpecModule.

Return type:: None
Parameters:: path (Path, optional) – The path in the hierarchy to place this module at. Defaults to Path([]).
Returns:: return the instantiated module.
Return type:: SpecModule

is_leftcopy()

class pycaliper.per.per.AuxPort(width=1, name='', root=None): Bases: Logic

class pycaliper.per.per.AuxReg(width=1, name=''): Bases: Logic

class pycaliper.per.per.Clock(name=''): Bases: Logic

class pycaliper.per.per.CondEq(cond, logic)

Bases: PER

Conditional equality assertion

get_sva(cpy1='a', cpy2='b')

Get the SVA representation of the conditional equality assertion.

Return type:: str

class pycaliper.per.per.CondEqHole(cond, per, spec_ctx)

Bases: Hole

A synthesis hole for a conditional equality PER

class pycaliper.per.per.Context(value)

Bases: Enum

Context of specification declarations made within a module.

INPUT = 0

OUTPUT = 2

STATE = 1

UNROLL = 3

class pycaliper.per.per.CtrAlignHole(ctr, sigs): Bases: Hole

class pycaliper.per.per.Eq(logic)

Bases: PER

Relational equality assertion.

get_sva(cpy1='a', cpy2='b')

Return type:

str

Parameters:

cpy1 (str, optional) – Hierarchy prefix of left copy. Defaults to ‘a’.
cpy2 (str, optional) – Hierarchy prefix of right copy. Defaults to ‘b’.

Returns:

SVA representation of the equality assertion.

Return type:

str

class pycaliper.per.per.FSMHole(guardsigs, statesig): Bases: Hole

class pycaliper.per.per.Group(name='')

Bases: object

A hierarchical group; does not have any hierarchical position associated with itself.

get_repr(reprs)

instantiate(path)

class pycaliper.per.per.Hole

Bases: object

A synthesis hole

deactivate()

class pycaliper.per.per.Inv(expr)

Bases: Prop

Invariant class

get_sva(pref='a')

class pycaliper.per.per.Logic(width=1, name='', root=None)

Bases: Expr, TypedElem

Class for single bitvectors/signals

get_hier_path(sep='.')

get_hier_path_flatindex()

get_hier_path_nonindex()

get_sva(pref='a')

Return type:: str
Parameters:: pref (str, optional) – Top-level module prefix string. Defaults to ‘a’.
Returns:: SVA representation of the signal.
Return type:: str

instantiate(path, parent=None)

Instantiate the logic signal with a path and parent array

Return type:

Logic

Parameters:

path (Path) – Path object representing the hierarchical path
parent (LogicArray, optional) – Parent array. Defaults to None.

Returns:

return self

Return type:

Logic

is_arr_elem()

Check if this signal is an element of an array (inspects the path to see if last level is indexed).

Return type:: bool
Returns:: True if the signal is an array element.
Return type:: bool

class pycaliper.per.per.LogicArray(typ_const, size, base=0, name='', root=None)

Bases: TypedElem

An array of logic signals

get_hier_path(sep='.')

instantiate(path)

class pycaliper.per.per.PER

Bases: Prop

Partial Equivalence Relation (PER) base class

get_sva(cpy1, cpy2)

class pycaliper.per.per.PERHole(per, spec_ctx)

Bases: Hole

A synthesis hole for a PER

class pycaliper.per.per.Path(path, slicelow=-1, slicehigh=-1)

Bases: object

Path: representing a hierarchical path in the specification.

path

At each hierarchical level, string represents identifier and the list represents the indexing (if unindexed, then the index is an empty list []).

Type:: list[tuple[str, list]]

slicehigh

High index of the slice (default 0).

Type:: int

slicelow

Low index of the slice (default 0).

Type:: int

add_level(name)

Add a new level to the path. For example, a.b[0] -> a.b[0].c

Return type:: Path
Parameters:: name (str) – name of the new level
Returns:: new path with the level added.
Return type:: Path

add_level_index(i)

Add an index to the last level of the path. For example, a.b[0].c -> a.b[0].c[1]

Return type:: Path
Parameters:: i (int) – index to be added
Returns:: new path with the index added.
Return type:: Path

get_hier_path(sep='.')

Get the hierarchical path as a string

Return type:: str
Parameters:: sep (str, optional) – Separator in generated path string. Defaults to ‘.’.
Returns:: Path string.
Return type:: str

get_hier_path_flatindex()

Return type:: str

Get the hierarchical path string with all indices flattened. Uses ‘_’ as separator.: For example: a.b[0].c[1] -> a_b_0_c_1

Returns:: Path string.
Return type:: str

get_hier_path_nonindex()

Return type:: str

Get the hierarchical path string without last level index. Uses ‘_’ as separator.: For example: a.b[0].c[1] -> a_b_0_c

Returns:: Path string.
Return type:: str

path: list[tuple[str, list]]

slicehigh: int = -1

slicelow: int = -1

class pycaliper.per.per.Prop

Bases: object

Property class

get_sva(pref='a')

class pycaliper.per.per.SVFunc(name=''): Bases: object

class pycaliper.per.per.SVFuncApply(func, args)

Bases: Expr

Apply a SystemVerilog function to a list of arguments

get_sva(pref='a')

Get the SVA representation of the function application.

Return type:: str

class pycaliper.per.per.SimulationSchedule(name, depth)

Bases: object

step(step)

property steps

class pycaliper.per.per.SimulationStep: Bases: object

class pycaliper.per.per.SpecModule(name='', **kwargs)

Bases: object

SpecModule class for specifications related to a SV HW module

condeqhole(cond, exprs)

Creates a Conditional Eq (synthesis) hole.

Parameters:

cond (Expr) – the condition for the Eq.
exprs (list[Expr]) – the list of expressions to consider as candidates for filling this hole.

ctralignhole(ctr, sigs)

Creates a Control Alignment hole.

Parameters:

ctr (Logic) – the control signal that the branch conditions are based on.
sigs (list[Logic]) – the signals to learn lookup tables for.

eq(*elems)

Create an relational equality invariant

Return type:: None

eqhole(exprs)

Creates an Eq (synthesis) hole.

Parameters:: exprs (list[Expr]) – the list of expressions to consider as candidates for filling this hole.

fsmhole(guardsigs, statesig)

Creates an FSM hole.

Parameters:

guardsigs (list[Logic]) – the guard signals for the FSM.
statesig (Logic) – the state signal for the FSM.

full_repr()

get_clk()

Return type:: Clock

get_hier_path(sep='.'): Call inner get_hier_path method.

get_repr(reprs)

get_unroll_kind_depths()

incr(x)

input()

Return type:: None

instantiate(path=Path(path=[], slicelow=-1, slicehigh=-1))

Instantiate the current SpecModule.

Return type:: SpecModule
Parameters:: path (Path, optional) – The path in the hierarchy to place this module at. Defaults to Path([]).
Returns:: return the instantiated module.
Return type:: SpecModule

inv(expr)

Add single trace invariants to the current context.

Return type:: None
Parameters:: expr (Expr) – the invariant expression.

is_instantiated()

output()

Return type:: None

pprint()

prev(elem)

Get the previous value of a signal.

Return type:: Logic
Parameters:: elem (Logic) – the signal to get the previous value of.
Returns:: the previous value of the signal.
Return type:: Logic

pycassert(expr)

Add an assertion to the current context.

Return type:: None
Parameters:: expr (Expr) – the assertion expression.

pycassume(expr)

Add an assumption to the current context.

Return type:: None
Parameters:: expr (Expr) – the assumption expression.

sprint()

stable(x)

state()

Return type:: None

when(cond)

Conditional equality PER.

Return type:: Callable
Parameters:: cond (Expr) – the condition Expr to enforce nested PER under.
Returns:: a lambda that is applied to the nested PER.
Return type:: Callable

class pycaliper.per.per.Struct(name='', root=None, **kwargs)

Bases: TypedElem

Struct as seen in SV

eq(expr)

Return type:: None

get_repr(reprs)

get_sva(pref='a')

Return type:: str

instantiate(path)

pprint(): Pretty print the struct definition

sprint()

Pretty string for the struct definition

Return type:: str

state()

when(cond)

class pycaliper.per.per.TypedElem(root=None)

Bases: object

An element in the design hierarchy (Logic, LogicArray, Struct, …) with a type.

instantiate(path)

pycaliper.per.per.get_path_from_hierarchical_str(pathstr)

Get a path with a single level Args: name (str): name of the singleton path Returns: Path object

Return type:: Path

pycaliper.per.per.kinduct(b): Decorator to set the k-induction depth for a state invariant specification.

pycaliper.per.per.nonreserved_or_fresh(name)

pycaliper.per.per.unroll(b): Decorator to set the unroll depth for a function in a SpecModule.

pycaliper.per.per.when(cond)

Create a Conditional equality PER generator. This returns a lambda that returns a CondEq object.

Parameters:: cond (Expr) – the condition to apply the PER under

pycaliper.per package

Submodules

pycaliper.per.expr module

pycaliper.per.per module

Module contents