# 'ltl' Dialect

This dialect provides operations and types to model Linear Temporal Logic, sequences, and properties, which are useful for hardware verification.

## Rationale ¶

The main goal of the `ltl`

dialect is to capture the core formalism underpinning SystemVerilog Assertions (SVAs), the de facto standard for describing temporal logic sequences and properties in hardware verification. (See IEEE 1800-2017 section 16 “Assertions”.) We expressly try *not* to model this dialect like an AST for SVAs, but instead try to strip away all the syntactic sugar and Verilog quirks, and distill out the core foundation as an IR. Within the CIRCT project, this dialect intends to enable emission of rich temporal assertions as part of the Verilog output, but also provide a foundation for formal tools built ontop of CIRCT.

### Sequences and Properties ¶

The core building blocks for modeling temporal logic in the `ltl`

dialect are *sequences* and *properties*. In a nutshell, sequences behave like regular expressions over time, whereas properties provide the quantifiers to express that sequences must be true under certain conditions.

**Sequences** describe boolean expressions at different points in time. They can be easily verified by a finite state automaton, similar to how regular expressions and languages have an equivalent automaton that recognizes the language. For example:

- The boolean
`a`

is a sequence. It holds if`a`

is true in cycle 0 (the current cycle). - The boolean expression
`a & b`

is also a sequence. It holds if`a & b`

is true in cycle 0. `##1 a`

checks that`a`

is true in cycle 1 (the next cycle).`##[1:4] a`

checks that`a`

is true anywhere in cycle 1, 2, 3, or 4.`a ##1 b`

checks that`a`

holds in cycle 0 and`b`

holds in cycle 1.`##1 (a ##1 b)`

checks that`a`

holds in cycle 1 and`b`

holds in cycle 2.`(a ##1 b) ##5 (c ##1 d)`

checks that the sequence`(a ##1 b)`

holds and is followed by the sequence`(c ##1 d)`

5 or 6 cycles later. Concretely, this checks that`a`

holds in cycle 0,`b`

holds in cycle 1,`c`

holds in cycle 6 (5 cycles after the first sequence ended in cycle 1), and`d`

holds in cycle 7.

**Properties** describe concrete, testable propositions or claims built from sequences. While sequences can observe and match a certain behavior in a circuit at a specific point in time, properties allow you to express that these sequences hold in every cycle, or hold at some future point in time, or that one sequence is always followed by another. For example:

`always s`

checks that the sequence`s`

holds in every cycle. This is often referred to as the**G**(or “globally”) operator in LTL.`eventually s`

checks that the sequence`s`

will hold at some cycle now or in the future. This is often referred to as the**F**(or “finally”) operator in LTL.`p until q`

checks that the property`p`

holds in every cycle before the first cycle`q`

holds. This is often referred to as the**U**(or “until”) operator in LTL.`s implies t`

checks that whenever the sequence`s`

is observed, it is immediately followed by sequence`t`

.

Traditional definitions of the LTL formalism do not make a distinction between sequences and properties. Most of their operators fall into the property category, for example, quantifiers like *globally*, *finally*, *release*, and *until*. The set of sequence operators is usually very small, since it is not necessary for academic treatment, consisting only of the *next* operator. The `ltl`

dialect provides a richer set of operations to model sequences.

## Representing SVAs ¶

### Sequence Concatenation and Cycle Delay ¶

The primary building block for sequences in SVAs is the *concatenation* expression. Concatenation is always associated with a cycle delay, which indicates how many cycles pass between the end of the LHS sequence and the start of the RHS sequence. One, two, or more sequences can be concatenated at once, and the overall concatenation can have an initial cycle delay. For example:

```
a ##1 b ##1 c // 1 cycle delay between a, b, and c
##2 a ##1 b ##1 c // same, plus 2 cycles of initial delay before a
```

In the simplest form, a cycle delay can appear as a prefix of another sequence, e.g., `##1 a`

. This is essentially a concatenation with only one sequence, `a`

, and an initial cycle delay of the concatenation of `1`

. The prefix delays map to the LTL dialect as follows:

`##N seq`

.**Fixed delay.**Sequence`seq`

has to match exactly`N`

