Merge remote-tracking branch 'origin/main' into lenny/fix-7078

include/circt/Conversion/Passes.td

@@ -654,7 +654,7 @@ def ConvertToArcs : Pass<"convert-to-arcs", "mlir::ModuleOp"> {
     latency.
   }];
   let constructor = "circt::createConvertToArcsPass()";
-  let dependentDialects = ["circt::arc::ArcDialect"];
+  let dependentDialects = ["circt::arc::ArcDialect", "circt::hw::HWDialect"];
   let options = [
     Option<"tapRegisters", "tap-registers", "bool", "true",
       "Make registers observable">,

include/circt/Dialect/Arc/ArcOps.td

@@ -134,6 +134,9 @@ def StateOp : ArcOp<"state", [
   DeclareOpInterfaceMethods<SymbolUserOpInterface>,
   AttrSizedOperandSegments,
   DeclareOpInterfaceMethods<ClockedOpInterface>,
+  PredOpTrait<"types of initial arguments match result types",
+    CPred<[{getInitials().empty() ||
+              llvm::equal(getInitials().getType(), getResults().getType())}]>>
 ]> {
   let summary = "State transfer arc";
 
@@ -143,35 +146,40 @@ def StateOp : ArcOp<"state", [
     Optional<I1>:$enable,
     Optional<I1>:$reset,
     I32Attr:$latency,
-    Variadic<AnyType>:$inputs);
+    Variadic<AnyType>:$inputs,
+    Variadic<AnyType>:$initials);
   let results = (outs Variadic<AnyType>:$outputs);
 
   let assemblyFormat = [{
     $arc `(` $inputs `)` (`clock` $clock^)? (`enable` $enable^)?
-    (`reset` $reset^)? `latency` $latency attr-dict
-    `:` functional-type($inputs, results)
+    (`reset` $reset^)?
+    ( `initial` ` ` `(` $initials^ `:` type($initials) `)`)?
+    `latency` $latency attr-dict `:` functional-type($inputs, results)
   }];
 
   let hasFolder = 1;
   let hasCanonicalizeMethod = 1;
 
   let builders = [
     OpBuilder<(ins "DefineOp":$arc, "mlir::Value":$clock, "mlir::Value":$enable,
-      "unsigned":$latency, CArg<"mlir::ValueRange", "{}">:$inputs), [{
+      "unsigned":$latency, CArg<"mlir::ValueRange", "{}">:$inputs,
+      CArg<"mlir::ValueRange", "{}">:$initials), [{
       build($_builder, $_state, mlir::SymbolRefAttr::get(arc),
             arc.getFunctionType().getResults(), clock, enable, latency,
-            inputs);
+            inputs, initials);
     }]>,
     OpBuilder<(ins "mlir::SymbolRefAttr":$arc, "mlir::TypeRange":$results,
       "mlir::Value":$clock, "mlir::Value":$enable, "unsigned":$latency,
-      CArg<"mlir::ValueRange", "{}">:$inputs
+      CArg<"mlir::ValueRange", "{}">:$inputs,
+      CArg<"mlir::ValueRange", "{}">:$initials
     ), [{
       build($_builder, $_state, arc, results, clock, enable, Value(), latency,
-      inputs);
+      inputs, initials);
     }]>,
     OpBuilder<(ins "mlir::SymbolRefAttr":$arc, "mlir::TypeRange":$results,
       "mlir::Value":$clock, "mlir::Value":$enable, "mlir::Value":$reset,
-      "unsigned":$latency, CArg<"mlir::ValueRange", "{}">:$inputs
+      "unsigned":$latency, CArg<"mlir::ValueRange", "{}">:$inputs,
+      CArg<"mlir::ValueRange", "{}">:$initials
     ), [{
       if (clock)
         $_state.addOperands(clock);
@@ -180,30 +188,34 @@ def StateOp : ArcOp<"state", [
       if (reset)
         $_state.addOperands(reset);
       $_state.addOperands(inputs);
+      $_state.addOperands(initials);
       $_state.addAttribute("arc", arc);
       $_state.addAttribute("latency", $_builder.getI32IntegerAttr(latency));
       $_state.addAttribute(getOperandSegmentSizeAttr(),
         $_builder.getDenseI32ArrayAttr({
           clock ? 1 : 0,
           enable ? 1 : 0,
           reset ? 1 : 0,
-          static_cast<int32_t>(inputs.size())}));
+          static_cast<int32_t>(inputs.size()),
+          static_cast<int32_t>(initials.size())}));
       $_state.addTypes(results);
     }]>,
     OpBuilder<(ins "mlir::StringAttr":$arc, "mlir::TypeRange":$results,
       "mlir::Value":$clock, "mlir::Value":$enable, "unsigned":$latency,
-      CArg<"mlir::ValueRange", "{}">:$inputs
+      CArg<"mlir::ValueRange", "{}">:$inputs,
+      CArg<"mlir::ValueRange", "{}">:$initials
     ), [{
       build($_builder, $_state, mlir::SymbolRefAttr::get(arc), results, clock,
-            enable, latency, inputs);
+            enable, latency, inputs, initials);
     }]>,
     OpBuilder<(ins "mlir::StringRef":$arc, "mlir::TypeRange":$results,
       "mlir::Value":$clock, "mlir::Value":$enable, "unsigned":$latency,
-      CArg<"mlir::ValueRange", "{}">:$inputs
+      CArg<"mlir::ValueRange", "{}">:$inputs,
+      CArg<"mlir::ValueRange", "{}">:$initials
     ), [{
       build($_builder, $_state,
             mlir::StringAttr::get($_builder.getContext(), arc),
-            results, clock, enable, latency, inputs);
+            results, clock, enable, latency, inputs, initials);
     }]>
   ];
   let skipDefaultBuilders = 1;
