Merge branch 'main' into dev/dobios/clocked-assert-verif-op

.github/workflows/esiRuntimePublish.yml

@@ -32,13 +32,15 @@ jobs:
 
     steps:
       - name: Get CIRCT
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           fetch-depth: 0
           submodules: false
 
       - name: Setup Python
-        uses: actions/setup-python@v3
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.10'
 
       - name: Install cibuildwheel
         run: python -m pip install cibuildwheel==2.16.2
@@ -50,11 +52,18 @@ jobs:
           CIBW_MANYLINUX_X86_64_IMAGE: ghcr.io/circt/images/pycde-build
           SETUPTOOLS_SCM_DEBUG: True
 
-      - name: Upload (stage) wheels as artifacts
-        uses: actions/upload-artifact@v3
+      - name: Get wheel name
+        shell: bash
+        id: whl-name
+        run: |
+          cd wheelhouse
+          echo WHL=`ls *.whl` >> "$GITHUB_OUTPUT"
+
+      - name: Upload wheels as artifacts
+        uses: actions/upload-artifact@v4
         with:
-          name: python-wheels
-          path: ./wheelhouse/*.whl
+          name: ${{ steps.whl-name.outputs.WHL }}
+          path: wheelhouse/${{ steps.whl-name.outputs.WHL }}
           retention-days: 7
           if-no-files-found: error
 
@@ -73,7 +82,6 @@ jobs:
       - name: Download wheels
         uses: actions/download-artifact@v3
         with:
-          name: python-wheels
           path: ./wheelhouse/
 
       - name: List downloaded wheels

.github/workflows/pycdePublish.yml

@@ -0,0 +1,60 @@
+name: PyCDE Test and Publish
+
+# Build the wheels for a series of Python versions and OSes and publish them to
+# PyPI.
+
+on:
+  workflow_dispatch:
+
+jobs:
+  # Build CIRCT and run its tests using a Docker container with all the
+  # integration testing prerequisite installed.
+  build-circt:
+    name: Build
+    runs-on: ubuntu-latest
+    strategy:
+      # Keep the 'matrix' strategy with one data point to make it obvious that
+      # this is one point in the overall matrix.
+      matrix:
+        python-env:
+          - cp38-win_amd64
+    steps:
+      # Clone the CIRCT repo and its submodules. Do shallow clone to save clone
+      # time.
+      - name: Get CIRCT
+        uses: actions/checkout@v3
+        with:
+          submodules: true
+
+      # --------
+      # Build and test CIRCT
+      # --------
+      - name: Install dependencies
+        run: |
+          set -o errexit
+          sudo apt install -y python3-pip
+          python3 -m pip install --upgrade pip
+          python3 -m pip install cibuildwheel twine
+      - name: Build wheel
+        env:
+          CC: clang
+          CXX: clang++
+          CIBW_BUILD: ${{ matrix.python-env }}
+          CIBW_ENVIRONMENT: CMAKE_GENERATOR=Ninja
+          SETUPTOOLS_SCM_DEBUG: True
+          BUILD_TYPE: RelWithAsserts
+          RUN_TESTS: True
+        run: |
+          export PATH=$PATH:$HOME/.local/bin
+          cd $(Pipeline.Workspace)/circt
+
+          echo "Fetching history and tags from CIRCT repo"
+          git fetch --depth=1000000 --tags --no-recurse-submodules
+
+          echo "Building wheel"
+          cibuildwheel --output-dir wheelhouse frontends/PyCDE
+      - name: Upload Binary (Non-Tag)
+        uses: actions/upload-artifact@v3
+        with:
+          path: wheelhouse/*.whl
+          retention-days: 7

cmake/modules/AddCIRCT.cmake

@@ -11,8 +11,9 @@ function(add_circt_interface interface)
 endfunction()
 
 function(add_circt_public_c_api_library name)
-  add_mlir_public_c_api_library(${ARGV})
+  add_mlir_public_c_api_library(${ARGV} DISABLE_INSTALL)
   add_dependencies(circt-capi ${name})
+  add_circt_library_install(${name})
 endfunction()
 
 # Additional parameters are forwarded to tablegen.

docs/Dialects/LTL.md

@@ -9,8 +9,6 @@ This dialect provides operations and types to model [Linear Temporal Logic](http
 
 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
 
@@ -30,6 +28,7 @@ The core building blocks for modeling temporal logic in the `ltl` dialect are *s
 
 - `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.
@@ -133,6 +132,19 @@ The `ltl.implication` op implements the overlapping case `|->`, such that the tw
 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.
@@ -176,14 +188,21 @@ The `ltl.delay` sequence operation represents various shorthands for the *next*/
 | `ltl.delay %a, 2`    | **XXF**a                    |
 
 