cycles in the future. Equivalent to`ltl.delay %seq, N, 0`

.`##[N:M] seq`

.**Bounded range delay.**Sequence`seq`

has to match anywhere between`N`

and`M`

cycles in the future, inclusive. Equivalent to`ltl.delay %seq, N, (M-N)`

`##[N:$] seq`

.**Unbounded range delay.**Sequence`seq`

has to match anywhere at or beyond`N`

cycles in the future, after a finite amount of cycles. Equivalent to`ltl.delay %seq, N`

.`##[*] seq`

. Shorthand for`##[0:$]`

. Equivalent to`ltl.delay %seq, 0`

.`##[+] seq`

. Shorthand for`##[1:$]`

. Equivalent to`ltl.delay %seq, 1`

.

Concatenation of two sequences always involves a cycle delay specification in between them, e.g., `a ##1 b`

where sequence `b`

starts in the cycle after `a`

ends. Zero-cycle delays can be specified, e.g., `a ##0 b`

where `b`

starts in the same cycle as `a`

ends. If `a`

and `b`

are booleans, `a ##0 b`

is equivalent to `a && b`

.

The dialect separates concatenation and cycle delay into two orthogonal operations, `ltl.concat`

and `ltl.delay`

, respectively. The former models concatenation as `a ##0 b`

, and the latter models delay as a prefix `##1 c`

. The SVA concatenations with their infix delays map to the LTL dialect as follows:

`seqA ##N seqB`

.**Binary concatenation.**Sequence`seqB`

follows`N`

cycles after`seqA`

. This can be represented as`seqA ##0 (##N seqB)`

, which is equivalent to`%0 = ltl.delay %seqB, N, 0 ltl.concat %seqA, %0`

`seqA ##N seqB ##M seqC`

.**Variadic concatenation.**Sequence`seqC`

follows`M`

cycles after`seqB`

, which itself follows`N`

cycles after`seqA`

. This can be represented as`seqA ##0 (##N seqB) ##0 (##M seqC)`

, which is equivalent to`%0 = ltl.delay %seqB, N, 0 %1 = ltl.delay %seqC, M, 0 ltl.concat %seqA, %0, %1`

Since concatenation is associative, this is also equivalent to

`seqA ##N (seqB ##M seqC)`

:`%0 = ltl.delay %seqC, M, 0 %1 = ltl.concat %seqB, %0 %2 = ltl.delay %1, N, 0 ltl.concat %seqA, %2`

And also

`(seqA ##N seqB) ##M seqC`

:`%0 = ltl.delay %seqB, N, 0 %1 = ltl.concat %seqA, %0 %2 = ltl.delay %seqC, M, 0 ltl.concat %1, %2`

`##N seqA ##M seqB`

.**Initial delay.**Sequence`seqB`

follows`M`

cycles afer`seqA`

, which itself starts`N`

cycles in the future. This is equivalent to a delay on`seqA`

within the concatenation:`%0 = ltl.delay %seqA, N, 0 %1 = ltl.delay %seqB, M, 0 ltl.concat %0, %1`

Alternatively, the delay can also be placed on the entire concatenation:

`%0 = ltl.delay %seqB, M, 0 %1 = ltl.concat %seqA, %0 ltl.delay %1, N, 0`

Only the fixed delay

`##N`

is shown here for simplicity, but the examples extend to the other delay flavors`##[N:M]`

,`##[N:$]`

,`##[*]`

, and`##[+]`

.

### Implication ¶

```
seq |-> prop
seq |=> prop
```

The overlapping `|->`

and non-overlapping `|=>`

implication operators of SVA, which only check a property after a precondition sequence matches, map to the `ltl.implication`

operation. When the sequence matches in the overlapping case `|->`

, the property check starts at the same time the matched sequence ended. In the non-overlapping case `|=>`

, the property check starts *at the clock tick after the* end of the matched sequence, unless the matched sequence was empty, in which special rules apply. (See IEEE 1800-2017 section 16.12.7 “Implication”.) The non-overlapping operator can be expressed in terms of the overlapping operator:

```
seq |=> prop
```

is equivalent to

```
(seq ##1 true) |-> prop
```

