Skip to content

Ltl

ltl

Implementation of the LTL dialect by CIRCT.

See external documentation.

LTL = Dialect('ltl', [AndOp], [Property, Sequence]) module-attribute

Property dataclass

Bases: ParametrizedAttribute, TypeAttribute

The ltl.property type represents a verifiable property built from linear temporal logic sequences and quantifiers, for example, "if you see sequence A, eventually you will see sequence B".

Source code in xdsl/dialects/ltl.py 
24
25
26
27
28
29
30
31
32
@irdl_attr_definition
class Property(ParametrizedAttribute, TypeAttribute):
    """
    The `ltl.property` type represents a verifiable property built from linear
    temporal logic sequences and quantifiers, for example,
    "if you see sequence A, eventually you will see sequence B".
    """

    name = "ltl.property"

name = 'ltl.property' class-attribute instance-attribute

Sequence dataclass

Bases: ParametrizedAttribute, TypeAttribute

The ltl.sequence type represents a sequence of linear temporal logic, for example, “A is true two cycles after B is true”.

Source code in xdsl/dialects/ltl.py 
35
36
37
38
39
40
41
42
@irdl_attr_definition
class Sequence(ParametrizedAttribute, TypeAttribute):
    """
    The ltl.sequence type represents a sequence of linear temporal logic, for example,
    “A is true two cycles after B is true”.
    """

    name = "ltl.sequence"

name = 'ltl.sequence' class-attribute instance-attribute

AndOp

Bases: IRDLOperation

A conjunction of booleans, sequences, or properties. If any of the inputs is of type !ltl.property or !ltl.sequence or 1-bit signless int, the result of the op is consistent with the input type.

Source code in xdsl/dialects/ltl.py 
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
@irdl_op_definition
class AndOp(IRDLOperation):
    """
    A conjunction of booleans, sequences, or properties. If any of the `inputs` is of type
    !ltl.property or !ltl.sequence or 1-bit signless int, the result of the op is consistent with the input type.
    """

    name = "ltl.and"

    T: ClassVar = VarConstraint("T", AnyOf([Sequence, Property, IntegerType(1)]))

    input = var_operand_def(T)

    result = result_def(T)

    def __init__(
        self,
        operand: SSAValue,
    ):
        super().__init__(operands=[operand])

name = 'ltl.and' class-attribute instance-attribute

T: ClassVar = VarConstraint('T', AnyOf([Sequence, Property, IntegerType(1)])) class-attribute instance-attribute

input = var_operand_def(T) class-attribute instance-attribute

result = result_def(T) class-attribute instance-attribute

__init__(operand: SSAValue)

Source code in xdsl/dialects/ltl.py 
60
61
62
63
64
def __init__(
    self,
    operand: SSAValue,
):
    super().__init__(operands=[operand])