CIRCT

Circuit IR Compilers and Tools

'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:

OperationLTL Formula
ltl.delay %a, 0, 0a
ltl.delay %a, 1, 0Xa
ltl.delay %a, 3, 0XXXa
ltl.delay %a, 0, 2a ∨ Xa ∨ XXa
ltl.delay %a, 1, 2X(a ∨ Xa ∨ XXa)
ltl.delay %a, 0Fa
ltl.delay %a, 2XXFa

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 ∧ XXv. If u has a dynamic length though, for example a delay between 1 and 2, ltl.delay %u, 1, 1 or Xu ∨ XXu 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: (Xu ∧ XXv) ∨ (XXu ∧ XXXv). 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: 

OperandDescription
inputsvariadic of 1-bit signless integer or LTL sequence type or LTL property type

Results: 

ResultDescription
result1-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: 

AttributeMLIR TypeDescription
edgecirct::ltl::ClockEdgeAttrclock edge

Operands: 

OperandDescription
input1-bit signless integer or LTL sequence type or LTL property type
clock1-bit signless integer

Results: 

ResultDescription
resultLTL 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: 

OperandDescription
inputsvariadic of 1-bit signless integer or LTL sequence type

Results: 

ResultDescription
resultLTL 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

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes: 

AttributeMLIR TypeDescription
delay::mlir::IntegerAttr64-bit signless integer attribute
length::mlir::IntegerAttr64-bit signless integer attribute

Operands: 

OperandDescription
input1-bit signless integer or LTL sequence type

Results: 

ResultDescription
resultLTL 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

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands: 

OperandDescription
input1-bit signless integer or LTL sequence type or LTL property type
condition1-bit signless integer

Results: 

ResultDescription
resultLTL 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

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands: 

OperandDescription
input1-bit signless integer or LTL sequence type or LTL property type

Results: 

ResultDescription
resultLTL 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

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands: 

OperandDescription
antecedent1-bit signless integer or LTL sequence type
consequent1-bit signless integer or LTL sequence type or LTL property type

Results: 

ResultDescription
resultLTL 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

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands: 

OperandDescription
input1-bit signless integer or LTL sequence type or LTL property type

Results: 

ResultDescription
resultLTL 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

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands: 

OperandDescription
inputsvariadic of 1-bit signless integer or LTL sequence type or LTL property type

Results: 

ResultDescription
result1-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

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes: 

AttributeMLIR TypeDescription
base::mlir::IntegerAttr64-bit signless integer attribute
more::mlir::IntegerAttr64-bit signless integer attribute

Operands: 

OperandDescription
input1-bit signless integer or LTL sequence type

Results: 

ResultDescription
resultLTL 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

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands: 

OperandDescription
input1-bit signless integer or LTL sequence type or LTL property type
condition1-bit signless integer or LTL sequence type or LTL property type

Results: 

ResultDescription
resultLTL property type