-### Concatenation
+### Until and Eventually
+
+`ltl.until` is *weak*, meaning the property will hold even if the trace does not contain enough clock cycles to evaluate the property. `ltl.eventually` is *strong*, where `ltl.eventually %p` means `p` must hold at some point in the trace.
+
+
+### Concatenation and Repetition
 
 The `ltl.concat` sequence operation does not have a direct equivalent in LTL. It builds a longer sequence by composing multiple shorter sequences one after another. LTL has no concept of concatenation, or a *"v happens after u"*, where the point in time at which v starts is dependent on how long the sequence u was.
 
 For a sequence u with a fixed length of 2, concatenation can be represented as *"(u happens) and (v happens 2 cycles in the future)"*, u ∧ **XX**v. If u has a dynamic length though, for example a delay between 1 and 2, `ltl.delay %u, 1, 1` or **X**u ∨ **XX**u in LTL, there is no fixed number of cycles by which the sequence v can be delayed to make it start after u. Instead, all different-length variants of sequence u have to be enumerated and combined with a copy of sequence v delayed by the appropriate amount: (**X**u ∧ **XX**v) ∨ (**XX**u ∧ **XXX**v). This is basically saying "u delayed by 1 to 2 cycles followed by v" is the same as either *"u delayed by 1 cycle and v delayed by 2 cycles"*, or *"u delayed by 2 cycles and v delayed by 3 cycles"*.
 
 The *"v happens after u"* relationship is crucial to express sequences efficiently, which is why the LTL dialect has the `ltl.concat` op. If sequences are thought of as regular expressions over time, for example, `a(b|cd)` or *"a followed by either (b) or (c followed by d)"*, the importance of having a concatenation operation as temporal connective becomes apparent. Why LTL formalisms tend to not include such an operator is unclear.
 
+As for `ltl.repeat`, it also relies on the semantics of *v happens after u* to compose the repeated sequences. Unlike `ltl.concat`, which can be expanded by LTL operators within a finite formula size, unbounded repetition cannot be expanded by listing all cases. This means unbounded repetition imports semantics that LTL cannot describe. The LTL dialect has this operation because it is necessary and useful for regular expressions and SVA.
+
 
 ## Types
 

frontends/PyCDE/setup.py

@@ -45,6 +45,7 @@ class CMakeBuild(build_py):
 
   def run(self):
     target_dir = self.build_lib
+    test = os.getenv("RUN_TESTS")
     cmake_build_dir = os.getenv("PYCDE_CMAKE_BUILD_DIR")
     if not cmake_build_dir:
       cmake_build_dir = os.path.join(target_dir, "..", "cmake_build")
@@ -81,9 +82,24 @@ def run(self):
     if os.path.exists(cmake_cache_file):
       os.remove(cmake_cache_file)
     subprocess.check_call(["cmake", src_dir] + cmake_args, cwd=cmake_build_dir)