@@ -429,26 +441,37 @@ def ClockDomainOp : ArcOp<"clock_domain", [
   let hasCanonicalizeMethod = 1;
 }
 
-def ClockTreeOp : ArcOp<"clock_tree", [NoTerminator, NoRegionArguments]> {
+//===----------------------------------------------------------------------===//
+// (Pseudo) Clock Trees
+//===----------------------------------------------------------------------===//
+
+class ClockTreeLikeOp<string mnemonic, list<Trait> traits = []>:
+  ArcOp<mnemonic, !listconcat(traits, [
+    RecursiveMemoryEffects, NoTerminator, NoRegionArguments, SingleBlock,
+    HasParent<"ModelOp">
+])> {
+  let regions = (region SizedRegion<1>:$body);
+}
+
+def ClockTreeOp : ClockTreeLikeOp<"clock_tree"> {
   let summary = "A clock tree";
   let arguments = (ins I1:$clock);
-  let regions = (region SizedRegion<1>:$body);
   let assemblyFormat = [{
     $clock attr-dict-with-keyword $body
   }];
-  let extraClassDeclaration = [{
-    mlir::Block &getBodyBlock() { return getBody().front(); }
-  }];
 }
 
-def PassThroughOp : ArcOp<"passthrough", [NoTerminator, NoRegionArguments]> {
+def PassThroughOp : ClockTreeLikeOp<"passthrough"> {
   let summary = "Clock-less logic that is on the pass-through path";
-  let regions = (region SizedRegion<1>:$body);
   let assemblyFormat = [{
     attr-dict-with-keyword $body
   }];
-  let extraClassDeclaration = [{
-    mlir::Block &getBodyBlock() { return getBody().front(); }
+}
+
+def InitialOp : ClockTreeLikeOp<"initial"> {
+  let summary = "Clock-less logic called at the start of simulation";
+  let assemblyFormat = [{
+    attr-dict-with-keyword $body
   }];
 }
 
@@ -651,19 +674,22 @@ def TapOp : ArcOp<"tap"> {
   let assemblyFormat = [{ $value attr-dict `:` type($value) }];
 }
 
-def ModelOp : ArcOp<"model", [RegionKindInterface, IsolatedFromAbove,
-                              NoTerminator, Symbol]> {
+def ModelOp : ArcOp<"model", [
+  RegionKindInterface, IsolatedFromAbove, NoTerminator, Symbol,
+  DeclareOpInterfaceMethods<SymbolUserOpInterface>
+]> {
   let summary = "A model with stratified clocks";
   let description = [{
     A model with stratified clocks. The `io` optional attribute
     specifies the I/O of the module associated to this model.
   }];
   let arguments = (ins SymbolNameAttr:$sym_name,
-                       TypeAttrOf<ModuleType>:$io);
+                       TypeAttrOf<ModuleType>:$io,
+                       OptionalAttr<FlatSymbolRefAttr>:$initialFn);
   let regions = (region SizedRegion<1>:$body);
 
   let assemblyFormat = [{
-    $sym_name `io` $io attr-dict-with-keyword $body
+    $sym_name `io` $io (`initializer` $initialFn^)? attr-dict-with-keyword $body
   }];
 
   let extraClassDeclaration = [{

include/circt/Dialect/Arc/ModelInfo.h

@@ -36,11 +36,13 @@ struct ModelInfo {
   std::string name;
   size_t numStateBytes;
   llvm::SmallVector<StateInfo> states;
+  mlir::FlatSymbolRefAttr initialFnSym;
 
   ModelInfo(std::string name, size_t numStateBytes,
-            llvm::SmallVector<StateInfo> states)
+            llvm::SmallVector<StateInfo> states,
+            mlir::FlatSymbolRefAttr initialFnSym)
       : name(std::move(name)), numStateBytes(numStateBytes),
-        states(std::move(states)) {}
+        states(std::move(states)), initialFnSym(initialFnSym) {}
 };
 
 /// Collects information about states within the provided Arc model storage

include/circt/Dialect/FIRRTL/FIRRTLDeclarations.td

@@ -36,10 +36,50 @@ class ReferableDeclOp<string mnemonic, list<Trait> traits = []> :
 /// located in a hardware-creating context, such as the body of a module.
 class HardwareDeclOp<string mnemonic, list <Trait> traits = []> :
   ReferableDeclOp<mnemonic, traits # [
-    ParentOneOf<[
+    ParentOneOf<[ 
       "firrtl::FModuleOp", "firrtl::LayerBlockOp",
       "firrtl::WhenOp", "firrtl::MatchOp", "sv::IfDefOp"]>]> {}
 
+def FormalOp : FIRRTLOp<"formal", [
+    HasParent<"firrtl::CircuitOp">,
+    DeclareOpInterfaceMethods<Symbol>,
+    DeclareOpInterfaceMethods<SymbolUserOpInterface>
+]> {
+  let summary = "A formal test definition.";
+  let description = [{
+    The `firrtl.formal` operation defines a formal verification problem in the same 
+    context as the rest of the design. This problem is solved using bounded model 
+    checking and should be given a bound k, which represents the number of cycles considered 
+    during model checking. This definition marks a test harness defined as an internal module to 
+    be verified using bounded model checking.
+
+    Example:
+    ```mlir
+    // DUT
+    firrtl.module @Foo(in %bar: !firrtl.uint<8>, out %out: !firrtl.uint<8>) { ... }
+
+    // Test harness
+    firrtl.module @FooTest(in %bar_s: !firrtl.uint<8>) {
+      %bar, %out = firrtl.instance foo @Foo(in bar: %bar_s: !firrtl.uint<8>, out out: !firrtl.uint<8>) 
+      %c42_8 = firrtl.constant 42 : !firrtl.uint<8>
+      firrtl.connect %bar, %c42_8: !firrtl.uint<8>, !firrtl.uint<8>
+      %c69_8 = firrtl.constant 69 : !firrtl.uint<8>
+      %cond = firrtl.eq %c69_8, %out : (!firrtl.uint<8>, !firrtl.uint<8>) -> !firrtl.uint<1>
+      firrtl.assert %cond
+    }
+
+    // Mark test harness as formal test
+    firrtl.formal @formal1 of @FooTest bound 20
+    ```
+  }];
+
+  let arguments = (ins SymbolNameAttr:$sym_name, FlatSymbolRefAttr:$moduleName, UI64Attr:$bound);
+  let results = (outs);
+  let assemblyFormat = [{
+    $sym_name `of` $moduleName `bound` $bound attr-dict
+  }];
+}
+
 def InstanceOp : HardwareDeclOp<"instance", [
     DeclareOpInterfaceMethods<FInstanceLike>,
     DeclareOpInterfaceMethods<SymbolUserOpInterface>,

include/circt/Dialect/FIRRTL/Passes.h

@@ -214,6 +214,8 @@ std::unique_ptr<mlir::Pass> createLowerDPIPass();
 std::unique_ptr<mlir::Pass>
 createAssignOutputDirsPass(mlir::StringRef outputDir = "");
 
+std::unique_ptr<mlir::Pass> createCheckRecursiveInstantiation();
+
 /// Generate the code for registering passes.
 #define GEN_PASS_REGISTRATION
 #include "circt/Dialect/FIRRTL/Passes.h.inc"

include/circt/Dialect/FIRRTL/Passes.td

@@ -970,4 +970,18 @@ def ProbesToSignals : Pass<"firrtl-probes-to-signals", "firrtl::CircuitOp"> {
   let constructor = "circt::firrtl::createProbesToSignalsPass()";
 }
 
+def CheckRecursiveInstantiation : Pass<"firrtl-check-recursive-instantiation",
+    "firrtl::CircuitOp"> {
+  let summary = "Check for illegal recursive instantiation";
+  let description = [{
+    This pass checks for illegal recursive module instantion.  Recursive
+    instantiation is when a module instantiates itself, either directly or
+    indirectly through other modules it instantiates.  Recursive module 
+    instantiation is illegal because it would require infinite hardware to
+    synthesize. Recursive class instantiation is illegal as it would create an
+    infinite loop.
+  }];
+  let constructor = "circt::firrtl::createCheckRecursiveInstantiation()";
+}
+
 #endif // CIRCT_DIALECT_FIRRTL_PASSES_TD

include/circt/Dialect/LLHD/IR/LLHDSignalOps.td

@@ -11,12 +11,14 @@
 //===----------------------------------------------------------------------===//
 
 include "mlir/IR/EnumAttr.td"
-
-def SigOp : LLHDOp<"sig", [
-    TypesMatchWith<
-      "type of 'init' and underlying type of 'signal' have to match.",
-      "init", "result", "hw::InOutType::get($_self)">
-  ]> {
+include "mlir/IR/OpAsmInterface.td"
+
+def SignalOp : LLHDOp<"sig", [
+  DeclareOpInterfaceMethods<OpAsmOpInterface, ["getAsmResultNames"]>,
+  TypesMatchWith<
+    "type of 'init' and underlying type of 'signal' have to match.",
+    "init", "result", "hw::InOutType::get($_self)">
+]> {
   let summary = "Create a signal.";
   let description = [{
     The `llhd.sig` instruction introduces a new signal in the IR. The input
@@ -28,17 +30,22 @@ def SigOp : LLHDOp<"sig", [
 
     ```mlir
     %c123_i64 = hw.constant 123 : i64
-    %sig_i64 = llhd.sig "foo" %c123_i64 : i64
+    %foo = llhd.sig %c123_i64 : i64
+    %0 = llhd.sig name "foo" %c123_i64 : i64
     ```
 
     This example creates a new signal named "foo", carrying an `i64` type with
     initial value of 123.
   }];
-
-  let arguments = (ins StrAttr: $name, HWValueType: $init);
-  let results = (outs InOutType: $result);
-
-  let assemblyFormat = "$name $init attr-dict `:` qualified(type($init))";
+  let arguments = (ins
+    OptionalAttr<StrAttr>:$name,
+    HWValueType:$init
+  );
+  let results = (outs Res<InOutType, "", [MemAlloc]>:$result);
+  let assemblyFormat = [{
+    `` custom<ImplicitSSAName>($name) $init attr-dict
+    `:` type($init)
+  }];
 }
 
 def PrbOp : LLHDOp<"prb", [