The `ltl.implication`

op implements the overlapping case `|->`

, such that the two SVA operator flavors map to the `ltl`

dialect as follows:

`seq |-> prop`

.**Overlapping implication.**Equivalent to`ltl.implication %seq, %prop`

.`seq |=> prop`

.**Non-overlapping implication.**Equivalent to`%true = hw.constant true %0 = ltl.delay %true, 1, 0 %1 = ltl.concat %seq, %0 ltl.implication %1, %prop`

An important benefit of only modeling the overlapping `|->`

implication operator is that it does not interact with a clock. The end point of the left-hand sequence is the starting point of the right-hand sequence. There is no notion of delay between the end of the left and the start of the right sequence. Compare this to the `|=>`

operator in SVA, which implies that the right-hand sequence happens at “strictly the next clock tick”, which requires the operator to have a notion of time and clocking. As described above, it is still possible to model this using an explicit `ltl.delay`

op, which already has an established interaction with a clock.

### Repetition ¶

Consecutive repetition repeats the sequence by a number of times. For example, `s[*3]`

repeats the sequence `s`

three times, which is equivalent to `s ##1 s ##1 s`

. This also applies when the sequence `s`

matches different traces with different lengths. For example `(##[0:3] a)[*2]`

is equivalent to the disjunction of all the combinations such as `a ##1 a`

, `a ##1 (##3 a)`

, `(##3 a) ##1 (##2 a)`

. However, the repetition with unbounded range cannot be expanded to the concatenations as it produces an infinite formula.

The definition of `ltl.repeat`

is similar to that of `ltl.delay`

. The mapping from SVA’s consecutive repetition to the LTL dialect is as follows:

`seq[*N]`

.**Fixed repeat.**Repeats`N`

times. Equivalent to`ltl.repeat %seq, N, 0`

.`seq[*N:M]`

.**Bounded range repeat.**Repeats`N`

to`M`

times. Equivalent to`ltl.repeat %seq, N, (M-N)`

.`seq[*N:$]`

.**Unbounded range repeat.**Repeats`N`

to an indefinite finite number of times. Equivalent to`ltl.repeat %seq, N`

.`seq[*]`

. Shorthand for`seq[*0:$]`

. Equivalent to`ltl.repeat %seq, 0`

.`seq[+]`

. Shorthand for`seq[*1:$]`

. Equivalent to`ltl.repeat %seq, 1`

.

### Clocking ¶

Sequence and property expressions in SVAs can specify a clock with respect to which all cycle delays are expressed. (See IEEE 1800-2017 section 16.16 “Clock resolution”.) These map to the `ltl.clock`

operation.

`@(posedge clk) seqOrProp`

.**Trigger on low-to-high clock edge.**Equivalent to`ltl.clock %seqOrProp, posedge %clk`

.`@(negedge clk) seqOrProp`

.**Trigger on high-to-low clock edge.**Equivalent to`ltl.clock %seqOrProp, negedge %clk`

.`@(edge clk) seqOrProp`

.**Trigger on any clock edge.**Equivalent to`ltl.clock %seqOrProp, edge %clk`

.

### Disable Iff ¶

Properties in SVA can have a disable condition attached, which allows for preemptive resets to be expressed. If the disable condition is true at any time during the evaluation of a property, the property is considered disabled. (See IEEE 1800-2017 end of section 16.12 “Declaring properties”.) This maps to the `ltl.disable`

operation.

`disable iff (expr) prop`

.**Disable condition.**Equivalent to`ltl.disable %prop if %expr`

.

Note that SVAs only allow for entire properties to be disabled, at the point at which they are passed to an assert, assume, or cover statement. It is explicitly forbidden to define a property with a `disable iff`

clause and then using it within another property. For example, the following is forbidden:

```
property p0; disable iff (cond) a |-> b; endproperty
property p1; eventually p0; endproperty
```

In this example, `p1`

refers to property `p0`

, which is illegal in SVA since `p0`

itself defines a disable condition.

In contrast, the LTL dialect explicitly allows for properties to be disabled at arbitrary points, and disabled properties to be used in other properties. Since a disabled nested property also disables the parent property, the IR can always be rewritten into a form where there is only one `disable iff`