-    subprocess.check_call(["cmake", "--build", ".", "--target", "check-pycde"] +
-                          build_args,
+    subprocess.check_call([
+        "cmake",
+        "--build",
+        ".",
+        "--target",
+        "check-pycde",
+    ] + build_args,
                           cwd=cmake_build_dir)
+    if test.lower() == "true":
+      subprocess.check_call([
+          "cmake",
+          "--build",
+          ".",
+          "--target",
+          "check-pycde-integration",
+          "check-circt",
+      ] + build_args,
+                            cwd=cmake_build_dir)
     install_cmd = ["cmake", "--build", ".", "--target", "install-PyCDE"]
     subprocess.check_call(install_cmd + build_args, cwd=cmake_build_dir)
     shutil.copytree(os.path.join(cmake_install_dir, "python_packages"),

include/circt-c/Dialect/Moore.h

@@ -25,15 +25,6 @@ MLIR_DECLARE_CAPI_DIALECT_REGISTRATION(Moore, moore);
 // Types
 //===----------------------------------------------------------------------===//
 
-enum MooreRealKind {
-  /// A `shortreal`.
-  MooreShortReal,
-  /// A `real`.
-  MooreReal,
-  /// A `realtime`.
-  MooreRealTime,
-};
-
 /// Create a void type.
 MLIR_CAPI_EXPORTED MlirType mooreVoidTypeGet(MlirContext ctx);
 /// Create a string type.
@@ -48,8 +39,7 @@ MLIR_CAPI_EXPORTED MlirType mooreIntTypeGetInt(MlirContext ctx, unsigned width);
 MLIR_CAPI_EXPORTED MlirType mooreIntTypeGetLogic(MlirContext ctx,
                                                  unsigned width);
 /// Create a real type.
-MLIR_CAPI_EXPORTED MlirType mooreRealTypeGet(MlirContext ctx,
-                                             enum MooreRealKind kind);
+MLIR_CAPI_EXPORTED MlirType mooreRealTypeGet(MlirContext ctx);
 /// Create a packed unsized dimension type.
 MLIR_CAPI_EXPORTED MlirType moorePackedUnsizedDimTypeGet(MlirType inner);
 /// Create a packed range dimension type.

include/circt/Conversion/ExportVerilog.h

@@ -17,6 +17,9 @@
 #include "mlir/Pass/Pass.h"
 
 namespace circt {
+namespace hw {
+class HWModuleLike;
+} // namespace hw
 
 std::unique_ptr<mlir::Pass>
 createTestApplyLoweringOptionPass(llvm::StringRef options);

include/circt/Dialect/Arc/ArcPasses.td

@@ -269,6 +269,19 @@ def SimplifyVariadicOps : Pass<"arc-simplify-variadic-ops", "mlir::ModuleOp"> {
   ];
 }
 
+def SplitFuncs : Pass<"arc-split-funcs", "mlir::ModuleOp"> {
+  let summary = "Split large funcs into multiple smaller funcs";
+  let dependentDialects = ["mlir::func::FuncDialect"];
+  let options = [
+    Option<"splitBound", "split-bound", "unsigned", "20000",
+      "Size threshold (in ops) above which to split funcs">
+  ];
+  let statistics = [
+    Statistic<"numFuncsCreated", "funcs-created",
+      "Number of new functions created">,
+  ];
+}
+
 def SplitLoops : Pass<"arc-split-loops", "mlir::ModuleOp"> {
   let summary = "Split arcs to break zero latency loops";
   let constructor = "circt::arc::createSplitLoopsPass()";

include/circt/Dialect/FIRRTL/FIRRTLCanonicalization.td

@@ -120,6 +120,9 @@ def AllOneConstantOp : Constraint<CPred<"$0.getDefiningOp<ConstantOp>() && $0.ge
 def TypeWidthAdjust32 : NativeCodeCall<
   "$_builder.getI32IntegerAttr(type_cast<FIRRTLBaseType>($0.getType()).getBitWidthOrSentinel() - type_cast<FIRRTLBaseType>($1.getType()).getBitWidthOrSentinel())">;
 
+// Int 1 is one higher than int 2
+def AdjInt : Constraint<CPred<"$0.getValue() + 1 == $1.getValue()">>;
+
 /// Drop the writer to the first argument and passthrough the second
 def DropWrite : NativeCodeCall<"dropWrite($_builder, $0, $1)">;
 
@@ -658,7 +661,7 @@ def MuxPadSel : Pat<
   (MuxPrimOp:$old $cond, $a, $b),
   (MoveNameHint $old, (MuxPrimOp
     (ConstantOp
-      (NativeCodeCall<"$_builder.getUI32IntegerAttr(0)">),
+      (NativeCodeCall<"getIntZerosAttr($_builder.getType<UIntType>(1))">),
       (returnType "$_builder.getType<UIntType>(1)")),
     $a, $b)),
   [(IntTypeWidthLTX<1> $cond)]>;
@@ -668,7 +671,7 @@ def Mux2PadSel : Pat<
   (Mux2CellIntrinsicOp:$old $cond, $a, $b),
   (MoveNameHint $old, (Mux2CellIntrinsicOp
     (ConstantOp
-      (NativeCodeCall<"$_builder.getUI32IntegerAttr(0)">),
+      (NativeCodeCall<"getIntZerosAttr($_builder.getType<UIntType>(1))">),
       (returnType "$_builder.getType<UIntType>(1)")),
     $a, $b)),
   [(IntTypeWidthLTX<1> $cond)]>;
@@ -693,6 +696,12 @@ def CatCast : Pat <
   (MoveNameHint $old, (CatPrimOp $x, $y)),
   [(EqualSigns $x, $y)]>;
 
+// cat(bits a:b x, bits b+1:c x) -> bits( a:c x)
+def CatBitsBits : Pat <
+  (CatPrimOp:$old (BitsPrimOp $x, I32Attr:$hi, I32Attr:$mid), (BitsPrimOp $x, I32Attr:$mid2, I32Attr:$low)),
+  (MoveNameHint $old, (BitsPrimOp $x, $hi, $low)),
+  [(AdjInt $mid2, $mid)]>;
+
 // regreset(clock, constant_zero, resetValue) -> reg(clock)
 def RegResetWithZeroReset : Pat<
   (RegResetOp $clock, $reset, $_, $name, $nameKind, $annotations, $inner_sym, $forceable),

include/circt/Dialect/FIRRTL/FIRRTLExpressions.td

@@ -1429,10 +1429,20 @@ def LTLDelayIntrinsicOp : LTLIntrinsicOp<"delay"> {
   }];
 }
 def LTLConcatIntrinsicOp : BinaryLTLIntrinsicOp<"concat">;
+def LTLRepeatIntrinsicOp : LTLIntrinsicOp<"repeat"> {
+  let arguments = (ins UInt1Type:$input,
+                       I64Attr:$base,
+                       OptionalAttr<I64Attr>:$more);
+  let assemblyFormat = [{
+    $input `,` $base (`,` $more^)? attr-dict `:`
+    functional-type(operands, results)
+  }];
+}
 
 // Properties
 def LTLNotIntrinsicOp : UnaryLTLIntrinsicOp<"not">;
 def LTLImplicationIntrinsicOp : BinaryLTLIntrinsicOp<"implication">;
+def LTLUntilIntrinsicOp : BinaryLTLIntrinsicOp<"until">;
 def LTLEventuallyIntrinsicOp : UnaryLTLIntrinsicOp<"eventually">;
 
 // Clocking

include/circt/Dialect/FIRRTL/FIRRTLVisitors.h

@@ -50,10 +50,11 @@ class ExprVisitor {
             IsXIntrinsicOp, PlusArgsValueIntrinsicOp, PlusArgsTestIntrinsicOp,
             SizeOfIntrinsicOp, ClockGateIntrinsicOp, ClockInverterIntrinsicOp,
             ClockDividerIntrinsicOp, LTLAndIntrinsicOp, LTLOrIntrinsicOp,
-            LTLDelayIntrinsicOp, LTLConcatIntrinsicOp, LTLNotIntrinsicOp,
-            LTLImplicationIntrinsicOp, LTLEventuallyIntrinsicOp,
-            LTLClockIntrinsicOp, LTLDisableIntrinsicOp, Mux2CellIntrinsicOp,
-            Mux4CellIntrinsicOp, HasBeenResetIntrinsicOp,
+            LTLDelayIntrinsicOp, LTLConcatIntrinsicOp, LTLRepeatIntrinsicOp,
+            LTLNotIntrinsicOp, LTLImplicationIntrinsicOp, LTLUntilIntrinsicOp,
+            LTLEventuallyIntrinsicOp, LTLClockIntrinsicOp,
+            LTLDisableIntrinsicOp, Mux2CellIntrinsicOp, Mux4CellIntrinsicOp,
+            HasBeenResetIntrinsicOp,
             // Miscellaneous.
             BitsPrimOp, HeadPrimOp, MuxPrimOp, PadPrimOp, ShlPrimOp, ShrPrimOp,
             TailPrimOp, VerbatimExprOp, HWStructCastOp, BitCastOp, RefSendOp,
@@ -171,8 +172,10 @@ class ExprVisitor {
   HANDLE(LTLOrIntrinsicOp, Unhandled);
   HANDLE(LTLDelayIntrinsicOp, Unhandled);
   HANDLE(LTLConcatIntrinsicOp, Unhandled);
+  HANDLE(LTLRepeatIntrinsicOp, Unhandled);
   HANDLE(LTLNotIntrinsicOp, Unhandled);
   HANDLE(LTLImplicationIntrinsicOp, Unhandled);
+  HANDLE(LTLUntilIntrinsicOp, Unhandled);
   HANDLE(LTLEventuallyIntrinsicOp, Unhandled);
   HANDLE(LTLClockIntrinsicOp, Unhandled);
   HANDLE(LTLDisableIntrinsicOp, Unhandled);

include/circt/Dialect/FIRRTL/Passes.h

@@ -201,6 +201,8 @@ std::unique_ptr<mlir::Pass> createSpecializeOptionPass();
 
 std::unique_ptr<mlir::Pass> createCreateCompanionAssume();
 
+std::unique_ptr<mlir::Pass> createModuleSummaryPass();
+
 /// Generate the code for registering passes.
 #define GEN_PASS_REGISTRATION
 #include "circt/Dialect/FIRRTL/Passes.h.inc"

include/circt/Dialect/FIRRTL/Passes.td

@@ -900,4 +900,13 @@ def SpecializeOption :
   ];
 }
 
+def ModuleSummary :
+  Pass<"firrtl-module-summary", "firrtl::CircuitOp"> {
+    let summary = "Print a summary of modules.";
+    let description = [{
+      The pass produces a summary of modules.
+    }];
+    let constructor = "circt::firrtl::createModuleSummaryPass()";
+  }
+
 #endif // CIRCT_DIALECT_FIRRTL_PASSES_TD