Add LTL and Verif dialects (#5255)

Add two new dialects to CIRCT.

The `ltl` dialect represents Linear Temporal Logic expressions and
borrows from SystemVerilog's rich assertion system (SVAs). The current
implementation is fairly minimal, but is sufficient to capture basic
liveness properties and something akin to "regular expressions over
time". Since the mapping from SVAs to this dialect is non-trivial, there
is an `LTL.md` doc accompanying the dialect to capture some of the
design decisions.

The `verif` dialect captures various verification-related operations.
It currently contains just a trivial flavor of assert, assume, and
cover, without any labels, messages, or value interpolation. The
intention is for these operations to be expanded in the future until
they can replace the corresponding operations in the SV dialect. The
`verif` dialect will also be a good place to introduce
verification-specific concepts such as test programs, clock generators,
pre- and post-condition checks.

The LTL operations have a few basic folds and canonicalizations defined
on them, to be expanded later. Something like a "never" sequence or
property would be useful to have unreachable/unmatachable sequences fold
to something.

Support for emission in ExportVerilog will be done in a separate commit.

docs/Dialects/LTL.md

@@ -0,0 +1,209 @@
+# 'ltl' Dialect
+
+This dialect provides operations and types to model [Linear Temporal Logic](https://en.wikipedia.org/wiki/Linear_temporal_logic), sequences, and properties, which are useful for hardware verification.
+
+[TOC]
+
+
+## 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.
+
+As a primary reference, the `ltl` dialect attempts to model SVAs after the [Linear Temporal Logic](https://en.wikipedia.org/wiki/Linear_temporal_logic) formalism as a way to distill SystemVerilog's syntactic sugar and quirks down to a core representation. However, most definitions of LTL tend to be rather academic in nature and may be lacking certain building blocks to make them useful in practice. (See section on [concatenation](#concatenation) below.) To inform some practical design decisions, the `ltl` dialect tries to think of temporal sequences as "regular expressions over time", borrowing from their wide applicability and usefulness.
+
+
+### 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.
+- `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.
+
+
+### 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` | **X**a                      |
+| `ltl.delay %a, 3, 0` | **XXX**a                    |
+| `ltl.delay %a, 0, 2` | a ∨ **X**a ∨ **XX**a        |
+| `ltl.delay %a, 1, 2` | **X**(a ∨ **X**a ∨ **XX**a) |
+| `ltl.delay %a, 0`    | **F**a                      |
+| `ltl.delay %a, 2`    | **XXF**a                    |
+
+
+### Concatenation
+
+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.
+
+
+## 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`.
+
+[include "Dialects/LTLTypes.md"]
+
+
+## Operations
+
+[include "Dialects/LTLOps.md"]

docs/Dialects/Verif.md

@@ -0,0 +1,9 @@
+# 'verif' Dialect
+
+This dialect provides a collection of operations to express various verification concerns, such as assertions and interacting with a piece of hardware for the sake of verifying its proper functioning.
+
+[TOC]
+
+## Operations
+
+[include "Dialects/VerifOps.md"]

include/circt/Dialect/CMakeLists.txt

@@ -19,6 +19,7 @@ add_subdirectory(HWArith)
 add_subdirectory(Interop)
 add_subdirectory(LLHD)
 add_subdirectory(LoopSchedule)
+add_subdirectory(LTL)
 add_subdirectory(Moore)
 add_subdirectory(MSFT)
 add_subdirectory(OM)
@@ -27,3 +28,4 @@ add_subdirectory(Seq)
 add_subdirectory(SSP)
 add_subdirectory(SV)
 add_subdirectory(SystemC)
+add_subdirectory(Verif)

include/circt/Dialect/LTL/CMakeLists.txt

@@ -0,0 +1,13 @@
+add_circt_dialect(LTL ltl)
+add_circt_doc(LTLOps Dialects/LTLOps -gen-op-doc)
+add_circt_doc(LTLTypes Dialects/LTLTypes -gen-typedef-doc -dialect ltl)
+
+set(LLVM_TARGET_DEFINITIONS LTL.td)
+mlir_tablegen(LTLEnums.h.inc -gen-enum-decls)
+mlir_tablegen(LTLEnums.cpp.inc -gen-enum-defs)
+add_public_tablegen_target(CIRCTLTLEnumsIncGen)
+add_dependencies(circt-headers CIRCTLTLEnumsIncGen)
+
+mlir_tablegen(LTLFolds.cpp.inc -gen-rewriters)
+add_public_tablegen_target(CIRCTLTLFoldsIncGen)
+add_dependencies(circt-headers CIRCTLTLFoldsIncGen)

include/circt/Dialect/LTL/LTL.td

@@ -0,0 +1,17 @@
+//===- LTL.td - LTL dialect definition ---------------------*- tablegen -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_LTL_LTL_TD
+#define CIRCT_DIALECT_LTL_LTL_TD
+
+include "circt/Dialect/LTL/LTLDialect.td"
+include "circt/Dialect/LTL/LTLTypes.td"
+include "circt/Dialect/LTL/LTLOps.td"
+include "circt/Dialect/LTL/LTLFolds.td"
+
+#endif // CIRCT_DIALECT_LTL_LTL_TD

include/circt/Dialect/LTL/LTLDialect.h

@@ -0,0 +1,19 @@
+//===- LTLDialect.h - LTL dialect definition --------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_LTL_LTLDIALECT_H
+#define CIRCT_DIALECT_LTL_LTLDIALECT_H
+
+#include "circt/Support/LLVM.h"
+#include "mlir/IR/BuiltinOps.h"
+#include "mlir/IR/Dialect.h"
+
+#include "circt/Dialect/LTL/LTLDialect.h.inc"
+#include "circt/Dialect/LTL/LTLEnums.h.inc"
+
+#endif // CIRCT_DIALECT_LTL_LTLDIALECT_H

include/circt/Dialect/LTL/LTLDialect.td

@@ -0,0 +1,23 @@
+//===- LTLDialect.td - LTL dialect definition --------------*- tablegen -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_LTL_LTLDIALECT_TD
+#define CIRCT_DIALECT_LTL_LTLDIALECT_TD
+
+include "mlir/IR/OpBase.td"
+
+def LTLDialect : Dialect {
+  let name = "ltl";
+  let summary = "Linear temporal logic, sequences, and properties.";
+  // See `docs/Dialect/LTL.md` for detailed dialect documentation.
+  let cppNamespace = "circt::ltl";
+  let useDefaultTypePrinterParser = 1;
+  let dependentDialects = ["hw::HWDialect", "comb::CombDialect"];
+}
+
+#endif // CIRCT_DIALECT_LTL_LTLDIALECT_TD

include/circt/Dialect/LTL/LTLFolds.td

@@ -0,0 +1,65 @@
+//===- LTLFolds.td - LTL dialect declarative rewrites ------*- tablegen -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_LTL_LTLFOLDS_TD
+#define CIRCT_DIALECT_LTL_LTLFOLDS_TD
+
+include "circt/Dialect/LTL/LTLOps.td"
+include "mlir/IR/PatternBase.td"
+
+//===----------------------------------------------------------------------===//
+// Utilities
+//===----------------------------------------------------------------------===//
+
+def valueHead : NativeCodeCall<"$0[0]">;
+def valueTail : NativeCodeCall<"$0.drop_front()">;
+def concatValues : NativeCodeCall<
+  "concatValues(ValueRange{$0}, ValueRange{$1})">;
+
+//===----------------------------------------------------------------------===//
+// DelayOp
+//===----------------------------------------------------------------------===//
+
+// delay(delay(s, I), J) -> delay(s, I+J)
+// delay(delay(s, I), J, N) -> delay(s, I+J)
+// delay(delay(s, I, N), J) -> delay(s, I+J)
+// delay(delay(s, I, N), J, M) -> delay(s, I+J, N+M)
+def mergedDelays : NativeCodeCall<
+  "$_builder.getI64IntegerAttr($0.getInt() + $1.getInt())">;
+def mergedLengths : NativeCodeCall<[{
+  $0 && $1 ? $_builder.getI64IntegerAttr($0.getInt() + $1.getInt())
+           : IntegerAttr{}
+}]>;
+def NestedDelays : Pat<
+  (DelayOp (DelayOp $input, $delay1, $length1), $delay2, $length2),
+  (DelayOp $input, (mergedDelays $delay1, $delay2),
+                   (mergedLengths $length1, $length2))>;
+
+// delay(concat(s, ...), N, M) -> concat(delay(s, N, M), ...)
+def MoveDelayIntoConcat : Pat<
+  (DelayOp (ConcatOp $inputs), $delay, $length),
+  (ConcatOp (concatValues (DelayOp (valueHead $inputs), $delay, $length),
+                          (valueTail $inputs)))>;
+
+//===----------------------------------------------------------------------===//
+// ConcatOp
+//===----------------------------------------------------------------------===//
+
+// concat(..., concat(s0, s1), ...) -> concat(..., s0, s1, ...)
+def AnyDefiningOpIsConcat : Constraint<CPred<[{
+    llvm::any_of($0, [](auto v){
+      return !!v.template getDefiningOp<ConcatOp>();
+    })
+  }]>,
+  "any value is defined by ConcatOp">;
+def flattenConcats : NativeCodeCall<"flattenConcats($0)">;
+def FlattenConcats : Pat<
+  (ConcatOp $inputs), (ConcatOp (flattenConcats $inputs)),
+  [(AnyDefiningOpIsConcat $inputs)]>;
+
+#endif // CIRCT_DIALECT_LTL_LTLFOLDS_TD

include/circt/Dialect/LTL/LTLOps.h

@@ -0,0 +1,20 @@
+//===- LTLOps.h - LTL dialect operations --------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_LTL_LTLOPS_H
+#define CIRCT_DIALECT_LTL_LTLOPS_H
+
+#include "mlir/Interfaces/InferTypeOpInterface.h"
+
+#include "circt/Dialect/LTL/LTLDialect.h"
+#include "circt/Dialect/LTL/LTLTypes.h"
+
+#define GET_OP_CLASSES
+#include "circt/Dialect/LTL/LTL.h.inc"
+
+#endif // CIRCT_DIALECT_LTL_LTLOPS_H

include/circt/Dialect/LTL/LTLOps.td

@@ -0,0 +1,316 @@
+//===- LTLOps.td - LTL dialect operations ------------------*- tablegen -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_LTL_LTLOPS_TD
+#define CIRCT_DIALECT_LTL_LTLOPS_TD
+
+include "circt/Dialect/LTL/LTLDialect.td"
+include "circt/Dialect/LTL/LTLTypes.td"
+include "mlir/IR/EnumAttr.td"
+include "mlir/IR/PatternBase.td"
+include "mlir/Interfaces/InferTypeOpInterface.td"
+include "mlir/Interfaces/SideEffectInterfaces.td"
+
+class LTLOp<string mnemonic, list<Trait> traits = []> :
+  Op<LTLDialect, mnemonic, traits>;
+
+//===----------------------------------------------------------------------===//
+// Generic Operations
+//===----------------------------------------------------------------------===//
+
+class AssocLTLOp<string mnemonic, list<Trait> traits = []> :
+  LTLOp<mnemonic, traits # [Pure, Commutative, InferTypeOpInterface,
+                            DeclareOpInterfaceMethods<InferTypeOpInterface>]> {
+  let arguments = (ins Variadic<LTLAnyPropertyType>:$inputs);
+  let results = (outs LTLAnyPropertyType:$result);
+  let assemblyFormat = [{
+    $inputs attr-dict `:` type($inputs)
+  }];
+}
+
+def AndOp : AssocLTLOp<"and"> {
+  let summary = "A conjunction of booleans, sequences, or properties.";
+  let description = [{
+    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`.
+  }];
+}
+
+def OrOp : AssocLTLOp<"or"> {
+  let summary = "A disjunction of booleans, sequences, or properties.";
+  let description = [{
+    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`.
+  }];
+}
+
+//===----------------------------------------------------------------------===//
+// Sequences
+//===----------------------------------------------------------------------===//
+
+def DelayOp : LTLOp<"delay", [Pure]> {
+  let arguments = (ins
+    LTLAnySequenceType:$input,
+    I64Attr:$delay,
+    OptionalAttr<I64Attr>:$length);
+  let results = (outs LTLSequenceType:$result);
+  let assemblyFormat = [{
+    $input `,` $delay (`,` $length^)? attr-dict `:` type($input)
+  }];
+  let hasFolder = 1;
+  let hasCanonicalizer = 1;
+
+  let summary = "Delay a sequence by a number of cycles.";
+  let description = [{
+    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`](#ltlclock-circtltlclockop) operation can be used to associate
+    all delays within a sequence with a clock.
+  }];
+}
+
+def ConcatOp : LTLOp<"concat", [Pure]> {
+  let arguments = (ins Variadic<LTLAnySequenceType>:$inputs);
+  let results = (outs LTLSequenceType:$result);
+  let assemblyFormat = [{
+    $inputs attr-dict `:` type($inputs)
+  }];
+  let hasFolder = 1;
+  let hasCanonicalizer = 1;
+
+  let summary = "Concatenate sequences into a longer sequence.";
+  let description = [{
+    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.
+  }];
+}
+
+//===----------------------------------------------------------------------===//
+// Properties
+//===----------------------------------------------------------------------===//
+
+def NotOp : LTLOp<"not", [Pure]> {
+  let arguments = (ins LTLAnyPropertyType:$input);
+  let results = (outs LTLPropertyType:$result);
+  let assemblyFormat = [{
+    $input attr-dict `:` type($input)
+  }];
+
+  let summary = "A negation of a property.";
+  let description = [{
+    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.
+  }];
+}
+
+def ImplicationOp : LTLOp<"implication", [Pure]> {
+  let arguments = (ins LTLAnySequenceType:$antecedent,
+                       LTLAnyPropertyType:$consequent);
+  let results = (outs LTLPropertyType:$result);
+  let assemblyFormat = [{
+    operands attr-dict `:` type(operands)
+  }];
+
+  let summary = "Only check a property after a sequence matched.";
+  let description = [{
+    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.
+  }];
+}
+
+def EventuallyOp : LTLOp<"eventually", [Pure]> {
+  let arguments = (ins LTLAnyPropertyType:$input);
+  let results = (outs LTLPropertyType:$result);
+  let assemblyFormat = [{
+    $input attr-dict `:` type($input)
+  }];
+
+  let summary = "Ensure that a property will hold at some time in the future.";
+  let description = [{
+    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.
+  }];
+}
+
+//===----------------------------------------------------------------------===//
+// Clocking
+//===----------------------------------------------------------------------===//
+
+// Edge behavior enum for always block.  See SV Spec 9.4.2.
+
+/// AtPosEdge triggers on a rise from 0 to 1/X/Z, or X/Z to 1.
+def AtPosEdge: I32EnumAttrCase<"Pos", 0, "posedge">;
+/// AtNegEdge triggers on a drop from 1 to 0/X/Z, or X/Z to 0.
+def AtNegEdge: I32EnumAttrCase<"Neg", 1, "negedge">;
+/// AtEdge is syntactic sugar for AtPosEdge or AtNegEdge.
+def AtEdge   : I32EnumAttrCase<"Both", 2, "edge">;
+
+def ClockEdgeAttr : I32EnumAttr<"ClockEdge", "clock edge",
+                                [AtPosEdge, AtNegEdge, AtEdge]> {
+  let cppNamespace = "circt::ltl";
+}
+
+def ClockOp : LTLOp<"clock", [
+  Pure, InferTypeOpInterface, DeclareOpInterfaceMethods<InferTypeOpInterface>
+]> {
+  let arguments = (ins LTLAnyPropertyType:$input, ClockEdgeAttr:$edge, I1:$clock);
+  let results = (outs LTLSequenceOrPropertyType:$result);
+  let assemblyFormat = [{
+    $input `,` $edge $clock attr-dict `:` type($input)
+  }];
+
+  let summary = "Specify the clock for a property or sequence.";
+  let description = [{
+    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.
+  }];
+}
+
+def DisableOp : LTLOp<"disable", [Pure]> {
+  let arguments = (ins LTLAnyPropertyType:$input, I1:$condition);
+  let results = (outs LTLPropertyType:$result);
+  let assemblyFormat = [{
+    $input `if` $condition attr-dict `:` type($input)
+  }];
+  let hasFolder = 1;
+
+  let summary = "Disable the evaluation of a property based on a condition.";
+  let description = [{
+    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.
+  }];
+}
+
+#endif // CIRCT_DIALECT_LTL_LTLOPS_TD

include/circt/Dialect/LTL/LTLTypes.h

@@ -0,0 +1,18 @@
+//===- LTLTypes.h - LTL dialect types ---------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_LTL_LTLTYPES_H
+#define CIRCT_DIALECT_LTL_LTLTYPES_H
+
+#include "mlir/IR/BuiltinTypes.h"
+#include "mlir/IR/Types.h"
+
+#define GET_TYPEDEF_CLASSES
+#include "circt/Dialect/LTL/LTLTypes.h.inc"
+
+#endif // CIRCT_DIALECT_LTL_LTLTYPES_H

include/circt/Dialect/LTL/LTLTypes.td

@@ -0,0 +1,49 @@
+//===- LTLTypes.td - LTL dialect types ---------------------*- tablegen -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_LTL_LTLTYPES_TD
+#define CIRCT_DIALECT_LTL_LTLTYPES_TD
+
+include "circt/Dialect/LTL/LTLDialect.td"
+include "mlir/IR/AttrTypeBase.td"
+
+class LTLTypeDef<string name, string typeMnemonic> : TypeDef<LTLDialect, name> {
+  let mnemonic = typeMnemonic;
+}
+
+def LTLSequenceType : LTLTypeDef<"Sequence", "sequence"> {
+  let summary = "LTL sequence type";
+  let description = [{
+    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`.
+  }];
+}
+
+def LTLPropertyType : LTLTypeDef<"Property", "property"> {
+  let summary = "LTL property type";
+  let description = [{
+    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`.
+  }];
+}
+
+def LTLAnySequenceType : AnyTypeOf<[I1, LTLSequenceType]>;
+def LTLAnyPropertyType : AnyTypeOf<[I1, LTLSequenceType, LTLPropertyType]>;
+def LTLSequenceOrPropertyType : AnyTypeOf<[LTLSequenceType, LTLPropertyType]>;
+
+#endif // CIRCT_DIALECT_LTL_LTLTYPES_TD

include/circt/Dialect/LTL/LTLVisitors.h

@@ -0,0 +1,66 @@
+//===- LTLVisitors.h - LTL dialect visitors ---------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_LTL_LTLVISITORS_H
+#define CIRCT_DIALECT_LTL_LTLVISITORS_H
+
+#include "circt/Dialect/LTL/LTLOps.h"
+#include "llvm/ADT/TypeSwitch.h"
+
+namespace circt {
+namespace ltl {
+template <typename ConcreteType, typename ResultType = void,
+          typename... ExtraArgs>
+class Visitor {
+public:
+  ResultType dispatchLTLVisitor(Operation *op, ExtraArgs... args) {
+    auto *thisCast = static_cast<ConcreteType *>(this);
+    return TypeSwitch<Operation *, ResultType>(op)
+        .template Case<AndOp, OrOp, DelayOp, ConcatOp, NotOp, ImplicationOp,
+                       EventuallyOp, ClockOp, DisableOp>(
+            [&](auto op) -> ResultType {
+              return thisCast->visitLTL(op, args...);
+            })
+        .Default([&](auto) -> ResultType {
+          return thisCast->visitInvalidLTL(op, args...);
+        });
+  }
+
+  /// This callback is invoked on any non-LTL operations.
+  ResultType visitInvalidLTL(Operation *op, ExtraArgs... args) {
+    op->emitOpError("is not an LTL operation");
+    abort();
+  }
+
+  /// This callback is invoked on any LTL operations that were not handled by
+  /// their concrete `visitLTL(...)` callback.
+  ResultType visitUnhandledLTL(Operation *op, ExtraArgs... args) {
+    return ResultType();
+  }
+
+#define HANDLE(OPTYPE, OPKIND)                                                 \
+  ResultType visitLTL(OPTYPE op, ExtraArgs... args) {                          \
+    return static_cast<ConcreteType *>(this)->visit##OPKIND##LTL(op, args...); \
+  }
+
+  HANDLE(AndOp, Unhandled);
+  HANDLE(OrOp, Unhandled);
+  HANDLE(DelayOp, Unhandled);
+  HANDLE(ConcatOp, Unhandled);
+  HANDLE(NotOp, Unhandled);
+  HANDLE(ImplicationOp, Unhandled);
+  HANDLE(EventuallyOp, Unhandled);
+  HANDLE(ClockOp, Unhandled);
+  HANDLE(DisableOp, Unhandled);
+#undef HANDLE
+};
+
+} // namespace ltl
+} // namespace circt
+
+#endif // CIRCT_DIALECT_LTL_LTLVISITORS_H

include/circt/Dialect/Verif/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_circt_dialect(Verif verif)
+add_circt_doc(VerifOps Dialects/VerifOps -gen-op-doc)

include/circt/Dialect/Verif/Verif.td

@@ -0,0 +1,15 @@
+//===- Verif.td - Verif dialect definition -----------------*- tablegen -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_VERIF_VERIF_TD
+#define CIRCT_DIALECT_VERIF_VERIF_TD
+
+include "circt/Dialect/Verif/VerifDialect.td"
+include "circt/Dialect/Verif/VerifOps.td"
+
+#endif // CIRCT_DIALECT_VERIF_VERIF_TD

include/circt/Dialect/Verif/VerifDialect.h

@@ -0,0 +1,18 @@
+//===- VerifDialect.h - Verif dialect definition ----------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_VERIF_VERIFDIALECT_H
+#define CIRCT_DIALECT_VERIF_VERIFDIALECT_H
+
+#include "circt/Support/LLVM.h"
+#include "mlir/IR/BuiltinOps.h"
+#include "mlir/IR/Dialect.h"
+
+#include "circt/Dialect/Verif/VerifDialect.h.inc"
+
+#endif // CIRCT_DIALECT_VERIF_VERIFDIALECT_H

include/circt/Dialect/Verif/VerifDialect.td

@@ -0,0 +1,21 @@
+//===- VerifDialect.td - Verif dialect definition ----------*- tablegen -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_VERIF_VERIFDIALECT_TD
+#define CIRCT_DIALECT_VERIF_VERIFDIALECT_TD
+
+include "mlir/IR/OpBase.td"
+
+def VerifDialect : Dialect {
+  let name = "verif";
+  let summary = "Verification constructs and utilities.";
+  // See `docs/Dialect/Verif.md` for detailed dialect documentation.
+  let cppNamespace = "circt::verif";
+}
+
+#endif // CIRCT_DIALECT_VERIF_VERIFDIALECT_TD

include/circt/Dialect/Verif/VerifOps.h

@@ -0,0 +1,17 @@
+//===- VerifOps.h - Verif dialect operations --------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_VERIF_VERIFOPS_H
+#define CIRCT_DIALECT_VERIF_VERIFOPS_H
+
+#include "circt/Dialect/Verif/VerifDialect.h"
+
+#define GET_OP_CLASSES
+#include "circt/Dialect/Verif/Verif.h.inc"
+
+#endif // CIRCT_DIALECT_VERIF_VERIFOPS_H

include/circt/Dialect/Verif/VerifOps.td

@@ -0,0 +1,42 @@
+//===- VerifOps.td - Verif dialect operations --------------*- tablegen -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_VERIF_VERIFOPS_TD
+#define CIRCT_DIALECT_VERIF_VERIFOPS_TD
+
+include "circt/Dialect/Verif/VerifDialect.td"
+include "circt/Dialect/LTL/LTLTypes.td"
+
+class VerifOp<string mnemonic, list<Trait> traits = []> :
+  Op<VerifDialect, mnemonic, traits>;
+
+//===----------------------------------------------------------------------===//
+// Assertions
+//===----------------------------------------------------------------------===//
+
+class AssertLikeOp<string mnemonic, list<Trait> traits = []> :
+  VerifOp<mnemonic, traits> {
+  let arguments = (ins LTLAnyPropertyType:$property);
+  let assemblyFormat = [{
+    $property attr-dict `:` type($property)
+  }];
+}
+
+def AssertOp : AssertLikeOp<"assert"> {
+  let summary = "Assert that a property holds.";
+}
+
+def AssumeOp : AssertLikeOp<"assume"> {
+  let summary = "Assume that a property holds.";
+}
+
+def CoverOp : AssertLikeOp<"cover"> {
+  let summary = "Ensure that a property can hold.";
+}
+
+#endif // CIRCT_DIALECT_VERIF_VERIFOPS_TD

include/circt/Dialect/Verif/VerifVisitors.h

@@ -0,0 +1,59 @@
+//===- VerifVisitors.h - Verif dialect visitors -----------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_VERIF_VERIFVISITORS_H
+#define CIRCT_DIALECT_VERIF_VERIFVISITORS_H
+
+#include "circt/Dialect/Verif/VerifOps.h"
+#include "llvm/ADT/TypeSwitch.h"
+
+namespace circt {
+namespace verif {
+template <typename ConcreteType, typename ResultType = void,
+          typename... ExtraArgs>
+class Visitor {
+public:
+  ResultType dispatchVerifVisitor(Operation *op, ExtraArgs... args) {
+    auto *thisCast = static_cast<ConcreteType *>(this);
+    return TypeSwitch<Operation *, ResultType>(op)
+        .template Case<AssertOp, AssumeOp, CoverOp>([&](auto op) -> ResultType {
+          return thisCast->visitVerif(op, args...);
+        })
+        .Default([&](auto) -> ResultType {
+          return thisCast->visitInvalidVerif(op, args...);
+        });
+  }
+
+  /// This callback is invoked on any non-verif operations.
+  ResultType visitInvalidVerif(Operation *op, ExtraArgs... args) {
+    op->emitOpError("is not a verif operation");
+    abort();
+  }
+
+  /// This callback is invoked on any verif operations that were not handled by
+  /// their concrete `visitVerif(...)` callback.
+  ResultType visitUnhandledVerif(Operation *op, ExtraArgs... args) {
+    return ResultType();
+  }
+
+#define HANDLE(OPTYPE, OPKIND)                                                 \
+  ResultType visitVerif(OPTYPE op, ExtraArgs... args) {                        \
+    return static_cast<ConcreteType *>(this)->visit##OPKIND##Verif(op,         \
+                                                                   args...);   \
+  }
+
+  HANDLE(AssertOp, Unhandled);
+  HANDLE(AssumeOp, Unhandled);
+  HANDLE(CoverOp, Unhandled);
+#undef HANDLE
+};
+
+} // namespace verif
+} // namespace circt
+
+#endif // CIRCT_DIALECT_VERIF_VERIFVISITORS_H

include/circt/InitAllDialects.h

@@ -27,6 +27,7 @@
 #include "circt/Dialect/Handshake/HandshakeDialect.h"
 #include "circt/Dialect/Interop/InteropDialect.h"
 #include "circt/Dialect/LLHD/IR/LLHDDialect.h"
+#include "circt/Dialect/LTL/LTLDialect.h"
 #include "circt/Dialect/LoopSchedule/LoopScheduleDialect.h"
 #include "circt/Dialect/MSFT/MSFTDialect.h"
 #include "circt/Dialect/Moore/MooreDialect.h"
@@ -36,6 +37,7 @@
 #include "circt/Dialect/SV/SVDialect.h"
 #include "circt/Dialect/Seq/SeqDialect.h"
 #include "circt/Dialect/SystemC/SystemCDialect.h"
+#include "circt/Dialect/Verif/VerifDialect.h"
 #include "mlir/IR/Dialect.h"
 
 namespace circt {
@@ -53,19 +55,21 @@ inline void registerAllDialects(mlir::DialectRegistry &registry) {
     firrtl::FIRRTLDialect,
     fsm::FSMDialect,
     handshake::HandshakeDialect,
+    hw::HWDialect,
+    hwarith::HWArithDialect,
     interop::InteropDialect,
     llhd::LLHDDialect,
     loopschedule::LoopScheduleDialect,
-    msft::MSFTDialect,
+    ltl::LTLDialect,
     moore::MooreDialect,
-    hw::HWDialect,
+    msft::MSFTDialect,
-    seq::SeqDialect,
-    ssp::SSPDialect,
     om::OMDialect,
     pipeline::PipelineDialect,
+    seq::SeqDialect,
+    ssp::SSPDialect,
     sv::SVDialect,
-    hwarith::HWArithDialect,
+    systemc::SystemCDialect,
-    systemc::SystemCDialect
+    verif::VerifDialect
   >();
   // clang-format on
 }

lib/Dialect/CMakeLists.txt

@@ -22,6 +22,7 @@ add_subdirectory(HWArith)
 add_subdirectory(Interop)
 add_subdirectory(LLHD)
 add_subdirectory(LoopSchedule)
+add_subdirectory(LTL)
 add_subdirectory(Moore)
 add_subdirectory(MSFT)
 add_subdirectory(OM)
@@ -30,3 +31,4 @@ add_subdirectory(Seq)
 add_subdirectory(SSP)
 add_subdirectory(SV)
 add_subdirectory(SystemC)
+add_subdirectory(Verif)

lib/Dialect/LTL/CMakeLists.txt

@@ -0,0 +1,21 @@
+add_circt_dialect_library(CIRCTLTL
+  LTLDialect.cpp
+  LTLFolds.cpp
+  LTLOps.cpp
+
+  ADDITIONAL_HEADER_DIRS
+  ${CIRCT_MAIN_INCLUDE_DIR}/circt/Dialect/LTL
+
+  DEPENDS
+  CIRCTLTLEnumsIncGen
+  MLIRLTLIncGen
+
+  LINK_COMPONENTS
+  Support
+
+  LINK_LIBS PUBLIC
+  CIRCTComb
+  CIRCTHW
+  MLIRIR
+  MLIRInferTypeOpInterface
+)

lib/Dialect/LTL/LTLDialect.cpp

@@ -0,0 +1,35 @@
+//===- LTLDialect.cpp - LTL dialect implementation ------------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "circt/Dialect/LTL/LTLDialect.h"
+#include "circt/Dialect/Comb/CombDialect.h"
+#include "circt/Dialect/HW/HWDialect.h"
+#include "circt/Dialect/LTL/LTLOps.h"
+#include "circt/Dialect/LTL/LTLTypes.h"
+#include "mlir/IR/DialectImplementation.h"
+#include "llvm/ADT/TypeSwitch.h"
+
+using namespace circt;
+using namespace ltl;
+
+void LTLDialect::initialize() {
+  addTypes<
+#define GET_TYPEDEF_LIST
+#include "circt/Dialect/LTL/LTLTypes.cpp.inc"
+      >();
+  addOperations<
+#define GET_OP_LIST
+#include "circt/Dialect/LTL/LTL.cpp.inc"
+      >();
+}
+
+#include "circt/Dialect/LTL/LTLDialect.cpp.inc"
+#include "circt/Dialect/LTL/LTLEnums.cpp.inc"
+
+#define GET_TYPEDEF_CLASSES
+#include "circt/Dialect/LTL/LTLTypes.cpp.inc"

lib/Dialect/LTL/LTLFolds.cpp

@@ -0,0 +1,103 @@
+//===- LTLFolds.cpp -------------------------------------------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "circt/Dialect/Comb/CombOps.h"
+#include "circt/Dialect/HW/HWOps.h"
+#include "circt/Dialect/LTL/LTLOps.h"
+#include "mlir/IR/PatternMatch.h"
+
+using namespace circt;
+using namespace ltl;
+using namespace mlir;
+
+/// Check if an attribute is an integer zero.
+static bool isConstantZero(Attribute attr) {
+  if (!attr)
+    return false;
+  if (auto intAttr = dyn_cast<IntegerAttr>(attr))
+    return intAttr.getValue().isZero();
+  return false;
+}
+
+/// Concatenate two value ranges into a larger range. Useful for declarative
+/// rewrites.
+static SmallVector<Value> concatValues(ValueRange a, ValueRange b) {
+  SmallVector<Value> v;
+  v.append(a.begin(), a.end());
+  v.append(b.begin(), b.end());
+  return v;
+}
+
+/// Inline all `ConcatOp`s in a range of values.
+static SmallVector<Value> flattenConcats(ValueRange values) {
+  SmallVector<Value> flatInputs;
+  for (auto value : values) {
+    if (auto concatOp = value.getDefiningOp<ConcatOp>()) {
+      auto inputs = concatOp.getInputs();
+      flatInputs.append(inputs.begin(), inputs.end());
+    } else {
+      flatInputs.push_back(value);
+    }
+  }
+  return flatInputs;
+}
+
+//===----------------------------------------------------------------------===//
+// Declarative Rewrites
+//===----------------------------------------------------------------------===//
+
+namespace patterns {
+#include "circt/Dialect/LTL/LTLFolds.cpp.inc"
+} // namespace patterns
+
+//===----------------------------------------------------------------------===//
+// DelayOp
+//===----------------------------------------------------------------------===//
+
+OpFoldResult DelayOp::fold(FoldAdaptor adaptor) {
+  // delay(s, 0, 0) -> s
+  if (adaptor.getDelay() == 0 && adaptor.getLength() == 0)
+    return getInput();
+
+  return {};
+}
+
+void DelayOp::getCanonicalizationPatterns(RewritePatternSet &results,
+                                          MLIRContext *context) {
+  results.add<patterns::NestedDelays>(results.getContext());
+  results.add<patterns::MoveDelayIntoConcat>(results.getContext());
+}
+
+//===----------------------------------------------------------------------===//
+// ConcatOp
+//===----------------------------------------------------------------------===//
+
+OpFoldResult ConcatOp::fold(FoldAdaptor adaptor) {
+  // concat(s) -> s
+  if (getInputs().size() == 1)
+    return getInputs()[0];
+
+  return {};
+}
+
+void ConcatOp::getCanonicalizationPatterns(RewritePatternSet &results,
+                                           MLIRContext *context) {
+  results.add<patterns::FlattenConcats>(results.getContext());
+}
+
+//===----------------------------------------------------------------------===//
+// DisableOp
+//===----------------------------------------------------------------------===//
+
+OpFoldResult DisableOp::fold(FoldAdaptor adaptor) {
+  // disable(p, false) -> p
+  if (isConstantZero(adaptor.getCondition()))
+    return getInput();
+
+  return {};
+}

lib/Dialect/LTL/LTLOps.cpp

@@ -0,0 +1,74 @@
+//===- LTLOps.cpp ==-------------------------------------------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "circt/Dialect/LTL/LTLOps.h"
+#include "circt/Dialect/LTL/LTLTypes.h"
+#include "mlir/IR/Builders.h"
+#include "mlir/IR/FunctionImplementation.h"
+#include "mlir/IR/OpImplementation.h"
+#include "mlir/IR/PatternMatch.h"
+#include "mlir/IR/SymbolTable.h"
+#include "mlir/Interfaces/SideEffectInterfaces.h"
+
+using namespace circt;
+using namespace ltl;
+using namespace mlir;
+
+#define GET_OP_CLASSES
+#include "circt/Dialect/LTL/LTL.cpp.inc"
+
+//===----------------------------------------------------------------------===//
+// AndOp / OrOp
+//===----------------------------------------------------------------------===//
+
+static LogicalResult inferAndLikeReturnTypes(MLIRContext *context,
+                                             ValueRange operands,
+                                             SmallVectorImpl<Type> &results) {
+  if (llvm::any_of(operands, [](auto operand) {
+        return isa<PropertyType>(operand.getType());
+      })) {
+    results.push_back(PropertyType::get(context));
+  } else {
+
+    results.push_back(SequenceType::get(context));
+  }
+  return success();
+}
+
+LogicalResult
+AndOp::inferReturnTypes(MLIRContext *context, std::optional<Location> loc,
+                        ValueRange operands, DictionaryAttr attributes,
+                        OpaqueProperties properties, RegionRange regions,
+                        SmallVectorImpl<Type> &inferredReturnTypes) {
+  return inferAndLikeReturnTypes(context, operands, inferredReturnTypes);
+}
+
+LogicalResult
+OrOp::inferReturnTypes(MLIRContext *context, std::optional<Location> loc,
+                       ValueRange operands, DictionaryAttr attributes,
+                       OpaqueProperties properties, RegionRange regions,
+                       SmallVectorImpl<Type> &inferredReturnTypes) {
+  return inferAndLikeReturnTypes(context, operands, inferredReturnTypes);
+}
+
+//===----------------------------------------------------------------------===//
+// ClockOp
+//===----------------------------------------------------------------------===//
+
+LogicalResult
+ClockOp::inferReturnTypes(MLIRContext *context, std::optional<Location> loc,
+                          ValueRange operands, DictionaryAttr attributes,
+                          OpaqueProperties properties, RegionRange regions,
+                          SmallVectorImpl<Type> &inferredReturnTypes) {
+  if (isa<PropertyType>(operands[0].getType())) {
+    inferredReturnTypes.push_back(PropertyType::get(context));
+  } else {
+    inferredReturnTypes.push_back(SequenceType::get(context));
+  }
+  return success();
+}

lib/Dialect/Verif/CMakeLists.txt

@@ -0,0 +1,17 @@
+add_circt_dialect_library(CIRCTVerif
+  VerifDialect.cpp
+  VerifOps.cpp
+
+  ADDITIONAL_HEADER_DIRS
+  ${CIRCT_MAIN_INCLUDE_DIR}/circt/Dialect/Verif
+
+  DEPENDS
+  MLIRVerifIncGen
+
+  LINK_COMPONENTS
+  Support
+
+  LINK_LIBS PUBLIC
+  CIRCTLTL
+  MLIRIR
+)

lib/Dialect/Verif/VerifDialect.cpp

@@ -0,0 +1,22 @@
+//===- VerifDialect.cpp - Verif dialect implementation --------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "circt/Dialect/Verif/VerifDialect.h"
+#include "circt/Dialect/Verif/VerifOps.h"
+
+using namespace circt;
+using namespace verif;
+
+void VerifDialect::initialize() {
+  addOperations<
+#define GET_OP_LIST
+#include "circt/Dialect/Verif/Verif.cpp.inc"
+      >();
+}
+
+#include "circt/Dialect/Verif/VerifDialect.cpp.inc"

lib/Dialect/Verif/VerifOps.cpp

@@ -0,0 +1,23 @@
+//===- VerifOps.cpp -------------------------------------------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "circt/Dialect/Verif/VerifOps.h"
+#include "circt/Dialect/LTL/LTLTypes.h"
+#include "mlir/IR/Builders.h"
+#include "mlir/IR/FunctionImplementation.h"
+#include "mlir/IR/OpImplementation.h"
+#include "mlir/IR/PatternMatch.h"
+#include "mlir/IR/SymbolTable.h"
+#include "mlir/Interfaces/SideEffectInterfaces.h"
+
+using namespace circt;
+using namespace verif;
+using namespace mlir;
+
+#define GET_OP_CLASSES
+#include "circt/Dialect/Verif/Verif.cpp.inc"

test/Dialect/LTL/basic.mlir

@@ -0,0 +1,108 @@
+// RUN: circt-opt %s | circt-opt | FileCheck %s
+
+%true = hw.constant true
+
+//===----------------------------------------------------------------------===//
+// Types
+//===----------------------------------------------------------------------===//
+
+// CHECK: unrealized_conversion_cast to !ltl.sequence
+// CHECK: unrealized_conversion_cast to !ltl.property
+%s = unrealized_conversion_cast to !ltl.sequence
+%p = unrealized_conversion_cast to !ltl.property
+
+//===----------------------------------------------------------------------===//
+// Generic
+//===----------------------------------------------------------------------===//
+
+// CHECK-NEXT: ltl.and {{%.+}}, {{%.+}} : i1, i1
+// CHECK-NEXT: ltl.and {{%.+}}, {{%.+}} : !ltl.sequence, !ltl.sequence
+// CHECK-NEXT: ltl.and {{%.+}}, {{%.+}} : !ltl.property, !ltl.property
+ltl.and %true, %true : i1, i1
+ltl.and %s, %s : !ltl.sequence, !ltl.sequence
+ltl.and %p, %p : !ltl.property, !ltl.property
+
+// CHECK-NEXT: ltl.or {{%.+}}, {{%.+}} : i1, i1
+// CHECK-NEXT: ltl.or {{%.+}}, {{%.+}} : !ltl.sequence, !ltl.sequence
+// CHECK-NEXT: ltl.or {{%.+}}, {{%.+}} : !ltl.property, !ltl.property
+ltl.or %true, %true : i1, i1
+ltl.or %s, %s : !ltl.sequence, !ltl.sequence
+ltl.or %p, %p : !ltl.property, !ltl.property
+
+// Type inference. `unrealized_conversion_cast` used to detect unexpected return
+// types on `ltl.and`.
+%s0 = ltl.and %true, %true : i1, i1
+%s1 = ltl.and %true, %s : i1, !ltl.sequence
+%s2 = ltl.and %s, %true : !ltl.sequence, i1
+%p0 = ltl.and %true, %p : i1, !ltl.property
+%p1 = ltl.and %p, %true : !ltl.property, i1
+%p2 = ltl.and %s, %p : !ltl.sequence, !ltl.property
+%p3 = ltl.and %p, %s : !ltl.property, !ltl.sequence
+unrealized_conversion_cast %s0 : !ltl.sequence to index
+unrealized_conversion_cast %s1 : !ltl.sequence to index
+unrealized_conversion_cast %s2 : !ltl.sequence to index
+unrealized_conversion_cast %p0 : !ltl.property to index
+unrealized_conversion_cast %p1 : !ltl.property to index
+unrealized_conversion_cast %p2 : !ltl.property to index
+unrealized_conversion_cast %p3 : !ltl.property to index
+
+//===----------------------------------------------------------------------===//
+// Sequences
+//===----------------------------------------------------------------------===//
+
+// CHECK: ltl.delay {{%.+}}, 0 : !ltl.sequence
+// CHECK: ltl.delay {{%.+}}, 42, 1337 : !ltl.sequence
+ltl.delay %s, 0 : !ltl.sequence
+ltl.delay %s, 42, 1337 : !ltl.sequence
+
+// CHECK: ltl.concat {{%.+}} : !ltl.sequence
+// CHECK: ltl.concat {{%.+}}, {{%.+}} : !ltl.sequence, !ltl.sequence
+// CHECK: ltl.concat {{%.+}}, {{%.+}}, {{%.+}} : !ltl.sequence, !ltl.sequence, !ltl.sequence
+ltl.concat %s : !ltl.sequence
+ltl.concat %s, %s : !ltl.sequence, !ltl.sequence
+ltl.concat %s, %s, %s : !ltl.sequence, !ltl.sequence, !ltl.sequence
+
+//===----------------------------------------------------------------------===//
+// Properties
+//===----------------------------------------------------------------------===//
+
+// CHECK: ltl.not {{%.+}} : i1
+// CHECK: ltl.not {{%.+}} : !ltl.sequence
+// CHECK: ltl.not {{%.+}} : !ltl.property
+ltl.not %true : i1
+ltl.not %s : !ltl.sequence
+ltl.not %p : !ltl.property
+
+// CHECK: ltl.implication {{%.+}}, {{%.+}} : !ltl.sequence, !ltl.property
+ltl.implication %s, %p : !ltl.sequence, !ltl.property
+
+// CHECK: ltl.eventually {{%.+}} : i1
+// CHECK: ltl.eventually {{%.+}} : !ltl.sequence
+// CHECK: ltl.eventually {{%.+}} : !ltl.property
+ltl.eventually %true : i1
+ltl.eventually %s : !ltl.sequence
+ltl.eventually %p : !ltl.property
+
+//===----------------------------------------------------------------------===//
+// Clocking
+//===----------------------------------------------------------------------===//
+
+// CHECK: ltl.clock {{%.+}}, posedge {{%.+}} : !ltl.sequence
+// CHECK: ltl.clock {{%.+}}, negedge {{%.+}} : !ltl.sequence
+// CHECK: ltl.clock {{%.+}}, edge {{%.+}} : i1
+// CHECK: ltl.clock {{%.+}}, edge {{%.+}} : !ltl.sequence
+// CHECK: ltl.clock {{%.+}}, edge {{%.+}} : !ltl.property
+ltl.clock %s, posedge %true : !ltl.sequence
+ltl.clock %s, negedge %true : !ltl.sequence
+%clk0 = ltl.clock %true, edge %true : i1
+%clk1 = ltl.clock %s, edge %true : !ltl.sequence
+%clk2 = ltl.clock %p, edge %true : !ltl.property
+
+// Type inference. `unrealized_conversion_cast` used to detect unexpected return
+// types on `ltl.and`.
+unrealized_conversion_cast %clk0 : !ltl.sequence to index
+unrealized_conversion_cast %clk1 : !ltl.sequence to index
+unrealized_conversion_cast %clk2 : !ltl.property to index
+
+// CHECK: ltl.disable {{%.+}} if {{%.+}} : !ltl.property
+ltl.disable %p if %true : !ltl.property

test/Dialect/LTL/canonicalization.mlir

@@ -0,0 +1,105 @@
+// RUN: circt-opt %s --canonicalize | FileCheck %s
+
+func.func private @Bool(%arg0: i1)
+func.func private @Seq(%arg0: !ltl.sequence)
+func.func private @Prop(%arg0: !ltl.property)
+
+// CHECK-LABEL: @DelayFolds
+func.func @DelayFolds(%arg0: !ltl.sequence) {
+  // delay(s, 0, 0) -> s
+  // CHECK-NEXT: call @Seq(%arg0)
+  %0 = ltl.delay %arg0, 0, 0 : !ltl.sequence
+  call @Seq(%0) : (!ltl.sequence) -> ()
+
+  // delay(delay(s, 1), 2) -> delay(s, 3)
+  // CHECK-NEXT: ltl.delay %arg0, 3 :
+  // CHECK-NEXT: call
+  %1 = ltl.delay %arg0, 1 : !ltl.sequence
+  %2 = ltl.delay %1, 2 : !ltl.sequence
+  call @Seq(%2) : (!ltl.sequence) -> ()
+
+  // delay(delay(s, 1, N), 2) -> delay(s, 3)
+  // N is dropped
+  // CHECK-NEXT: ltl.delay %arg0, 3 :
+  // CHECK-NEXT: ltl.delay %arg0, 3 :
+  // CHECK-NEXT: call
+  // CHECK-NEXT: call
+  %3 = ltl.delay %arg0, 1, 0 : !ltl.sequence
+  %4 = ltl.delay %arg0, 1, 42 : !ltl.sequence
+  %5 = ltl.delay %3, 2 : !ltl.sequence
+  %6 = ltl.delay %4, 2 : !ltl.sequence
+  call @Seq(%5) : (!ltl.sequence) -> ()
+  call @Seq(%6) : (!ltl.sequence) -> ()
+
+  // delay(delay(s, 1), 2, N) -> delay(s, 3)
+  // N is dropped
+  // CHECK-NEXT: ltl.delay %arg0, 3 :
+  // CHECK-NEXT: ltl.delay %arg0, 3 :
+  // CHECK-NEXT: call
+  // CHECK-NEXT: call
+  %7 = ltl.delay %arg0, 1 : !ltl.sequence
+  %8 = ltl.delay %arg0, 1 : !ltl.sequence
+  %9 = ltl.delay %7, 2, 0 : !ltl.sequence
+  %10 = ltl.delay %8, 2, 42 : !ltl.sequence
+  call @Seq(%9) : (!ltl.sequence) -> ()
+  call @Seq(%10) : (!ltl.sequence) -> ()
+
+  // delay(delay(s, 1, 2), 3, 0) -> delay(s, 4, 2)
+  // delay(delay(s, 1, 2), 3, 5) -> delay(s, 4, 7)
+  // CHECK-NEXT: ltl.delay %arg0, 4, 2 :
+  // CHECK-NEXT: ltl.delay %arg0, 4, 7 :
+  // CHECK-NEXT: call
+  // CHECK-NEXT: call
+  %11 = ltl.delay %arg0, 1, 2 : !ltl.sequence
+  %12 = ltl.delay %arg0, 1, 2 : !ltl.sequence
+  %13 = ltl.delay %11, 3, 0 : !ltl.sequence
+  %14 = ltl.delay %12, 3, 5 : !ltl.sequence
+  call @Seq(%13) : (!ltl.sequence) -> ()
+  call @Seq(%14) : (!ltl.sequence) -> ()
+  return
+}
+
+// CHECK-LABEL: @ConcatFolds
+func.func @ConcatFolds(%arg0: !ltl.sequence, %arg1: !ltl.sequence, %arg2: !ltl.sequence) {
+  // concat(s) -> s
+  // CHECK-NEXT: call @Seq(%arg0)
+  %0 = ltl.concat %arg0 : !ltl.sequence
+  call @Seq(%0) : (!ltl.sequence) -> ()
+
+  // concat(concat(s0, s1), s2) -> concat(s0, s1, s2)
+  // concat(s0, concat(s1, s2)) -> concat(s0, s1, s2)
+  // concat(concat(s0, s1), s2, s0, concat(s1, s2)) -> concat(s0, s1, s2, s0, s1, s2)
+  // CHECK-NEXT: ltl.concat %arg0, %arg1, %arg2 :
+  // CHECK-NEXT: ltl.concat %arg0, %arg1, %arg2 :
+  // CHECK-NEXT: ltl.concat %arg0, %arg1, %arg2, %arg0, %arg1, %arg2 :
+  // CHECK-NEXT: call
+  // CHECK-NEXT: call
+  // CHECK-NEXT: call
+  %1 = ltl.concat %arg0, %arg1 : !ltl.sequence, !ltl.sequence
+  %2 = ltl.concat %1, %arg2 : !ltl.sequence, !ltl.sequence
+  %3 = ltl.concat %arg1, %arg2 : !ltl.sequence, !ltl.sequence
+  %4 = ltl.concat %arg0, %3 : !ltl.sequence, !ltl.sequence
+  %5 = ltl.concat %1, %arg2, %arg0, %3 : !ltl.sequence, !ltl.sequence, !ltl.sequence, !ltl.sequence
+  call @Seq(%2) : (!ltl.sequence) -> ()
+  call @Seq(%4) : (!ltl.sequence) -> ()
+  call @Seq(%5) : (!ltl.sequence) -> ()
+
+  // delay(concat(s0, s1), N, M) -> concat(delay(s0, N, M), s1)
+  // CHECK-NEXT: [[TMP:%.+]] = ltl.delay %arg0, 2, 3 :
+  // CHECK-NEXT: ltl.concat [[TMP]], %arg1 :
+  // CHECK-NEXT: call
+  %6 = ltl.concat %arg0, %arg1 : !ltl.sequence, !ltl.sequence
+  %7 = ltl.delay %6, 2, 3 : !ltl.sequence
+  call @Seq(%7) : (!ltl.sequence) -> ()
+  return
+}
+
+// CHECK-LABEL: @ClockingFolds
+func.func @ClockingFolds(%arg0: !ltl.property) {
+  // disable(p, false) -> p
+  // CHECK-NEXT: call @Prop(%arg0)
+  %false = hw.constant false
+  %0 = ltl.disable %arg0 if %false : !ltl.property
+  call @Prop(%0) : (!ltl.property) -> ()
+  return
+}

test/Dialect/Verif/basic.mlir

@@ -0,0 +1,30 @@
+// RUN: circt-opt %s | circt-opt | FileCheck %s
+
+%true = hw.constant true
+%s = unrealized_conversion_cast to !ltl.sequence
+%p = unrealized_conversion_cast to !ltl.property
+
+//===----------------------------------------------------------------------===//
+// Assertions
+//===----------------------------------------------------------------------===//
+
+// CHECK: verif.assert {{%.+}} : i1
+// CHECK: verif.assert {{%.+}} : !ltl.sequence
+// CHECK: verif.assert {{%.+}} : !ltl.property
+verif.assert %true : i1
+verif.assert %s : !ltl.sequence
+verif.assert %p : !ltl.property
+
+// CHECK: verif.assume {{%.+}} : i1
+// CHECK: verif.assume {{%.+}} : !ltl.sequence
+// CHECK: verif.assume {{%.+}} : !ltl.property
+verif.assume %true : i1
+verif.assume %s : !ltl.sequence
+verif.assume %p : !ltl.property
+
+// CHECK: verif.cover {{%.+}} : i1
+// CHECK: verif.cover {{%.+}} : !ltl.sequence
+// CHECK: verif.cover {{%.+}} : !ltl.property
+verif.cover %true : i1
+verif.cover %s : !ltl.sequence
+verif.cover %p : !ltl.property

tools/circt-opt/CMakeLists.txt

@@ -52,6 +52,7 @@ target_link_libraries(circt-opt
   CIRCTHWTransforms
   CIRCTLoopSchedule
   CIRCTLoopScheduleToCalyx
+  CIRCTLTL
   CIRCTSCFToCalyx
   CIRCTScheduling
   CIRCTSeq
@@ -69,6 +70,7 @@ target_link_libraries(circt-opt
   CIRCTSystemC
   CIRCTSystemCTransforms
   CIRCTTransforms
+  CIRCTVerif
 
   MLIRIR
   MLIRLLVMDialect