condition at the root of a property expression.

## Representing the LTL Formalism ¶

### Next / Delay ¶

The `ltl.delay`

sequence operation represents various shorthands for the *next*/**X** operator in LTL:

Operation | LTL Formula |
---|---|

`ltl.delay %a, 0, 0` | a |

`ltl.delay %a, 1, 0` | Xa |

`ltl.delay %a, 3, 0` | XXXa |

`ltl.delay %a, 0, 2` | a ∨ Xa ∨ XXa |

`ltl.delay %a, 1, 2` | X(a ∨ Xa ∨ XXa) |

`ltl.delay %a, 0` | Fa |

`ltl.delay %a, 2` | XXFa |

### Until and Eventually ¶

`ltl.until`

is *weak*, meaning the property will hold even if the trace does not contain enough clock cycles to evaluate the property. `ltl.eventually`

is *strong*, where `ltl.eventually %p`

means `p`

must hold at some point in the trace.

### Concatenation and Repetition ¶

The `ltl.concat`

sequence operation does not have a direct equivalent in LTL. It builds a longer sequence by composing multiple shorter sequences one after another. LTL has no concept of concatenation, or a *“v happens after u”*, where the point in time at which v starts is dependent on how long the sequence u was.

For a sequence u with a fixed length of 2, concatenation can be represented as *"(u happens) and (v happens 2 cycles in the future)"*, u ∧ **XX**v. If u has a dynamic length though, for example a delay between 1 and 2, `ltl.delay %u, 1, 1`

or **X**u ∨ **XX**u in LTL, there is no fixed number of cycles by which the sequence v can be delayed to make it start after u. Instead, all different-length variants of sequence u have to be enumerated and combined with a copy of sequence v delayed by the appropriate amount: (**X**u ∧ **XX**v) ∨ (**XX**u ∧ **XXX**v). This is basically saying “u delayed by 1 to 2 cycles followed by v” is the same as either *“u delayed by 1 cycle and v delayed by 2 cycles”*, or *“u delayed by 2 cycles and v delayed by 3 cycles”*.

The *“v happens after u”* relationship is crucial to express sequences efficiently, which is why the LTL dialect has the `ltl.concat`

op. If sequences are thought of as regular expressions over time, for example, `a(b|cd)`

or *“a followed by either (b) or (c followed by d)”*, the importance of having a concatenation operation as temporal connective becomes apparent. Why LTL formalisms tend to not include such an operator is unclear.

As for `ltl.repeat`

, it also relies on the semantics of *v happens after u* to compose the repeated sequences. Unlike `ltl.concat`

, which can be expanded by LTL operators within a finite formula size, unbounded repetition cannot be expanded by listing all cases. This means unbounded repetition imports semantics that LTL cannot describe. The LTL dialect has this operation because it is necessary and useful for regular expressions and SVA.

## Types ¶

### Overview ¶

The `ltl`

dialect operations defines two main types returned by its operations: sequences and properties. These types form a hierarchy together with the boolean type `i1`

:

- a boolean
`i1`

is also a valid sequence - a sequence
`!ltl.sequence`

is also a valid property

```
i1 <: ltl.sequence <: ltl.property
```

The two type constraints `AnySequenceType`

and `AnyPropertyType`

are provided to implement this hierarchy. Operations use these constraints for their operands, such that they can properly accept `i1`

as a sequence, `i1`

or a sequence as a property. The return type is an explicit `!ltl.sequence`

or `!ltl.property`

.

### PropertyType ¶

LTL property type

Syntax: `!ltl.property`

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”*.

Note that this type explicitly identifies a *property*. However, a boolean
value (`i1`

) or a sequence (`ltl.sequence`

) is also a valid property.
Operations that accept a property as an operand will use the `AnyProperty`

constraint, which also accepts `ltl.sequence`

and `i1`

.

### SequenceType ¶

LTL sequence type

Syntax: `!ltl.sequence`

The `ltl.sequence`

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

Note that this type explicitly identifies a *sequence*. However, a boolean
value (`i1`

) is also a valid sequence. Operations that accept a sequence as
an operand will use the `AnySequence`

constraint, which also accepts `i1`

.

## Operations ¶

`ltl.and`

(circt::ltl::AndOp) ¶

*A conjunction of booleans, sequences, or properties.*

Syntax:

```
operation ::= `ltl.and` $inputs attr-dict `:` type($inputs)
```

If any of the `$inputs`

is of type `!ltl.property`

, the result of the op is
an `!ltl.property`

. Otherwise it is an `!ltl.sequence`

.

Traits: `AlwaysSpeculatableImplTrait`

, `Commutative`

Interfaces: `ConditionallySpeculatable`

, `InferTypeOpInterface`

, `NoMemoryEffect (MemoryEffectOpInterface)`

Effects: `MemoryEffects::Effect{}`

#### Operands: ¶

Operand | Description |
---|---|

`inputs` | variadic of 1-bit signless integer or LTL sequence type or LTL property type |

#### Results: ¶

Result | Description |
---|---|

`result` | 1-bit signless integer or LTL sequence type or LTL property type |

`ltl.clock`

(circt::ltl::ClockOp) ¶

*Specify the clock for a property or sequence.*

Syntax:

```
operation ::= `ltl.clock` $input `,` $edge $clock attr-dict `:` type($input)
```

Specifies the `$edge`

on a given `$clock`

to be the clock for an `$input`

property or sequence. All cycle delays in the `$input`

implicitly refer to a
clock that advances the state to the next cycle. The `ltl.clock`

operation
provides that clock. The clock applies to the entire property or sequence
expression tree below `$input`

, up to any other nested `ltl.clock`

operations.

The operation returns a property if the `$input`

is a property, and a
sequence otherwise.

Traits: `AlwaysSpeculatableImplTrait`

Interfaces: `ConditionallySpeculatable`

, `InferTypeOpInterface`

, `NoMemoryEffect (MemoryEffectOpInterface)`

Effects: `MemoryEffects::Effect{}`

#### Attributes: ¶

Attribute | MLIR Type | Description |
---|---|---|

`edge` | circt::ltl::ClockEdgeAttr | clock edge |

#### Operands: ¶

Operand | Description |
---|---|

`input` | 1-bit signless integer or LTL sequence type or LTL property type |

`clock` | 1-bit signless integer |

#### Results: ¶

Result | Description |
---|---|

`result` | LTL sequence type or LTL property type |

`ltl.concat`

(circt::ltl::ConcatOp) ¶

*Concatenate sequences into a longer sequence.*

Syntax:

```
operation ::= `ltl.concat` $inputs attr-dict `:` type($inputs)
```

Concatenates all of the `$inputs`

sequences one after another into one
longer sequence. The sequences are arranged such that the end time of the
previous sequences coincides with the start time of the next sequence. This
means there is no implicit cycle of delay between the concatenated
sequences, which may be counterintuitive.

If a sequence should follow in the cycle after another sequence finishes,
that cycle of delay needs to be explicit. For example, *“u followed by v in
next cycle”* (`u ##1 v`

in SVA) is represented as
`concat(u, delay(v, 1, 0))`

:

```
%0 = ltl.delay %v, 1, 0 : i1
ltl.concat %u, %v : !ltl.sequence, !ltl.sequence
```

The resulting sequence checks for `u`

in the first cycle and `v`

in the
second, `[u, v]`

in short.

Without this explicit delay, the previous sequence’s end overlaps with the
next sequence’s start. For example, consider the two sequences `u = a ##1 b`

and `v = c ##1 d`

, which check for `a`

and `c`

in the first, and `b`

and `d`

in the second cycle. When these two sequences are concatenated,
`concat(u, v)`

, the end time of the first sequence coincides with the start
time of the second. As a result, the check for `b`

at the end of the first
sequence will coincide with the check for `c`

at the start of the second
sequence: `concat(u, v) = a ##1 (b && c) ##1 d`

. The resulting sequence
checks for `a`

in the first cycle, `b`

and `c`

in the second, and `d`

in the
third, `[a, (b && c), d]`

in short.

By making the delay between concatenated sequences explicit, the `concat`

operation behaves nicely in the presence of zero-length sequences. An empty,
zero-length sequence in a concatenation behaves as if the sequence wasn’t
present at all. Compare this to SVAs which struggle with empty sequences.
For example, `x ##1 y ##1 z`

would become `x ##2 z`

if `y`

was empty.
Similarly, expressing zero or more repetitions of a sequence, `w ##[*]`

, is
challenging in SVA since concatenation always implies a cycle of delay, but
trivial if the delay is made explicit. This is related to the handling of
empty rules in a parser’s grammar.

Note that concatenating two boolean values *a* and *b* is equivalent to
computing the logical AND of them. Booleans are sequences that check if the
boolean is true in the current cycle, which means that the sequence starts
and ends in the same cycle. Since concatenation aligns the sequences such
that end time of *a* and start time of *b* coincide, the resulting sequence
checks if *a* and *b* both are true in the current cycle, which is an AND
operation.

Traits: `AlwaysSpeculatableImplTrait`

Interfaces: `ConditionallySpeculatable`

, `InferTypeOpInterface`

, `NoMemoryEffect (MemoryEffectOpInterface)`

Effects: `MemoryEffects::Effect{}`

#### Operands: ¶

Operand | Description |
---|---|

`inputs` | variadic of 1-bit signless integer or LTL sequence type |

#### Results: ¶

Result | Description |
---|---|

`result` | LTL sequence type |

`ltl.delay`

(circt::ltl::DelayOp) ¶

*Delay a sequence by a number of cycles.*

Syntax:

```
operation ::= `ltl.delay` $input `,` $delay (`,` $length^)? attr-dict `:` type($input)
```

Delays the `$input`

sequence by the number of cycles specified by `$delay`

.
The delay must be greater than or equal to zero. The optional `$length`

specifies during how many cycles after the initial delay the sequence can
match. Omitting `$length`

indicates an unbounded but finite delay. For
example:

`ltl.delay %seq, 2, 0`

delays`%seq`

by exactly 2 cycles. The resulting sequence matches if`%seq`

matches exactly 2 cycles in the future.`ltl.delay %seq, 2, 2`

delays`%seq`

by 2, 3, or 4 cycles. The resulting sequence matches if`%seq`

matches 2, 3, or 4 cycles in the future.`ltl.delay %seq, 2`

delays`%seq`

by 2 or more cycles. The number of cycles is unbounded but finite, which means that`%seq`

*has*to match at some point, instead of effectively never occuring by being delayed an infinite number of cycles.`ltl.delay %seq, 0, 0`

is equivalent to just`%seq`

.

#### Clocking ¶

The cycle delay specified on the operation refers to a clocking event. This
event is not directly specified by the delay operation itself. Instead, the
`ltl.clock`

operation can be used to associate
all delays within a sequence with a clock.

Traits: `AlwaysSpeculatableImplTrait`

`ConditionallySpeculatable`

, `InferTypeOpInterface`

, `NoMemoryEffect (MemoryEffectOpInterface)`

Effects: `MemoryEffects::Effect{}`

#### Attributes: ¶

Attribute | MLIR Type | Description |
---|---|---|

`delay` | ::mlir::IntegerAttr | 64-bit signless integer attribute |

`length` | ::mlir::IntegerAttr | 64-bit signless integer attribute |

#### Operands: ¶

Operand | Description |
---|---|

`input` | 1-bit signless integer or LTL sequence type |

#### Results: ¶

Result | Description |
---|---|

`result` | LTL sequence type |

`ltl.disable`

(circt::ltl::DisableOp) ¶

*Disable the evaluation of a property based on a condition.*

Syntax:

```
operation ::= `ltl.disable` $input `if` $condition attr-dict `:` type($input)
```

Creates a new property which evaluates the given `$input`

property only if
the given disable `$condition`

is false throughout the entire evaluation. If
the `$condition`

is true at any point in time during the evaluation of
`$input`

, the resulting property is disabled.

The disabling is “infectious”. If a property is disabled, it also implicitly disables all properties that use it. Consider the following example:

```
%0 = ltl.disable %prop if %cond
%1 = ltl.or %0, %otherProp
```

If the property `%0`

is disabled, the derived property `%1`

is also
disabled.

As a result, it is always legal to canonicalize the IR into a form where
there is only one `ltl.disable`

operation at the root of a property
expression.

Note that a property being disabled based on a condition is different from a property that trivially evaluates to true if the condition does not hold. The former ensures that a property is only checked when a certain condition is true, but the number of cases in which the property holds or doesn’t hold remains unchanged. The latter adds additional cases where the property holds, which can offer a solver unintended ways to make assertions or coverage proofs derived from the property pass. For example:

```
%p0 = ltl.or %prop, %cond
%p1 = ltl.disable %prop if %cond
```

`$cond`

being true would disable the evaluation of `%p0`

and would make
`%p1`

evaluate to true. These are subtly different. If used in an assertion
during simulation, `$cond`

would adequately disable triggering of the
assertion in both cases. However, if used in a formal verification setting
where proofs for `%p0`

and `%p1`

always holding or never holding are sought,
a solver might use `%cond = true`

to trivially make `%p0`

hold, which is not
possible for `%p1`

. Consider the following more concrete example:

```
%p2 = ltl.or %protocolCorrectProperty, %reset
%p3 = ltl.disable %protocolCorrectProperty if %reset
verif.cover %p2
verif.cover %p3
```

The intent is to formally prove coverage for `%protocolCorrectProperty`

while the circuit is in regular operation (i.e., out of reset). A formal
solver would trivially prove coverage for `%p2`

by assigning
`%reset = true`

, but would have to actually prove coverage for the
underlying `%protocolCorrectProperty`

for `%p3`

. The latter is almost always
the intended behavior.

Traits: `AlwaysSpeculatableImplTrait`

`ConditionallySpeculatable`

, `InferTypeOpInterface`

, `NoMemoryEffect (MemoryEffectOpInterface)`

Effects: `MemoryEffects::Effect{}`

#### Operands: ¶

Operand | Description |
---|---|

`input` | 1-bit signless integer or LTL sequence type or LTL property type |

`condition` | 1-bit signless integer |

#### Results: ¶

Result | Description |
---|---|

`result` | LTL property type |

`ltl.eventually`

(circt::ltl::EventuallyOp) ¶

*Ensure that a property will hold at some time in the future.*

Syntax:

```
operation ::= `ltl.eventually` $input attr-dict `:` type($input)
```

Checks that the `$input`

property will hold at a future time. This operator
is strong: it requires that the `$input`

holds after a *finite* number of
cycles. The operator does *not* hold if the `$input`

can’t hold in the
future.

Traits: `AlwaysSpeculatableImplTrait`

`ConditionallySpeculatable`

, `InferTypeOpInterface`

, `NoMemoryEffect (MemoryEffectOpInterface)`

Effects: `MemoryEffects::Effect{}`

#### Operands: ¶

Operand | Description |
---|---|

`input` | 1-bit signless integer or LTL sequence type or LTL property type |

#### Results: ¶

Result | Description |
---|---|

`result` | LTL property type |

`ltl.implication`

(circt::ltl::ImplicationOp) ¶

*Only check a property after a sequence matched.*

Syntax:

```
operation ::= `ltl.implication` operands attr-dict `:` type(operands)
```

Preconditions the checking of the `$consequent`

property on the
`$antecedent`

sequence. In a nutshell, if the `$antecedent`

sequence matches
at a given point in time, the `$consequent`

property is checked starting at
the point in time at which the matched sequence ends. The result property of
the `ltl.implication`

holds if the `$consequent`

holds. Conversely, if the
`$antecedent`

does *not* match at a given point in time, the result property
trivially holds. This is conceptually identical to the implication operator
→, but with additional temporal semantics.

Traits: `AlwaysSpeculatableImplTrait`

`ConditionallySpeculatable`

, `InferTypeOpInterface`

, `NoMemoryEffect (MemoryEffectOpInterface)`

Effects: `MemoryEffects::Effect{}`

#### Operands: ¶

Operand | Description |
---|---|

`antecedent` | 1-bit signless integer or LTL sequence type |

`consequent` | 1-bit signless integer or LTL sequence type or LTL property type |

#### Results: ¶

Result | Description |
---|---|

`result` | LTL property type |

`ltl.not`

(circt::ltl::NotOp) ¶

*A negation of a property.*

Syntax:

```
operation ::= `ltl.not` $input attr-dict `:` type($input)
```

Negates the `$input`

property. The resulting property evaluates to true if
`$input`

evaluates to false, and it evaluates to false if `$input`

evaluates
to true.

Traits: `AlwaysSpeculatableImplTrait`

`ConditionallySpeculatable`

, `InferTypeOpInterface`

, `NoMemoryEffect (MemoryEffectOpInterface)`

Effects: `MemoryEffects::Effect{}`

#### Operands: ¶

Operand | Description |
---|---|

`input` | 1-bit signless integer or LTL sequence type or LTL property type |

#### Results: ¶

Result | Description |
---|---|

`result` | LTL property type |

`ltl.or`

(circt::ltl::OrOp) ¶

*A disjunction of booleans, sequences, or properties.*

Syntax:

```
operation ::= `ltl.or` $inputs attr-dict `:` type($inputs)
```

If any of the `$inputs`

is of type `!ltl.property`

, the result of the op is
an `!ltl.property`

. Otherwise it is an `!ltl.sequence`

.

Traits: `AlwaysSpeculatableImplTrait`

, `Commutative`

`ConditionallySpeculatable`

, `InferTypeOpInterface`

, `NoMemoryEffect (MemoryEffectOpInterface)`

Effects: `MemoryEffects::Effect{}`

#### Operands: ¶

Operand | Description |
---|---|

`inputs` | variadic of 1-bit signless integer or LTL sequence type or LTL property type |

#### Results: ¶

Result | Description |
---|---|

`result` | 1-bit signless integer or LTL sequence type or LTL property type |

`ltl.repeat`

(circt::ltl::RepeatOp) ¶

*Repeats a sequence by a number of times.*

Syntax:

```
operation ::= `ltl.repeat` $input `,` $base (`,` $more^)? attr-dict `:` type($input)
```

Repeat the `$input`

sequence at least `$base`

times, at most `$base`

+
`$more`

times. The number must be greater than or equal to zero. Omitting
`$more`

indicates an unbounded but finite repetition. For example:

`ltl.repeat %seq, 2, 0`

repeats`%seq`

exactly 2 times.`ltl.repeat %seq, 2, 2`

repeats`%seq`

2, 3, or 4 times.`ltl.repeat %seq, 2`

repeats`%seq`

2 or more times. The number of times is unbounded but finite.`ltl.repeat %seq, 0, 0`

represents an empty sequence.

Traits: `AlwaysSpeculatableImplTrait`

`ConditionallySpeculatable`

, `InferTypeOpInterface`

, `NoMemoryEffect (MemoryEffectOpInterface)`

Effects: `MemoryEffects::Effect{}`

#### Attributes: ¶

Attribute | MLIR Type | Description |
---|---|---|

`base` | ::mlir::IntegerAttr | 64-bit signless integer attribute |

`more` | ::mlir::IntegerAttr | 64-bit signless integer attribute |

#### Operands: ¶

Operand | Description |
---|---|

`input` | 1-bit signless integer or LTL sequence type |

#### Results: ¶

Result | Description |
---|---|

`result` | LTL sequence type |

`ltl.until`

(circt::ltl::UntilOp) ¶

*Property always holds until another property holds.*

Syntax:

```
operation ::= `ltl.until` operands attr-dict `:` type(operands)
```

Checks that the `$input`

property always holds until the `$condition`

property holds once. This operator is weak: the property will hold even if
`$input`

always holds and `$condition`

never holds. This operator is
nonoverlapping: `$input`

does not have to hold when `$condition`

holds.

Traits: `AlwaysSpeculatableImplTrait`

`ConditionallySpeculatable`

, `InferTypeOpInterface`

, `NoMemoryEffect (MemoryEffectOpInterface)`

Effects: `MemoryEffects::Effect{}`

#### Operands: ¶

Operand | Description |
---|---|

`input` | 1-bit signless integer or LTL sequence type or LTL property type |

`condition` | 1-bit signless integer or LTL sequence type or LTL property type |

#### Results: ¶

Result | Description |
---|---|

`result` | LTL property type |